Proof Theory

Proof theory is the study of formal proofs as mathematical objects in their own right. Where model theory studies semantics — the structures that satisfy a theory — proof theory studies syntax: the finite, rule-governed derivations that establish theorems, treated not as a means to an end but as combinatorial objects to be analyzed, transformed, and measured. Its informal slogan is

$$\text{proof theory}=\text{the mathematics of}⊢,$$

the symbolic counterpart of model theory's mathematics of $\models$. This page builds on the syntax and deductive systems of sentential and first-order logic, and connects directly to intuitionistic logic (whose proof theory motivates much of the subject) and to Gödel's incompleteness theorems (which set the limits of what proof-theoretic methods can certify).

What proof theory studies

Proof theory takes the proof itself as its object of study. Before asking anything about proofs, one needs a precise definition of what they are.

What is a proof?

A formal proof system is given by three effective (decidable) pieces:

1. a set of formulas — the language;
2. a decidable set of axioms;
3. a finite set of inference rules, each a decidable relation "conclusion $\psi$ follows from premises ${\phi }_1,\dots ,{\phi }_k$."

A proof (or derivation) is then defined in either of two equivalent ways:

• List form (Hilbert-style). A derivation of $\phi$ from a set $\Gamma$ is a finite sequence ${\phi }_1,\dots ,{\phi }_n$ with ${\phi }_n=\phi$ in which each ${\phi }_i$ is an axiom, a member of $\Gamma$, or the conclusion of a rule whose premises all occur earlier (among ${\phi }_1,\dots ,{\phi }_{i-1}$). We write $\Gamma ⊢\phi$ when such a sequence exists.
• Tree form (natural-deduction-style). Inductively: an axiom or assumption alone is a derivation (a leaf); and if $d_1,\dots ,d_k$ are derivations with roots matching the premises of a rule $R$ with conclusion $\psi$, then joining them under $R$ is a derivation with root $\psi$. The proof is the whole tree.

The two coincide — a list is just a linearization of a tree — and the toy systems below are concrete instances. What makes the notion formal is decidability: because axioms and rules are decidable, the relation "$p$ is a valid proof of $\phi$" is itself mechanically checkable, even though "$\phi$ is provable" (the existence of some $p$) is only semi-decidable. This is exactly the ${\Delta }_0$ proof predicate ${\mathrm{Prf}}_T(p,x)$ versus the ${\Sigma }_1$ provability predicate ${\mathrm{Prov}}_T$ split — and it is the whole premise of the subject: proof theory studies the objects $p$, not merely the relation $⊢$.

The questions

Once proofs are formal objects, one can ask structural questions about them:

• Existence: is there a proof of $\phi$ from $T$? (provability, $T⊢\phi$)
• Shape: can every proof be put in a normal form, and what does that form guarantee?
• Transformation: how do proofs reduce, compose, and relate to computation?
• Strength: how much proof power does a theorem need — what must one assume to prove it?

Two foundational pressures gave the subject its shape. Hilbert's program (1920s) sought to secure all of mathematics by finitary consistency proofs — establishing, by uncontroversial finite combinatorial means, that strong theories cannot prove $0=1$. Gödel's second incompleteness theorem showed this is impossible in its original form, but the modified program — measuring exactly how much non-finitary strength a consistency proof needs — became ordinal analysis and is thriving. Independently, the proof theory of intuitionistic logic revealed that proofs are programs, launching the connection to computation.

Proof systems

The same provability relation $⊢$ can be presented by very different calculi. The three classical styles trade off readability against analyzability.

• Hilbert systems (axiomatic): many axiom schemes, one or two rules (typically modus ponens). Compact to state and easy to reason about (good for metatheory and arithmetization, as in incompleteness), but proofs are unstructured and painful to build.
• Natural deduction (Gentzen, Prawitz): each connective comes with introduction and elimination rules, and reasoning proceeds under discharged assumptions — close to actual mathematical practice. Classical $\mathbf{NK}$ is intuitionistic $\mathbf{NJ}$ plus double-negation elimination (see intuitionistic logic).
• Sequent calculus (Gentzen's $\mathbf{LK}$/$\mathbf{LJ}$): manipulates sequents $\Gamma ⊢\Delta$ ("if all of $\Gamma$ then some of $\Delta$"). Every connective has left and right introduction rules, and there are explicit structural rules — weakening, contraction, exchange — plus the cut rule. The intuitionistic restriction $\mathbf{LJ}$ is simply "at most one formula on the right," $|\Delta |\le 1$.

These are inter-translatable for the same logic; the art is choosing the presentation in which the theorem you want is visible. Sequent calculus is the natural home of the subject's central result.

Cut elimination (Gentzen's Hauptsatz)

The cut rule is the formal counterpart of using a lemma: $$\frac{\Gamma ⊢\Delta ,AA,\Sigma ⊢\Pi }{\Gamma ,\Sigma ⊢\Delta ,\Pi }\text{(cut)}.$$ The cut formula $A$ appears in the premises but not the conclusion — a proof using cut can invoke arbitrary intermediate concepts. Gentzen's cut-elimination theorem (the Hauptsatz, 1934) says cut is eliminable:

Every sequent-calculus proof in $\mathbf{LK}$ (or $\mathbf{LJ}$) can be transformed into a proof of the same sequent that uses no cuts.

The payoff is the subformula property: a cut-free proof contains only subformulas of its conclusion. Nothing extraneous appears — the proof cannot "detour" through foreign lemmas. The consequences are immediate and powerful:

• Consistency. There is no cut-free proof of the empty sequent $⊢$ (it has no subformulas to build from), so $⊬\perp$. This is a syntactic consistency proof, using no models.
• The disjunction and existence properties (for intuitionistic $\mathbf{LJ}$): a cut-free proof of $⊢A\vee B$ must end in a right-$\vee$ rule, so it already proves $⊢A$ or $⊢B$; likewise a proof of $⊢\exists x\phi$ exhibits a witness. Constructivity is read off the normal form.
• Decidability of fragments. Cut-free proof search is bounded by subformulas, giving decision procedures for propositional logic and many fragments.
• Interpolation (Craig's theorem) and conservativity results follow by analyzing cut-free derivations.

Cut elimination is constructive but costly: removing cuts can blow up proof size super-exponentially (a tower of exponentials). That non-elementary cost is not a defect — it is where the logical strength hides, and it is exactly what ordinal analysis measures.

Normalization and the Curry–Howard correspondence

The natural-deduction analogue of cut elimination is normalization: an introduction immediately followed by the matching elimination is a detour (a redex) that can be reduced away, e.g. $$\frac{[A]⋮B}{A\to B}(\to I)\frac{}{A}⇝\text{(substitute the proof of }A\text{ into the assumption)}.$$ Prawitz's normalization theorem says every $\mathbf{NJ}$ derivation reduces to a unique normal form. Read through the Curry–Howard correspondence, this is computation:

$$\text{propositions}\leftrightarrow \text{types},\text{proofs}\leftrightarrow \text{programs},\text{normalization}\leftrightarrow \text{evaluation}.$$

A proof of $A\to B$ is a function from proofs of $A$ to proofs of $B$; normalizing the proof is running the program. This identification makes proof theory the foundation of type theory and proof assistants (Lean, Coq/Rocq, Agda), and it is why intuitionistic — not classical — logic is the native logic of computation. (Classical reasoning corresponds, via Griffin, to control operators.)

Structural and substructural proof theory

Isolating the structural rules of sequent calculus exposes a whole landscape. Dropping one of weakening, contraction, or exchange yields substructural logics:

This is more than bookkeeping. Contraction is the structural rule behind the paraconsistent diagnosis of the paradoxes: Curry's paradox and the set-theoretic paradoxes turn on contracting a duplicated hypothesis, so contraction-free systems can host naive comprehension without triviality. Linear logic (Girard) refines intuitionistic logic by tracking the number of uses of each assumption, with the exponential modality $!A$ marking the reusable propositions — a proof-theoretic account of resources that feeds back into computation (memory, concurrency).

Ordinal analysis and the modified Hilbert program

Gödel's second theorem blocks a consistency proof of Peano arithmetic $\mathsf{PA}$ within $\mathsf{PA}$. Gentzen (1936) showed exactly what extra is needed:

$\mathsf{PA}$ is consistent, provably so by transfinite induction up to the ordinal ${\epsilon }_0$ — and no smaller ordinal suffices.

Here ${\epsilon }_0=\sup \{\omega ,{\omega }^{\omega },{\omega }^{{\omega }^{\omega }},\dots \}$ is the least ordinal closed under $\alpha \mapsto {\omega }^{\alpha }$. The proof is otherwise finitary; the single non-finitary ingredient is well-foundedness of ${\epsilon }_0$. This both confirms the second incompleteness theorem ($\mathsf{PA}$ cannot prove that induction, so it cannot prove its own consistency) and quantifies the gap precisely.

This launched ordinal analysis: assign to each theory $T$ its proof-theoretic ordinal $|T|$, the supremum of the ordinals $T$ can prove well-founded, equivalently the exact transfinite-induction strength needed for $\mathrm{Con}(T)$.

The ordinal is a robust, presentation-independent measure of a theory's strength, and computing it for strong subsystems of second-order arithmetic and set theory is the technical frontier of the field. It is the modified Hilbert program: not absolute finitary security (impossible), but an exact calibration of how much ideal strength each theory needs.

Reverse mathematics

A complementary calibration asks, for each ordinary theorem, which axioms are needed to prove it — and answers by proving the theorem equivalent to its axioms over a weak base. Working in subsystems of second-order arithmetic, Friedman and Simpson found that the vast majority of classical theorems cluster into the "big five":

$${\mathsf{RCA}}_0\subset {\mathsf{WKL}}_0\subset {\mathsf{ACA}}_0\subset {\mathsf{ATR}}_0\subset {\Pi }_1^1\text{-}{\mathsf{CA}}_0,$$

from computable mathematics (${\mathsf{RCA}}_0$), through weak König's lemma (compactness arguments), arithmetical comprehension (equivalent to Bolzano–Weierstrass), arithmetical transfinite recursion, up to ${\Pi }_1^1$-comprehension. A typical result: the Bolzano–Weierstrass theorem is equivalent to ${\mathsf{ACA}}_0$ over ${\mathsf{RCA}}_0$ — so it is neither stronger nor weaker than "arithmetical sets exist." Reverse mathematics turns "what does this theorem really require?" into a precise theorem.

How much is needed to express provability?

A natural question, given the toy systems above: how strong must a system be before "provable" becomes an internal, self-referential predicate? The dividing line is the ability to encode its own syntax — a proof is a finite sequence of symbols, and coding sequences as single numbers requires a pairing function, hence multiplication. This is exactly why the addition-only system $\mathsf{A}$ (and full Presburger arithmetic) cannot express provability and is in fact decidable; crossing the line means adding $\times$. Three thresholds then stack up:

• To express it — Robinson arithmetic $\mathsf{Q}$. The finitely axiomatized fragment with $0,S,+,\times$ and no induction already represents every computable relation, so the proof predicate is representable, the ${\Sigma }_1$ formula ${\mathrm{Prov}}_T(x)\equiv \exists p{\mathrm{Prf}}_T(p,x)$ genuinely applies, and the diagonal lemma gives self-reference. This is the "interprets enough arithmetic" hypothesis of the incompleteness theorems — the first theorem already bites at $\mathsf{Q}$.
• To reason about it — $\mathsf{I}{\Sigma }_1\subseteq \mathsf{PA}$. $\mathsf{Q}$ can write ${\mathrm{Prov}}_T$ down but is too weak to prove its laws; the derivability conditions D2/D3 need induction. The minimal well-behaved system is $\mathsf{I}{\Sigma }_1$ (${\Sigma }_1$-induction), where the second incompleteness theorem and Löb's theorem go through; $\mathsf{PA}$ is the usual home.
• To capture its abstract behavior — the modal logic $\mathsf{GL}$ (next section): strip the arithmetic and keep only the laws of $\square$.

The minimal system that can express provability at all is thus Robinson arithmetic $\mathsf{Q}$ — the smallest step past the addition-only toys, bought precisely by adding the multiplication that lets a system encode its own proofs.

Provability logic The resulting system GL (Gödel–Löb) is axiomatized by the single schema

$$\square (\square \phi \to \phi )\to \square \phi (\text{Lo¨b’s axiom}),$$ on top of the normal modal logic $\mathsf{K}$. Solovay's completeness theorem (1976) is the striking payoff: GL proves exactly the schematic facts about provability in $\mathsf{PA}$. Gödel's second theorem ($⊬\square \perp \to \perp$ unless inconsistent) and Löb's theorem become one-line modal calculations, and the whole self-referential machinery of incompleteness is repackaged as a decidable propositional modal logic.

Proof theory vs. model theory

The two halves of logic mirror each other, and the central metatheorems of first-order logic are the bridges:

Soundness and completeness (Gödel) say $⊢$ and $\models$ have the same extension — proof theory and model theory describe the same provability relation from opposite sides. Proof theory keeps the finite, constructive viewpoint, which is exactly what makes it the side that talks to computation and to the limits set by incompleteness.

Summary

Proof theory is the constructive, finitary face of logic: it treats proofs as objects, normalizes them to extract computational content, and measures the exact ideal strength a theorem or a consistency statement requires. Its limits are set by Gödel — no theory certifies its own consistency — but within those limits it turns "how strong is this theorem?" into precise, answerable mathematics.