Editing Sequent calculus (section)

==The system LK==

This section introduces the rules of the sequent calculus '''LK''' (standing for Logistische Kalkül) as introduced by Gentzen in 1934.{{sfn|Indrzejczak|2021|pp=63–112}} A (formal) proof in this calculus is a finite [[sequence (mathematics)|sequence]] of sequents, where each of the sequents is derivable from sequents appearing earlier in the sequence by using one of the [[rule of inference|rules]] below.

===Inference rules===

The following notation will be used:
* <math>\vdash</math> known as the [[Turnstile (symbol)|turnstile]], separates the ''assumptions'' on the left from the ''propositions'' on the right
* <math>A</math> and <math>B</math> denote formulas of first-order predicate logic (one may also restrict this to propositional logic),
* <math>\Gamma, \Delta, \Sigma</math>, and <math>\Pi</math> are finite (possibly empty) sequences of formulas (in fact, the order of formulas does not matter; see {{slink||Structural rules}}),  called contexts,
** when on the ''left'' of the <math>\vdash</math>, the sequence of formulas is considered ''conjunctively'' (all assumed to hold at the same time),
** while on the ''right'' of the <math>\vdash</math>, the sequence of formulas is considered ''disjunctively'' (at least one of the formulas must hold for any assignment of variables),
* <math>t</math> denotes an arbitrary term,
* <math>x</math> and <math>y</math> denote variables.
* a variable is said to occur [[Free variables and bound variables|free]] within a formula if it is not bound by quantifiers <math>\forall</math> or <math>\exists</math>.
* <math>A[t/x]</math> denotes the formula that is obtained by substituting the term <math>t</math> for every free occurrence of the variable <math>x</math> in formula <math>A</math> with the restriction that the term <math>t</math> must be free for the variable <math>x</math> in <math>A</math> (i.e., no occurrence of any variable in <math>t</math> becomes bound in <math>A[t/x]</math>).
* <math>WL</math>, <math>WR</math>, <math>CL</math>, <math>CR</math>, <math>PL</math>, <math>PR</math>: These six stand for the two versions of each of three structural rules; one for use on the left ('L') of a <math>\vdash</math>, and the other on its right ('R'). The rules are abbreviated 'W' for ''Weakening (Left/Right)'', 'C' for ''Contraction'', and 'P' for ''Permutation''.

Note that, contrary to the rules for proceeding along the reduction tree presented above, the following rules are for moving in the opposite directions, from axioms to theorems. Thus they are exact mirror-images of the rules above, except that here symmetry is not implicitly assumed, and rules regarding [[quantifier (logic)|quantification]] are added.

{| class="wikitable"
|-
! Axiom
! Cut
|-
| <math> \cfrac{\qquad }{ A \vdash A} \quad (I) </math>
| <math> 
   \cfrac{\Gamma \vdash \Delta, A \qquad A, \Sigma \vdash \Pi} {\Gamma, \Sigma \vdash \Delta, \Pi} \quad (\mathit{Cut})
 </math>
|}
{| class="wikitable"
|-
! Left logical rules
! Right logical rules
|-
| <math> \cfrac{\Gamma, A \vdash \Delta} {\Gamma, A \land B \vdash \Delta} \quad ({\land}L_1)
 </math>
| <math> \cfrac{\Gamma \vdash A, \Delta}{\Gamma \vdash A \lor B, \Delta} \quad  ({\lor}R_1)
 </math>
|-
| <math> \cfrac{\Gamma, B \vdash \Delta}{\Gamma, A \land B \vdash \Delta}  \quad ({\land}L_2)
 </math>
| <math> \cfrac{\Gamma \vdash B, \Delta}{\Gamma \vdash A \lor B, \Delta} \quad ({\lor}R_2)
 </math>
|-
| <math> \cfrac{\Gamma, A \vdash \Delta \qquad \Gamma, B \vdash \Delta}{\Gamma, A \lor B \vdash \Delta} \quad ({\lor}L)
 </math>
| <math> \cfrac{\Gamma \vdash A, \Delta \qquad \Gamma \vdash B, \Delta}{\Gamma \vdash A \land B, \Delta} \quad ({\land}R)
 </math>
|-
| <math>
  \cfrac{\Gamma \vdash A, \Delta \qquad \Sigma, B \vdash \Pi}{\Gamma, \Sigma, A\rightarrow B \vdash \Delta, \Pi} \quad  ({\rightarrow }L)
 </math>
| <math>
   \cfrac{\Gamma, A \vdash B, \Delta}{\Gamma \vdash A \rightarrow B, \Delta} \quad ({\rightarrow}R)
 </math>
|-
| <math>
  \cfrac{\Gamma \vdash A, \Delta}{\Gamma, \lnot A \vdash \Delta} \quad  ({\lnot}L)
 </math>
| <math>
  \cfrac{\Gamma, A \vdash \Delta}{\Gamma \vdash \lnot A, \Delta} \quad ({\lnot}R)
 </math>
|-
| <math>
  \cfrac{\Gamma, A[t/x] \vdash \Delta}{\Gamma, \forall x A \vdash \Delta} \quad  ({\forall}L)
 </math>
| <math>
  \cfrac{\Gamma \vdash A[y/x], \Delta}{\Gamma \vdash \forall x A, \Delta} \quad  ({\forall}R) 
 </math> (†)
|-
| <math>
  \cfrac{\Gamma, A[y/x] \vdash \Delta}{\Gamma, \exists x A \vdash \Delta} \quad  ({\exists}L)
 </math> (†)
| <math>
  \cfrac{\Gamma \vdash A[t/x], \Delta}{\Gamma \vdash \exists x A, \Delta} \quad  ({\exists}R)
 </math>
|}
{| class="wikitable"
|-
! Left structural rules
! Right structural rules
|-
| <math>
  \cfrac{\Gamma \vdash \Delta}{\Gamma, A \vdash \Delta} \quad (\mathit{WL})
 </math>
| <math>
  \cfrac{\Gamma \vdash \Delta}{\Gamma \vdash A, \Delta} \quad (\mathit{WR})
 </math>
|-
| <math>
  \cfrac{\Gamma, A, A \vdash \Delta}{\Gamma, A \vdash \Delta} \quad (\mathit{CL})
 </math>
| <math>
  \cfrac{\Gamma \vdash A, A, \Delta}{\Gamma \vdash A, \Delta} \quad (\mathit{CR})
 </math>
|-
| <math>
  \cfrac{\Gamma_1, A, B, \Gamma_2 \vdash \Delta}{\Gamma_1, B, A, \Gamma_2 \vdash \Delta} \quad (\mathit{PL})
 </math>
| <math>
  \cfrac{\Gamma \vdash \Delta_1, A, B, \Delta_2}{\Gamma \vdash \Delta_1, B, A, \Delta_2} \quad (\mathit{PR})
 </math>
|}

'''''Restrictions''': In the rules marked with (†), <math>({\forall}R)</math> and <math>({\exists}L)</math>, the variable <math>y</math> must not occur free anywhere in the respective lower sequents.''

===An intuitive explanation===

The above rules can be divided into two major groups: ''logical'' and ''structural'' ones. Each of the logical rules introduces a new logical formula either on the left or on the right of the [[Turnstile (symbol)|turnstile]] <math>\vdash</math>. In contrast, the structural rules operate on the structure of the sequents, ignoring the exact shape of the formulas. The two exceptions to this general scheme are the axiom of identity (I) and the rule of (Cut).

Although stated in a formal way, the above rules allow for a very intuitive reading in terms of classical logic. Consider, for example, the rule <math>({\land}L_1)</math>. It says that, whenever one can prove that <math>\Delta</math> can be concluded from some sequence of formulas that contain <math>A</math>, then one can also conclude <math>\Delta</math> from the (stronger) assumption that <math>A \land B</math> holds. Likewise, the rule <math>({\neg}R)</math> states that, if <math>\Gamma</math> and <math>A</math> suffice to conclude <math>\Delta</math>, then from <math>\Gamma</math> alone one can either still conclude <math>\Delta</math> or <math>A</math> must be false, i.e. <math>{\neg}A</math> holds. All the rules can be interpreted in this way.

For an intuition about the quantifier rules, consider the rule <math>({\forall}R)</math>. Of course concluding that <math>\forall{x} A</math> holds just from the fact that <math>A[y/x]</math> is true is not in general possible. If, however, the variable y is not mentioned elsewhere (i.e. it can still be chosen freely, without influencing the other formulas), then one may assume, that <math>A[y/x]</math> holds for any value of y. The other rules should then be pretty straightforward.

Instead of viewing the rules as descriptions for legal derivations in predicate logic, one may also consider them as instructions for the construction of a proof for a given statement. In this case the rules can be read bottom-up; for example, <math>({\land}R)</math> says that, to prove that <math>A \land B</math> follows from the assumptions <math>\Gamma</math> and <math>\Sigma</math>, it suffices to prove that <math>A</math> can be concluded from <math>\Gamma</math> and <math>B</math> can be concluded from <math>\Sigma</math>, respectively. Note that, given some antecedent, it is not clear how this is to be split into <math>\Gamma</math> and <math>\Sigma</math>. However, there are only finitely many possibilities to be checked since the antecedent by assumption is finite. This also illustrates how proof theory can be viewed as operating on proofs in a combinatorial fashion: given proofs for both <math>A</math> and <math>B</math>, one can construct a proof for <math>A \land B</math>.

When looking for some proof, most of the rules offer more or less direct recipes of how to do this. The rule of cut is different: it states that, when a formula <math>A</math> can be concluded and this formula may also serve as a premise for concluding other statements, then the formula <math>A</math> can be "cut out" and the respective derivations are joined. When constructing a proof bottom-up, this creates the problem of guessing <math>A</math> (since it does not appear at all below). The [[cut-elimination theorem]] is thus crucial to the applications of sequent calculus in [[automated deduction]]: it states that all uses of the cut rule can be eliminated from a proof, implying that any provable sequent can be given a ''cut-free'' proof.

The second rule that is somewhat special is the axiom of identity (I). The intuitive reading of this is obvious: every formula proves itself.  Like the cut rule, the axiom of identity is somewhat redundant: the [[completeness of atomic initial sequents]] states that the rule can be restricted to [[atomic formula]]s without any loss of provability.

Observe that all rules have mirror companions, except the ones for implication. This reflects the fact that the usual language of first-order logic does not include the "is not implied by" connective <math>\not\leftarrow</math> that would be the De Morgan dual of implication. Adding such a connective with its natural rules would make the calculus completely left–right symmetric.

===Example derivations===

Here is the derivation of "<math> \vdash A \lor \lnot A </math>", known as
the ''[[Law of excluded middle]]'' (''tertium non datur'' in Latin).
{| align=center border=0 cellspacing=0 cellpadding=0
|-
| &nbsp;
| &nbsp;
| rowspan=2 | <math>
      (I)
    </math>
|-
| align=center style='border-top:1px solid black;' rowspan=2 | <math>
      A \vdash A
    </math>
| &nbsp;
|-
| &nbsp;
| rowspan=2 | <math>
      (\lnot R)
    </math>
|-
| align=center style='border-top:1px solid black;' rowspan=2 | <math>
      \vdash \lnot A , A
    </math>
| &nbsp;
|-
| &nbsp;
| rowspan=2 | <math>
      (\lor R_2)
    </math>
|-
| align=center style='border-top:1px solid black;' rowspan=2 | <math>
      \vdash A \lor \lnot A , A
    </math>
| &nbsp;
|-
| &nbsp;
| rowspan=2 | <math>
      (PR)
    </math>
|-
| align=center style='border-top:1px solid black;' rowspan=2 | <math>
      \vdash A , A \lor \lnot A
    </math>
| &nbsp;
|-
| &nbsp;
| rowspan=2 | <math>
      (\lor R_1)
    </math>
|-
| align=center style='border-top:1px solid black;' rowspan=2 | <math>
      \vdash A \lor \lnot A , A \lor \lnot A
    </math>
| &nbsp;
|-
| &nbsp;
| rowspan=2 | <math>
      (CR)
    </math>
|-
| align=center style='border-top:1px solid black;' rowspan=2 | <math>
      \vdash A \lor \lnot A
    </math>
| &nbsp;
|-
| &nbsp;
| &nbsp;
|}

Next is the proof of a simple fact involving quantifiers. Note that the converse is not true, and its falsity can be seen when attempting to derive it bottom-up, because an existing free variable cannot be used in substitution in the rules <math>(\forall R)</math> and <math>(\exists L)</math>.
{| align=center border=0 cellspacing=0 cellpadding=0
|-
| &nbsp;
| &nbsp;
| rowspan=2 | <math>
      (I)
    </math>
|-
| align=center style='border-top:1px solid black;' rowspan=2 | <math>
      p(x,y) \vdash p(x,y)
    </math>
| &nbsp;
|-
| &nbsp;
| rowspan=2 | <math>
      (\forall L)
    </math>
|-
| align=center style='border-top:1px solid black;' rowspan=2 | <math>
      \forall x \left( p(x,y) \right) \vdash p(x,y)
    </math>
| &nbsp;
|-
| &nbsp;
| rowspan=2 | <math>
      (\exists R)
    </math>
|-
| align=center style='border-top:1px solid black;' rowspan=2 | <math>
      \forall x \left( p(x,y) \right) \vdash \exists y \left( p(x,y) \right)
    </math>
| &nbsp;
|-
| &nbsp;
| rowspan=2 | <math>
      (\exists L)
    </math>
|-
| align=center style='border-top:1px solid black;' rowspan=2 | <math>
      \exists y \left( \forall x \left( p(x,y) \right) \right) \vdash \exists y \left( p(x,y) \right)
    </math>
| &nbsp;
|-
| &nbsp;
| rowspan=2 | <math>
      (\forall R)
    </math>
|-
| align=center style='border-top:1px solid black;' rowspan=2 | <math>
      \exists y \left( \forall x \left( p(x,y) \right) \right) \vdash \forall x \left( \exists y \left( p(x,y) \right) \right)
    </math>
| &nbsp;
|-
| &nbsp;
| &nbsp;
|}

For something more interesting we shall prove <math>{\left( \left( A \rightarrow \left( B \lor C \right) \right) \rightarrow \left( \left( \left( B \rightarrow \lnot A \right) \land \lnot C \right) \rightarrow \lnot A \right) \right)}</math>. It is straightforward to find the derivation, which exemplifies the usefulness of LK in automated proving.
{| align=center border=0 cellspacing=0 cellpadding=0
|-
|
{| align=center border=0 cellspacing=0 cellpadding=0
|-
| valign=bottom |
{| align=center border=0 cellspacing=0 cellpadding=0
|-
| &nbsp;
| &nbsp;
| rowspan=2 | <math>
      (I)
    </math>
|-
| align=center style='border-top:1px solid black;' rowspan=2 | <math>
      A \vdash A
    </math>
| &nbsp;
|-
| &nbsp;
| rowspan=2 | <math>
      (\lnot R)
    </math>
|-
| align=center style='border-top:1px solid black;' rowspan=2 | <math>
      \vdash \lnot A , A
    </math>
| &nbsp;
|-
| &nbsp;
| rowspan=2 | <math>
      (PR)
    </math>
|-
| align=center style='border-top:1px solid black;' rowspan=2 | <math>
      \vdash A , \lnot A
    </math>
| &nbsp;
|-
| &nbsp;
| &nbsp;
|}
| &nbsp;&nbsp;
| valign=bottom |
{| align=center border=0 cellspacing=0 cellpadding=0
|-
|
{| align=center border=0 cellspacing=0 cellpadding=0
|-
| valign=bottom |
{| align=center border=0 cellspacing=0 cellpadding=0
|-
|
{| align=center border=0 cellspacing=0 cellpadding=0
|-
| valign=bottom |
{| align=center border=0 cellspacing=0 cellpadding=0
|-
|
|  | &nbsp;
| rowspan=2 | <math>
      (I)
    </math>
|-
| align=center style='border-top:1px solid black;' rowspan=2 | <math>
      B \vdash B
    </math>
| &nbsp;
|-
| &nbsp;
| rowspan=2 | <math>
      (WR)
    </math>
|-
| align=center style='border-top:1px solid black;' rowspan=2 | <math>
      B \vdash B, C
    </math>
| &nbsp;
|-
| &nbsp;
| &nbsp;
|}
| &nbsp;&nbsp;
| valign=bottom |
{| align=center border=0 cellspacing=0 cellpadding=0
|-
|
|  | &nbsp;
| rowspan=2 | <math>
      (I)
    </math>
|-
| align=center style='border-top:1px solid black;' rowspan=2 | <math>
      C \vdash C
    </math>
| &nbsp;
|-
| &nbsp;
| rowspan=2 | <math>
      (WR)
    </math>
|-
| align=center style='border-top:1px solid black;' rowspan=2 | <math>
      C \vdash B, C
    </math>
| &nbsp;
|-
| &nbsp;
| &nbsp;
|}
|}
| &nbsp;
| rowspan=2 valign=bottom | <math>
      (\lor L)
    </math>
|-
| align=center style='border-top:1px solid black;' rowspan=2 | <math>
      B \lor C \vdash B , C
    </math>
| &nbsp;
|-
| &nbsp;
| rowspan=2 | <math>
      (PR)
    </math>
|-
| align=center style='border-top:1px solid black;' rowspan=2 | <math>
      B \lor C \vdash C , B
    </math>
| &nbsp;
|-
| &nbsp;
| rowspan=2 | <math>
      (\lnot L)
    </math>
|-
| align=center style='border-top:1px solid black;' rowspan=2 | <math>
      B \lor C , \lnot C \vdash B
    </math>
| &nbsp;
|-
| &nbsp;
| &nbsp;
|}
| &nbsp;&nbsp;
| valign=bottom |
{| align=center border=0 cellspacing=0 cellpadding=0
|-
| &nbsp;
| &nbsp;
| rowspan=2 | <math>
      (I)
    </math>
|-
| align=center style='border-top:1px solid black;' rowspan=2 | <math>
      \lnot A \vdash \lnot A
    </math>
| &nbsp;
|-
| &nbsp;
| &nbsp;
|}
|}
| &nbsp;
| rowspan=2 valign=bottom | <math>
      (\rightarrow L)
    </math>
|-
| align=center style='border-top:1px solid black;' rowspan=2 | <math>
      \left( B \lor C \right) , \lnot C , \left( B \rightarrow \lnot A \right) \vdash \lnot A
    </math>
| &nbsp;
|-
| &nbsp;
| rowspan=2 | <math>
      (\land L_1)
    </math>
|-
| align=center style='border-top:1px solid black;' rowspan=2 | <math>
      \left( B \lor C \right) , \lnot C , \left( \left( B \rightarrow \lnot A \right) \land \lnot C \right) \vdash \lnot A
    </math>
| &nbsp;
|-
| &nbsp;
| rowspan=2 | <math>
      (PL)
    </math>
|-
| align=center style='border-top:1px solid black;' rowspan=2 | <math>
      \left( B \lor C \right) , \left( \left( B \rightarrow \lnot A \right) \land \lnot C \right) , \lnot C \vdash \lnot A
    </math>
| &nbsp;
|-
| &nbsp;
| rowspan=2 | <math>
      (\land L_2)
    </math>
|-
| align=center style='border-top:1px solid black;' rowspan=2 | <math>
      \left( B \lor C \right) , \left( \left( B \rightarrow \lnot A \right) \land \lnot C \right) , \left( \left( B \rightarrow \lnot A \right) \land \lnot C \right) \vdash \lnot A
    </math>
| &nbsp;
|-
| &nbsp;
| rowspan=2 | <math>
      (CL)
    </math>
|-
| align=center style='border-top:1px solid black;' rowspan=2 | <math>
      \left( B \lor C \right) , \left( \left( B \rightarrow \lnot A \right) \land \lnot C \right) \vdash \lnot A
    </math>
| &nbsp;
|-
| &nbsp;
| rowspan=2 | <math>
      (PL)
    </math>
|-
| align=center style='border-top:1px solid black;' rowspan=2 | <math>
      \left( \left( B \rightarrow \lnot A \right) \land \lnot C \right) , \left( B \lor C \right) \vdash \lnot A
    </math>
| &nbsp;
|-
| &nbsp;
| &nbsp;
|}
|}
| &nbsp;
| rowspan=2 valign=bottom | <math>
      (\rightarrow L)
    </math>
|-
| align=center style='border-top:1px solid black;' rowspan=2 | <math>
      \left( \left( B \rightarrow \lnot A \right) \land \lnot C \right) , \left( A \rightarrow \left( B \lor C \right) \right) \vdash \lnot A , \lnot A
    </math>
| &nbsp;
|-
| &nbsp;
| rowspan=2 | <math>
      (CR)
    </math>
|-
| align=center style='border-top:1px solid black;' rowspan=2 | <math>
      \left( \left( B \rightarrow \lnot A \right) \land \lnot C \right) , \left( A \rightarrow \left( B \lor C \right) \right) \vdash \lnot A
    </math>
| &nbsp;
|-
| &nbsp;
| rowspan=2 | <math>
      (PL)
    </math>
|-
| align=center style='border-top:1px solid black;' rowspan=2 | <math>
      \left( A \rightarrow \left( B \lor C \right) \right) , \left( \left( B \rightarrow \lnot A \right) \land \lnot C \right) \vdash \lnot A
    </math>
| &nbsp;
|-
| &nbsp;
| rowspan=2 | <math>
      (\rightarrow R)
    </math>
|-
| align=center style='border-top:1px solid black;' rowspan=2 | <math>
      \left( A \rightarrow \left( B \lor C \right) \right) \vdash \left( \left( \left( B \rightarrow \lnot A \right) \land \lnot C \right) \rightarrow \lnot A \right)
    </math>
| &nbsp;
|-
| &nbsp;
| rowspan=2 | <math>
      (\rightarrow R)
    </math>
|-
| align=center style='border-top:1px solid black;' rowspan=2 | <math>
      \vdash \left( \left( A \rightarrow \left( B \lor C \right) \right) \rightarrow \left( \left( \left( B \rightarrow \lnot A \right) \land \lnot C \right) \rightarrow \lnot A \right) \right)
    </math>
| &nbsp;
|-
| &nbsp;
| &nbsp;
|}

These derivations also emphasize the strictly formal structure of the sequent calculus. For example, the logical rules as defined above always act on a formula immediately adjacent to the turnstile, such that the permutation rules are necessary. Note, however, that this is in part an artifact of the presentation, in the original style of Gentzen. A common simplification involves the use of [[multiset]]s of formulas in the interpretation of the sequent, rather than sequences, eliminating the need for an explicit permutation rule. This corresponds to shifting commutativity of assumptions and derivations outside the sequent calculus, whereas LK embeds it within the system itself.

===Relation to analytic tableaux===
For certain formulations (i.e. variants) of the sequent calculus, a proof in such a calculus is isomorphic to an upside-down, closed [[method of analytic tableaux|analytic tableau]].<ref>{{harvnb|Smullyan|1995|p=107}}</ref>

===Structural rules===

The structural rules deserve some additional discussion.

Weakening (W) allows the addition of arbitrary elements to a sequence.  Intuitively, this is allowed in the antecedent because we can always restrict the scope of our proof (if all cars have wheels, then it's safe to say that all black cars have wheels); and in the succedent because we can always allow for alternative conclusions (if all cars have wheels, then it's safe to say that all cars have either wheels or wings).

Contraction (C) and Permutation (P) assure that neither the order (P) nor the multiplicity of occurrences (C) of elements of the sequences matters. Thus, one could instead of [[sequence]]s also consider [[Set (mathematics)|sets]].

The extra effort of using sequences, however, is justified since part or all of the structural rules may be omitted. Doing so, one obtains the so-called [[substructural logic]]s.

===Properties of the system LK===

This system of rules can be shown to be both [[soundness|sound]] and [[completeness (logic)|complete]] with respect to first-order logic, i.e. a statement <math>A</math> follows [[semantics|semantically]] from a set of premises <math>\Gamma</math> <math>(\Gamma \vDash A)</math> [[if and only if]] the sequent <math>\Gamma \vdash A</math> can be derived by the above rules.<ref>{{harvnb|Kleene|2002|p=336}}, wrote in 1967 that "it was a major logical discovery by Gentzen 1934–5 that, when there is any (purely logical) proof of a proposition, there is a direct proof. The implications of this discovery are in theoretical logical investigations, rather than in building collections of proved formulas."</ref>

In the sequent calculus, the rule of [[cut-elimination|cut is admissible]]. This result is also referred to as Gentzen's ''Hauptsatz'' ("Main Theorem").<ref name=curry_cut_elimination /><ref name=kleene_cut_elimination />