Sequent Calculus - The System LK - Example Derivations

Example Derivations

Here is the derivation of "", known as the Law of excluded middle (tertium non datur in Latin).

(I)
A \vdash A
(\lnot R)
\vdash \lnot A, A
(\or R_2)
\vdash A \or \lnot A, A
(PR)
\vdash A, A \or \lnot A
(\or R_1)
\vdash A \or \lnot A, A \or \lnot A
(CR)
\vdash A \or \lnot A

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

(I)
p(x,y) \vdash p(x,y)
(\forall L)
\forall x \left( p(x,y) \right) \vdash p(x,y)
(\exists R)
\forall x \left( p(x,y) \right) \vdash \exists y \left( p(x,y) \right)
(\exists L)
\exists y \left( \forall x \left( p(x,y) \right) \right) \vdash \exists y \left( p(x,y) \right)
(\forall R)
\exists y \left( \forall x \left( p(x,y) \right) \right) \vdash \forall x \left( \exists y \left( p(x,y) \right) \right)

For something more interesting we shall prove . It is straightforward to find the derivation, which exemplifies the usefulness of LK in automated proving.

(I)
A \vdash A
(\lnot R)
\vdash \lnot A, A
(PR)
\vdash A, \lnot A
(I)
B \vdash B
(I)
C \vdash C
(\or L)
B \or C \vdash B, C
(PR)
B \or C \vdash C, B
(\lnot L)
B \or C, \lnot C \vdash B
(I)
\lnot A \vdash \lnot A
(\rightarrow L)
\left( B \or C \right), \lnot C, \left( B \rightarrow \lnot A \right) \vdash \lnot A
(\and L_1)
\left( B \or C \right), \lnot C, \left( \left( B \rightarrow \lnot A \right) \and \lnot C \right) \vdash \lnot A
(PL)
\left( B \or C \right), \left( \left( B \rightarrow \lnot A \right) \and \lnot C \right), \lnot C \vdash \lnot A
(\and L_2)
\left( B \or C \right), \left( \left( B \rightarrow \lnot A \right) \and \lnot C \right), \left( \left( B \rightarrow \lnot A \right) \and \lnot C \right) \vdash \lnot A
(CL)
\left( B \or C \right), \left( \left( B \rightarrow \lnot A \right) \and \lnot C \right) \vdash \lnot A
(PL)
\left( \left( B \rightarrow \lnot A \right) \and \lnot C \right), \left( B \or C \right) \vdash \lnot A
(\rightarrow L)
\left( \left( B \rightarrow \lnot A \right) \and \lnot C \right), \left( A \rightarrow \left( B \or C \right) \right) \vdash \lnot A, \lnot A
(CR)
\left( \left( B \rightarrow \lnot A \right) \and \lnot C \right), \left( A \rightarrow \left( B \or C \right) \right) \vdash \lnot A
(PL)
\left( A \rightarrow \left( B \or C \right) \right), \left( \left( B \rightarrow \lnot A \right) \and \lnot C \right) \vdash \lnot A
(\rightarrow R)
\left( A \rightarrow \left( B \or C \right) \right) \vdash \left( \left( \left( B \rightarrow \lnot A \right) \and \lnot C \right) \rightarrow \lnot A \right)
(\rightarrow R)
\vdash \left( \left( A \rightarrow \left( B \or C \right) \right) \rightarrow \left( \left( \left( B \rightarrow \lnot A \right) \and \lnot C \right) \rightarrow \lnot A \right) \right)

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

Read more about this topic:  Sequent Calculus, The System LK