Resources
The notation of the Sequent Calculus looks something like:
There is no inherent interpretation of this notation. The common inference rules to simulate formal logic say that the left side of a turnstile are conjunctive assumptions and the right side are disjunctive conclusions. Each side can be seen as a (possibly empty) list of metavariables.
These turnstile-based terms can be composed into an inference rule:
The top can be seen as the inputs and the bottom as outputs. The separating line is an inference line.
To develop a Proof System, we add some Axioms and structural inference rules:
- Exch: Exchange, reordering lists
- Weak: Weakening, introduce more assumptions or conclusions
- Contr: Contraction, remove duplicate assumptions or conclusions
L(eft) refers to assumptions and R(ight) to conclusions.
Now here are some inference rules for conjunction:
These inference rules can be composed into a derivation tree. A derivation tree starting with all Axioms, and following valid inference rules, is a proof of the bottom-most sequent.
Sequent Natural Deduction & Natural Deduction
We can make any structural rule implicit and arrive at Sequent Natural Deduction:
Note that there is only ever 1 conclusion in a turnstile term. Leveraging this fact, we can simplify once again to arrive at Natural Deduction:
The transformation from Sequent Natural Deduction to Natural Deduction merges the duplication between the assumptions and the inputs above its inference line.
Some of the previous rules in the Sequent Calculus no longer apply to either Natural Deduction, due to the 1-conclusion property. Instead, there are introduction and elimination rules:
One-Sided Sequent Calculus
Another approach is a One-sided Sequent Calculus, where terms only appear on the right side of the turnstile. Starting from scratch, we try to recreate classical logic:
Note that the