Structural Proof Theory
Structural proof theory is the subfield of proof theory that studies the properties of proof systems at the level of their structural rules — the rules governing how context (the set of available hypotheses) can be manipulated independently of the logical content of the formulas involved. The three classical structural rules are:
- Weakening: a hypothesis can be added to any proof even if it is not used.
- Contraction: a hypothesis used twice can be identified as a single occurrence.
- Exchange: the order of hypotheses does not matter.
In classical and intuitionistic logic, these rules are admissible without restriction. Their restriction or removal gives rise to substructural logics — including linear logic (which restricts contraction and weakening, treating hypotheses as resources that must be used exactly once), relevant logic (which restricts weakening, requiring that every hypothesis be used), and other systems. These are not merely formal curiosities: linear logic has found applications in programming language semantics, quantum computing, and resource accounting systems where the "use-once" character of resources is semantically significant.
Sequent Calculus and Proof Nets
Structural proof theory works primarily with Gentzen's sequent calculus — a proof formalism in which derivations operate on sequents (pairs of formula-lists) rather than formulas directly. The sequent calculus was specifically designed to make structural properties visible: each rule manipulates the context in an explicit, inspectable way.
Proof nets, introduced by Jean-Yves Girard in the context of linear logic, are a geometric representation of proofs that factors out irrelevant structural rearrangements. Two proof-net representations that differ only in the order of independent inference steps are identified as the same proof — capturing a genuine mathematical equivalence that the sequent calculus obscures. Proof nets have been extended to other logics and provide a bridge between proof theory and category theory via the Curry-Howard-Lambek correspondence.
Deep Inference
Deep inference proof systems (developed by Alessio Guglielmi and others) permit inference rules to apply to any subformula of a proof, not merely to the outermost connective. This generalization breaks the sequential, tree-structured character of traditional proofs and enables proofs that are polynomially shorter than their sequent-calculus equivalents. Deep inference is a demonstration that the structure of a proof system is not a neutral choice — it directly determines what complexity of reasoning is expressible within bounded-length proofs.
The lesson of structural proof theory is that the syntax of reasoning is not trivial scaffolding. The structural rules of a proof system encode assumptions about the nature of hypotheses and their relationship to conclusions — assumptions that, when made explicit, reveal the logic as a theory of resource use, not merely of truth. Classical logic assumes hypotheses are unlimited, reusable, and freely available. These assumptions are not forced. Where they fail, a different logic, with a different proof theory, is the right tool.