202310120910

Tags : Logic

---

Sequent Calculus

Gerhard Gentzen

Big Induction Thingy

The guy introduced Sequent Calculus as a method to study Natural Deduction

Hilbert Style Proofs are a mathematically simple model, while Natural Deduction proofs are closer in spriti to teh proofs written by humans. The goal of Sequent Calculus is to be a more adequate tool for proof construction than natural deductions by getting rid of elimination rules. This makes sure that if you read the proof bottom-up, the more complex formulas are always derived from more simpler ones.

Definition

A sequent is a pair $(\Gamma ,\Delta )$ where $\Gamma$ and $\Delta$ are finite sequences for formulae called antecedent and succedent respectively, we also write it as $\Gamma ⊢\Delta$

The intuitive meaning of $\Gamma ⊢\Delta$ is that the conjunctions of all the formulas in $\Gamma$ implies the disjunction of all formulas in $\Delta$.

The rules for Sequent Calculus are

Logics that can be expressed using Sequent Calculus

Adding restriction or getting rid of the rules changes the logic that is being used by the calculus, for example

• Enforcing that $|\Delta |\le 1$ makes this intuitionistic logic
• Enforcing that $|\Delta |=1$ makes it minimal logic
• Enforcing that $|\Delta |\ge 1$ makes it Pierce Type logic
• Getting rid of the contraction rules makes it linear logic and so on

---

References