Sequent Calculus

Verifications

\(A\uparrow\) means $A$ has a verification.

\(A\downarrow\) means $A$ ay be used

A conversion rule ($\downarrow\uparrow$):

\[\frac{P\downarrow} {P\uparrow}\]

where $P$ is atomic

Conjunctions

Introduction rule ($I$):

\[\frac{A\uparrow,B\uparrow} {A\wedge B\uparrow}\]

Elimination rules ($E$):

\[\frac{A\wedge B\downarrow} {A\downarrow}\] \[\frac{A\wedge B\downarrow} {B\downarrow}\]

Implications

Introduction rule ($I^x$):

\[\frac{\overline{A\downarrow}^x\ B\uparrow} {A\supset B\uparrow}\]

Elimination rules ($E$):

\[\frac{A\supset B\downarrow A\uparrow} {B\downarrow}\]

Disjunctions

Introduction rule ($I$):

\[\frac{A\uparrow} {A\vee B\uparrow}\] \[\frac{B\uparrow} {A\vee B\uparrow}\]

Elimination rules ($E$):

\[\frac{A\vee B\downarrow,\overline{A\downarrow}^x\ C\uparrow,\overline{B\downarrow}^y\ C\uparrow} {C\uparrow}\]

Note: We can’t use elimination right after introduction, becasue the arrows don’t match

Sequents

So for natural deduction, we have elimination rules and introduction rules. For sequent calculus, we have left rules and right rules, where left rules are just the inverse of the elimination rules, and right rules are just the same as introduction rules.

The reasoning behind it is that elimination rules always produce down arrows, and introduction rules always produce up arrows. If we use natural deduction, we will kind of need to work on two directions, and when they meet, we stop and use the conversion rule ($\downarrow\uparrow$).

To simplify things, we reverse the elimination rules so that it is also pointing upward, so that we will only need to work in one direction. And we stop at something called identity rule.

Basically everything with $uparrow$ should be on the right of $\Rightarrow$, and vice versa.

We use the following notation:

\[B_1,\ldots,B_n\Rightarrow A\]

Identity rule:

\[\frac{} {P,P\Rightarrow P}\]

Conjunctions

Right rules:

\[\frac{\Gamma\Rightarrow A,\Gamma\Rightarrow b} {\Gamma\Rightarrow A\wedge B}\]

Left rules:

\[\frac{\Gamma,A\wedge B,A\Rightarrow C} {\Gamma,A\wedge B\Rightarrow C}\] \[\frac{\Gamma,A\wedge B,C\Rightarrow C} {\Gamma,A\wedge B\Rightarrow C}\]

Implications

Right rules:

\[\frac{\Gamma,A\Rightarrow B} {\Gamma\Rightarrow A\supset B}\]

Left rules:

\[\frac{\Gamma,A\supset B\Rightarrow A\ \ \ \Gamma,A\supset B,B\Rightarrow C} {\Gamma,A\supset B\Rightarrow C}\]

Disjunctions

Right rules:

\[\frac{\Gamma\Rightarrow A} {\Gamma\Rightarrow A\vee B}\] \[\frac{\Gamma\Rightarrow B} {\Gamma\Rightarrow A\vee B}\]

Left rules:

\[\frac{\Gamma,A\vee B,A\Rightarrow C\ \ \ \Gamma,A\vee B,B\Rightarrow C} {\Gamma,A\vee B\Rightarrow C}\]

Falsehood

Right rules:

\[no\ \perp R\]

Left rules:

\[\frac{} {\Gamma,\perp\Rightarrow C}\]