The Lumenary · First-year graduate

Proof theory

Name: ______________________

Date: ______________________

You will learn to

Present classical and intuitionistic sequent calculi, and prove cut elimination for classical propositional logic by Gentzen-style reductions
Derive the subformula property, consistency and the intuitionistic disjunction property from cut elimination
Distinguish syntactic cut elimination from semantic cut admissibility via cut-free completeness
Explain the idea of Gentzen's consistency proof for $\mathsf{PA}$ by transfinite induction up to $\varepsilon_0$ , and what an ordinal analysis measures
Describe the Curry–Howard correspondence, in which normalising a proof is running a program

1.
Which rule of the one-sided calculus GS can introduce a formula that is not a subformula of its conclusion?
- A.Cut: from $\vdash \Gamma, A$ and $\vdash \Gamma, A^\perp$ infer $\vdash \Gamma$
- B. $\wedge$ : from $\vdash \Gamma, A$ and $\vdash \Gamma, B$ infer $\vdash \Gamma, A \wedge B$
- C. $\vee$ : from $\vdash \Gamma, A, B$ infer $\vdash \Gamma, A \vee B$
- D.The axiom $\vdash \Gamma, p, \neg p$
2.
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?
- A.The new cut formulas $C$ and $B$ have fewer connectives than $A$ .
- B.The new derivations are lower than the old ones.
- C.There are fewer cuts afterwards.
- D.The context $\Gamma$ gets smaller.
3.
Which statement about cut elimination and proof length is correct?
- A.Eliminating cuts can make proofs vastly longer — non-elementarily so in first-order logic.
- B.Cut-free proofs are always shorter, since they contain no detours.
- C.Cut elimination preserves proof length up to a constant factor.
- D.Proof length is not meaningful because cut is admissible.
4.
Why is $\Rightarrow p \vee \neg p$ not derivable in LJ?
- A.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.
- B.Its truth table has a false row.
- C.LJ has no cut rule.
- D.LJ cannot express negation.
5.
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.
Which statement about $\mathsf{PA}$ and transfinite induction (for Gentzen's standard notation system) is correct?
- A. $\mathsf{PA}$ proves transfinite induction up to each $\alpha \lt \varepsilon_0$ , but not up to $\varepsilon_0$ .
- B. $\mathsf{PA}$ proves transfinite induction up to $\varepsilon_0$ , which is how it proves its own consistency.
- C. $\mathsf{PA}$ proves transfinite induction only up to $\omega$ , which is ordinary induction.
- D.Transfinite induction cannot be expressed in the language of arithmetic.
7.
The Lean proof of cut_admissible is cut_free_complete _ Γ rfl (soundness d). What does this tell you about the proof?
- A.It is the semantic route: a derivation with cuts is sound, and every valid sequent has a cut-free derivation.
- B.It is Gentzen's reduction: each cut is pushed upwards until it disappears.
- C.It assumes cut elimination as an axiom.
- D.It is trivial because Deriv false and Deriv true are the same predicate.
8.
In the Lean file, Deriv : Bool → List Fml → Prop. What does the Boolean argument control?
- A.Whether the cut rule may be used (true) or not (false).
- B.Whether the logic is classical or intuitionistic.
- C.Whether the sequent is valid.
- D.Whether weakening is allowed.
9.
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).
Computational — Practice

Answer key — Proof theory

1.
Only cut: its premises contain $A$ and $A^\perp$ , which disappear in the conclusion. Every other rule's premises consist of subformulas of the conclusion, which is why cut-free derivations have the subformula property.
2.
The cut on $B \wedge C$ becomes a cut on $C$ (with context $\Gamma, B^\perp$ ) followed by a cut on $B$ . Both cut formulas have fewer connectives than $B \wedge C$ , so the induction hypothesis on formula complexity applies. The number of cuts goes up, which is why a naive count would not work.
3.
Cut elimination can increase proof size enormously: exponentially in propositional logic and non-elementarily (a tower of exponentials) in first-order logic. The cut-free proof is analytic, not short.
4.
By cut elimination, a derivation can be taken cut-free; with an empty antecedent and one formula on the right, its last rule must be $\vee R$ , so $\Rightarrow p$ or $\Rightarrow \neg p$ would be derivable. Neither is (the valuations $p$ = false, respectively $p$ = true, refute them, and LJ is sound for classical semantics). This is the disjunction property.
5.
$26 = 2 \cdot 3^2 + 2 \cdot 3 + 2$ . Bumping the base gives $2 \cdot 4^2 + 2 \cdot 4 + 2 = 42$ , and subtracting $1$ gives $g_2 = 41$ . Its ordinal is $\omega^2 \cdot 2 + \omega \cdot 2 + 1$ , smaller than that of $g_1$ , which is $\omega^2 \cdot 2 + \omega \cdot 2 + 2$ .
6.
Gentzen (1943) showed that $\mathsf{PA}$ proves $\mathrm{TI}(\alpha)$ for every $\alpha \lt \varepsilon_0$ ; and since $\mathsf{PRA} + \mathrm{TI}(\varepsilon_0) \vdash \mathrm{Con}_{\mathsf{PA}}$ , the second incompleteness theorem shows $\mathsf{PA} \nvdash \mathrm{TI}(\varepsilon_0)$ . So $\varepsilon_0$ is exactly the boundary.
7.
soundness d : Valid Γ turns the derivation with cuts into a semantic fact, and cut_free_complete turns validity back into a cut-free derivation by terminating proof search. This is cut admissibility by the semantic route; the syntactic procedure of the lesson is not formalised.
8.
The flag says whether cut is allowed: cut produces Deriv true Γ, and every other constructor is generic in c. cut_admissible says Deriv true Γ → Deriv false Γ.

def bump(n, b):
    total, power = 0, 0
    while n:
        n, digit = divmod(n, b)
        if digit:
            total += digit * (b + 1) ** bump(power, b)
        power += 1
    return total


def goodstein(n, steps):
    terms, base = [n], 2
    while len(terms) <= steps and n > 0:
        n = bump(n, base) - 1
        base += 1
        terms.append(n)
    return terms

Each base- $b$ digit $d$ at position $e$ contributes $d \cdot (b+1)^{\mathrm{bump}(e)}$ : the exponent $e$ is itself bumped, which is what makes the representation hereditary. With $\omega$ in place of the base, each term becomes an ordinal below $\varepsilon_0$ , and these decrease — Goodstein's theorem.