Pourquoi le calcul des séquents PAS gauche et droit pas de règles de travail?

Question

Les règles que je envisage sont $ \ frac {\ neg A, \ \ Gamma \ implique \ Delta} {\ Gamma \ implique \ Delta, \ A} (\ neg L) $ et $ \ frac {\ Gamma \ implique \ Delta, \ \ neg A} {A, \ \ Gamma \ implique \ Delta} (\ neg R) $

Je suis en train d'obtenir ma tête autour de quelques-unes des règles de calcul des séquents, et alors que je pense que je comprends la plupart d'entre eux, je me bats pour appliquer une intuition aux règles de négation ci-dessus.

L'intuition de regarder à gauche comme une conjonction de littéraux et le droit comme une disjonction de littéraux semble tomber en panne, et je suis pas clair comment expliquer ces règles à moi-même.

Quelle est une façon raisonnable de voir ces règles et de mettre une certaine compréhension sur eux?

Answer 1

Vous pourriez commencer par examiner les versions simplifiées des règles et construire l'intuition en considérant ces cas. Par exemple,

$$ \ frac {\ neg A, \ B \ C implique} {B \ implique C, \ A} (\ neg L) $$

peut être interprétée comme indiquant que $ (\ neg A \ wedge B) \ Rightarrow C $ implique $ B \ Rightarrow (C \ Vee A) $.

Donc, si c'est le cas que $ \ neg A $ et $ B $ sont vraies implique $ C $ est vrai, puis si seulement $ B $ est vrai, soit $ C $ est vrai (indépendamment de $ \ neg A $) ou $ A $ est vrai, car autrement $ \ neg A $ serait vrai, qui, combiné avec $ B $ étant vrai ferait $ C $ true.

Un jeu similaire peut être joué avec l'autre cas.

Answer 2

L'application de votre intuition, la prémisse de $ (\ neg L) $ est: sous les hypothèses $ \ Gamma $, et en supposant $ A $ est fausse, alors l'une des conclusions $ \ Delta détient $. Donc, si je sais que $ \ Gamma $, que puis-je conclure?

• Peut-être $ \ Delta détient $.
• Si $ \ Delta $ ne tient pas, il ne peut être que l'hypothèse que $ A $ est erroné n'est pas remplie. En d'autres termes, $ \ neg (\ neg A) $ est vrai, ce qui signifie que $ A $ est vrai.

Dans l'ensemble, à partir de la prémisse de $ (\ neg L) $, nous obtenons que $ \ Gamma $ implique $ \ Delta $ ou $ A $. Telle est la conclusion de $ (\ neg L).

De même, $ (\ neg R) $: sous les hypothèses $ \ Gamma $, soit l'un des conslusions $ \ Delta $ détient, ou $ \ A $ neg cales. Supposons maintenant qu'en plus de $ \ Gamma $ nous savons que $ A $ est vrai. Ensuite, parmi les conclusions $ \ Delta, \ neg A $, l'élément $ \ neg A $ ne peut pas être vrai, parce que vous ne pouvez pas avoir les deux $ A $ et $ \ neg A $ (milieu exclu). Il doit donc être une des conclusions de $ \ Delta $ qui détient (ou plus). Dans l'ensemble, (\ neg R) $ \ Gamma $ et $ A $ ensemble entail $ \ Delta $, ce qui est la conclusion de $ $.

Vous remarquerez que $ (\ neg L) $ repose sur le milieu exclu. Cette règle ne tient pas dans la logique intuitionniste, où juste parce que $ \ neg A $ conduit à une contradiction ne signifie pas que vous pouvez prouver $ A $. $ (\ Neg R) fonctionne $ dans la logique intuitionniste, mais peut-être pas dans une logique floue.