Proof theory · The Lumenary

MotivationH

Studying proofs themselves

Hilbert hoped to prove the consistency of arithmetic by treating proofs as finite combinatorial objects and showing that none of them ends in $0 = 1$ . Gödel's second theorem (see the incompleteness theorems) shows that such a proof cannot be carried out inside $\mathsf{PA}$ itself. Yet in 1936 Gerhard Gentzen proved the consistency of $\mathsf{PA}$ by a finitary argument plus one carefully isolated non-finitary principle: transfinite induction along the ordinals below $\varepsilon_0 = \sup\{\omega, \omega^\omega, \omega^{\omega^\omega}, \dots\}$ .

The tools Gentzen built for this — the sequent calculus and the Hauptsatz (cut elimination) — became the backbone of modern logic. They explain why proof search is possible, why intuitionistic proofs contain witnesses, how strong a theory is (its proof-theoretic ordinal), and, through the Curry–Howard correspondence, why a proof in Lean is literally a program. This lesson develops the core: sequent calculi, a complete proof of cut elimination for propositional logic, and a guided tour of Gentzen's consistency proof.

IntuitionH

Lemmas are detours

In everyday mathematics we prove a lemma $A$ and then use it to prove $B$ . Formally this is the cut rule: from " $\Gamma$ yields $A$ " and " $A$ yields $B$ ", conclude " $\Gamma$ yields $B$ ". The lemma $A$ may be far more complicated than $\Gamma$ or $B$ — think of proving a statement about integers by complex analysis.

Gentzen's Hauptsatz says that, in pure logic, every lemma can be eliminated: the proof can be rewritten so that it never mentions any formula that is not already a piece (a subformula) of the conclusion. Such a proof is analytic: it only takes the goal apart. Two consequences are immediate. A cut-free proof of a contradiction would have to be built from pieces of "nothing", so there is none — consistency. And to search for a proof of a formula we need only look at its subformulas, a finite space — decidability of propositional logic.

The price is size. Inlining a lemma used many times copies its proof many times, and lemmas about lemmas compound the effect: eliminating cuts can make proofs enormously longer.

DefinitionsH

Sequent calculi

Definition— sequent

A sequent $\Gamma \Rightarrow \Delta$ consists of two finite multisets of formulas. It means: the conjunction of the formulas in $\Gamma$ implies the disjunction of those in $\Delta$ . An empty $\Gamma$ means "true", an empty $\Delta$ means "false"; so $\;\Rightarrow\;$ (both empty) is a contradiction.

Definition— LK and LJ

Gentzen's classical calculus LK has the axioms $A \Rightarrow A$ and, for each connective, a left and a right rule. For example

\dfrac{\Gamma \Rightarrow \Delta, A \qquad \Gamma \Rightarrow \Delta, B}{\Gamma \Rightarrow \Delta, A \wedge B}\;(\wedge R) \qquad \dfrac{A, B, \Gamma \Rightarrow \Delta}{A \wedge B, \Gamma \Rightarrow \Delta}\;(\wedge L) \qquad \dfrac{A, \Gamma \Rightarrow \Delta, B}{\Gamma \Rightarrow \Delta, A \to B}\;(\to R)

together with structural rules (weakening, contraction, exchange) and the cut rule

\dfrac{\Gamma \Rightarrow \Delta, A \qquad A, \Gamma' \Rightarrow \Delta'}{\Gamma, \Gamma' \Rightarrow \Delta, \Delta'}\;(\mathrm{cut}).

The intuitionistic calculus LJ is obtained by allowing at most one formula on the right of every sequent. The quantifier rules are $\forall R$ : from $\Gamma \Rightarrow \Delta, A(y)$ infer $\Gamma \Rightarrow \Delta, \forall x\, A(x)$ when $y$ is not free in the conclusion, and dually for $\exists$ .

The restriction defining LJ is exactly what blocks classical reasoning: the classical proof of $\Rightarrow p \vee \neg p$ passes through the sequent $\Rightarrow p, \neg p$ , which has two formulas on the right.

For classical logic it is convenient to use a one-sided calculus (Schütte, Tait). Formulas are in negation normal form: built from literals $p_n$ and $\neg p_n$ by $\wedge$ and $\vee$ (every formula is classically equivalent to one). The dual $A^\perp$ pushes a negation inwards: $p^\perp = \neg p$ , $(\neg p)^\perp = p$ , $(A \wedge B)^\perp = A^\perp \vee B^\perp$ , $(A \vee B)^\perp = A^\perp \wedge B^\perp$ .

Definition— the one-sided calculus GS

A sequent $\vdash \Gamma$ is a finite set of formulas, read as their disjunction; " $\Gamma, A$ " means $\Gamma \cup \{A\}$ . The rules are

\dfrac{}{\vdash \Gamma, p, \neg p}\;(\mathrm{Ax}) \qquad \dfrac{\vdash \Gamma, A \qquad \vdash \Gamma, B}{\vdash \Gamma, A \wedge B}\;(\wedge) \qquad \dfrac{\vdash \Gamma, A, B}{\vdash \Gamma, A \vee B}\;(\vee) \qquad \dfrac{\vdash \Gamma, A \qquad \vdash \Gamma, A^\perp}{\vdash \Gamma}\;(\mathrm{cut}).

We write $\vdash^n \Gamma$ if $\Gamma$ has a cut-free derivation of height at most $n$ . Weakening and contraction are not rules: the axiom allows any side formulas, and sets absorb repetitions.

Definition— subformula

The subformulas of $A$ are $A$ itself and, if $A = B \wedge C$ or $B \vee C$ , the subformulas of $B$ and of $C$ . A derivation has the subformula property if every formula in it is a subformula of a formula in its conclusion.

Every rule of GS except cut has the subformula property: its premises consist of subformulas of its conclusion. Cut introduces an arbitrary formula $A$ .

Worked examplesH

Examples

Example— Excluded middle and Peirce's law

In GS: $\vdash p, \neg p$ is an axiom, so one $\vee$ -step gives $\vdash p \vee \neg p$ . Peirce's law $((p \to q) \to p) \to p$ has negation normal form $((\neg p \vee q) \wedge \neg p) \vee p$ ; after the $\vee$ -step, the $\wedge$ -rule leaves $\vdash \neg p \vee q, p$ and $\vdash \neg p, p$ , both closed quickly. Neither formula is provable in LJ: a cut-free LJ proof of $\Rightarrow p \vee \neg p$ would end with $\vee R$ (see the disjunction property below), so $\Rightarrow p$ or $\Rightarrow \neg p$ would be provable, and neither is.

Example— A failed search is a countermodel

Search for a proof of $\vdash p \vee (q \wedge \neg p)$ : the $\vee$ -step gives $\vdash p, q \wedge \neg p$ , and the $\wedge$ -step gives $\vdash p, q$ and $\vdash p, \neg p$ . The second is an axiom; the first consists of literals with no complementary pair, so it is not derivable — and the valuation making $p$ and $q$ false refutes it, hence refutes the original formula.

Example— A useful cut

Suppose $\vdash \Gamma, A$ and $\vdash \Delta, A^\perp$ have short proofs, and $A$ is used many times in a long argument. Eliminating the cut replaces each use of $A$ by a copy of its proof. For first-order logic, Statman (1979) and Orevkov (1979) found sequences of formulas with proofs of size polynomial in $n$ using cuts whose shortest cut-free proofs have size at least a tower $2^{2^{\cdot^{\cdot^{2}}}}$ of height about $n$ — non-elementary growth.

ProofH

Cut elimination for propositional logic

We prove that cut is admissible in GS by Gentzen-style syntactic reductions. Three lemmas about cut-free derivations come first.

Theorem— Lemma 1 (weakening)

If $\vdash^n \Gamma$ then $\vdash^n \Gamma \cup \Sigma$ for every finite set $\Sigma$ .

Proof

Induction on the derivation: add $\Sigma$ to every sequent. Axioms stay axioms, and each rule instance remains an instance because the rules share their context.

∎

Theorem— Lemma 2 (inversion)

If $\vdash^n \Gamma$ and $A \wedge B \in \Gamma$ , then $\vdash^n (\Gamma \setminus \{A \wedge B\}) \cup \{A\}$ and $\vdash^n (\Gamma \setminus \{A \wedge B\}) \cup \{B\}$ . If $\vdash^n \Gamma$ and $A \vee B \in \Gamma$ , then $\vdash^n (\Gamma \setminus \{A \vee B\}) \cup \{A, B\}$ .

Proof

We treat $A \wedge B$ and the conclusion with $A$ ; the other cases are the same. Write $\Gamma^- = \Gamma \setminus \{A \wedge B\}$ and argue by induction on $n$ , looking at the last rule.

Axiom. $\Gamma$ contains a complementary pair of literals; so does $\Gamma^- \cup \{A\}$ .
Principal formula $A \wedge B$ . The premise $\vdash^{n-1} \Sigma, A$ has $\Sigma \cup \{A \wedge B\} = \Gamma$ , so $\Sigma \subseteq \Gamma$ . If $A \wedge B \notin \Sigma$ , then $\Sigma = \Gamma^-$ and we are done (raising the height bound is harmless). If $A \wedge B \in \Sigma$ , apply the induction hypothesis to the premise to remove it: $\vdash^{n-1} (\Sigma \setminus \{A \wedge B\}) \cup \{A\} = \Gamma^- \cup \{A\}$ .
Another principal formula $C$ (so $C \neq A \wedge B$ ), with premises $\Sigma \cup \Pi_i$ , where $\Pi_i$ is $\{C_1\}$ , $\{C_2\}$ for $C = C_1 \wedge C_2$ or $\{C_1, C_2\}$ for $C = C_1 \vee C_2$ , and $\Sigma \cup \{C\} = \Gamma$ ; thus $A \wedge B \in \Sigma$ . Put $\Sigma^- = \Sigma \setminus \{A \wedge B\}$ and turn each premise into a derivation of $(\Sigma^- \cup \{A\}) \cup \Pi_i$ of height at most $n - 1$ : if $A \wedge B \notin \Pi_i$ , by the induction hypothesis; if $A \wedge B \in \Pi_i$ , by weakening the premise with $A$ (the premise already equals $\Sigma^- \cup \Pi_i$ ). The same rule with context $\Sigma^- \cup \{A\}$ then gives $\Sigma^- \cup \{A, C\} = \Gamma^- \cup \{A\}$ at height $n$ . $\blacksquare$

∎

Theorem— Lemma 3 (atomic cuts)

If $\vdash \Gamma, p$ and $\vdash \Gamma, \neg p$ cut-free, then $\vdash \Gamma$ cut-free.

Proof

If $p \in \Gamma$ or $\neg p \in \Gamma$ , one of the hypotheses already is $\vdash \Gamma$ . Otherwise argue by induction on the height of the derivation of $\vdash \Gamma, p$ . If it is an axiom, its complementary pair cannot involve $p$ (that would need $\neg p \in \Gamma$ ), so $\Gamma$ is an axiom. If its last rule has principal formula $C \in \Gamma$ , say $C = C_1 \wedge C_2$ , let $\Gamma_0 = \Gamma \setminus \{C\}$ . Weakening and inversion turn the premises into derivations of $\vdash \Gamma_0, C_i, p$ of smaller height, and inversion applied to $\vdash \Gamma, \neg p$ gives $\vdash \Gamma_0, C_i, \neg p$ . By the induction hypothesis $\vdash \Gamma_0, C_1$ and $\vdash \Gamma_0, C_2$ ; the $\wedge$ -rule gives $\vdash \Gamma$ . The case $C = C_1 \vee C_2$ is the same with one premise.

∎

Theorem— Hauptsatz (cut elimination; Gentzen 1935, propositional case)

If $\vdash \Gamma, A$ and $\vdash \Gamma, A^\perp$ have cut-free derivations, so does $\vdash \Gamma$ . Consequently every sequent derivable in GS with cuts has a cut-free derivation.

Proof

Induction on the number of connectives in $A$ . If $A \in \Gamma$ or $A^\perp \in \Gamma$ there is nothing to prove, so assume neither is.

$A$ is a literal: Lemma 3 (for $A = \neg p$ , exchange the roles of the two derivations).
$A = B \wedge C$ , so $A^\perp = B^\perp \vee C^\perp$ . Inversion gives $\vdash \Gamma, B$ and $\vdash \Gamma, C$ from the first derivation, and $\vdash \Gamma, B^\perp, C^\perp$ from the second. Weakening $\vdash \Gamma, C$ to $\vdash \Gamma, B^\perp, C$ and using the induction hypothesis for the smaller formula $C$ with context $\Gamma \cup \{B^\perp\}$ gives $\vdash \Gamma, B^\perp$ . The induction hypothesis for $B$ with context $\Gamma$ gives $\vdash \Gamma$ .
$A = B \vee C$ : the same, with the two derivations exchanged, since $A^\perp = B^\perp \wedge C^\perp$ .

For the consequence, remove the cuts of a derivation one at a time, always choosing a cut whose premises are already cut-free (an uppermost cut).

∎

The same strategy — invertibility where available, then induction on the cut formula and, in general, on the height of the derivations — proves cut elimination for first-order LK and for LJ (Gentzen 1935). For LJ, not all rules are invertible and the induction on height does real work; see Troelstra and Schwichtenberg (2000, chapter 4).

Theorem— Corollaries

Subformula property. Every derivable sequent has a derivation using only its subformulas.
Consistency. The empty sequent is not derivable, even with cut: no cut-free rule has the empty set as conclusion.
Decidability. Propositional derivability is decidable: a cut-free derivation of $\vdash \Gamma$ involves only subsets of the (finite) set of subformulas of $\Gamma$ .
Disjunction property of LJ. If $\Rightarrow A \vee B$ is derivable in LJ, then $\Rightarrow A$ or $\Rightarrow B$ is derivable.

Proof

1–3 are immediate from the shape of the cut-free rules. For 4, take a cut-free LJ derivation of $\Rightarrow A \vee B$ . Its last rule cannot be a left rule (the antecedent is empty), nor contraction on the right (the right side holds one formula), nor weakening on the right (its premise would be the empty sequent, which has no cut-free LJ derivation, by the argument of 2); so it is $\vee R$ , whose premise is $\Rightarrow A$ or $\Rightarrow B$ .

∎

The disjunction property is the logical form of the slogan that intuitionistic proofs contain witnesses; for first-order LJ the same argument gives the existence property: if $\Rightarrow \exists x\, A(x)$ is derivable then so is $\Rightarrow A(t)$ for some term $t$ .

Theorem— Semantic route: cut-free completeness

If $\Gamma$ is valid (every valuation makes some formula of $\Gamma$ true), then $\vdash \Gamma$ has a cut-free derivation. Hence, with soundness, cut is admissible.

Proof

Induction on the number of connectives in $\Gamma$ . The rules are semantically invertible: if $\Gamma, A \wedge B$ is valid so are $\Gamma, A$ and $\Gamma, B$ ; if $\Gamma, A \vee B$ is valid so is $\Gamma, A, B$ . So if $\Gamma$ contains a compound formula, decompose it and apply the induction hypothesis. If $\Gamma$ consists of literals and contains no complementary pair, the valuation making $p$ true exactly when $\neg p \in \Gamma$ makes every member of $\Gamma$ false; so a valid $\Gamma$ of literals contains a pair, and is an axiom. A derivation with cuts is sound, so its conclusion is valid, so it has a cut-free derivation.

∎

This argument is short but uses the completeness theorem in miniature. Gentzen's syntactic proof gives more: an explicit transformation of proofs, bounds on its cost, and a method that extends to systems such as arithmetic where no completeness theorem rescues us.

ExplanationH

Gentzen's consistency proof and ordinal analysis

In $\mathsf{PA}$ the induction schema cannot be eliminated like a cut: a derivation may use the induction rule, from $\Gamma, A(x) \Rightarrow A(Sx), \Delta$ infer $\Gamma, A(0) \Rightarrow A(t), \Delta$ , with induction formulas of unbounded complexity. Gentzen's idea was to measure derivations by ordinals.

Ordinals below $\varepsilon_0$ . Every ordinal $\alpha$ with $0 \lt \alpha \lt \varepsilon_0$ has a unique Cantor normal form $\alpha = \omega^{\alpha_1} + \cdots + \omega^{\alpha_k}$ with $\alpha \gt \alpha_1 \ge \cdots \ge \alpha_k$ , and the exponents again have normal forms. So these ordinals are coded by finite trees, with a primitive recursive order: a notation system. Here $\varepsilon_0$ is the least ordinal $\varepsilon$ with $\omega^\varepsilon = \varepsilon$ (see ordinals and cardinals).

The proof (outline).

Work with a sequent calculus for $\mathsf{PA}$ whose axioms are true closed atomic sequents and whose only non-logical rule is the induction rule, and assign to each derivation $d$ an ordinal $o(d) \lt \varepsilon_0$ , computed from the shape of $d$ and the complexity of its cut and induction formulas.
Define a primitive recursive reduction $d \mapsto d'$ on derivations of the empty sequent: replace an induction by finitely many cuts (unfolding it up to the numeral concerned), or reduce a cut on a complex formula to cuts on simpler ones, always so that $o(d') \lt o(d)$ .
A derivation of $\;\Rightarrow\;$ (of $0 = 1$ ) would yield an infinite sequence $d, d', d'', \dots$ with strictly decreasing ordinals below $\varepsilon_0$ .
Transfinite induction up to $\varepsilon_0$ , applied to quantifier-free (primitive recursive) predicates, rules this out.

Everything except step 4 can be carried out in primitive recursive arithmetic $\mathsf{PRA}$ . So $\mathsf{PRA} + \mathrm{TI}(\varepsilon_0)$ proves $\mathrm{Con}_{\mathsf{PA}}$ , and by Gödel's second theorem $\mathsf{PA}$ does not prove $\mathrm{TI}(\varepsilon_0)$ for this notation system. Gentzen (1943) showed the converse half: $\mathsf{PA}$ proves transfinite induction up to every ordinal below $\varepsilon_0$ in the system. Hence $\varepsilon_0$ is the proof-theoretic ordinal of $\mathsf{PA}$ , written $|\mathsf{PA}| = \varepsilon_0$ .

Ordinal analysis computes such ordinals for stronger theories: for example $|\mathsf{ACA}_0| = \varepsilon_0$ as well, while the predicative theory $\mathsf{ATR}_0$ has ordinal $\Gamma_0$ , the Feferman–Schütte ordinal. The ordinal also measures computational strength: the functions $\mathsf{PA}$ proves total are exactly those computable in time bounded by some $F_\alpha$ , $\alpha \lt \varepsilon_0$ , of the fast-growing hierarchy. Goodstein's theorem (the computation below) is true, provable from $\mathrm{TI}(\varepsilon_0)$ , and unprovable in $\mathsf{PA}$ (Kirby and Paris, 1982).

ExplanationH

Proofs as programs

In Gentzen's natural deduction, a proof of $A \to B$ ends with $\to$ -introduction (assume $A$ , derive $B$ , discharge), and $\to$ -elimination is modus ponens. A detour is an introduction immediately followed by an elimination; removing it is the natural-deduction analogue of eliminating a cut (Prawitz 1965).

The Curry–Howard correspondence reads this as computation. Propositions are types; a proof of $A \to B$ is a function $\lambda x{:}A.\, t$ ; modus ponens is application; and removing a detour is the $\beta$ -reduction $(\lambda x.\, t)\, u \to t[u/x]$ . Conjunction is the product type, disjunction the sum type. Normalisation of proofs (every proof reduces to one without detours) becomes strong normalisation of the simply typed $\lambda$ -calculus (see the λ-calculus and type theory). Lean is built on this: a Lean proof is a term of a dependent type theory, and the kernel checks it by type-checking.

Formal mathematicsF

A sequent calculus in Lean

The Lean module formalises the one-sided calculus of this lesson (with lists for sequents and an explicit exchange rule), its semantics, and the semantic route to cut admissibility. Formulas in negation normal form, the dual, and truth under a valuation:

FmlLean 4Formally verified

/-- Propositional formulas in **negation normal form**: atoms `pos n` (the variable `pₙ`),
negated atoms `neg n` (`¬pₙ`), conjunction and disjunction. Every propositional formula is
equivalent to one of these (push negations inwards with De Morgan's laws). -/
inductive Fml : Type
  | pos : ℕ → Fml
  | neg : ℕ → Fml
  | and : Fml → Fml → Fml
  | or : Fml → Fml → Fml
  deriving DecidableEq

Axioms used: No axiomsformal/Lumenary/ProofTheory.leanTry it in the Lean web editor

dualLean 4Formally verified

/-- The **dual** `Aᗮ` of a formula: its negation, pushed to the atoms by De Morgan's laws. -/
def dual : Fml → Fml
  | pos n => neg n
  | neg n => pos n
  | and A B => or (dual A) (dual B)
  | or A B => and (dual A) (dual B)

Axioms used: No axiomsformal/Lumenary/ProofTheory.leanTry it in the Lean web editor

eval_dualLean 4Proved here from basic factsFormally verified

/-- The dual really is the negation: `Aᗮ` is true exactly when `A` is false. By induction on
`A`, using De Morgan's laws at the connectives. -/
theorem eval_dual (v : ℕ → Prop) : ∀ A : Fml, eval v (dual A) ↔ ¬ eval v A
  | pos n => by simp [dual, eval]
  | neg n => by simp [dual, eval]
  | and A B => by
      simp only [dual, eval, eval_dual v A, eval_dual v B]
      tauto
  | or A B => by
      simp only [dual, eval, eval_dual v A, eval_dual v B]
      tauto

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/ProofTheory.leanTry it in the Lean web editor

Validity, and derivability with a flag saying whether cut is allowed:

ValidLean 4Formally verified

/-- A one-sided sequent `⊢ Γ` is read as the disjunction of the formulas in `Γ`. It is
**valid** if every valuation makes at least one formula of `Γ` true. -/
def Valid (Γ : List Fml) : Prop :=
  ∀ v : ℕ → Prop, ∃ A ∈ Γ, A.eval v

Axioms used: No axiomsformal/Lumenary/ProofTheory.leanTry it in the Lean web editor

DerivLean 4Formally verified

/-- Derivations in a one-sided sequent calculus (after Schütte and Tait). `Deriv c Γ` means
`⊢ Γ` is derivable, using the cut rule only if the flag `c` is `true`. The rules:
* **axiom**: `⊢ Γ` whenever `Γ` contains both `pₙ` and `¬pₙ`;
* **∧**: from `⊢ A, Γ` and `⊢ B, Γ` infer `⊢ A ∧ B, Γ`;
* **∨**: from `⊢ A, B, Γ` infer `⊢ A ∨ B, Γ`;
* **exchange**: reorder a sequent;
* **cut**: from `⊢ A, Γ` and `⊢ Aᗮ, Γ` infer `⊢ Γ` (only when `c = true`).
No weakening or contraction rules are needed: the axiom allows any side formulas, and both rules
are admissible (a consequence of `cut_free_complete` below). -/
inductive Deriv : Bool → List Fml → Prop
  | ax {c : Bool} {Γ : List Fml} (n : ℕ) :
      pos n ∈ Γ → neg n ∈ Γ → Deriv c Γ
  | and {c : Bool} {Γ : List Fml} (A B : Fml) :
      Deriv c (A :: Γ) → Deriv c (B :: Γ) → Deriv c (Fml.and A B :: Γ)
  | or {c : Bool} {Γ : List Fml} (A B : Fml) :
      Deriv c (A :: B :: Γ) → Deriv c (Fml.or A B :: Γ)
  | exchange {c : Bool} {Γ Δ : List Fml} :
      Γ.Perm Δ → Deriv c Γ → Deriv c Δ
  | cut {Γ : List Fml} (A : Fml) :
      Deriv true (A :: Γ) → Deriv true (dual A :: Γ) → Deriv true Γ

Axioms used: No axiomsformal/Lumenary/ProofTheory.leanTry it in the Lean web editor

excluded_middleLean 4Proved here from basic factsFormally verified

/-- A first cut-free derivation: `⊢ p₀ ∨ ¬p₀`. Apply the ∨-rule, then the axiom. -/
theorem excluded_middle : Deriv false [Fml.or (pos 0) (neg 0)] :=
  Deriv.or _ _ (Deriv.ax 0 (by simp) (by simp))

Axioms used: propextformal/Lumenary/ProofTheory.leanTry it in the Lean web editor

Soundness is an induction over derivations. Its cut case is the only place where eval_dual is needed: $A$ and $A^\perp$ cannot both be true.

soundnessLean 4Proved here from basic factsFormally verified

/-- **Soundness**: every derivable sequent — with or without cut — is valid. By induction on
the derivation. For the cut rule: if neither `A` nor `Aᗮ` is the true formula supplied by the
premises, some formula of `Γ` is true; and `A`, `Aᗮ` cannot both be true. -/
theorem soundness {c : Bool} {Γ : List Fml} (d : Deriv c Γ) : Valid Γ := by
  induction d with
  | ax n hp hn =>
      intro v
      by_cases h : v n
      · exact ⟨pos n, hp, h⟩
      · exact ⟨neg n, hn, h⟩
  | and A B _ _ ihA ihB =>
      intro v
      obtain ⟨C, hC, hCv⟩ := ihA v
      obtain ⟨D, hD, hDv⟩ := ihB v
      rcases List.mem_cons.mp hC with rfl | hC
      · rcases List.mem_cons.mp hD with rfl | hD
        · exact ⟨Fml.and C D, by simp, hCv, hDv⟩
        · exact ⟨D, List.mem_cons_of_mem _ hD, hDv⟩
      · exact ⟨C, List.mem_cons_of_mem _ hC, hCv⟩
  | or A B _ ih =>
      intro v
      obtain ⟨C, hC, hCv⟩ := ih v
      rcases List.mem_cons.mp hC with rfl | hC
      · exact ⟨Fml.or C B, by simp, Or.inl hCv⟩
      rcases List.mem_cons.mp hC with rfl | hC
      · exact ⟨Fml.or A C, by simp, Or.inr hCv⟩
      · exact ⟨C, List.mem_cons_of_mem _ hC, hCv⟩
  | exchange hp _ ih =>
      intro v
      obtain ⟨C, hC, hCv⟩ := ih v
      exact ⟨C, hp.subset hC, hCv⟩
  | cut A _ _ ih₁ ih₂ =>
      intro v
      obtain ⟨C, hC, hCv⟩ := ih₁ v
      obtain ⟨D, hD, hDv⟩ := ih₂ v
      rcases List.mem_cons.mp hC with rfl | hC
      · rcases List.mem_cons.mp hD with rfl | hD
        · exact absurd hCv ((eval_dual v C).mp hDv)
        · exact ⟨D, hD, hDv⟩
      · exact ⟨C, hC, hCv⟩

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/ProofTheory.leanTry it in the Lean web editor

consistencyLean 4Proved here from basic factsFormally verified

/-- **Consistency**: the empty sequent (which would mean "false") has no derivation, even with
cut — no valuation makes a formula of the empty list true. -/
theorem consistency : ¬ Deriv true [] := by
  intro d
  obtain ⟨A, hA, _⟩ := soundness d (fun _ => True)
  simp at hA

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/ProofTheory.leanTry it in the Lean web editor

The main theorem is cut-free completeness, proved exactly as in the semantic route above: strong induction on the number of connectives, using semantic invertibility and the "literal case" lemma that builds a falsifying valuation. Cut admissibility is then one line.

cut_free_completeLean 4Proved here from basic factsFormally verified

/-- **Completeness of the cut-free calculus**: every valid sequent has a cut-free derivation.
By strong induction on the number of connectives in `Γ`. If `Γ` contains `A ∧ B`, move it to the
front; `⊢ A, Γ'` and `⊢ B, Γ'` are still valid (invertibility) and smaller, so derivable; apply
the ∧-rule. Similarly for `A ∨ B`. If `Γ` consists of literals, validity forces a complementary
pair, and the axiom applies. Note that only subformulas of `Γ` ever appear: this is the
*subformula property* of cut-free proofs. -/
theorem cut_free_complete : ∀ (k : ℕ) (Γ : List Fml), weightSum Γ = k → Valid Γ →
    Deriv false Γ := by
  intro k
  induction k using Nat.strong_induction_on with
  | _ k ih =>
    intro Γ hk hv
    by_cases hand : ∃ A B, Fml.and A B ∈ Γ
    · obtain ⟨A, B, hmem⟩ := hand
      have hp : Γ.Perm (Fml.and A B :: Γ.erase (Fml.and A B)) := List.perm_cons_erase hmem
      have hw := weightSum_perm hp
      rw [weightSum_cons] at hw
      have hv' := valid_perm hp hv
      have dA : Deriv false (A :: Γ.erase (Fml.and A B)) :=
        ih _ (by simp only [Fml.weight] at hw; rw [weightSum_cons]; omega) _ rfl
          (valid_and_left hv')
      have dB : Deriv false (B :: Γ.erase (Fml.and A B)) :=
        ih _ (by simp only [Fml.weight] at hw; rw [weightSum_cons]; omega) _ rfl
          (valid_and_right hv')
      exact Deriv.exchange hp.symm (Deriv.and A B dA dB)
    by_cases hor : ∃ A B, Fml.or A B ∈ Γ
    · obtain ⟨A, B, hmem⟩ := hor
      have hp : Γ.Perm (Fml.or A B :: Γ.erase (Fml.or A B)) := List.perm_cons_erase hmem
      have hw := weightSum_perm hp
      rw [weightSum_cons] at hw
      have d : Deriv false (A :: B :: Γ.erase (Fml.or A B)) :=
        ih _ (by simp only [Fml.weight] at hw; rw [weightSum_cons, weightSum_cons]; omega) _ rfl
          (valid_or (valid_perm hp hv))
      exact Deriv.exchange hp.symm (Deriv.or A B d)
    push Not at hand hor
    obtain ⟨n, hp, hn⟩ := literal_case hv hand hor
    exact Deriv.ax n hp hn

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/ProofTheory.leanTry it in the Lean web editor

cut_admissibleLean 4Proved here from basic factsFormally verified

/-- **Cut is admissible** in classical propositional logic: whatever can be derived with cuts can
be derived without. Here by the semantic route — soundness, then cut-free completeness —
rather than by Gentzen's syntactic reduction of cuts, which the lesson gives by hand. -/
theorem cut_admissible {Γ : List Fml} (d : Deriv true Γ) : Deriv false Γ :=
  cut_free_complete _ Γ rfl (soundness d)

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/ProofTheory.leanTry it in the Lean web editor

not_derivable_atomLean 4Proved here from basic factsFormally verified

/-- A non-example: the sequent `⊢ p₀` is not derivable, even with cut — the valuation making
every variable false refutes it (soundness). -/
theorem not_derivable_atom : ¬ Deriv true [pos 0] := by
  intro d
  obtain ⟨A, hA, hAv⟩ := soundness d (fun _ => False)
  simp only [List.mem_singleton] at hA
  subst hA
  exact hAv

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/ProofTheory.leanTry it in the Lean web editor

So the formal statement "cut is admissible in classical propositional logic" is fully verified, but by the semantic proof, not by Gentzen's reduction of cuts (which is the one that generalises to arithmetic). A proof term is a program, as Curry and Howard observed:

curry_howard_swapLean 4Proved here from basic factsFormally verified

/-- In Lean, as in the Curry–Howard correspondence, a proof of `A ∧ B → B ∧ A` *is* a program:
the function that takes a pair and swaps its components. Normalising the proof is running the
program. -/
theorem curry_howard_swap (A B : Prop) : A ∧ B → B ∧ A :=
  fun h => ⟨h.2, h.1⟩

Axioms used: No axiomsformal/Lumenary/ProofTheory.leanTry it in the Lean web editor

Finally, $\varepsilon_0$ in Mathlib (Mathlib.SetTheory.Ordinal.Veblen defines it as the first fixed point of $\alpha \mapsto \omega^\alpha$ ):

epsilon_zero_fixedLean 4Applies a library theoremFormally verified

/-- `ε₀` is a fixed point of `α ↦ ω^α`: `ω^ε₀ = ε₀`. It is the least one, the limit of
`ω, ω^ω, ω^ω^ω, …`. This applies Mathlib's `Ordinal.omega0_opow_epsilon`. -/
theorem epsilon_zero_fixed : ω ^ ε₀ = ε₀ :=
  omega0_opow_epsilon 0

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/ProofTheory.leanTry it in the Lean web editor

omega_tower_lt_epsilon_zeroLean 4Applies a library theoremFormally verified

/-- Every finite tower `ω^ω^…^ω` lies below `ε₀`; conversely every ordinal below `ε₀` lies below
such a tower (`Ordinal.lt_epsilon_zero`). Gentzen's proof uses induction along exactly these
ordinals. This applies Mathlib's `Ordinal.iterate_omega0_opow_lt_epsilon_zero`. -/
theorem omega_tower_lt_epsilon_zero (n : ℕ) : (fun a => ω ^ a)^[n] 0 < ε₀ :=
  iterate_omega0_opow_lt_epsilon_zero n

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/ProofTheory.leanTry it in the Lean web editor

omega_pow_omega_lt_epsilon_zeroLean 4Proved here from basic factsFormally verified

/-- A concrete instance: `ω^ω < ε₀`, since `ω^ω` is the third stage `ω^(ω^(ω^0))` of the tower
(`ω^0 = 1`, `ω^1 = ω`). -/
theorem omega_pow_omega_lt_epsilon_zero : ω ^ ω < ε₀ := by
  have h := iterate_omega0_opow_lt_epsilon_zero 3
  simpa [Function.iterate_succ, opow_zero, opow_one] using h

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/ProofTheory.leanTry it in the Lean web editor

Not formalised: the syntactic cut-elimination procedure, first-order LK and LJ, and Gentzen's consistency proof. Mathlib also has ONote, a computable notation system for the ordinals below $\varepsilon_0$ , which would be the starting point for formalising Gentzen's ordinal assignment.

ComputationC

Proof search and Goodstein sequences

The first experiment implements cut-free proof search in GS. Every proof it finds is checked for the subformula property; when the search fails, the failed branch is turned into a falsifying valuation — the completeness proof run as a program. It also measures how the order of decomposition affects proof size for $\vdash A^\perp, A$ : exponential in one order, linear in another. (Finding short proofs is hard in general: Cook and Reckhow (1979) showed that a propositional proof system with polynomial-size proofs of all tautologies exists if and only if $\mathsf{NP} = \mathsf{coNP}$ .)

Cut-free proof search and the subformula propertyPythonExact computationExhaustive finite checkComputationally tested

"""Cut-free proof search in a one-sided sequent calculus.

Formulas are in negation normal form: literals p_n and ~p_n, conjunctions and
disjunctions. A sequent is a list of formulas read as their disjunction. The
cut-free rules (the same calculus as the lesson's Lean file) are:
    axiom: a sequent containing p_n and ~p_n;
    or:    from |- A, B, G infer |- A | B, G;
    and:   from |- A, G and |- B, G infer |- A & B, G.
Read upwards, each rule replaces a formula by its immediate subformulas, so a
search for a cut-free proof only ever meets subformulas of the goal (the
subformula property) and always terminates. If some branch ends in literals
with no complementary pair, that branch yields a falsifying valuation: this
is the completeness proof, run as a program.

We (1) prove some classical tautologies and check the subformula property,
(2) extract a countermodel for a non-tautology, and (3) compare the sizes of
the proofs found for the identity sequent |- A*, A with two search orders.

Runs unchanged in the browser (Pyodide) using only the standard library.
"""

import textwrap

def P(n):
    """The propositional variable p_n."""
    return ("pos", n)

def N(n):
    """The negated variable ~p_n."""
    return ("neg", n)

def And(a, b):
    """Conjunction a & b."""
    return ("and", a, b)

def Or(a, b):
    """Disjunction a | b."""
    return ("or", a, b)

def dual(f):
    """The negation of f, pushed to the atoms by De Morgan's laws."""
    tag = f[0]
    if tag == "pos":
        return ("neg", f[1])
    if tag == "neg":
        return ("pos", f[1])
    if tag == "and":
        return ("or", dual(f[1]), dual(f[2]))
    return ("and", dual(f[1]), dual(f[2]))

def show(f):
    """Readable text for a formula."""
    if f[0] == "pos":
        return f"p{f[1]}"
    if f[0] == "neg":
        return f"~p{f[1]}"
    op = " & " if f[0] == "and" else " | "
    return "(" + show(f[1]) + op + show(f[2]) + ")"

def evaluate(f, valuation):
    """Truth value of f when valuation[n] is the value of p_n."""
    tag = f[0]
    if tag == "pos":
        return valuation[f[1]]
    if tag == "neg":
        return not valuation[f[1]]
    if tag == "and":
        return evaluate(f[1], valuation) and evaluate(f[2], valuation)
    return evaluate(f[1], valuation) or evaluate(f[2], valuation)

def subformulas(f):
    """The set of subformulas of f (including f)."""
    out = {f}
    if f[0] in ("and", "or"):
        out |= subformulas(f[1]) | subformulas(f[2])
    return out

def _choose(seq, strategy):
    """Index of the compound formula to decompose next, or None."""
    compound = [i for i, f in enumerate(seq) if f[0] in ("and", "or")]
    if not compound:
        return None
    if strategy == "leftmost":
        return compound[0]
    ors = [i for i in compound if seq[i][0] == "or"]
    if ors:
        return ors[0]

    def score(i):
        f = seq[i]
        return (dual(f[1]) in seq) + (dual(f[2]) in seq)

    return max(compound, key=lambda i: (score(i), -i))

def search(seq, strategy="leftmost"):
    """Return ("proof", tree) or ("countermodel", falsifying valuation).

    A tree is (rule, sequent, children). ``strategy`` is "leftmost" (decompose
    the first compound formula) or "guided" (disjunctions first, then the
    conjunction with the most conjuncts whose duals already occur).
    """
    seq = tuple(seq)
    if any(f[0] == "pos" and ("neg", f[1]) in seq for f in seq):
        return "proof", ("axiom", seq, ())
    i = _choose(seq, strategy)
    if i is None:
        atoms = {f[1] for f in seq}
        return "countermodel", {n: ("neg", n) in seq for n in sorted(atoms)}
    f, rest = seq[i], seq[:i] + seq[i + 1:]
    premises = [(f[1], f[2]) + rest] if f[0] == "or" else [(f[1],) + rest, (f[2],) + rest]
    children = []
    for premise in premises:
        kind, result = search(premise, strategy)
        if kind == "countermodel":
            return kind, result
        children.append(result)
    return "proof", (f[0], seq, tuple(children))

def size(tree):
    """Number of rule applications in a proof tree."""
    return 1 + sum(size(c) for c in tree[2])

def depth(tree):
    """Height of a proof tree."""
    return 1 + max((depth(c) for c in tree[2]), default=0)

def has_subformula_property(tree, goal):
    """Does every formula in the proof occur as a subformula of the goal?"""
    allowed = set().union(*(subformulas(f) for f in goal))
    stack = [tree]
    while stack:
        rule, seq, children = stack.pop()
        if not set(seq) <= allowed:
            return False
        stack.extend(children)
    return True

def disjunction(formulas):
    """Right-nested disjunction of a non-empty list of formulas."""
    result = formulas[-1]
    for f in reversed(formulas[:-1]):
        result = Or(f, result)
    return result

#: Classical tautologies (in negation normal form) and one non-tautology.
EXAMPLES = [
    ("excluded middle", [Or(P(0), N(0))]),
    ("De Morgan", [Or(And(N(0), N(1)), Or(P(0), P(1)))]),
    ("distributivity", [Or(dual(And(P(0), Or(P(1), P(2)))),
                           Or(And(P(0), P(1)), And(P(0), P(2))))]),
    ("Peirce's law", [Or(And(Or(N(0), P(1)), N(0)), P(0))]),
    ("not valid", [Or(P(0), And(P(1), N(0)))]),
]

def main():
    print("1. Searching for cut-free proofs, and countermodels")
    for name, goal in EXAMPLES:
        kind, result = search(goal)
        if kind == "proof":
            sub = has_subformula_property(result, goal)
            print(f"   {name:<16} proof: size {size(result):>2}, depth "
                  f"{depth(result)}, subformula property {sub}")
        else:
            falsified = not any(evaluate(f, result) for f in goal)
            values = " ".join(f"p{k}={'TF'[not v]}" for k, v in result.items())
            print(f"   {name:<16} no proof; {values} falsifies it: {falsified}")
    print("   The last goal, " + show(EXAMPLES[-1][1][0]) + ", is not a tautology.")
    print()
    print("3. Proof sizes for |- A*, A with A = (p0 & p1) | ... | (p2n-2 & p2n-1)")
    print("    n   leftmost order   guided order")
    for n in range(1, 9):
        a = disjunction([And(P(2 * i), P(2 * i + 1)) for i in range(n)])
        sizes = [size(search([dual(a), a], s)[1]) for s in ("leftmost", "guided")]
        print(f"   {n:>2}   {sizes[0]:>14}   {sizes[1]:>12}")
    print()
    print(textwrap.fill(
        "Epistemic status: exact computation on the formulas shown. Every proof "
        "found is checked for the subformula property and the countermodel is "
        "checked against the formula. The size table shows that cut-free proof "
        "size depends on the search order (here exponential versus linear); it "
        "does not measure the cost of cut elimination, which can be far worse "
        "(non-elementary in first-order logic).",
        width=78,
    ))

if __name__ == "__main__":
    main()

Runs entirely in your browser, in an isolated worker. Nothing is sent to a server.

The second experiment computes Goodstein sequences: write $n$ in hereditary base $b$ , replace $b$ by $b + 1$ , subtract $1$ , repeat. The numbers grow enormously, but replacing the base by $\omega$ turns each term into an ordinal below $\varepsilon_0$ , and these ordinals strictly decrease — the experiment checks this along the computed terms. That they always reach $0$ is a theorem whose proof needs $\mathrm{TI}(\varepsilon_0)$ .

Goodstein sequences and ordinals below epsilon_0PythonExact computationExhaustive finite checkComputationally tested

"""Goodstein sequences and the ordinals below epsilon_0.

Write n in hereditary base b (exponents are written in base b too, and so on),
replace every b by b + 1, subtract 1, and repeat with the next base. Goodstein
(1944) proved that every such sequence eventually reaches 0, although the
numbers first grow enormously. The proof replaces the base by omega: each term
becomes an ordinal below epsilon_0 in Cantor normal form, and these ordinals
strictly decrease - so they must reach 0, because the ordinals are well
ordered. Kirby and Paris (1982) showed that Peano arithmetic cannot prove
Goodstein's theorem: its proof needs exactly the transfinite induction up to
epsilon_0 that Gentzen used to prove the consistency of PA.

We compute the first terms of several sequences, attach the ordinal of each
term, and check that the ordinals strictly decrease along the computed terms.

Runs unchanged in the browser (Pyodide) using only the standard library.
"""

import textwrap

def hereditary(n, base):
    """Hereditary base-``base`` form of n: a list of (exponent form, digit),
    highest exponent first; each exponent form is again such a list."""
    if base < 2 or n < 0:
        raise ValueError("need base >= 2 and n >= 0")
    terms, power = [], 0
    while n:
        n, digit = divmod(n, base)
        if digit:
            terms.append((hereditary(power, base), digit))
        power += 1
    return terms[::-1]

def evaluate(form, base):
    """The number denoted by a hereditary form when the base is ``base``."""
    return sum(digit * base ** evaluate(exp, base) for exp, digit in form)

def bump(n, base):
    """Replace the base by base + 1 everywhere in the hereditary form of n."""
    return evaluate(hereditary(n, base), base + 1)

def goodstein(n, steps):
    """The first terms g_0 = n, g_1, ... (at most steps + 1 of them), with bases."""
    terms, base = [(n, 2)], 2
    while len(terms) <= steps and n > 0:
        n = bump(n, base) - 1
        base += 1
        terms.append((n, base))
    return terms

def ordinal(n, base):
    """The ordinal of n at this base: replace the base by omega.

    An ordinal below epsilon_0 is a tuple of (exponent ordinal, coefficient)
    pairs, exponents strictly decreasing; 0 is the empty tuple. Python's tuple
    order on these is exactly the ordinal order.
    """
    return tuple((ordinal_of_form(exp), digit) for exp, digit in hereditary(n, base))

def ordinal_of_form(form):
    """Convert a hereditary form to an ordinal tuple."""
    return tuple((ordinal_of_form(exp), digit) for exp, digit in form)

def show(alpha):
    """Cantor normal form as text, writing w for omega."""
    if not alpha:
        return "0"
    parts = []
    for exp, coeff in alpha:
        if not exp:
            parts.append(str(coeff))
            continue
        e = show(exp)
        if e == "1":
            power = "w"
        elif any(c in e for c in " +*"):
            power = f"w^({e})"
        else:
            power = "w^" + e
        parts.append(power if coeff == 1 else f"{power}*{coeff}")
    return " + ".join(parts)

def strictly_decreasing(terms):
    """Do the ordinals of the given (value, base) terms strictly decrease?"""
    ords = [ordinal(n, b) for n, b in terms]
    return all(a > b for a, b in zip(ords, ords[1:]))

def main():
    print("Goodstein sequence of 3 (term, base, ordinal):")
    for n, b in goodstein(3, 10):
        print(f"   {n:>3}  base {b}   {show(ordinal(n, b))}")
    print("Goodstein sequence of 4, first terms:")
    for n, b in goodstein(4, 7):
        print(f"   {n:>4}  base {b:>2}   {show(ordinal(n, b))}")
    print()
    print("Do the ordinals strictly decrease along the computed terms?")
    for start, steps in [(3, 10), (4, 2000), (5, 300), (6, 300), (19, 3)]:
        terms = goodstein(start, steps)
        digits = len(str(max(n for n, _ in terms)))
        print(f"   n = {start:>2}: {len(terms) - 1} steps, largest term has "
              f"{digits} digits, decreasing: {strictly_decreasing(terms)}")
    print()
    print(textwrap.fill(
        "Epistemic status: exact computation of finitely many terms. That the "
        "ordinals decrease at every step, and hence that every Goodstein sequence "
        "reaches 0, is Goodstein's theorem (the sequence of 4 needs about "
        "3 * 2^402653211 steps). Its proof uses the well-ordering of the ordinals "
        "below epsilon_0, which Peano arithmetic cannot prove (Kirby-Paris).",
        width=78,
    ))

if __name__ == "__main__":
    main()

Runs entirely in your browser, in an isolated worker. Nothing is sent to a server.

Explore

Explore: validity and cut-free provability

By cut-free completeness, a propositional formula is derivable in GS exactly when its truth table is all true. Use the truth table to check the classical tautologies of this lesson — Peirce's law below, then $p \vee \neg p$ and $\neg\neg p \to p$ . All three are classical tautologies, and none is provable in LJ: a truth table cannot see the difference between classical and intuitionistic logic, which is why intuitionistic logic needs other semantics (Kripke models, Heyting algebras).

Truth tables

Type a formula of propositional logic and see its value in every possible case.

Formula

Read as: ((p → q) → p) → p

Use the symbols ¬ ∧ ∨ → ↔, the words not, and, or, implies, iff, or ASCII ~ & | -> <->. Variables are single lowercase letters. ¬ binds tightest, then ∧, ∨, →, ↔; p → q → r means p → (q → r).

Try:

Tautology — true in all 4 rows.

p	q	p → q	(p → q) → p	((p → q) → p) → p
T	T	T	T	T
T	F	F	T	T
F	T	T	F	T
F	F	T	F	T

4 rows: one for every way of making the 2 variables true or false.

Exercises

1. Proof theory

Warm-upHuman

Which rule of the one-sided calculus GS can introduce a formula that is not a subformula of its conclusion?

Choose one

Cut: from

\vdash \Gamma, A

and

\vdash \Gamma, A^\perp

infer

\vdash \Gamma

\wedge

: from

\vdash \Gamma, A

and

\vdash \Gamma, B

infer

\vdash \Gamma, A \wedge B

\vee

: from

\vdash \Gamma, A, B

infer

\vdash \Gamma, A \vee B

The axiom

\vdash \Gamma, p, \neg p

2. Proof theory

CoreHuman

In the lesson's proof of the Hauptsatz, the case $A = B \wedge C$ replaces one cut on $A$ by two cuts. What makes the induction go through?

Choose one

The new cut formulas

C

and

B

have fewer connectives than

A

.The new derivations are lower than the old ones.There are fewer cuts afterwards.The context

\Gamma

gets smaller.

3. Proof theory

CoreHuman

Which statement about cut elimination and proof length is correct?

Choose one

Eliminating cuts can make proofs vastly longer — non-elementarily so in first-order logic.Cut-free proofs are always shorter, since they contain no detours.Cut elimination preserves proof length up to a constant factor.Proof length is not meaningful because cut is admissible.

4. Proof theory

CoreHuman

Why is $\Rightarrow p \vee \neg p$ not derivable in LJ?

Choose one

A cut-free LJ proof of

\Rightarrow p \vee \neg p

would end with

\vee R

, so

\Rightarrow p

or

\Rightarrow \neg p

would be derivable — and neither is.Its truth table has a false row.LJ has no cut rule.LJ cannot express negation.

5. Proof theory

Warm-upHuman

The Goodstein sequence of $4$ starts $g_0 = 4$ (base 2) and $g_1 = 26$ (base 3), since $4 = 2^2 \mapsto 3^3 - 1 = 26$ . Compute $g_2$ .

6. Proof theory

StretchHuman

Which statement about $\mathsf{PA}$ and transfinite induction (for Gentzen's standard notation system) is correct?

Choose one

\mathsf{PA}

proves transfinite induction up to each

\alpha \lt \varepsilon_0

, but not up to

\varepsilon_0

.

\mathsf{PA}

proves transfinite induction up to

\varepsilon_0

, which is how it proves its own consistency.

\mathsf{PA}

proves transfinite induction only up to

\omega

, which is ordinary induction.Transfinite induction cannot be expressed in the language of arithmetic.

7. Proof theory

CoreFormal

The Lean proof of cut_admissible is cut_free_complete _ Γ rfl (soundness d). What does this tell you about the proof?

Choose one

It is the semantic route: a derivation with cuts is sound, and every valid sequent has a cut-free derivation.It is Gentzen's reduction: each cut is pushed upwards until it disappears.It assumes cut elimination as an axiom.It is trivial because Deriv false and Deriv true are the same predicate.

8. Proof theory

Warm-upFormal

In the Lean file, Deriv : Bool → List Fml → Prop. What does the Boolean argument control?

Choose one

Whether the cut rule may be used (true) or not (false).Whether the logic is classical or intuitionistic.Whether the sequent is valid.Whether weakening is allowed.

9. Proof theory

StretchComputational

Write bump(n, b), which writes $n$ in hereditary base $b$ (exponents in base $b$ too, recursively) and replaces every $b$ by $b + 1$ , and goodstein(n, steps), which returns the list $[g_0, g_1, \dots]$ of at most steps + 1 terms, stopping early at $0$ (start in base 2; $g_{k+1}$ = bump of $g_k$ in base $k + 2$ , minus 1).

Runs entirely in your browser, in an isolated worker. Nothing is sent to a server.

Common misconceptionsH

Common misconceptions

Misconception

"Gentzen's consistency proof is circular." It does not assume the consistency of $\mathsf{PA}$ . It uses a principle — quantifier-free transfinite induction up to $\varepsilon_0$ — that $\mathsf{PA}$ cannot prove, but which is different in kind: it is about a concrete, primitive recursive ordering of finite trees. Whether this principle is more evident than $\mathrm{Con}_{\mathsf{PA}}$ is a philosophical question; the mathematical content is a precise reduction.

Misconception

"Cut elimination makes proofs shorter." It makes them simpler in structure, not shorter. Eliminating cuts can increase size exponentially in propositional logic and non-elementarily in first-order logic (Statman, Orevkov). Lemmas are a compression device.

Misconception

"Cut is a rule of logic we could do without, so it is useless." Cut is admissible, not derivable: adding it changes no theorems but changes which proofs exist. Cut-free calculi are good for analysing proofs and searching for them; calculi with cut are good for writing short ones.

Misconception

" $\varepsilon_0$ is a large, exotic ordinal." It is countable, and every ordinal below it is written by a finite tree of symbols. What is strong is not the ordinal but the assertion that its notation system is well-founded.

ViewpointsH

Many ways of seeing

Computation— Normalisation is evaluation

Under Curry–Howard, a proof of $\forall x\, \exists y\, R(x, y)$ in an intuitionistic system is a program computing $y$ from $x$ , and cut elimination is execution. Kreisel's "unwinding" programme and Kohlenbach's proof mining extract explicit bounds from classical proofs in analysis by proof-theoretic transformations (functional interpretation). In the other direction, Lean's kernel evaluates proofs: decide proves a decidable proposition by running the decision procedure. Proof complexity asks how long proofs must be — the Cook–Reckhow theorem ties the existence of a polynomially bounded propositional proof system to $\mathsf{NP} = \mathsf{coNP}$ .

Combinatorics— Fast-growing functions and the pigeonhole principle

The strength of a theory shows up in combinatorics. Every function provably total in $\mathsf{PA}$ is eventually dominated by some $F_\alpha$ , $\alpha \lt \varepsilon_0$ , in the fast-growing hierarchy; the Goodstein function and the Paris–Harrington function are dominated by none of them (they grow at the level of $F_{\varepsilon_0}$ ), which is why $\mathsf{PA}$ cannot prove them total. At the propositional level, Haken (1985) proved that the pigeonhole principle " $n + 1$ pigeons do not fit in $n$ holes" needs resolution refutations of size exponential in $n$ , while it has polynomial-size proofs in Frege systems with cut-like reasoning (Buss 1987).

Topology— Proof nets and paths

Girard's linear logic (1987) represents proofs as proof nets: graphs whose vertices are formula occurrences and links. A graph is a correct proof exactly when every "switching" (keeping one of the two premise edges at each par-link, ⅋) yields an acyclic, connected graph — the Danos–Regnier criterion, a topological condition. Cut elimination becomes local graph rewriting. In homotopy type theory, a proof of an equation $a = b$ is interpreted as a path from $a$ to $b$ in a space, proofs of equality between proofs as homotopies, and Martin-Löf's identity types have models in homotopy theory (Awodey–Warren 2009, Voevodsky). See homotopy type theory.

Algebra— Proofs as polynomial identities

Algebraic proof systems refute a set of polynomial equations $f_1 = \cdots = f_m = 0$ (encoding a propositional formula, with $x^2 = x$ for each variable) by exhibiting a certificate $\sum_i g_i f_i = 1$ , whose existence is guaranteed by Hilbert's Nullstellensatz. The Nullstellensatz and polynomial calculus proof systems (Beame, Impagliazzo, Krajíček, Pitassi, Pudlák 1994; Clegg, Edmonds, Impagliazzo 1996) measure proof size by the degree of the $g_i$ , and lower bounds come from algebra and combinatorics. On the semantic side, intuitionistic propositional logic is complete for Heyting algebras, and cut elimination yields the finite model property and decidability.

Category theory— Curry–Howard–Lambek

Lambek observed that proofs in the conjunction–implication fragment of intuitionistic logic, identified up to normalisation ( $\beta\eta$ -equality), are the morphisms of the free cartesian closed category on the atomic propositions: conjunction is product, implication is exponential, and cut is composition. Cut elimination says that every morphism has a normal form. See categorical logic, and Lambek and Scott, Introduction to Higher Order Categorical Logic (1986).

History & global context

History and context

Gerhard Gentzen introduced natural deduction and the sequent calculi LK and LJ, and proved the Hauptsatz, in "Untersuchungen über das logische Schließen" (1935). Stanisław Jaśkowski in Poland independently developed a system of natural deduction (1934).
Gentzen's consistency proof for arithmetic appeared in 1936, with a revised version in 1938; his 1943 paper showed that $\mathsf{PA}$ proves transfinite induction below $\varepsilon_0$ but not up to it. Gentzen died in Prague in 1945. Wilhelm Ackermann (1940) gave another consistency proof up to $\varepsilon_0$ , using Hilbert's $\varepsilon$ -substitution method.
Kurt Schütte developed infinitary proof theory; he and Solomon Feferman independently identified $\Gamma_0$ as the limit of predicativity (1964–65). William Tait popularised the one-sided calculus used here. Gaisi Takeuti conjectured cut elimination for higher-order logic; it was proved for second-order logic by Tait (1966) and in general by Moto-o Takahashi (1967) and Dag Prawitz (1968), and Jean-Yves Girard proved normalisation for System F (1971).
Dag Prawitz (1965) proved normalisation for natural deduction. Haskell Curry (1934, 1958) and William Howard (manuscript 1969, published 1980) formulated the correspondence between proofs and programs.
Richard Statman and Vladimir Orevkov (1979) proved non-elementary lower bounds for cut elimination; Laurie Kirby and Jeff Paris (1982) connected Goodstein's theorem to $\varepsilon_0$ .

Studying proofs themselves

Lemmas are detours

Sequent calculi

Examples

Cut elimination for propositional logic

Gentzen's consistency proof and ordinal analysis

Proofs as programs

A sequent calculus in Lean

Proof search and Goodstein sequences

Explore: validity and cut-free provability

Exercises

Common misconceptions

Many ways of seeing

History and context

Further reading