Editing Sequent calculus (section)

===Intuitionistic sequent calculus: System LJ===

Surprisingly, some small changes in the rules of LK suffice to turn it into a proof system for [[intuitionistic logic]].<ref>{{harvnb|Gentzen|1934|p=194}}, wrote: "Der Unterschied zwischen ''intuitionistischer'' und ''klassischer'' Logik ist bei den Kalkülen ''LJ'' und ''LK'' äußerlich ganz anderer Art als bei ''NJ'' und ''NK''. Dort bestand er in Weglassung bzw. Hinzunahme des Satzes vom ausgeschlossenen Dritten, während er hier durch die Sukzedensbedingung ausgedrückt wird." English translation: "The difference between ''intuitionistic'' and ''classical'' logic is in the case of the calculi ''LJ'' and ''LK'' of an extremely, totally different kind to the case of ''NJ'' and ''NK''. In the latter case, it consisted of the removal or addition respectively of the excluded middle rule, whereas in the former case, it is expressed through the succedent conditions."</ref> To this end, one has to restrict to sequents with at most one formula on the right-hand side,{{sfn|Tiomkin|1988}} and modify the rules to maintain this invariant.  For example, <math>({\lor}L)</math> is reformulated as follows (where C is an arbitrary formula):

:<math>
  \cfrac{\Gamma, A \vdash C \qquad \Gamma, B \vdash C }{\Gamma, A \lor B \vdash C} \quad ({\lor}L)
</math>

The resulting system is called LJ. It is sound and complete with respect to intuitionistic logic and admits a similar cut-elimination proof. This can be used in proving [[disjunction and existence properties]].

In fact, the only rules in LK that need to be restricted to single-formula consequents are <math>({\to}R)</math>, <math>(\neg R)</math> (which can be seen as a special case of <math>{\to}R</math>, as described above) and <math>({\forall}R)</math>.  When multi-formula consequents are interpreted as disjunctions, all of the other inference rules of LK are derivable in LJ, while the rules <math>({\to}R)</math> and <math>({\forall}R)</math> become
:<math>
  \cfrac{\Gamma, A \vdash B \lor C}{\Gamma \vdash (A \to B) \lor C} 
</math>
and (when <math>y</math> does not occur free in the bottom sequent)
:<math>
  \cfrac{\Gamma \vdash A[y/x] \lor C}{\Gamma \vdash (\forall x A) \lor C}.
</math>

These rules are not intuitionistically valid.