Editing Sequent calculus (section)

===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.