Sequent Calculus

VerificationsPermalink

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

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

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

where $P$ is atomic

ConjunctionsPermalink

Introduction rule ($I$):

Elimination rules ($E$):

ImplicationsPermalink

Introduction rule ($I^x$):

Elimination rules ($E$):

DisjunctionsPermalink

Introduction rule ($I$):

Elimination rules ($E$):

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

SequentsPermalink

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:

Identity rule:

ConjunctionsPermalink

Right rules:

Left rules:

ImplicationsPermalink

Right rules:

Left rules:

DisjunctionsPermalink

Right rules:

Left rules:

FalsehoodPermalink

Right rules:

Left rules: