Proof theory studies formal proofs as mathematical objects in their own right. Rather than treating proofs only as certificates that a statement is true, the course asks how proofs are represented, transformed, and measured, and what those transformations reveal about logic itself. The central themes are the structure of deduction systems, the correspondence between proofs and computations, and the relationship between syntactic proof methods and semantic notions such as validity, completeness, and consistency. The course begins with the basic idea of formal proofs and natural deduction for propositional logic, then develops normalization to show how redundant proof steps can be eliminated and why that matters. From there, the Curry-Howard correspondence connects proofs with programs, and the theory expands to first-order logic and sequent calculus, where cut elimination becomes a major organizing principle. Later chapters use these proof-theoretic tools to derive completeness and compactness, prove Herbrand’s theorem, and then move into arithmetic and formal theories, ordinal analysis, Gentzen’s consistency proof, and finally the links between proof theory and computability. The chapters are arranged to build steadily from concrete proof systems to deeper metatheorems and applications. Early chapters establish the language and mechanics of formal deduction, middle chapters explain how proofs can be normalized and compared across systems, and the final chapters show how proof theory illuminates the foundations of mathematics, the limits of formalization, and the computational content of logical reasoning. # Introduction Proof theory begins from a change of viewpoint: instead of using proofs only as a means of reaching theorems, we study proofs themselves as finite mathematical objects. A proof has shape, subproofs, assumptions, rules, and transformations, and these features can be analysed with the same precision as formulas or models. This introductory chapter sets the agenda for the course: natural deduction will give us a language for ordinary mathematical reasoning, while normalization and cut elimination will show that proofs can be simplified in systematic ways. Chapters on normalization, cut elimination, Curry-Howard, arithmetic, and computability use these transformations to obtain consistency, conservativity, and computational information. ## What Is a Formal Proof? What must be fixed before a string of reasoning can be treated as a mathematical object? We need a language of formulas, a stock of inference rules, and a convention for how assumptions are recorded and discharged. Once these are specified, a proof is no longer an informal paragraph but a finite derivation tree whose correctness can be checked locally at each inference. [definition: Formal Proof System] A formal proof system consists of an object language, a specified class of formulas, a collection of inference rules, and a definition of derivation from assumptions. [/definition] The object language supplies the expressions being proved, while the rules describe the permitted local moves. The central proof-theoretic question is not only whether a formula is derivable, but how derivations can be compared, transformed, and simplified. [definition: Derivation Tree] A derivation tree is a finite rooted tree whose nodes are labelled by formulas or sequents, such that each non-leaf node is obtained from its immediate predecessors by an inference rule of the proof system. [/definition] Derivation trees make induction available. Many arguments in this course proceed by induction on the height of a derivation, on the final rule used, or on the complexity of formulas occurring in the derivation. [example: Modus Ponens As A Derivation] In a propositional proof system with implication elimination, take two open assumption leaves: \begin{align*} A \qquad A \to B . \end{align*} The implication elimination rule says that from a derivation of $A \to B$ and a derivation of $A$, one may infer $B$. Applying that rule to these two one-node derivations gives the derivation tree \begin{align*} \frac{A \to B \qquad A}{B}\;{\to}E . \end{align*} The open assumptions of the whole tree are exactly the open assumptions of its leaves, namely $A \to B$ and $A$, and its conclusion is the root formula $B$. Thus the informal inference “from $A$ and $A \to B$, infer $B$” is represented as a finite derivation tree whose final step is the recorded rule ${\to}E$. [/example] ## Syntax, Semantics, And Proof How is proof theory different from model theory or truth-functional semantics? Semantics asks when a formula is true under an interpretation, whereas proof theory asks how a formula is derived from rules. The two viewpoints interact through soundness and completeness, but the objects they inspect are different. [definition: Soundness] A proof system is sound for a semantics if every formula derivable in the proof system is valid in that semantics. [/definition] Soundness is needed because a derivation tree by itself only records legal rule applications. If the rules were chosen badly, a system could derive a formula such as $P \land \neg P$ from no assumptions, even though no classical valuation makes it true. Thus soundness is the test that local proof rules have not lost contact with the intended notion of truth. In the theorem below, $S \vdash t$ means that the formula $t$ is derivable from the set of assumptions $S$, while $S \models t$ means that every valuation making all formulas in $S$ true also makes $t$ true. This is the same proof-versus-truth distinction described above; when $S$ is a finite context $\Gamma$ and $t$ is a formula $A$, it reads as the familiar implication from $\Gamma \vdash A$ to $\Gamma \models A$. [quotetheorem:1453] [citeproof:1453] The finiteness of $\Gamma$ is not the essential point; it keeps the introductory statement close to the calculi used in the first part of the course. The named rules are essential, because changing a rule can destroy soundness, for instance by allowing $A$ to be inferred from $\neg A$ without contradiction. The theorem also does not say that every semantically valid formula has a proof; that reverse direction is completeness. Soundness connects proof rules to truth, but it does not yet explain the internal structure of proofs. Normalization and cut elimination are stronger structural analyses: they show how proofs can be reorganised without changing their conclusions. The remaining semantic question runs in the opposite direction. If a formula is forced by every interpretation of the assumptions, one can ask whether the formal rules are expressive enough to recover it as a derivation. This reverse comparison is recorded as completeness. [definition: Completeness] A proof system is complete for a semantics if every semantically valid formula is derivable in the proof system. [/definition] Completeness is a bridge from semantic validity back to derivability. In this course it serves mainly as background; the main emphasis is on transformations of given proofs rather than on constructing proofs from models. ## Natural Deduction As A Model Of Reasoning Why begin with natural deduction? Natural deduction separates the rules for each connective into introduction rules, which say how to prove a formula with that connective, and elimination rules, which say how to use such a formula. This mirrors ordinary mathematical practice: to prove $A \to B$, assume $A$ and derive $B$; to use $A \land B$, extract either conjunct. [definition: Introduction Rule] An introduction rule is an inference rule whose conclusion has a specified logical connective as its main connective. [/definition] Introduction rules explain how evidence for a compound formula is built. To understand how that evidence is later consumed, the course pairs them with elimination rules. The missing half of the classification is a rule that starts from a compound formula already in hand and asks what may be extracted from it. Elimination rules name this second role, so that later detours can be described as an introduction immediately followed by a corresponding use. [definition: Elimination Rule] An elimination rule is an inference rule whose major premise has a specified logical connective as its main connective. [/definition] The pairing of introduction and elimination rules is the first place where proof theory sees redundancy. A proof may introduce a connective and then immediately eliminate it; such a segment is a detour, because the proof has constructed information only to unpack it at once. [example: Implication Detour] Let $\mathcal D$ be a derivation of $B$ from open assumptions contained in $\Gamma \cup \{A\}$, where the displayed occurrences of $A$ are discharged by implication introduction. Let $\mathcal E$ be a separate derivation of $A$ from open assumptions contained in $\Gamma$. The detour has the form \begin{align*} \frac{ \frac{ [A] \quad \mathcal D }{ B } {\to}I \qquad \mathcal E }{ B } {\to}E . \end{align*} The upper left part first packages the hypothetical derivation of $B$ as a derivation of $A \to B$, and the final rule immediately unpacks that implication by supplying a proof of $A$. The reduction removes the introduction-elimination pair by replacing every discharged leaf occurrence of $A$ in $\mathcal D$ with a copy of $\mathcal E$: \begin{align*} \frac{ \frac{ [A] \quad \mathcal D }{ B } {\to}I \qquad \mathcal E }{ B } {\to}E \quad\leadsto\quad \mathcal D[\mathcal E/A]. \end{align*} Here $\mathcal D[\mathcal E/A]$ denotes the derivation obtained by substitution: each leaf formerly labelled by the discharged assumption $A$ is replaced by the whole derivation $\mathcal E$, while every other inference rule in $\mathcal D$ is left unchanged. The conclusion remains $B$, because the root of $\mathcal D$ was already labelled $B$; the open assumptions are contained in $\Gamma$, because the only open assumptions newly introduced by the substitutions are the open assumptions of $\mathcal E$, and those are contained in $\Gamma$. Thus the original proof used $A \to B$ only as a temporary package for a derivation that could have been applied directly. This is the basic implication-reduction step used in normalization. [/example] This example depends on the formal treatment of temporary assumptions. Without a discharge rule, the assumption $A$ would remain open forever, and the proof would not justify an implication from $\Gamma$ alone. The next issue is not the particular detour just displayed, but the general license behind implication introduction. We need a precise theorem saying when a derivation carried out under one extra temporary assumption can be closed into a derivation of a conditional formula from the original context. [quotetheorem:4619] [citeproof:4619] The discharge mechanism is the decisive hypothesis: if the calculus allowed implication elimination but not implication introduction, the conclusion $A \to B$ would not follow from a derivation of $B$ under an extra assumption $A$. The statement also does not say that every proof of $A \to B$ literally arose by first writing a proof of $B$ under assumption $A$; it says that such hypothetical derivations can be internalised as implications. This theorem is not merely a familiar meta-theorem in new notation. It explains why natural deduction is well suited to representing proofs with temporary hypotheses, especially in implication, negation, and proof by contradiction. ## Proof Transformations What can be gained by changing a proof while preserving its conclusion? Proof transformations reveal which uses of rules are essential and which are artifacts of presentation. The course focuses on two major transformations: normalization for natural deduction and cut elimination for sequent calculus. [definition: Normal Form] A derivation is in normal form if it contains no reducible detour consisting of an introduction rule immediately followed by a corresponding elimination rule. [/definition] The exact definition depends on the proof system, but the guiding idea is stable: a normal proof does not prove an intermediate formula only to dismantle it at once. The obstruction is visible in implication detours: the proof first packages a derivation as a function-like object and then immediately applies it, leaving a longer derivation than necessary. Normal forms often have the subformula property, meaning that the formulas appearing in the proof are controlled by the formulas in the assumptions and conclusion. [quotetheorem:4620] [citeproof:4620] The restriction to a fixed intuitionistic propositional calculus matters because normalization is sensitive to the exact rules, especially rules for classical reasoning and for additional connectives. The theorem does not claim that the normal derivation is unique, nor that the reduction process is efficient; some normalization procedures can greatly increase proof size before terminating. Its force is structural rather than computational complexity-theoretic: it guarantees that every proof has an analytic representative. Normalization is a prototype for much of proof theory. It converts a syntactic transformation into mathematical information: consistency follows because a normal proof of falsity would have a restricted shape, and computational content appears because reductions resemble evaluation of programs. ## Sequents, Contexts, And Structural Rules Why introduce sequent calculus after natural deduction? Natural deduction is close to informal reasoning, but sequent calculus exposes the management of assumptions. A sequent records a context on the left and a conclusion, or conclusions, on the right; the rules then separate logical operations from structural operations such as weakening, contraction, and exchange. [definition: Sequent] A sequent is an expression of the form $\Gamma \vdash A$, where $\Gamma$ is a finite context of formulas and $A$ is a formula. [/definition] Natural deduction records assumptions through open leaves and discharge annotations, which can make large derivations hard to inspect. Sequents solve this bookkeeping problem by putting the available assumptions into the displayed object being transformed. In classical systems one may allow several formulas on the right, but the single-conclusion form is enough for intuitionistic logic. The context $\Gamma$ records the assumptions currently available, and the turnstile marks derivability rather than semantic entailment. [definition: Structural Rule] A structural rule is an inference rule governing the use of formulas in contexts rather than the internal logical form of a formula. [/definition] Weakening permits unused assumptions, contraction permits repeated assumptions to be merged, and exchange permits reordering. By controlling these rules, proof theorists can study logics where resources matter, such as linear logic. [example: Weakening] Suppose a derivation has already ended in the sequent $\Gamma \vdash A$: \begin{align*} \mathcal D \quad \frac{}{\Gamma \vdash A}. \end{align*} The weakening rule permits one additional formula to be added to the context while leaving the conclusion unchanged: \begin{align*} \frac{\Gamma \vdash A}{\Gamma, B \vdash A}\;W . \end{align*} Applying this rule to the derivation $\mathcal D$ gives the larger derivation \begin{align*} \frac{ \mathcal D \quad \Gamma \vdash A }{ \Gamma, B \vdash A }\;W . \end{align*} The formula $B$ is not used in the subderivation $\mathcal D$; it is simply added to the list of available assumptions by the structural rule. Thus ordinary intuitionistic and classical sequent systems permit irrelevant assumptions, whereas a resource-sensitive system that omits weakening would not allow this inference. [/example] ## Cut And Its Elimination What is the proof-theoretic analogue of using a lemma? In sequent calculus it is the cut rule: prove an intermediate formula $A$, then use $A$ to prove the desired conclusion. Cut is useful for writing proofs, but cut elimination says that every proof using such intermediate lemmas can be transformed into one that does not use cut. [definition: Cut Rule] The cut rule is the inference rule that derives $\Gamma, \Delta \vdash B$ from derivations of $\Gamma \vdash A$ and $\Delta, A \vdash B$. [/definition] Cut expresses composition of proofs. Its obstruction is that the cut formula $A$ may be absent from the final sequent, so a proof with cut can hide intermediate concepts that are not visible in the conclusion. Eliminating cut does not mean mathematicians should avoid lemmas; it means that the formal system has enough analytic strength that intermediate formulas can be removed from derivations in principle. [quotetheorem:4621] [citeproof:4621] The structural rules listed in the statement are part of the hypothesis, not decoration: weakening and contraction affect how cuts are permuted through derivations. The result is also system-specific; adding unrestricted new axioms or non-analytic rules can break the subformula behaviour that cut elimination reveals. The theorem does not say that the cut-free proof is shorter or more readable than the original proof with lemmas. Cut elimination is the sequent-calculus counterpart of normalization. Its consequences include consistency, the subformula property, and interpolation-style results in suitable settings. ## Arithmetic, Consistency, And Computation Why does a course on proof systems lead to arithmetic and computation? Once proofs are finite objects, they can be encoded by natural numbers, manipulated by recursive functions, and studied inside formal arithmetic. This opens the route from local proof transformations to global metamathematical results. [definition: Arithmetisation Of Syntax] Arithmetisation of syntax is the coding of formulas, proofs, and syntactic operations by natural numbers and number-theoretic relations. [/definition] Without such a coding, statements about formal systems remain external metatheory: we can say that a derivation exists, but arithmetic itself cannot express that a number codes a valid proof. Arithmetisation removes this barrier by replacing syntactic predicates with number-theoretic predicates. This coding lets formal systems speak about their own proofs. It is the background for incompleteness phenomena, but in proof theory it also supports consistency proofs, ordinal analyses, and the extraction of computational bounds from formal derivations. The first metatheoretic property to track is whether the system avoids proving incompatible claims. To state that property cleanly, we need a definition that marks the basic failure mode in which derivations collapse contradiction into ordinary theoremhood. [definition: Consistency] A formal system is consistent if there is no formula $A$ such that both $A$ and $\neg A$ are derivable in the system. [/definition] For systems with falsity $\bot$, consistency is often expressed as non-derivability of $\bot$. Proof transformations give one route to consistency: if every derivation normalizes and no normal derivation can conclude $\bot$, then no derivation of $\bot$ exists. [example: Computational Reading Of Implication] Under the proofs-as-programs interpretation, a derivation of $A \to B$ is read as a function which takes a proof of $A$ as input and returns a proof of $B$ as output. Suppose $\mathcal D$ is a derivation of $B$ from a temporary assumption $x:A$, and suppose $\mathcal E$ is a derivation of $A$. The implication introduction rule reads $\mathcal D$ as the function \begin{align*} \lambda x.\mathcal D : A \to B, \end{align*} and implication elimination applies that function to the argument $\mathcal E$: \begin{align*} (\lambda x.\mathcal D)\,\mathcal E : B. \end{align*} The corresponding computation is beta-reduction: \begin{align*} (\lambda x.\mathcal D)\,\mathcal E &\leadsto \mathcal D[\mathcal E/x]. \end{align*} Here $\mathcal D[\mathcal E/x]$ means that each occurrence of the temporary proof variable $x:A$ inside $\mathcal D$ is replaced by the whole proof $\mathcal E$ of $A$. The output type remains $B$, because the body $\mathcal D$ had conclusion $B$ under the assumption $x:A$, and the substitution supplies exactly the proof of $A$ required at each use of $x$. Thus the proof-theoretic reduction \begin{align*} \frac{ \frac{[A]\ \mathcal D}{A \to B}\;{\to}I \qquad \mathcal E }{ B }\;{\to}E \quad\leadsto\quad \mathcal D[\mathcal E/A] \end{align*} is the same pattern as function application followed by substitution. Normalization therefore resembles computation because eliminating a proof detour performs the proof-level analogue of evaluating a function call. [/example] ## How The Course Will Proceed The course now has its roadmap. We first formalise derivations and induction principles, then study natural deduction for propositional logic, including assumptions and discharge. We then prove normalization, read it computationally through Curry-Howard, extend natural deduction to first-order logic, move to sequent calculus and cut elimination, and finish with completeness, Herbrand methods, arithmetic, ordinal analysis, and computability. [remark: Working Method] Most proofs in the course use induction on formulas, induction on derivations, or induction on a complexity measure assigned to proof transformations. When reading a proof, identify the object being inducted over and the quantity that decreases. This habit is the main technical discipline of the course. [/remark] These introductory notes should be read as a map rather than as a replacement for the later chapters. Each definition introduced here will reappear with sharper formal details, and each theorem labelled as a theme will later become a precise theorem for a specified proof system. Chapter 1 picks up exactly where the introduction leaves off: proof theory stops treating proofs as informal justifications and begins treating them as explicit mathematical objects. With formulas, contexts, sequents, and derivation trees now fixed, the course can ask not only what is true, but what counts as a proof and how proofs are built. # 1. Formal Proofs as Mathematical Objects Proof theory begins by changing the subject of study: instead of asking only whether a statement is true in a model, we ask what a proof of the statement is made of. This chapter fixes the basic syntactic objects that later chapters manipulate: formulas, contexts, sequents, and derivation trees. The guiding question is how a proof can be represented with enough precision that induction, transformation, and comparison become ordinary mathematical operations. The semantic ideas from a first course in logic remain in the background. A valuation still tells us when a propositional formula is true, and a structure still interprets first-order formulas. The new point is that a proof system has its own internal geometry, and theorems such as soundness relate that geometry back to semantics. ## From Formulas to Derivation Trees What data must be specified before a proof can be inspected as a finite mathematical object? We need an object language, a grammar for forming expressions, and a way to record which assumptions are being used. This section introduces those ingredients in the propositional setting, where the notation is light enough to make the shape of derivations visible. [definition: Propositional Object Language] A propositional object language consists of a countable set $\mathsf{Prop}$ of propositional letters, the constant $\bot$, and the connectives $\land$, $\lor$, $\to$, and $\neg$. [/definition] The object language is the language inside which proofs are built. It is separate from the metalanguage in which these notes describe the proof system. For instance, $A \to B$ is a formula of the object language, while the sentence "from $A$ and $A \to B$ we may derive $B$" is a metalinguistic statement about derivability. To make induction on expressions legitimate, the notes need more than an informal stock of symbols. The grammar must specify exactly which strings count as formulas and how their last construction step is determined. [definition: Formula] The set $\mathsf{Form}$ of formulas is the smallest set satisfying the following clauses: 1. Every propositional letter $p \in \mathsf{Prop}$ belongs to $\mathsf{Form}$. 2. The constant $\bot$ belongs to $\mathsf{Form}$. 3. If $A,B \in \mathsf{Form}$, then $(A \land B)$, $(A \lor B)$, and $(A \to B)$ belong to $\mathsf{Form}$. 4. If $A \in \mathsf{Form}$, then $\neg A$ belongs to $\mathsf{Form}$. [/definition] Parentheses will often be suppressed when the intended parsing is unambiguous. The formal definition matters because later induction arguments follow this recursive construction: atomic formulas and $\bot$ form the base cases, and each connective gives an induction step. [example: Parsing A Compound Formula] Let $p,q,r \in \mathsf{Prop}$. By the atomic clause in the definition of formula, $p,q,r \in \mathsf{Form}$. Since $p,q \in \mathsf{Form}$, the binary-connective clause gives $(p \land q)\in \mathsf{Form}$. Since $r\in \mathsf{Form}$, the negation clause gives $\neg r\in \mathsf{Form}$. Applying the implication clause to the two formulas $(p\land q)$ and $\neg r$ gives \begin{align*} (p\land q)\in \mathsf{Form} \quad\text{and}\quad \neg r\in \mathsf{Form} \quad\Longrightarrow\quad ((p\land q)\to \neg r)\in \mathsf{Form}. \end{align*} Thus $(p\land q)\to \neg r$ is a formula because it is produced by the finite construction sequence \begin{align*} p,\ q,\ r \quad\leadsto\quad (p\land q),\ r \quad\leadsto\quad (p\land q),\ \neg r \quad\leadsto\quad ((p\land q)\to \neg r). \end{align*} The point is that well-formedness is certified by this construction tree, not by the expression merely looking like meaningful logical notation. [/example] The construction tree explains what counts as a formula, but proofs also need to record which formulas are being assumed. Instead of carrying an informal phrase such as "assuming $A$ and $B$", proof theory packages assumptions into a syntactic object. This package is called a context, and it must be explicit because later rules will add, remove, duplicate, or discharge assumptions. [definition: Context] A context $\Gamma$ is a finite list, finite set, or finite multiset of formulas, depending on the proof system under consideration. [/definition] For most natural deduction presentations in this course, contexts may be read as finite sets of undischarged assumptions. In structural proof theory, the distinction between lists, multisets, and sets becomes significant because exchange, contraction, and weakening may be treated as explicit rules. Once assumptions have been packaged, the next object must bind such a context to the formula claimed from it. A sequent is this complete judgment, allowing inference rules to operate on the relation between assumptions and conclusion rather than on isolated formulas. [definition: Sequent] A sequent is an expression of the form $\Gamma \vdash A$, where $\Gamma$ is a context and $A$ is a formula. [/definition] The intended reading is that $A$ is derivable from the assumptions in $\Gamma$. The turnstile $\vdash$ is syntactic: it records the existence of a derivation in a specified proof system, not semantic truth under an interpretation. A sequent by itself is only the endpoint of a proof, so it does not record which rules were used or where assumptions enter the argument. To reason about proofs as mathematical objects, we need a structure that displays the dependencies among sequents and lets each inference be checked locally. [definition: Derivation Tree] A derivation tree is a finite rooted tree whose nodes are labelled by sequents and whose edges are arranged according to inference rules of a proof system. [/definition] The root of the tree is the conclusion of the derivation. The leaves are initial sequents or open assumptions. Reading a derivation upward decomposes the proof into its immediate subproofs; reading it downward describes how the conclusion is assembled from premises. [example: Modus Ponens As A Derivation Tree] Let $\Gamma$ be a context with $A \in \Gamma$ and $A \to B \in \Gamma$. The assumption rule gives the two one-node derivations \begin{align*} \Gamma \vdash A \qquad\text{and}\qquad \Gamma \vdash A \to B, \end{align*} because each displayed formula is a member of the same context $\Gamma$. Implication elimination then combines these two derivations: the left premise proves the implication $A \to B$, the right premise proves its antecedent $A$, and the conclusion is the consequent $B$. \begin{align*} \frac{\Gamma \vdash A \to B \qquad \Gamma \vdash A}{\Gamma \vdash B}\;{\to}E \end{align*} Thus the derivation tree has exactly two premise leaves, $\Gamma \vdash A \to B$ and $\Gamma \vdash A$, and one inference step whose root is $\Gamma \vdash B$; no assumption in $\Gamma$ is discharged by this rule. [/example] The next rule has a different structural profile: it keeps all assumptions exactly as they were, because using a conjunct does not cancel any assumption. [example: Conjunction Elimination As A Derivation Tree] Let $A$ and $B$ be formulas, and suppose a derivation $D$ has root sequent $\Gamma \vdash A \land B$. The two conjunction-elimination rules form new derivation trees by placing $D$ as the single immediate subderivation and changing only the root sequent: \begin{align*} \frac{D}{\Gamma \vdash A}\;{\land}E_1 \qquad\text{where the root of }D\text{ is }\Gamma \vdash A \land B, \end{align*} and \begin{align*} \frac{D}{\Gamma \vdash B}\;{\land}E_2 \qquad\text{where the root of }D\text{ is }\Gamma \vdash A \land B. \end{align*} Written without naming $D$, the two rule instances are \begin{align*} \frac{\Gamma \vdash A \land B}{\Gamma \vdash A}\;{\land}E_1 \qquad \frac{\Gamma \vdash A \land B}{\Gamma \vdash B}\;{\land}E_2. \end{align*} In both cases the premise context and conclusion context are the same $\Gamma$, so no formula is added to $\Gamma$, no formula is removed from $\Gamma$, and no temporary assumption is discharged. The rule extracts the left or right conjunct from the already derived conjunction while preserving the open assumptions exactly as they were. [/example] ## Proof Systems and Semantic Validity How do we know that a formal derivation proves something genuinely valid, rather than merely producing a well-shaped tree? This question separates syntax from semantics. A proof system gives rules for building derivations; semantics gives meanings to formulas and lets us ask whether an inference preserves truth. [definition: Valuation] A valuation is a function $v: \mathsf{Prop} \to \{0,1\}$ assigning a truth value to each propositional letter. [/definition] Every valuation extends recursively to all formulas. For example, $v(A \land B)=1$ exactly when $v(A)=1$ and $v(B)=1$, while $v(A \to B)=1$ exactly when either $v(A)=0$ or $v(B)=1$. The semantic analogue of a sequent asks whether truth of the assumptions forces truth of the conclusion under every valuation. This relation is needed before derivability can be compared with truth preservation. [definition: Semantic Consequence] For a context $\Gamma$ and formula $A$, write $\Gamma \vDash A$ if, for every valuation $v: \mathsf{Prop} \to \{0,1\}$, whenever $v(B)=1$ for every $B \in \Gamma$, we also have $v(A)=1$. [/definition] The symbol $\vDash$ belongs to the semantic side. The central comparison is therefore between $\Gamma \vdash A$, existence of a formal derivation, and $\Gamma \vDash A$, preservation of truth across valuations. The first half of this comparison asks whether derivations are trustworthy. A sound proof system is one whose syntactic rules never take us from semantically true assumptions to a semantically false conclusion. [definition: Soundness] A proof system is sound for propositional semantics if, for every context $\Gamma$ and formula $A$, $\Gamma \vdash A$ implies $\Gamma \vDash A$. [/definition] Soundness is a safety condition on rules: it rules out proof systems that can manufacture false conclusions from true assumptions. The converse issue is not safety but strength. After ruling out false derivations, one can ask whether the rules are powerful enough to derive every conclusion already forced by the semantics. [definition: Completeness] A proof system is complete for propositional semantics if, for every context $\Gamma$ and formula $A$, $\Gamma \vDash A$ implies $\Gamma \vdash A$. [/definition] Soundness says that derivability does not outrun truth. Completeness says that the rules are strong enough to derive every semantic consequence. This chapter proves the soundness direction for propositional derivations; completeness requires a separate construction and belongs later in a logic course. Without a soundness condition, an arbitrary extra rule such as "from no premises infer $p$" would derive $\varnothing \vdash p$, even though a valuation with $v(p)=0$ refutes $\varnothing \vDash p$. The template used throughout the course is to reduce a global statement about all derivations to a local verification for each inference rule. The hypotheses are needed at exactly the points where the induction uses them: leaves must already be semantically legitimate, and each final rule must carry semantic legitimacy from its premises to its conclusion. If a proof system includes the zero-premise rule $\frac{}{\Gamma \vdash p}$ for an arbitrary propositional letter $p$, then the induction has no truthful premise from which to obtain $v(p)=1$, so soundness fails whenever $v(p)=0$. Soundness also does not imply that every true formula is derivable; that stronger reverse direction is completeness. The formal soundness theorem below packages that rule-by-rule verification into a single statement about all derivations. It is the bridge that lets later examples check individual inference rules while relying on the global conclusion that derivability preserves semantic consequence. [quotetheorem:1453] [citeproof:1453] [example: Soundness Check For Implication Elimination] Assume $v$ makes every formula in $\Gamma$ true, and consider an instance of implication elimination \begin{align*} \frac{\Gamma \vdash A \to B \qquad \Gamma \vdash A}{\Gamma \vdash B}\;{\to}E. \end{align*} To check truth preservation for this rule, suppose the two premise formulas are true under $v$: \begin{align*} v(A \to B)=1 \qquad\text{and}\qquad v(A)=1. \end{align*} By the truth condition for implication, $v(A \to B)=1$ means that either $v(A)=0$ or $v(B)=1$. Since the second premise gives $v(A)=1$, the alternative $v(A)=0$ is impossible. Therefore the remaining alternative is \begin{align*} v(B)=1. \end{align*} So whenever a valuation satisfies $\Gamma$ and makes both premises of ${\to}E$ true, it also makes the conclusion true; implication elimination is truth-preserving. [/example] Once derivations are finite trees, they can be compared and modified as objects in their own right. [explanation: Proof Transformations] A proof transformation is a rule or algorithm with an explicit source and target class of derivations. It may be a map from derivations in one proof system $\mathcal P$ to derivations in another proof system $\mathcal Q$, or a map from derivations of a fixed end-sequent $\Gamma \vdash A$ to new derivations of the same end-sequent inside a single system. Normalization, cut elimination, and translations between proof systems are all examples. The essential point is that such transformations are defined on proofs themselves, not merely on the formulas proved. For a transformation to be mathematically controlled, it should preserve the end-sequent, reduce a well-founded measure, or translate derivations in a way compatible with the inference rules. Later chapters will use these ideas to remove detours from natural deduction and remove cuts from sequent calculus. [/explanation] ## Induction On Syntax And Derivations Why are induction principles so central in proof theory? The objects under study are generated recursively and are finite by construction. Formulas are built from smaller formulas, and derivations are built from smaller derivations, so their basic proof method is structural induction. A proof method that checks only atomic formulas would miss, for example, whether the property survives passage from $A$ and $B$ to $A \to B$; recursive formation forces the proof to follow every constructor. [quotetheorem:4622] [citeproof:4622] This theorem justifies proofs by cases on the final connective of a formula. Each closure hypothesis is necessary: if a property holds for all atoms and for $\bot$ but is not preserved under $\neg$, it may fail for $\neg p$ even though it holds for $p$. The theorem does not prove a property from scattered examples of formulas; it proves a property only when the argument covers every formation clause in the grammar. This is the formal reason recursive definitions, such as complexity or substitution, are legitimate, and it is the bridge to later induction proofs about substitution lemmas and normal forms. [example: Complexity Of A Formula] Define the complexity $c(A)$ of a formula recursively by \begin{align*} c(p)&=0 &&\text{for }p\in \mathsf{Prop},\\ c(\bot)&=0,\\ c(\neg A)&=c(A)+1,\\ c(A\circ B)&=c(A)+c(B)+1 &&\text{for }\circ\in\{\land,\lor,\to\}. \end{align*} For the formula $((p\to q)\land \neg r)$, first compute the two immediate subformulas. Since $p$ and $q$ are propositional letters, \begin{align*} c(p\to q) &=c(p)+c(q)+1\\ &=0+0+1\\ &=1. \end{align*} Since $r$ is a propositional letter, \begin{align*} c(\neg r) &=c(r)+1\\ &=0+1\\ &=1. \end{align*} Now apply the binary-connective clause to the outer conjunction: \begin{align*} c((p\to q)\land \neg r) &=c(p\to q)+c(\neg r)+1\\ &=1+1+1\\ &=3. \end{align*} Thus the formula $((p\to q)\land \neg r)$ has complexity $3$, counting one step for each connective occurrence: $\to$, $\neg$, and $\land$. This measure is useful because its recursive calculation follows the same construction pattern as the formation of formulas. [/example] Formula complexity measures syntactic construction; derivations need an analogous measure for their tree structure. Height provides that measure by counting the longest path from a leaf to the root, making it possible to argue about a proof by passing to its immediate subproofs. [definition: Height Of A Derivation] The height $h(D)$ of a derivation tree $D$ is the maximum number of inference steps on a path from a leaf of $D$ to its root. [/definition] Once height has been defined, the main question is what kind of induction it supports. Because every non-leaf derivation is obtained from smaller immediate subderivations, the relevant theorem packages the rule-by-rule method for proving properties of all derivation trees. [quotetheorem:4623] [citeproof:4623] This is the proof-theoretic analogue of induction on formulas. Instead of asking for the outermost connective, we ask for the final inference rule. The hypothesis must cover every possible final inference, because a missing rule leaves a class of derivations for which the induction step has no case. The finiteness and well-foundedness of derivation height are also essential: infinite proof objects need a different argument, such as coinduction or an ordinal measure, and ordinary induction on $h(D)$ no longer applies. The theorem does not say that a proof system is sound or normalizing by itself; it supplies the induction scheme used after the relevant rule-by-rule checks have been made. [example: Proof By Contradiction As A Derivation Pattern] In a classical natural deduction system, proof by contradiction has the following rule shape: if a derivation of $\bot$ is available under the temporary assumption $\neg A$, then one may conclude $A$ after discharging that temporary assumption. Let $D$ be a derivation whose root sequent is \begin{align*} \Gamma,\neg A \vdash \bot. \end{align*} This sequent says that every open assumption of $D$ is either a formula already in $\Gamma$ or the additional formula $\neg A$. Applying proof by contradiction forms a new derivation tree with $D$ as its single immediate subderivation: \begin{align*} \frac{\Gamma,\neg A \vdash \bot}{\Gamma \vdash A}\;\mathrm{PBC}. \end{align*} The conclusion context is $\Gamma$, not $\Gamma,\neg A$, because the occurrence of $\neg A$ used to obtain the contradiction is discharged by the rule. Thus the transformation of the end-sequent is exactly \begin{align*} \text{premise context } \Gamma,\neg A \quad\leadsto\quad \text{conclusion context } \Gamma, \end{align*} while the conclusion formula changes from $\bot$ to $A$. The point is that a derivation tree must record not only which formulas occur as assumptions, but which of those assumptions remain open at the root. [/example] This final pattern is the first place where proof theory visibly tracks more than truth values: it tracks the bookkeeping of open and discharged assumptions. [remark: What This Chapter Sets Up] The rest of the course repeatedly applies the same pattern. First specify the formal objects and rules, then prove properties of derivations by induction, and finally transform derivations while preserving their end-sequents. Chapter 2 applies this pattern to natural deduction, where assumption discharge becomes central; Chapters 6 and 7 apply it to sequent calculus, where structural rules and cut become explicit. [/remark] In Chapter 1, derivations become objects that can be inspected, compared, and transformed rather than merely accepted. Chapter 2 uses that viewpoint to formalize natural deduction, where the structure of ordinary reasoning is captured by local introduction and elimination rules and by the management of assumptions. # 2. Natural Deduction for Propositional Logic Natural deduction presents proof as structured reasoning from assumptions rather than as a list of formulas in a Hilbert system. The guiding question of this chapter is how the ordinary moves of mathematical argument can be represented by local rules: to prove a conjunction, prove both parts; to use an implication, combine it with its antecedent; to reason hypothetically, make an assumption and later discharge it. Chapter 1 treated formal derivations as mathematical objects, using contexts, sequents, and induction on derivation height; here we specialize that viewpoint to the propositional connectives and compare the minimal, intuitionistic, and classical versions of natural deduction. ## Rules for the Propositional Connectives How should the meaning of a connective be reflected in the way proofs involving it are built and used? Natural deduction answers this by assigning most connectives two kinds of rules: introduction rules, which say how to prove a formula with that connective as its main operator, and elimination rules, which say how to extract information from such a formula once it has been proved. [definition: Natural Deduction Derivation] A natural deduction derivation is a finite proof tree whose nodes are labelled by formulas, whose leaves are assumptions, and whose internal nodes are obtained from earlier nodes by applying inference rules. [/definition] A derivation is read upward from assumptions to conclusion, although proof trees are often displayed with premises above a horizontal line and the conclusion below. The open assumptions are those leaves that have not been discharged by a rule such as implication introduction or negation introduction. [definition: Conjunction Rules] For formulas $A$ and $B$, conjunction has the following rules: \begin{align*} \frac{A \quad B}{A \land B}\,\land I, \qquad \frac{A \land B}{A}\,\land E_1, \qquad \frac{A \land B}{B}\,\land E_2. \end{align*} [/definition] The introduction rule expresses that a proof of $A \land B$ consists of a proof of $A$ together with a proof of $B$. The elimination rules express that once a conjunction is available, either conjunct may be used separately. A common malformed use of conjunction is to infer $A \land B$ after proving only $A$; the rule blocks this by requiring independent derivations of both conjuncts. [example: Commuting Conjunction] Temporarily assume $A \land B$. From this open assumption, the second conjunction elimination rule gives the right conjunct: \begin{align*} \frac{A \land B}{B}\,\land E_2. \end{align*} From the same open assumption, the first conjunction elimination rule gives the left conjunct: \begin{align*} \frac{A \land B}{A}\,\land E_1. \end{align*} Now both $B$ and $A$ have been derived under the single open assumption $A \land B$, so conjunction introduction applies with $B$ as the left premise and $A$ as the right premise: \begin{align*} \frac{ \frac{A \land B}{B}\,\land E_2 \quad \frac{A \land B}{A}\,\land E_1 }{B \land A}\,\land I. \end{align*} Thus, under the temporary assumption $A \land B$, we have derived $B \land A$. Implication introduction discharges that assumption and yields \begin{align*} \frac{[A \land B] \; \vdots \; B \land A}{(A \land B) \to (B \land A)}\,\to I. \end{align*} The derivation shows that conjunction can be commuted: any proof of $A \land B$ contains exactly the two pieces needed to build a proof of $B \land A$. [/example] Conjunction rules do not change which assumptions are open; they only rearrange information already available under those assumptions. The next connective must account for genuinely hypothetical reasoning, where assuming $A$ temporarily and deriving $B$ becomes a proof of $A \to B$ after that assumption is closed. [definition: Implication Rules] For formulas $A$ and $B$, implication has the following rules: \begin{align*} \frac{[A] \; \vdots \; B}{A \to B}\,\to I, \qquad \frac{A \to B \quad A}{B}\,\to E. \end{align*} [/definition] In $\to I$, the displayed assumption occurrence $A$ is discharged. Implication introduction is the formal version of hypothetical reasoning: if, under the temporary assumption $A$, a derivation reaches $B$, then the assumption may be closed and the conclusion becomes $A \to B$. Implication elimination is modus ponens. [example: Identity Derivation] Temporarily assume $A$. At this point the only open assumption is the displayed occurrence of $A$, and that occurrence already gives a one-node derivation with conclusion $A$: \begin{align*} [A]. \end{align*} Implication introduction applies to a derivation whose conclusion is $A$ under the temporary assumption $A$, so it discharges that assumption occurrence and produces \begin{align*} \frac{[A]}{A \to A}\,\to I. \end{align*} The resulting derivation has no open assumption: it does not prove $A$ outright, but proves that if $A$ is temporarily granted, the same occurrence of $A$ may be returned, giving the identity implication $A \to A$. [/example] The identity derivation is also a warning about scope. A discharged assumption cannot be used later as though it were still open. The next rules make that bookkeeping more demanding because disjunction elimination opens two temporary cases and requires both branches to reach the same conclusion. [definition: Disjunction Rules] For formulas $A$, $B$, and $C$, disjunction has the following rules: \begin{align*} \frac{A}{A \lor B}\,\lor I_1, \qquad \frac{B}{A \lor B}\,\lor I_2, \qquad \frac{A \lor B \quad [A] \; \vdots \; C \quad [B] \; \vdots \; C}{C}\,\lor E. \end{align*} [/definition] In $\lor E$, the assumptions $A$ and $B$ in the two side derivations are discharged. The disjunction elimination rule is proof by cases. To use $A \lor B$ in order to prove $C$, it is not enough to inspect only one disjunct; both possible cases must lead to the same conclusion. A failed proof by cases would derive $C$ from $A$ alone and then ignore the $B$ case; such a derivation proves only that the left alternative is sufficient, not that the disjunction as a whole is sufficient. [definition: Falsity and Negation] The constant $\bot$ denotes falsity. Negation is defined by $\neg A := A \to \bot$. [/definition] With negation treated as implication into falsity, a derivation of $\neg A$ is a derivation that turns an assumption of $A$ into a contradiction. Whether an arbitrary formula may be inferred from $\bot$ is not fixed at this point: minimal natural deduction withholds that rule, while intuitionistic and classical natural deduction include it. This separation is needed because later comparisons between systems depend exactly on which uses of contradiction are admitted. [example: Modus Tollens] Suppose $A \to B$ and $\neg B$ are available, where $\neg B$ abbreviates $B \to \bot$. We show that these two assumptions are enough to derive $\neg A$, that is, $A \to \bot$. Temporarily assume $A$. From $A \to B$ and this temporary assumption $A$, implication elimination gives \begin{align*} \frac{A \to B \quad A}{B}\,\to E. \end{align*} Since $\neg B$ means $B \to \bot$, we may now apply implication elimination again, using $B \to \bot$ together with the just-derived $B$: \begin{align*} \frac{B \to \bot \quad B}{\bot}\,\to E. \end{align*} Thus, under the temporary assumption $A$, we have derived $\bot$. Implication introduction discharges that temporary occurrence of $A$ and yields \begin{align*} \frac{[A] \; \vdots \; \bot}{A \to \bot}\,\to I. \end{align*} Because $\neg A$ is defined as $A \to \bot$, the final conclusion is $\neg A$. The derivation shows that an implication $A \to B$ lets a contradiction to $B$ be pulled back to a contradiction to $A$. [/example] ## Assumptions and Discharge What distinguishes natural deduction from a mere collection of inference schemata is its management of assumptions. A proof tree does not only record which formula follows from which earlier formulas; it records which assumptions remain active at the end of the derivation. [definition: Open Assumption] An open assumption of a derivation is an assumption leaf whose occurrence has not been discharged by an inference rule. [/definition] The conclusion of a derivation is always relative to its open assumptions. We write $\Gamma \vdash A$ when there is a natural deduction derivation of $A$ whose open assumptions are contained in the context $\Gamma$. To explain rules such as implication introduction and proof by cases, we need a name for the operation that changes an assumption occurrence from active to closed. Discharge is that operation, and its occurrence-level nature is what keeps temporary hypotheses separate from the ambient context. [definition: Discharge] A rule discharges an assumption occurrence when that occurrence is marked as no longer open in the conclusion of the rule. [/definition] Discharge is occurrence-sensitive. If the same formula is assumed in two different places, a rule may discharge one occurrence while another occurrence remains open. [quotetheorem:4624] [citeproof:4624] This theorem explains why implication is the connective corresponding to hypothetical proof. The hypotheses matter because only selected occurrences of $A$ are discharged; assumptions belonging to $\Gamma$ remain part of the ambient context and cannot be erased by implication introduction. The theorem does not say that every derivation from $\Gamma \cup \{A\}$ is automatically a closed proof of $A \to B$; the derivation must expose the relevant occurrences of $A$ as temporary assumptions. It also gives a practical method for building derivations: to prove $A \to B$, temporarily assume $A$ and work toward $B$. This method will later become the main case in induction proofs over derivations, since implication introduction is the rule that changes the set of open assumptions. [example: Composition of Implications] Assume $(A \to B) \land (B \to C)$. From this single open assumption, the first conjunction elimination rule gives \begin{align*} \frac{(A \to B) \land (B \to C)}{A \to B}\,\land E_1, \end{align*} and the second conjunction elimination rule gives \begin{align*} \frac{(A \to B) \land (B \to C)}{B \to C}\,\land E_2. \end{align*} Now temporarily assume $A$. Using the derived implication $A \to B$ together with this temporary assumption, implication elimination gives \begin{align*} \frac{A \to B \quad A}{B}\,\to E. \end{align*} Using the derived implication $B \to C$ together with the just-derived $B$, implication elimination gives \begin{align*} \frac{B \to C \quad B}{C}\,\to E. \end{align*} Thus, under the temporary assumption $A$, and still under the original assumption $(A \to B) \land (B \to C)$, we have derived $C$. Implication introduction discharges the temporary occurrence of $A$ and yields \begin{align*} \frac{[A] \; \vdots \; C}{A \to C}\,\to I. \end{align*} Finally, implication introduction discharges the original assumption $(A \to B) \land (B \to C)$ and yields \begin{align*} \frac{[(A \to B) \land (B \to C)] \; \vdots \; A \to C}{((A \to B) \land (B \to C)) \to (A \to C)}\,\to I. \end{align*} The derivation expresses composition of implications: a proof that $A$ implies $B$ and $B$ implies $C$ contains exactly the two implication steps needed to turn any temporary proof of $A$ into a proof of $C$. [/example] The example has two nested discharges: the temporary assumption $A$ is closed before the original conjunction assumption is closed. Occurrence-sensitive tracking is what prevents the proof of $A \to C$ from accidentally depending on an assumption that should already have been discharged. The same bookkeeping is needed for disjunction elimination, where a proof by cases must keep the common context fixed while opening two temporary alternatives. [remark: Disjunction Elimination As Proof By Cases] At the sequent level, disjunction elimination says that from \begin{align*} \Gamma\vdash A\lor B,\qquad \Gamma,A\vdash C,\qquad \Gamma,B\vdash C \end{align*} one may infer $\Gamma\vdash C$. The major premise supplies the disjunction, and both branches must prove the same conclusion under their corresponding temporary assumptions. The rule does not permit different conclusions in the two branches, nor does it justify choosing whichever branch is convenient. This sequent-level form is useful in metatheorems because it records the shared context $\Gamma$ explicitly. [/remark] This rule-level statement prepares the next derived rule by emphasizing that natural-deduction abbreviations still have precise local shapes. Modus tollens is another abbreviation of this kind: it can be used efficiently, but its validity depends on the exact assumptions that let implication and negation interact. [quotetheorem:4626] [citeproof:4626] The assumptions in the theorem cannot be weakened to only $\Gamma \vdash A \to B$: without $\neg B$, the derivation has no route from $B$ to contradiction. The result also does not assert the converse implication $\neg A \vdash \neg B$, which is generally invalid and would reverse the direction of the original implication. Modus tollens is therefore a derived rule, not a new primitive connective rule, and later normalization arguments may expand it back into implication eliminations followed by implication introduction. Derived rules shorten derivations without changing what is derivable. In Chapter 3, this distinction matters because normalization studies the structure of proofs, and abbreviations may hide detours that need to be expanded before reductions are defined. ## Minimal, Intuitionistic, and Classical Systems Which principles about contradiction and excluded alternatives should count as basic proof rules? The answer separates minimal, intuitionistic, and classical natural deduction. [definition: Minimal Natural Deduction] Minimal natural deduction is the natural deduction system for $\land$, $\lor$, $\to$, and $\bot$ in which negation is defined by $\neg A := A \to \bot$ and no rule permits an arbitrary formula to be inferred from $\bot$. [/definition] Minimal logic treats contradiction as a terminal failure rather than as a source of every proposition. The next system asks what changes when contradiction is allowed to yield an arbitrary conclusion, while still avoiding classical principles such as excluded middle. [definition: Intuitionistic Natural Deduction] Intuitionistic natural deduction is minimal natural deduction extended by falsity elimination: \begin{align*} \frac{\bot}{A}\,\bot E. \end{align*} [/definition] Intuitionistic logic validates constructive reasoning with explosion, but it does not include the law of excluded middle or double-negation elimination as general principles. Thus a derivation of $\neg\neg A$ does not by itself supply a derivation of $A$; the system records the difference between refuting the refutation of $A$ and constructing $A$ directly. Many familiar informal arguments do treat a refuted refutation as enough to establish the original claim. The obstruction is not a missing connective rule, but a missing license to pass from the impossibility of $\neg A$ to a proof of $A$. To study that stronger style of reasoning proof-theoretically, we add a rule that explicitly permits the classical step while keeping the rest of the natural deduction rules visible. [definition: Classical Natural Deduction] Classical natural deduction is intuitionistic natural deduction extended by a classical rule, such as double-negation elimination \begin{align*} \frac{\neg\neg A}{A}\,\mathrm{DNE}, \end{align*} or proof by contradiction \begin{align*} \frac{[\neg A] \; \vdots \; \bot}{A}\,\mathrm{PBC}. \end{align*} [/definition] Different presentations choose different classical rules, but standard choices are interderivable over intuitionistic natural deduction. The contrast is not about truth tables alone; it is about what counts as a proof of existence, disjunction, or negation. The definition therefore leaves a presentation choice that must be checked rather than assumed harmless. If double-negation elimination and proof by contradiction generated different sets of derivations, then “classical natural deduction” would depend on an arbitrary convention. This raises the comparison problem for the proof system itself: when one presentation adds double-negation elimination and another adds proof by contradiction, do they determine the same derivable formulas? The theorem answers that question by showing that these common classical rules have the same deductive strength over the intuitionistic base. [quotetheorem:4627] [citeproof:4627] The equivalence depends on the intuitionistic base because implication introduction and implication elimination are needed to translate between the two rules. It does not say that either rule is intuitionistically admissible; adding one of them strictly strengthens the proof system by allowing a proof to pass from $\neg\neg A$ to $A$. The result is useful because classical natural deduction can be presented with whichever rule is more convenient, while metatheoretic arguments may replace it by the other without changing the set of derivable formulas. [example: Classical Use of Double Negation] Assume we are working in classical natural deduction and that a derivation of $(A \to \bot) \to \bot$ is available. Since negation is defined by $\neg A := A \to \bot$, the displayed formula is exactly $\neg A \to \bot$, hence it is $\neg\neg A$: \begin{align*} (A \to \bot) \to \bot &= \neg A \to \bot \\ &= \neg\neg A. \end{align*} Classical natural deduction includes double-negation elimination, so the derivation has the form \begin{align*} \frac{(A \to \bot) \to \bot}{A}\,\mathrm{DNE}. \end{align*} In intuitionistic natural deduction, the same premise still proves $\neg\neg A$, because $\neg\neg A$ abbreviates $(A \to \bot) \to \bot$, but there is no general rule \begin{align*} \frac{\neg\neg A}{A}. \end{align*} Thus the classical derivation crosses exactly one proof-theoretic boundary: it turns a proof that $\neg A$ leads to contradiction into a proof of $A$ itself. [/example] The chapter leaves us with two complementary views of natural deduction. Locally, each connective is governed by rules that explain how proofs of compound formulas are made and used. Globally, a derivation is a tree with a changing boundary of open assumptions, and the control of that boundary is what makes implication, negation, and case analysis precise. Chapter 2 shows how proofs in natural deduction are assembled from small rule applications. Chapter 3 then asks a different question: once a proof has been built, can it be simplified without changing its conclusion? Normalization studies exactly those reductions and the detours they remove. # 3. Normalization in Natural Deduction Normalization asks whether derivations can be simplified without changing what they prove. In Chapter 2 we learned the introduction and elimination rules as ways of building and using formulas; this chapter studies what happens when a proof immediately uses a formula in the very way it was just introduced. The guiding question is whether every propositional intuitionistic natural deduction proof can be transformed into one with no such unnecessary detours. The payoff is structural. Normal derivations have a restricted shape, and this restriction gives the subformula property: a normal derivation of a formula mentions only formulas already present in the assumptions or the conclusion. This is the first point in the course where proof transformation yields logical information, including consistency consequences. ## Detours in Natural Deduction What kind of redundancy can appear inside a formal proof? The most basic redundancy occurs when a connective is introduced and then immediately eliminated. Such a step creates a formula only to unpack it at once. [definition: Detour] A detour in a natural deduction derivation is an occurrence of a formula whose last inference is an introduction rule and whose next inference is an elimination rule for the same main connective. [/definition] The word "same" matters: introducing $A \wedge B$ and then applying $\wedge$-elimination is a detour, while introducing $A \wedge B$ and later using it as part of a larger derivation need not be. A detour is local because it can be replaced by a smaller derivation of the same end formula. [example: Projection From A Conjunction] Suppose $\Pi_A$ is a derivation of $A$ from open assumptions $\Gamma_A$, and $\Pi_B$ is a derivation of $B$ from open assumptions $\Gamma_B$. The detour has the following shape: \begin{align*} \frac{ \Pi_A : A \qquad \Pi_B : B }{ A \wedge B }\ \wedge I \qquad \frac{ A \wedge B }{ A }\ \wedge E_1 . \end{align*} The conclusion of this branch is $A$, and the only part of the conjunction introduction used by $\wedge E_1$ is the left component $\Pi_A : A$. Replacing the displayed branch by \begin{align*} \Pi_A : A \end{align*} therefore gives a derivation with the same conclusion $A$ and with open assumptions $\Gamma_A$, which are among the open assumptions $\Gamma_A \cup \Gamma_B$ of the original branch. Thus the formula $A \wedge B$ was introduced only to be projected back to $A$; normalization removes that temporary conjunction and also removes the proof of $B$ from this branch. [/example] This example should be read as a proof transformation, not as a semantic observation. We do not argue that $A \wedge B$ entails $A$ by truth tables; instead we replace one derivation tree by another derivation tree with the same undischarged assumptions and the same conclusion. To state normalization generally, we need a name for this kind of local proof rewrite independent of the particular connective involved. The key requirement is that the rewrite removes a detour without changing what the derivation proves from its open assumptions. [definition: Reduction] A reduction is a local transformation of a derivation tree that replaces a detour by a derivation of the same conclusion from the same open assumptions. [/definition] A reduction is designed to preserve derivability. Its purpose is to remove a local peak in complexity: the proof climbs up to a compound formula by an introduction rule and immediately descends from it by the matching elimination rule. ## Reduction Steps for the Logical Constants How is a detour actually removed for each connective? Each reduction says that if an elimination rule is applied to a formula whose introduction is visible, then the elimination may be performed directly on the data used in the introduction. For implication, the introduction rule packages a hypothetical derivation, and the elimination rule applies the resulting implication to an argument. The reduction substitutes the argument proof for the discharged assumption. [quotetheorem:4628] [citeproof:4628] This is the proof-theoretic analogue of function application. The derivation of $A \to B$ behaves like a procedure that turns a proof of $A$ into a proof of $B$, and implication reduction carries out that procedure. For conjunction, the introduction rule contains exactly the two components that the elimination rules later recover. The detour to be removed arises when a pair is first built by $\wedge I$ and then immediately taken apart by one of the projections $\wedge E_1$ or $\wedge E_2$: the elimination asks for a component that the introduction has already supplied directly. The question is how the reduction should pick out the relevant subderivation and discard the unused one, so that no derivation of $A \wedge B$ survives whose only purpose was to be dismantled. The following reduction answers this by projecting onto exactly the component named by the elimination rule. [quotetheorem:4629] [citeproof:4629] [example: Normalizing A And B Implies A] Consider first the usual derivation of $(A \wedge B) \to A$: \begin{align*} \frac{ [A \wedge B]^1 }{ A }\ \wedge E_1 \qquad \frac{ \begin{array}{c} [A \wedge B]^1\\ \vdots\\ A \end{array} }{ (A \wedge B) \to A }\ \to I^1 . \end{align*} The formula $A \wedge B$ used as the major premise of $\wedge E_1$ is the open assumption $[A \wedge B]^1$. It was not obtained by an immediately preceding $\wedge I$ step, so this occurrence is not a detour. The final $\to I$ discharges exactly that assumption and produces the conclusion $(A \wedge B) \to A$. By contrast, suppose $\Pi_A$ derives $A$ from open assumptions $\Gamma_A$, and $\Pi_B$ derives $B$ from open assumptions $\Gamma_B$. Then the branch \begin{align*} \frac{ \frac{ \Pi_A : A \qquad \Pi_B : B }{ A \wedge B }\ \wedge I }{ A }\ \wedge E_1 \end{align*} does contain a detour: the formula $A \wedge B$ is introduced by $\wedge I$ and immediately used as the major premise of $\wedge E_1$. The left elimination rule selects the left component of the displayed introduction, so the reduced branch is \begin{align*} \Pi_A : A . \end{align*} The conclusion remains $A$, and the open assumptions are reduced from $\Gamma_A \cup \Gamma_B$ to $\Gamma_A$. Thus normalization deletes the temporary conjunction $A \wedge B$ and removes the unused derivation of $B$ from this branch. [/example] Disjunction behaves differently because its introduction rule chooses a side, while its elimination rule demands two cases. If the disjunction was just introduced on the left, only the left case is relevant; if it was just introduced on the right, only the right case is relevant. The obstruction is that a case analysis appears to require both branches even when the preceding introduction already reveals which branch can occur. The reduction theorem records how normalization discards the unreachable case while preserving the conclusion of the derivation. [quotetheorem:4630] [citeproof:4630] [example: Removing a Case Analysis Detour] Suppose $\Pi_A$ is a derivation of $A$ from open assumptions $\Gamma_A$. Suppose also that $\Delta_A$ is a derivation of $C$ from open assumptions $\Gamma_C$ together with a marked assumption $A$, and that $\Delta_B$ is a derivation of $C$ from open assumptions $\Gamma_D$ together with a marked assumption $B$. The detour has the following shape: \begin{align*} \frac{ \frac{ \Pi_A : A }{ A \vee B }\ \vee I_1 \qquad \begin{array}{c} [A]^1\\ \Delta_A\\ C \end{array} \qquad \begin{array}{c} [B]^2\\ \Delta_B\\ C \end{array} }{ C }\ \vee E^{1,2}. \end{align*} The formula $A \vee B$ is introduced by $\vee I_1$ and is immediately used as the major premise of $\vee E$, so this is an introduction-elimination detour for disjunction. Since the displayed disjunction was introduced from the left component $\Pi_A : A$, the elimination does not need the $B$-case. The reduced derivation enters the $A$-case directly by replacing each discharged occurrence of $[A]^1$ in $\Delta_A$ with a copy of $\Pi_A$: \begin{align*} \begin{array}{c} \Pi_A : A\\ \Delta_A\\ C \end{array} \end{align*} where the notation means that every leaf $[A]^1$ formerly discharged by $\vee E$ is replaced by the derivation $\Pi_A$ of $A$. The resulting derivation still concludes $C$, and its open assumptions are among $\Gamma_A \cup \Gamma_C$; the assumptions $\Gamma_D$ from the discarded $B$-case no longer occur in this branch. Thus the original proof split into two cases even though the source of the disjunction was already known to be the left disjunct, and normalization removes that unnecessary case analysis. [/example] Falsity has no introduction rule in minimal or intuitionistic natural deduction. The elimination rule $\bot$-elimination therefore has no matching introduction-elimination detour of the same kind. [remark: Falsity and Detours] There is no principal reduction for $\bot$ matching an introduction rule, since $\bot$ has no introduction rule. Reductions involving $\bot$ instead arise indirectly when a derivation of $\bot$ contains a detour for another connective before $\bot$-elimination is applied. [/remark] Negation is usually treated as the abbreviation $\neg A := A \to \bot$. Under this convention, normalization for negation is inherited from implication and falsity rather than requiring a separate primitive reduction rule. ## Normal Derivations When should the process of reducing detours stop? We want a derivation in which no formula is immediately introduced and then eliminated. Such proofs are called normal. [definition: Normal Derivation] A natural deduction derivation is normal if it contains no detour. [/definition] Normality is a syntactic property of derivation trees. It does not say that the proof is short, unique, or semantically special; it says that the proof contains no local introduction-elimination redundancy. To prove that repeated reductions eventually stop, we need a way to compare detours by size. The size relevant to a detour is not the length of the surrounding proof but the logical complexity of the formula introduced and then eliminated. [definition: Degree of a Formula] The degree of a propositional formula is the number of occurrences of logical connectives in it. [/definition] A derivation may contain several detours of different logical sizes, and reducing one detour can change the height or placement of others. A termination proof therefore needs a global measure that decreases despite these local rearrangements, rather than merely counting the number of displayed inference steps. [definition: Complexity of a Derivation] The complexity of a derivation is measured by a finite tuple recording the degrees and positions of its detour formulas, ordered lexicographically by the largest detour degree first and then by derivation height. [/definition] The exact bookkeeping can vary between presentations, but the role of the measure is fixed: every permitted reduction must decrease it. This gives a termination argument for reduction sequences in the propositional system. With a decreasing complexity measure in hand, the next question is whether every derivation can actually be simplified all the way to a detour-free one. The normalization theorem answers this existence question for propositional natural deduction. [quotetheorem:4631] [citeproof:4631] This theorem is called weak normalization because it asserts the existence of at least one terminating reduction sequence. A stronger theorem would say that every possible reduction sequence terminates; that stronger statement requires a sharper argument and is not needed for the consequences developed here. [remark: Preservation of Assumptions] Normalization does not add new undischarged assumptions. Each reduction either selects an existing subderivation or substitutes a derivation into assumptions that were already marked for discharge. [/remark] ## The Subformula Property What does a normal proof reveal about the formulas that may occur inside it? If no connective is introduced merely to be eliminated, then the proof cannot freely wander through unrelated compound formulas. This restriction is captured by the subformula property. [definition: Subformula] A formula $B$ is a subformula of a formula $A$ if $B = A$ or if $B$ occurs as a constituent formula inside $A$. [/definition] For example, the subformulas of $(A \wedge B) \to C$ are $(A \wedge B) \to C$, $A \wedge B$, $A$, $B$, and $C$. Subformulas are computed syntactically, not up to logical equivalence. The point of normality is that it should prevent a proof from introducing formulas unrelated to its assumptions and conclusion, but that claim is stronger than the definition of subformula alone. What needs proof is a global restriction on every formula that appears anywhere inside a normal derivation. The subformula theorem supplies exactly that restriction by locating each such formula inside the formulas already present at the boundary of the proof. [quotetheorem:4632] [citeproof:4632] This theorem is one of the main reasons normal proofs are useful. It gives a finite search space for derivations with fixed assumptions and conclusion, because only finitely many subformulas are available. [example: Subformula Check for A And B Implies A] In the normal derivation of $(A \wedge B) \to A$, the derivation has the following shape: \begin{align*} \frac{ \frac{ [A \wedge B]^1 }{ A }\ \wedge E_1 }{ (A \wedge B) \to A }\ \to I^1 . \end{align*} Thus the formulas occurring in the displayed proof are exactly the assumption formula $A \wedge B$, the formula $A$ obtained by $\wedge E_1$, and the final conclusion $(A \wedge B) \to A$. We now check the subformulas of the conclusion syntactically. The outermost connective of $(A \wedge B) \to A$ is $\to$, so its immediate subformulas are $A \wedge B$ and $A$. The formula $A \wedge B$ has outermost connective $\wedge$, so its immediate subformulas are $A$ and $B$. Therefore the full list of subformulas of $(A \wedge B) \to A$ is \begin{align*} (A \wedge B) \to A,\qquad A \wedge B,\qquad A,\qquad B . \end{align*} Each formula occurring in the normal derivation, \begin{align*} A \wedge B,\qquad A,\qquad (A \wedge B) \to A, \end{align*} appears in this list. By contrast, $A \wedge (B \wedge A)$ is not a subformula of $(A \wedge B) \to A$: the only conjunctive subformula of the conclusion is $A \wedge B$, and its right component is $B$, not $B \wedge A$. A non-normal proof may introduce such an extra formula only as temporary material; when that material is introduced and then immediately eliminated, normalization removes that detour and returns the proof to formulas already present in the subformula list. [/example] The subformula property should not be confused with completeness. It does not say that a proof exists whenever a formula belongs to the subformula closure; it says that if a normal proof exists, its formulas are confined to that closure. ## Consistency Consequences How can transforming proofs tell us that certain formulas are unprovable? The key idea is that a closed normal proof of falsity would have to end with an introduction rule, but falsity has no introduction rule. The argument is syntactic: it does not rely on truth assignments, Kripke models, or algebraic semantics. It shows how proof theory can establish consistency by analyzing the possible shapes of proofs. [quotetheorem:4633] [citeproof:4633] [remark: Scope of the Consistency Result] The result here concerns the propositional intuitionistic system described in the previous chapter. Adding classical principles, first-order quantifiers, equality, or arithmetic axioms changes the normalization and consistency questions, and each extension requires its own proof-theoretic analysis. [/remark] Normalization also explains why introduction and elimination rules are matched. Introduction rules specify canonical ways to prove a connective, while elimination rules specify what may be extracted from such a proof. Reduction verifies locally that these two directions fit together. ## What Normalization Contributes to the Course Why does this chapter sit between natural deduction and sequent calculus? It gives the first systematic proof transformation theorem. In Chapter 7, cut elimination for the sequent calculus introduced in Chapter 6 will play a parallel role: it removes a rule that introduces an intermediate formula and then uses it elsewhere. [explanation: Normalization as Computation] The implication reduction is the prototype of computation in proofs. A proof of $A \to B$ formed by discharging an assumption $A$ behaves like a function, and applying it to a proof of $A$ is evaluated by substitution. Conjunction reduction behaves like projection from a pair, and disjunction reduction behaves like choosing the relevant branch of a case distinction. This is the Curry-Howard reading of natural deduction in its simplest propositional form. [/explanation] The main lesson is that proofs contain operational structure. They can be simplified, and their simplified forms expose constraints that are invisible if proofs are treated only as certificates of semantic validity. Normalization reveals that proofs are not just correct or incorrect, but computationally structured. Chapter 4 makes that structure explicit through the Curry-Howard correspondence, interpreting propositions as types and proofs as typed lambda terms. # 4. Curry-Howard Correspondence This chapter explains the computational reading of the natural deduction rules studied so far. The guiding question is: if a proof is a structured object, what kind of mathematical object is it? The Curry-Howard correspondence answers by reading propositions as types, proofs as typed lambda terms, and proof normalization as computation. In the previous chapter, normalization removed detours in natural deduction. Here the same reductions reappear as beta-reductions of lambda terms. This gives a precise bridge between proof transformations and programs: simplifying a proof corresponds to evaluating the program represented by that proof. ## Propositions as Types and Proofs as Terms What does it mean to regard a proof of $A$ as an object rather than as a certificate written in prose? The first step is to assign to each proposition $A$ a type, and to each derivation of $A$ a term inhabiting that type. Contexts of assumptions become typing contexts: an undischarged assumption $x:A$ is read as a variable $x$ of type $A$. [definition: Typing Context] A typing context is a finite list \begin{align*} \Gamma = x_1:A_1,\dots,x_n:A_n \end{align*} where the $x_i$ are distinct variables and the $A_i$ are types. [/definition] The judgement $\Gamma \vdash t:A$ says that, using variables declared in $\Gamma$, the term $t$ has type $A$. Under Curry-Howard this is read at the same time as a proof-theoretic judgement: from assumptions $\Gamma$, the term $t$ represents a proof of proposition $A$. To make this reading more than an analogy, each logical connective must be assigned a corresponding type former. The translation below fixes that dictionary so that later proof rules can be compared directly with term constructors and eliminators. [definition: Propositions as Types Interpretation] Fix a collection of propositional variables and corresponding atomic types. The propositions as types translation $(-)^\ast$ from formulas generated by $\to$, $\wedge$, and $\vee$ to type expressions is defined by \begin{align*} P^\ast &= P \quad\text{for each propositional variable } P,\\ (A \to B)^\ast &= A^\ast \to B^\ast,\\ (A \wedge B)^\ast &= A^\ast \times B^\ast,\\ (A \vee B)^\ast &= A^\ast + B^\ast. \end{align*} [/definition] Under this translation, a proof of a proposition is represented by a term of the corresponding type. This interpretation is not only a slogan. The introduction and elimination rules for each connective match the constructors and destructors of the corresponding type former. [example: Identity Proof as a Lambda Term] To represent the natural deduction proof of $A\to A$, begin with one temporary assumption $x:A$. By the variable rule in the typing context $x:A$, the variable itself has type $A$: \begin{align*} x:A \vdash x:A. \end{align*} The rule for lambda abstraction says that from a derivation of $\Gamma,x:A\vdash t:B$ one obtains $\Gamma\vdash \lambda x.t:A\to B$. Applying this rule with $\Gamma$ empty, $t=x$, and $B=A$ gives \begin{align*} \vdash \lambda x.x : A\to A. \end{align*} Thus the proof first uses the assumed proof of $A$ exactly as given, and then discharges that assumption by binding it as the input variable of the identity function. [/example] This pattern will recur throughout the chapter: a proof-theoretic operation is recorded by a corresponding term-forming operation, and the bookkeeping of discharged assumptions becomes the bookkeeping of bound variables. [remark: Inhabitation] To say that a type $A$ is inhabited means that there exists a closed term $t$ with $\vdash t:A$. In the proof-theoretic reading, this says exactly that the proposition $A$ has a proof with no open assumptions. [/remark] ## Implication and Function Types How should hypothetical reasoning be recorded inside a term? If a proof of $B$ depends on a temporary assumption $A$, then the completed proof of $A \to B$ must remember how to transform any proof of $A$ into a proof of $B$. This is the reason implication corresponds to function type. [definition: Lambda Abstraction and Application] For types $A$ and $B$, the function type $A \to B$ has terms generated by the following operations: \begin{align*} &\text{if } \Gamma,x:A \vdash t:B, \text{ then } \Gamma \vdash \lambda x.t:A\to B,\\ &\text{if } \Gamma \vdash f:A\to B \text{ and } \Gamma \vdash a:A, \text{ then } \Gamma \vdash f\,a:B. \end{align*} [/definition] The first rule is implication introduction: an assumption is discharged and becomes a bound variable. The second rule is implication elimination: a proof of $A \to B$ is applied to a proof of $A$ to obtain a proof of $B$. The rule-by-rule resemblance still needs a precise adequacy statement: every derivation in the implication fragment should correspond to a typed lambda term, and every such term should express a derivation. The theorem records this exact match for the fragment generated by variables, abstraction, and application. [quotetheorem:4634] [citeproof:4634] This theorem makes the syntax of proofs and the syntax of typed programs two presentations of the same structure, but only for the fragment it names. The restriction to implication matters because the term language currently has only variables, abstraction, and application; conjunction and disjunction require new term constructors such as pairs, projections, injections, and case analysis. The theorem is also not a claim that classical reasoning has the same direct computational reading, since principles such as excluded middle do not arise from these three rules alone. What it provides is the base case for the broader correspondence: once the rule-by-rule match is visible for implication, the other connectives can be added by extending both the natural deduction system and the typed term language in parallel. [example: Composition as a Proof Term] Consider the formula $(A \to B) \to ((B \to C) \to (A \to C))$. To build a closed term of this type, begin with the typing context \begin{align*} f:A\to B,\; g:B\to C,\; x:A. \end{align*} By the variable rule, $f:A\to B$ and $x:A$ are available in this context, so application gives \begin{align*} f:A\to B,\; g:B\to C,\; x:A &\vdash f:A\to B,\\ f:A\to B,\; g:B\to C,\; x:A &\vdash x:A,\\ f:A\to B,\; g:B\to C,\; x:A &\vdash f\,x:B. \end{align*} Again by the variable rule, $g:B\to C$ is available in the same context. Applying $g$ to the term $f\,x:B$ gives \begin{align*} f:A\to B,\; g:B\to C,\; x:A &\vdash g:B\to C,\\ f:A\to B,\; g:B\to C,\; x:A &\vdash f\,x:B,\\ f:A\to B,\; g:B\to C,\; x:A &\vdash g(f\,x):C. \end{align*} Now abstract over the assumptions in reverse order. First abstracting over $x:A$ gives \begin{align*} f:A\to B,\; g:B\to C \vdash \lambda x.g(f\,x):A\to C. \end{align*} Then abstracting over $g:B\to C$ gives \begin{align*} f:A\to B \vdash \lambda g.\lambda x.g(f\,x):(B\to C)\to(A\to C). \end{align*} Finally abstracting over $f:A\to B$ gives the closed term \begin{align*} \vdash \lambda f.\lambda g.\lambda x.g(f\,x):(A\to B)\to((B\to C)\to(A\to C)). \end{align*} Thus the proof term records ordinary composition: it turns a function from $A$ to $B$ and a function from $B$ to $C$ into a function from $A$ to $C$. [/example] ## Conjunction and Product Types What information is contained in a proof of $A \wedge B$? Such a proof contains both a proof of $A$ and a proof of $B$, so its term counterpart is a pair. Eliminating a conjunction amounts to projecting one component of that pair. [definition: Product Type] For types $A$ and $B$, the product type $A \times B$ has terms generated by pairing and projections: \begin{align*} &\text{if } \Gamma \vdash s:A \text{ and } \Gamma \vdash t:B, \text{ then } \Gamma \vdash (s,t):A\times B,\\ &\text{if } \Gamma \vdash p:A\times B, \text{ then } \Gamma \vdash \pi_1(p):A,\\ &\text{if } \Gamma \vdash p:A\times B, \text{ then } \Gamma \vdash \pi_2(p):B. \end{align*} [/definition] The product type $A\times B$ is the type-theoretic image of conjunction $A\wedge B$. Pairing is conjunction introduction, while $\pi_1$ and $\pi_2$ are the two conjunction elimination rules. [example: Product Projections as Conjunction Eliminations] Assume $p:A\times B$. By the variable rule in the context $p:A\times B$, we have \begin{align*} p:A\times B \vdash p:A\times B. \end{align*} The first product elimination rule says that from a term of type $A\times B$ one may form its left projection of type $A$, so \begin{align*} p:A\times B \vdash \pi_1(p):A. \end{align*} Discharging the assumption $p:A\times B$ by lambda abstraction gives \begin{align*} \vdash \lambda p.\pi_1(p):(A\times B)\to A. \end{align*} The right projection is obtained in the same way. From the same variable judgement \begin{align*} p:A\times B \vdash p:A\times B \end{align*} the second product elimination rule gives \begin{align*} p:A\times B \vdash \pi_2(p):B, \end{align*} and lambda abstraction therefore gives \begin{align*} \vdash \lambda p.\pi_2(p):(A\times B)\to B. \end{align*} Thus the two conjunction elimination rules become the two programs that consume a pair and return exactly one of its components. [/example] The projection examples also show a boundary of product elimination: a projection can consume exactly the information that pairing introduced, but it cannot manufacture the missing component of a product. [example: Swapping a Conjunction] The formula $A\wedge B \to B\wedge A$ is represented under propositions-as-types as a function of type $(A\times B)\to(B\times A)$. Assume one input pair: \begin{align*} p:A\times B. \end{align*} By the variable rule in the context $p:A\times B$, \begin{align*} p:A\times B \vdash p:A\times B. \end{align*} Applying the second product elimination rule to this term gives the right component: \begin{align*} p:A\times B \vdash \pi_2(p):B. \end{align*} Applying the first product elimination rule to the same term gives the left component: \begin{align*} p:A\times B \vdash \pi_1(p):A. \end{align*} Now the product introduction rule pairs these two derived terms, with the $B$-term placed first and the $A$-term placed second: \begin{align*} p:A\times B \vdash \pi_2(p):B,\qquad p:A\times B \vdash \pi_1(p):A, \end{align*} so \begin{align*} p:A\times B \vdash (\pi_2(p),\pi_1(p)):B\times A. \end{align*} Discharging the temporary assumption $p:A\times B$ by lambda abstraction yields the closed term \begin{align*} \vdash \lambda p.(\pi_2(p),\pi_1(p)):(A\times B)\to(B\times A). \end{align*} Thus the proof term consumes a proof of $A\wedge B$, extracts both conjuncts, and rebuilds them in the opposite order as a proof of $B\wedge A$. [/example] ## Disjunction and Sum Types What must a proof of $A\vee B$ tell us? It must identify which side has been proved and provide the corresponding proof. Treating disjunction as an untagged truth-value would lose this information: from a bare assertion that $A\vee B$ holds, there is no term-level way to decide whether to use an $A$-argument or a $B$-argument in a proof by cases. This is why disjunction is represented by a sum type with two injections. [definition: Sum Type] For types $A$ and $B$, the sum type $A+B$ has terms generated by injections and case analysis: \begin{align*} &\text{if } \Gamma \vdash s:A, \text{ then } \Gamma \vdash \operatorname{inl}(s):A+B,\\ &\text{if } \Gamma \vdash t:B, \text{ then } \Gamma \vdash \operatorname{inr}(t):A+B,\\ &\text{if } \Gamma \vdash u:A+B,\; \Gamma,x:A\vdash r:C,\; \Gamma,y:B\vdash q:C,\\ &\text{then } \Gamma \vdash \operatorname{case}(u;x.r;y.q):C. \end{align*} [/definition] The two injections correspond to the two disjunction introduction rules. Case analysis corresponds to disjunction elimination: to use a proof of $A\vee B$ to prove $C$, give a proof of $C$ from $A$ and a proof of $C$ from $B$. [example: Using a Disjunction by Cases] We construct a closed term of type $(A\to C)\to((B\to C)\to((A+B)\to C))$ by starting in the context \begin{align*} f:A\to C,\; g:B\to C,\; u:A+B. \end{align*} To use the sum term $u$, the sum elimination rule requires one branch of type $C$ from an assumed $A$ and one branch of type $C$ from an assumed $B$. In the left branch, extend the context by $x:A$. By the variable rule, \begin{align*} f:A\to C,\; g:B\to C,\; u:A+B,\; x:A &\vdash f:A\to C,\\ f:A\to C,\; g:B\to C,\; u:A+B,\; x:A &\vdash x:A. \end{align*} Application therefore gives \begin{align*} f:A\to C,\; g:B\to C,\; u:A+B,\; x:A &\vdash f\,x:C. \end{align*} In the right branch, extend the original context by $y:B$. Again by the variable rule, \begin{align*} f:A\to C,\; g:B\to C,\; u:A+B,\; y:B &\vdash g:B\to C,\\ f:A\to C,\; g:B\to C,\; u:A+B,\; y:B &\vdash y:B. \end{align*} Application gives \begin{align*} f:A\to C,\; g:B\to C,\; u:A+B,\; y:B &\vdash g\,y:C. \end{align*} Since the two branches both have result type $C$, and since \begin{align*} f:A\to C,\; g:B\to C,\; u:A+B \vdash u:A+B \end{align*} by the variable rule, the sum elimination rule gives \begin{align*} f:A\to C,\; g:B\to C,\; u:A+B \vdash \operatorname{case}(u;x.f\,x;y.g\,y):C. \end{align*} Now abstract over the assumptions in reverse order: \begin{align*} f:A\to C,\; g:B\to C &\vdash \lambda u.\operatorname{case}(u;x.f\,x;y.g\,y):(A+B)\to C,\\ f:A\to C &\vdash \lambda g.\lambda u.\operatorname{case}(u;x.f\,x;y.g\,y):(B\to C)\to((A+B)\to C),\\ &\vdash \lambda f.\lambda g.\lambda u.\operatorname{case}(u;x.f\,x;y.g\,y): (A\to C)\to((B\to C)\to((A+B)\to C)). \end{align*} Thus the term represents proof by cases: a proof of $A+B$ is consumed by selecting the branch matching its tag, and both branches are forced to produce the same target type $C$. [/example] The example also points to a boundary of the idea. The following remark, Constructive Content of Disjunction, records that interpretation before the construction is used again. [remark: Constructive Content of Disjunction] A proof of $A\vee B$ is stronger than a semantic assertion that at least one of $A$ and $B$ is true. It carries either a tagged proof of $A$ or a tagged proof of $B$. This is the constructive feature that makes the sum type interpretation fit intuitionistic logic. [/remark] ## Beta-Reduction and Proof Normalization What does it mean to simplify a proof after translating it into a lambda term? The answer is substitution. A detour in which an introduction rule is immediately followed by its matching elimination rule becomes a beta-redex, and reducing it substitutes the given proof into the place where the temporary assumption was used. [definition: Beta-Reduction] In the term language with variables, abstraction, application, pairs, projections, injections, and case analysis, beta-reduction for function types is the rewrite \begin{align*} (\lambda x.t)\,a \longrightarrow_{\beta} t[a/x], \end{align*} where $t[a/x]$ denotes capture-avoiding substitution of $a$ for free occurrences of $x$ in $t$. The one-step reduction relation is closed under all term contexts. [/definition] For products and sums, beta-reduction cannot be described by function application alone. The obstruction is that pairs and injections are introduced by different term constructors, and their eliminations inspect those constructors in different ways. To make normalization a uniform rewrite system, we must state the computation rules for projections and case analyses alongside the function rule. [definition: Product and Sum Reductions] The product reductions are \begin{align*} \pi_1(s,t) &\longrightarrow s, & \pi_2(s,t) &\longrightarrow t. \end{align*} The sum reductions are \begin{align*} \operatorname{case}(\operatorname{inl}(s);x.r;y.q) &\longrightarrow r[s/x],\\ \operatorname{case}(\operatorname{inr}(t);x.r;y.q) &\longrightarrow q[t/y]. \end{align*} [/definition] These reductions are the term-level images of the normalization reductions from the preceding chapter. Once they are treated as computation rules, a basic soundness question appears: simplifying a proof term should not change the proposition it proves. The capture-avoiding condition is part of that question, because if substitution allowed free variables of the argument to become bound inside the target term, then replacing a temporary proof could change which assumptions the resulting proof depends on. The preservation theorem records the invariant that well-typed reduction keeps the same type. [quotetheorem:4635] [citeproof:4635] Preservation says that computation does not change the proposition proved. The hypotheses are essential: the starting term must be well typed, and substitution must be capture-avoiding, because otherwise a reduction can change the assumptions on which a subterm depends or produce a term that no longer fits the surrounding typing rule. Preservation is also a local invariant, not a full normalization theorem: it does not by itself say that reduction terminates, that normal forms are unique, or that different reduction orders agree. Those stronger results require separate arguments such as strong normalization and confluence, and together they explain why the proof reductions from the previous chapter can be treated as a disciplined evaluation process. [example: Normalizing an Implication Detour] Let $a:A$ be a proof term. In the context $x:A$, the variable rule gives \begin{align*} x:A \vdash x:A. \end{align*} By lambda abstraction, this yields the closed identity proof \begin{align*} \vdash \lambda x.x:A\to A. \end{align*} Since $a:A$, application gives \begin{align*} a:A,\; \lambda x.x:A\to A \vdash (\lambda x.x)\,a:A. \end{align*} Now beta-reduction substitutes $a$ for the free occurrences of $x$ in the body $x$: \begin{align*} (\lambda x.x)\,a &\longrightarrow_{\beta} x[a/x]\\ &= a. \end{align*} Thus the normalized proof is the original proof $a$ of $A$; the temporary construction of the identity function and its immediate application have been removed. [/example] The previous example fixes one test case for the idea. The next example, Normalizing a Product Detour, changes the setting so the same mechanism can be recognized from another angle. [example: Normalizing a Product Detour] Assume $\Gamma \vdash s:A$ and $\Gamma \vdash t:B$. By the product introduction rule, these two derivations form the pair \begin{align*} \Gamma \vdash (s,t):A\times B. \end{align*} The first product elimination rule applies to any term of type $A\times B$, so applying it to $(s,t)$ gives \begin{align*} \Gamma \vdash \pi_1(s,t):A. \end{align*} The matching product reduction rule selects the first component of the pair: \begin{align*} \pi_1(s,t) \longrightarrow s. \end{align*} The type is preserved through this reduction because the selected component is exactly the original term $s:A$ in the same context $\Gamma$. Thus the detour first constructs a proof of $A\wedge B$ from proofs of $A$ and $B$, then immediately eliminates that conjunction by returning the left proof $s$. [/example] ## What the Correspondence Explains Why is Curry-Howard central in proof theory rather than only a useful analogy? It gives a uniform account of proofs, programs, and reductions. Natural deduction proofs are typed terms; normalization is evaluation; preservation of type is preservation of theoremhood. [explanation: Proofs as Computational Objects] The correspondence changes the role of syntax in logic. A derivation is no longer only evidence that a formula follows from assumptions; it is a structured object with operations, reductions, and normal forms. The introduction rules construct data, while the elimination rules consume data. This also clarifies the difference between intuitionistic and classical logic. The direct propositions-as-types reading matches intuitionistic reasoning because a proof of $A\vee B$ must provide a side and a proof, and a proof of $A\to B$ must transform proofs of $A$ into proofs of $B$. Classical principles require additional computational operators or control constructs, which are beyond this chapter. [/explanation] This perspective is also the starting point for programming-language semantics: type systems are designed so that evaluation preserves types, and proof theory supplies the logical explanation for that design. [remark: Link with the Previous Chapter] The preceding chapter studied normalization as a transformation of derivation trees. This chapter gives the same process a typed computational language. Chapter 5 next returns to natural deduction with first-order quantifiers, where substitution and variable binding become proof-theoretic side conditions. [/remark] Chapter 4 turns normalization into a typed computational language, showing that proof reduction mirrors computation. Chapter 5 returns to natural deduction, now with quantifiers, where the same proof-theoretic discipline must control variables, substitution, and witnesses. # 5. First-Order Natural Deduction First-order natural deduction extends the propositional natural deduction of Chapter 2 by allowing proofs to reason about arbitrary objects and about the existence of objects with specified properties. The new difficulty is not the shape of derivation trees, but the management of variables: a variable may stand for a completely arbitrary element, for a temporarily chosen witness, or for a bound placeholder inside a formula. This chapter develops the syntax of terms and capture-avoiding substitution before stating the quantifier rules and the eigenvariable side conditions that make them sound. ## Terms, Variables, and Substitution How can a formal proof replace an informal phrase such as "take an arbitrary object" or "substitute this term for that variable" without accidentally changing the meaning of a formula? First-order syntax separates variables that are available for substitution from variables that are bound by quantifiers. The quantifier rules later in the chapter depend on this separation. [definition: Term] A term of a first-order language is generated from variables, constant symbols, and function symbols as follows: 1. Every variable is a term. 2. Every constant symbol is a term. 3. If $f$ is an $n$-ary function symbol and $t_1,\dots,t_n$ are terms, then $f(t_1,\dots,t_n)$ is a term. [/definition] Terms are the syntactic expressions that may denote objects in a structure. They are not formulas, since they do not have truth values on their own. [example: Arithmetic Terms] In the language of arithmetic, $0$ is a constant symbol, so $0$ is a term. Since $S$ is unary and $0$ is a term, $S(0)$ is a term. Every variable is a term, so $x$, $y$, and $z$ are terms. Since $+$ is binary and $x$ and $S(y)$ are terms, $x+S(y)$ is a term. Since $S(0)$ is a term, $x+S(0)$ is a term; since $\cdot$ is binary and $x+S(0)$ and $z$ are terms, $(x+S(0))\cdot z$ is a term. The expression $x+S(y)=z$ has the form $t_1=t_2$, where $t_1$ is the term $x+S(y)$ and $t_2$ is the term $z$. Thus it is not itself a term; it is an atomic formula formed by applying the equality symbol to two terms. [/example] The first place where variable management matters is the distinction between occurrences of variables. A quantifier does not control every appearance of the same symbol in a formula; it controls only the appearances inside its scope. We therefore need a local classification of variable occurrences before we can define free variables or safe substitution. [definition: Free and Bound Occurrence] An occurrence of a variable $x$ in a formula $A$ is bound if it lies within the scope of a quantifier $\forall x$ or $\exists x$. An occurrence of $x$ in $A$ is free if it is not bound. [/definition] The same variable symbol can have both free and bound occurrences in a larger formula. In practice this is a source of mistakes, so proofs often rename bound variables before substitution. To state substitution and quantifier rules without ambiguity, we also need the set of variables whose values remain externally assignable in a formula. [definition: Free Variables] Let $\operatorname{Form}$ be the set of formulas of the first-order language and let $\operatorname{Var}$ be the set of variables. The free-variable operation is the map \begin{align*} FV:\operatorname{Form}\to \mathcal{P}(\operatorname{Var}) \end{align*} defined recursively by: 1. If $A$ is atomic, then $FV(A)$ is the set of variables occurring in its terms. 2. $FV(\neg A)=FV(A)$. 3. $FV(A\circ B)=FV(A)\cup FV(B)$ for $\circ\in\{\wedge,\vee,\to\}$. 4. $FV(\forall x A)=FV(A)\setminus\{x\}$. 5. $FV(\exists x A)=FV(A)\setminus\{x\}$. [/definition] A formula with no free variables is a sentence. Sentences are the formulas whose truth value is determined by a structure alone, without assigning values to free variables. [example: Free Variables in a Quantified Formula] For the formula $A=\forall x\,(R(x,y)\to \exists y\,S(y,z))$, compute free variables from the inside out using the recursive clauses in the definition of $FV$: \begin{align*} FV(R(x,y))&=\{x,y\},\\ FV(S(y,z))&=\{y,z\},\\ FV(\exists y\,S(y,z))&=FV(S(y,z))\setminus\{y\}\\ &=\{y,z\}\setminus\{y\}\\ &=\{z\}. \end{align*} Therefore the implication inside the outer quantifier has free variables \begin{align*} FV(R(x,y)\to \exists y\,S(y,z)) &=FV(R(x,y))\cup FV(\exists y\,S(y,z))\\ &=\{x,y\}\cup \{z\}\\ &=\{x,y,z\}. \end{align*} Finally, \begin{align*} FV(\forall x\,(R(x,y)\to \exists y\,S(y,z))) &=FV(R(x,y)\to \exists y\,S(y,z))\setminus\{x\}\\ &=\{x,y,z\}\setminus\{x\}\\ &=\{y,z\}. \end{align*} Thus the $x$ in $R(x,y)$ is bound by the outer $\forall x$, the $y$ in $S(y,z)$ is bound by the inner $\exists y$, and the remaining free variables are exactly $y$ and $z$. [/example] Substitution is the formal operation that replaces free occurrences of a variable by a term. The obstruction is variable capture: a free variable in the inserted term can accidentally become bound by a quantifier already present in the formula. The definition must therefore treat substitution as a controlled operation, not as a naive textual replacement. [definition: Substitution] Let $\operatorname{Term}$ be the set of terms. Substitution is the partial operation \begin{align*} (-)[-/ -] : \operatorname{Form}\times \operatorname{Term}\times \operatorname{Var} \rightharpoonup \operatorname{Form} \end{align*} whose value at $(A,t,x)$ is denoted $A[t/x]$. It is defined when replacing every free occurrence of $x$ in $A$ by $t$ causes no free variable of $t$ to become bound, and then $A[t/x]$ is the resulting formula. [/definition] When the proviso fails, we first rename bound variables in $A$ and then perform the substitution. This renaming is called alpha-conversion and does not change the logical content of the formula. [example: Avoiding Variable Capture] Consider the formula $\forall y\,R(x,y)$ and the proposed substitution of the term $y$ for the free occurrences of $x$. The occurrence of $x$ in $R(x,y)$ is free, while the occurrence of $y$ in $R(x,y)$ is bound by the outer quantifier $\forall y$. If we replace $x$ by $y$ without changing the bound variable, the syntactic replacement is \begin{align*} (\forall y\,R(x,y))[y/x] &=\forall y\,\bigl(R(x,y)[y/x]\bigr)\\ &=\forall y\,R(y,y). \end{align*} In the last formula, the inserted $y$ lies inside the scope of $\forall y$, so the variable that was free in the inserted term has become bound. This is variable capture. To avoid capture, first rename the bound variable $y$ to a fresh variable $z$: \begin{align*} \forall y\,R(x,y) &\equiv \forall z\,R(x,z). \end{align*} Now the substitution is capture-free, because the inserted term $y$ is not placed under a quantifier binding $y$: \begin{align*} (\forall z\,R(x,z))[y/x] &=\forall z\,\bigl(R(x,z)[y/x]\bigr)\\ &=\forall z\,R(y,z). \end{align*} Thus the intended result is $\forall z\,R(y,z)$, not $\forall y\,R(y,y)$; renaming the bound variable preserves the free occurrence of the inserted $y$. [/example] The example shows why a separate admissibility condition is needed. A term may be syntactically available for replacement and still be unsafe because one of its free variables would fall under an existing quantifier after substitution. The terminology “free for substitution” names exactly the absence of that capture obstruction. [definition: Free for Substitution] A term $t$ is free for $x$ in a formula $A$ if substituting $t$ for the free occurrences of $x$ in $A$ causes no variable of $t$ to become bound. [/definition] This condition is a syntactic guardrail. It is what allows the quantifier rules to be stated without hidden semantic qualifications. ## Universal Quantifier Rules How should a proof justify a universal statement, and how should it use one? The guiding idea is that $\forall x\,A(x)$ may be proved by proving $A(a)$ for an arbitrary object $a$, while it may be used by instantiating it at any term whose substitution is legitimate. [explanation: Universal Generalization Rule] Universal generalization is an inference rule, not a theorem about a particular mathematical object. In natural deduction, after deriving $A(a)$ with $a$ fresh for all undischarged assumptions, one may infer $\forall x\,A(x)$. The freshness condition expresses that the argument did not depend on any special information about $a$. [/explanation] The side condition is the whole point of the rule. If $a$ occurred in an open assumption, the proof might have used special information about $a$, so the conclusion would no longer be universal. For instance, an open assumption $P(a)$ permits the immediate derivation of $P(a)$, but it cannot justify $\forall x\,P(x)$, because the assumption singles out the object assigned to $a$. The rule also does not say that every variable occurring in the derivation must be new; it only restricts the eigenvariable used for generalisation. This prepares the contrast with existential elimination, where freshness prevents a witness name from escaping rather than preventing generalisation from special data. [explanation: Universal Instantiation Rule] Universal instantiation is the rule for using a universal premise. From $\forall x\,A(x)$ one may infer $A(t/x)$ whenever the term $t$ is free for $x$ in $A$. The side condition prevents variable capture, so the written instance really is the formula obtained by evaluating the universal statement at the proposed term. [/explanation] Universal elimination is often called universal instantiation. In formal natural deduction it is not a meta-level convenience but a rule whose admissibility depends on the substitution condition. The condition is necessary because substituting a term with free variables under a quantifier can change the binding structure of the formula. For example, replacing $x$ by $y$ in $\exists y\,R(x,y)$ without first renaming the bound $y$ gives $\exists y\,R(y,y)$, which is a different claim from the intended instance $\exists z\,R(y,z)$. The rule also does not allow us to infer a universal statement from a single instance; it only moves from all instances to one legitimate instance. This one-way use of a universal premise is what later derivations combine with propositional rules before introducing a new quantifier. [example: Deriving a Universal Consequent] [claim]From $\forall x(P(x)\to Q(x))$ and $\forall x P(x)$, one can derive $\forall x Q(x)$.[/claim] [proof]Let $a$ be a fresh variable. The open assumptions are \begin{align*} 1.\quad &\forall x(P(x)\to Q(x)),\\ 2.\quad &\forall x P(x). \end{align*} Since the term $a$ is free for $x$ in $P(x)\to Q(x)$, universal elimination applied to line $1$ yields \begin{align*} 3.\quad P(a)\to Q(a). \end{align*} Since $a$ is also free for $x$ in $P(x)$, universal elimination applied to line $2$ yields \begin{align*} 4.\quad P(a). \end{align*} Applying implication elimination to lines $3$ and $4$ gives \begin{align*} 5.\quad Q(a). \end{align*} The variable $a$ was chosen fresh, so it is not free in either undischarged assumption $\forall x(P(x)\to Q(x))$ or $\forall x P(x)$. Therefore universal introduction applied to line $5$ gives \begin{align*} 6.\quad \forall x Q(x). \end{align*} [/proof] The derivation shows the standard pattern: instantiate both universal premises at the same arbitrary variable, use propositional reasoning on the instances, and then generalise because the variable was not tied to any open assumption. [/example] The worked derivation used universal elimination in its most common informal form: choose a term and substitute it into the matrix of the quantified formula. To make that shortcut legitimate inside formal derivations, we need an admissibility statement that records exactly when substitution is allowed and confirms that the shorthand can always be expanded back into primitive rules. [explanation: Admissible Universal Instantiation] The common proof phrase "instantiate the universal premise at $t$" is an admissible shorthand for the primitive universal elimination rule, provided $t$ is free for the quantified variable. It adds no logical strength; it only packages a routine formal step in a readable way. [/explanation] The admissible rule is useful when writing proofs linearly. It lets us say "instantiate the universal premise at $t$" while remembering that the formal derivation contains a universal elimination step. Its hypotheses are exactly those of the primitive elimination rule, so it adds no new logical strength. If the term is not free for the quantified variable, the shortcut is unavailable for the same reason as before: the written instance would not be the matrix evaluated at the denotation of the term. This distinction matters when a proof alternates between informal proof prose and formal derivation trees, because every informal instantiation must still correspond to a valid formal substitution. ## Existential Quantifier Rules How should a proof introduce an existential statement, and how should it reason from one? To prove $\exists x\,A(x)$ it suffices to exhibit a term $t$ satisfying $A(t)$. To use $\exists x\,A(x)$, however, we may not choose a specific known object; we may only reason from a fresh temporary witness. [explanation: Existential Introduction Rule] Existential introduction is an inference rule. Once a derivation has produced an instance $A(t/x)$ with $t$ free for $x$ in $A$, it may infer $\exists x\,A(x)$. The rule hides the particular witness term and records only that some witness exists. [/explanation] Existential introduction is the rule that turns a found instance into a witness claim. The substitution condition is necessary here for the same reason as in universal elimination: the formula used as the instance must really be the matrix evaluated at the proposed witness. The rule does not identify the witness uniquely, and it does not license recovering the term $t$ from the existential formula later. It only records that at least one object satisfies the matrix. In practice it is often paired with conjunction elimination, equality substitution, or universal elimination to manufacture the instance before hiding the particular witness behind $\exists$. [example: Extracting an Existential Consequent] [claim]From $\exists x(P(x)\wedge Q(x))$, one can derive $\exists x\,Q(x)$.[/claim] [proof]Let the original premise be \begin{align*} 1.\quad &\exists x(P(x)\wedge Q(x)). \end{align*} To use existential elimination, introduce a temporary witness assumption with a fresh variable $a$: \begin{align*} 2.\quad &P(a)\wedge Q(a). \end{align*} From line $2$, conjunction elimination on the right conjunct yields \begin{align*} 3.\quad &Q(a). \end{align*} The term $a$ is free for $x$ in $Q(x)$, since substituting $a$ for $x$ in $Q(x)$ places $a$ under no quantifier. Therefore existential introduction applied to line $3$ gives \begin{align*} 4.\quad &\exists x\,Q(x). \end{align*} The formula $\exists x\,Q(x)$ has no free occurrence of $a$, and $a$ was chosen fresh for the original premise. Hence existential elimination applied to line $1$ and the subderivation from line $2$ to line $4$ discharges the temporary assumption $P(a)\wedge Q(a)$ and yields \begin{align*} 5.\quad &\exists x\,Q(x). \end{align*} [/proof] The proof extracts the $Q$-part inside the temporary witness branch and then hides the witness again, so no particular object is exported from the existential premise. [/example] The example illustrates why existential reasoning has a stricter discipline than universal instantiation. A temporary witness may be used inside a subderivation, but the final conclusion must not depend on the particular name chosen for that witness; otherwise the proof would turn mere existence into information about a specific object. [explanation: Existential Elimination Rule] Existential elimination is the rule for reasoning from an existential premise without naming a permanent witness. From $\exists x\,A(x)$, open a temporary branch with $A(a)$ for a fresh variable $a$. If that branch derives a conclusion $C$ in which $a$ is not free, and $a$ is absent from the other undischarged assumptions, then the branch may be closed and $C$ follows. [/explanation] Existential elimination is the first rule where the difference between a fresh placeholder and a named constant becomes essential. A temporary witness is not a new constant of the theory; it is a local name whose scope ends when the existential elimination is closed. The hypothesis that $a$ is absent from $C$ is necessary: from $\exists x\,P(x)$ we may reason under a temporary assumption $P(a)$, but concluding $P(a)$ would make the arbitrary witness name escape the subderivation. The restriction on other undischarged assumptions is equally important, since an open assumption mentioning $a$ could smuggle in extra information about the chosen witness. Thus the rule permits reasoning from existence only when the final result is independent of which witness was selected. [explanation: Admissible Existential Reasoning] The informal phrase "let $a$ be such that $A(a)$" is safe only under the eigenvariable restrictions of existential elimination. The final conclusion and all remaining open assumptions must not depend on the witness name $a$; otherwise the proof has let a temporary placeholder escape its scope. [/explanation] This admissible pattern is the formal version of the common phrase "let $a$ be such that $A(a)$". The phrase is safe only when the conclusion and remaining open assumptions do not depend on the particular name $a$. It is not a rule for choosing a distinguished element of the structure, and it does not produce a definable witness. If the intended conclusion still contains $a$ free, the argument has proved only something about the temporary branch, not something following from the existential premise alone. This is why existential reasoning often aims first at a witness-free conclusion such as another existential statement, a disjunction, or a contradiction. ## Eigenvariables and Quantifier Mistakes Which variable names in a proof carry information, and which are temporary placeholders? An eigenvariable is a variable introduced by a quantifier rule under a freshness condition. It represents arbitrary choice in universal introduction and unspecified witness choice in existential elimination. [definition: Eigenvariable] An eigenvariable is a fresh variable introduced in an application of universal introduction or existential elimination, subject to the rule's side condition that it is not free in specified open assumptions or conclusions. [/definition] The same syntactic condition has two different readings. For $\forall$-introduction, freshness prevents generalising from a special object. For $\exists$-elimination, freshness prevents a witness name from escaping its local scope. [example: Invalid Universal Generalisation] Assume $P(a)$ is an undischarged hypothesis. The only immediate derivation available from this hypothesis is the reiteration of that same formula: \begin{align*} 1.\quad &P(a) &&\text{undischarged assumption},\\ 2.\quad &P(a) &&\text{from line }1. \end{align*} Universal introduction cannot be applied to line $2$ to infer $\forall x\,P(x)$, because the variable $a$ occurs free in the undischarged assumption on line $1$. The failure is semantic, not merely notational. Let the domain be $\{0,1\}$, assign $a$ to $0$, and interpret $P$ by \begin{align*} P(0)&=\text{true},\\ P(1)&=\text{false}. \end{align*} Then the open assumption $P(a)$ is true, since $a$ denotes $0$, but \begin{align*} \forall x\,P(x) \end{align*} is false, since the element $1$ does not satisfy $P$. Thus the invalid generalisation would turn information about one assigned object into a statement about every object. [/example] The previous example fixes one test case for the idea. The next example, Invalid Existential Witness Escape, changes the setting so the same mechanism can be recognized from another angle. [example: Invalid Existential Witness Escape] From $\exists x\,P(x)$, it is invalid to infer $P(a)$ for a fixed variable $a$. Existential elimination permits a temporary witness assumption \begin{align*} P(a) \end{align*} only inside a subderivation whose final conclusion $C$ has no free occurrence of $a$. If we try to use that temporary assumption to conclude $P(a)$ itself, then $C=P(a)$, and \begin{align*} FV(P(a))=\{a\}. \end{align*} Thus $a$ is free in the proposed conclusion, so the eigenvariable side condition for existential elimination is not met. The mistake is also visible semantically. Let the domain be $\{0,1\}$, assign $a$ to $0$, and interpret $P$ by \begin{align*} P(0)&=\text{false},\\ P(1)&=\text{true}. \end{align*} Then \begin{align*} \exists x\,P(x) \end{align*} is true, because the element $1$ satisfies $P$, but \begin{align*} P(a) \end{align*} is false, because $a$ denotes $0$ and $P(0)$ is false. So the existential premise guarantees that some object satisfies $P$, but it does not justify assigning that property to the particular variable $a$. [/example] A related mistake is to instantiate a universal formula with a term that is not free for substitution. This is not a harmless typographical issue, because it changes which variables are bound. [example: Bad Substitution Under a Quantifier] From the premise \begin{align*} \forall x\,\exists y\,R(x,y), \end{align*} universal elimination would require a capture-free instance of the matrix $\exists y\,R(x,y)$. If we try to substitute the term $y$ for the free occurrence of $x$ without first changing the bound variable, the syntactic replacement proceeds as \begin{align*} (\exists y\,R(x,y))[y/x] &=\exists y\,\bigl(R(x,y)[y/x]\bigr)\\ &=\exists y\,R(y,y). \end{align*} The inserted $y$ is now inside the scope of the quantifier $\exists y$, so the variable that was free in the term $y$ has become bound. The resulting formula $\exists y\,R(y,y)$ says that some object is related to itself, not that the object denoted by the free variable $y$ is related to some object. To form the intended instance, first alpha-convert the bound variable in the matrix to a fresh variable $z$: \begin{align*} \exists y\,R(x,y) &\equiv \exists z\,R(x,z). \end{align*} Now substituting $y$ for $x$ is capture-free, because the inserted $y$ is not placed under any quantifier binding $y$: \begin{align*} (\exists z\,R(x,z))[y/x] &=\exists z\,\bigl(R(x,z)[y/x]\bigr)\\ &=\exists z\,R(y,z). \end{align*} Thus the legitimate instance of $\forall x\,\exists y\,R(x,y)$ at the term $y$ is $\exists z\,R(y,z)$, not $\exists y\,R(y,y)$. [/example] The substitution restrictions are not cosmetic syntax rules; they are what make the quantifier rules preserve truth under every interpretation. After seeing how capture can change the meaning of an instance, the natural question is whether the full natural deduction system remains semantically sound when the freshness and freeness side conditions are enforced. [quotetheorem:1485] [citeproof:1485] Soundness explains why the side conditions are part of the rules rather than optional bookkeeping. Without them, the induction step for the quantifier rules would fail: universal introduction would no longer be invariant under changing the eigenvariable assignment, and existential elimination would allow a witness name to appear in the final conclusion. The theorem also states only one direction, namely that derivability implies semantic validity; it does not assert that every semantically valid first-order formula has a derivation. That converse is completeness, a separate model-theoretic theorem. The present result is enough for the proof theory of this chapter because it guarantees that every permitted derivation rule preserves truth in every structure. ## Worked Derivation Patterns How do the quantifier rules look when combined with the propositional rules from earlier chapters? The two worked examples above give the basic patterns. In the universal case, instantiate all relevant universal premises at the same fresh variable, perform the propositional argument on the instances, and then generalise only if the variable is absent from the remaining open assumptions. In the existential case, open a temporary witness branch, do the local propositional work there, and close the branch only with a conclusion that no longer mentions the witness name. These patterns are reusable because they describe proof movement rather than the specific predicates $P$ and $Q$. The next explanation collects them as a strategy for first-order derivations, so the chapter can move from individual examples to proof planning. [explanation: Strategy for First-Order Derivations] When the goal is universal, begin a subderivation with a fresh variable and aim to prove the matrix for that variable. When a universal premise is available, instantiate it at the term or variable needed by the current branch of the proof. When the goal is existential, look for an available instance that can be turned into a witness. When an existential premise is available, open a temporary witness subderivation and ensure that the final conclusion does not mention the witness variable free. These strategies are syntactic reflections of the semantic meanings of the quantifiers. Universal statements demand uniform arguments; existential statements provide local witnesses that cannot be exported as named objects. The discipline of eigenvariables is what keeps these two forms of reasoning separate. [/explanation] With quantifiers in place, the rules of proof must distinguish uniform arguments from existential choices. Chapter 6 reorganizes that material into sequent calculus, where formulas move across the turnstile and structural rules make the flow of information explicit. # 6. Sequent Calculus Sequent calculus reorganises proofs around the movement of formulas across a turnstile. After Chapters 2-5 treated natural deduction through introduction, elimination, discharge, and quantifier side conditions, sequent calculus asks how a whole assertion of consequence can be decomposed into smaller assertions of consequence. This chapter introduces sequents, the Gentzen systems LJ and LK, and the structural rules that control how assumptions may be copied, discarded, reordered, or cut through a derivation. ## What Does a Sequent Assert? The first question is how to represent a local proof obligation. In natural deduction we usually keep a list of open assumptions and a target formula, but many proof transformations become more transparent when the target and the assumptions are displayed together. [definition: Sequent] A sequent is an expression \begin{align*} \Gamma \Rightarrow \Delta, \end{align*} where $\Gamma$ and $\Delta$ are finite lists, finite multisets, or finite sets of formulas, depending on the chosen presentation of the calculus. [/definition] In this course we read $\Gamma \Rightarrow \Delta$ as saying that the formulas on the right are derivable from the formulas on the left. In a single-conclusion system, $\Delta$ contains at most one formula. In a multiple-conclusion system, $\Delta$ may contain several formulas and has the classical reading that the conjunction of the formulas in $\Gamma$ entails the disjunction of the formulas in $\Delta$. [example: Reading Sequents] The sequent $A, A \to B \Rightarrow B$ reads as the proof obligation: with $A$ and $A \to B$ available on the left, derive $B$ on the right. The implication-left step makes the two required uses explicit: first show the antecedent $A$, and then show the desired conclusion $B$ assuming the consequent $B$ of the implication. \begin{align*} \frac{ A \Rightarrow A \qquad B \Rightarrow B }{ A, A \to B \Rightarrow B }(\to L). \end{align*} The two premises are initial sequents, so the derivation says exactly what implication elimination says in natural deduction: from $A$ and $A \to B$, use the implication on the left to replace the goal by the already available formula $B$. [/example] The turnstile separates two kinds of behaviour. A formula on the right is something we are trying to prove; a formula on the left is a resource, assumption, or available hypothesis used in the proof. [definition: Initial Sequent] An initial sequent is a sequent of the form \begin{align*} A \Rightarrow A. \end{align*} [/definition] Initial sequents are the leaves of derivation trees. They express that a formula proves itself when it is already available as an assumption. ## Why Do Connective Rules Come in Left and Right Forms? The second question is how logical connectives should be decomposed. In natural deduction each connective has introduction and elimination rules. In sequent calculus the corresponding distinction is between rules that introduce a connective on the right of $\Rightarrow$ and rules that introduce a connective on the left. [definition: Right Rule] A right rule for a connective is an inference rule whose conclusion has a principal formula containing that connective in the succedent. [/definition] A right rule explains what must be proved in order to prove a formula with that connective as its main connective. For instance, to prove $A \wedge B$ on the right, one must prove both $A$ and $B$ on the right. [definition: Left Rule] A left rule for a connective is an inference rule whose conclusion has a principal formula containing that connective in the antecedent. [/definition] A left rule explains how an assumption with that connective may be used. For instance, an assumption $A \wedge B$ on the left may be replaced by the two assumptions $A$ and $B$. [example: Conjunction Rules] For conjunction, the right rule and left rule may be written as \begin{align*} \frac{\Gamma \Rightarrow A \qquad \Gamma \Rightarrow B}{\Gamma \Rightarrow A \wedge B}(\wedge R), \qquad \frac{\Gamma, A, B \Rightarrow C}{\Gamma, A \wedge B \Rightarrow C}(\wedge L). \end{align*} The right rule has two premises because proving $A \wedge B$ requires proving both conjuncts: the first premise supplies $A$ from $\Gamma$, and the second premise supplies $B$ from the same context $\Gamma$. Thus the conclusion records both obligations at once: \begin{align*} \Gamma \Rightarrow A \quad\text{and}\quad \Gamma \Rightarrow B \quad\leadsto\quad \Gamma \Rightarrow A \wedge B. \end{align*} The left rule is read in the opposite direction during proof search: if the goal is $\Gamma, A \wedge B \Rightarrow C$, then using the assumption $A \wedge B$ amounts to replacing it by its two available components $A$ and $B$, giving the premise \begin{align*} \Gamma, A, B \Rightarrow C. \end{align*} So $\wedge R$ explains how to establish a conjunction as a conclusion, while $\wedge L$ explains how a conjunction on the left may be used as two separate assumptions. [/example] The example also points to a boundary of the idea. The following remark, Invertibility Intuition, records that interpretation before the construction is used again. [remark: Invertibility Intuition] Many sequent rules are designed so that proof search can proceed by reading them upwards from a goal sequent to simpler premises. Right rules analyse the desired conclusion, while left rules analyse the available hypotheses. [/remark] ## How Do LJ and LK Encode Intuitionistic and Classical Logic? The next question is where the difference between intuitionistic and classical reasoning enters. Gentzen's systems separate this issue from the connective rules: the main difference is the allowed shape of the succedent. [definition: Gentzen System LJ] The system LJ is the sequent calculus for intuitionistic logic in which every sequent has at most one formula in the succedent. [/definition] The single-conclusion restriction matches the constructive reading of proofs: a derivation of $\Gamma \Rightarrow A$ gives a proof of the particular formula $A$ from assumptions $\Gamma$. Classical reasoning needs a sequent format that can represent alternatives without choosing one constructively. Instead of forcing the right-hand side to name a single proved formula, the classical calculus allows a context of possible conclusions. That change is the structural place where excluded-middle behavior enters the sequent calculus. [definition: Gentzen System LK] The system LK is the sequent calculus for classical logic in which sequents may have multiple formulas in the succedent. [/definition] Multiple conclusions encode classical alternatives. The sequent $\Gamma \Rightarrow A, B$ may be read as saying that from $\Gamma$ we can derive $A \vee B$ in a classical sense, even when the proof does not construct a distinguished disjunct. [example: Classical Shape of Excluded Middle] In LK, the sequent $\Rightarrow A, \neg A$ has empty antecedent and two formulas in the succedent. Under the multiple-conclusion reading, the antecedent is read as the conjunction of no assumptions and the succedent is read as a disjunction of alternatives: \begin{align*} \Rightarrow A, \neg A \quad\text{means}\quad \top \Rightarrow A \vee \neg A. \end{align*} Since $\top$ contributes no hypothesis, this says that the classical alternative $A \vee \neg A$ is valid without assumptions. Thus the two formulas on the right do not record two separate constructed proofs; they record the single classical assertion that one of the alternatives $A$ or $\neg A$ holds. In LJ the same sequent shape is not legal, because LJ permits at most one formula in the succedent. So LK can represent excluded middle directly as $\Rightarrow A, \neg A$, while LJ would have to ask instead for a single-conclusion sequent such as $\Rightarrow A \vee \neg A$, which is not derivable intuitionistically for an arbitrary formula $A$. [/example] Natural deduction and sequent calculus organize proofs differently: natural deduction emphasizes introduction and elimination of connectives, while sequents expose assumptions and conclusions as explicit contexts. This raises a comparison problem: the sequent calculi should be different proof formalisms for the same logics, not new logics with different theorems. Before using sequents as a proof-theoretic tool, we must know that this change of format preserves the underlying notion of provability for the corresponding classical or intuitionistic system. [quotetheorem:4642] [citeproof:4642] This equivalence says that sequent calculus does not change which propositional formulas are provable once the intended system and translation conventions have been fixed. The single-conclusion hypothesis matters: without it, LK can express classically valid alternatives such as $\Rightarrow A, \neg A$, while LJ cannot represent that same proof obligation as a derivation of a distinguished formula. Conversely, translating an LK succedent as a disjunction is not a statement that the derivation has chosen one disjunct constructively; it records a classical alternative. The theorem therefore compares provability, not proof shape, and the next structural results ask how much of that provability remains when rules such as cut are restricted or removed. ## Which Structural Rules Govern Contexts? The connective rules analyse logical form, but proof systems also need rules for the contexts themselves. The central question is whether assumptions may be ignored, duplicated, reordered, or replaced by intermediate lemmas. [definition: Weakening] Weakening is the structural rule that permits adding formulas to a context: \begin{align*} \frac{\Gamma \Rightarrow \Delta}{\Gamma, A \Rightarrow \Delta}(WL), \qquad \frac{\Gamma \Rightarrow \Delta}{\Gamma \Rightarrow \Delta, A}(WR). \end{align*} [/definition] Weakening expresses monotonicity of consequence: adding more assumptions cannot destroy a derivation, and in a multiple-conclusion calculus adding more possible conclusions cannot destroy a derivation. A different context question concerns multiplicity. If the same formula appears twice, ordinary classical and intuitionistic consequence do not treat the two copies as two consumable resources. The contraction rule records this idempotence of contexts by allowing duplicate occurrences to be collapsed. [definition: Contraction] Contraction is the structural rule that permits replacing duplicate occurrences by a single occurrence: \begin{align*} \frac{\Gamma, A, A \Rightarrow \Delta}{\Gamma, A \Rightarrow \Delta}(CL), \qquad \frac{\Gamma \Rightarrow \Delta, A, A}{\Gamma \Rightarrow \Delta, A}(CR). \end{align*} [/definition] Contraction is the rule that allows assumptions and conclusions to be used without tracking exact multiplicity. Substructural logics modify or remove contraction when multiplicity is intended to matter. Multiplicity is only one way in which a context can carry structure. If contexts are written as ordered lists, then the same formulas in a different order may count as a different sequent unless the calculus explicitly permits reordering. To separate logical inference from bookkeeping about order, the calculus needs an explicit rule saying when the order of assumptions and conclusions may be ignored. Exchange names exactly that permission. [definition: Exchange] Exchange is the structural rule that permits reordering formulas in the antecedent or succedent of a sequent. [/definition] Exchange is often omitted when contexts are treated as sets or multisets. When contexts are treated as lists, exchange must be stated as a rule or proved admissible from the chosen list conventions. Formal proofs often proceed by proving an intermediate assertion and then using it inside a larger argument. A sequent calculus needs a rule that records this lemma-use explicitly, because the intermediate formula may disappear from the final conclusion even though the proof passed through it. The key obstruction is that such a rule can hide non-analytic reasoning: the intermediate formula need not be a subformula of the final sequent. Naming the rule sets up the later question of whether every proof can be transformed so that this hidden intermediate step is unnecessary. [definition: Cut] In a single-conclusion calculus, cut is the structural rule \begin{align*} \frac{\Gamma \Rightarrow A \qquad \Sigma, A \Rightarrow \Delta}{\Gamma, \Sigma \Rightarrow \Delta}(Cut). \end{align*} In a multiple-conclusion calculus such as LK, cut is the structural rule \begin{align*} \frac{\Gamma \Rightarrow \Delta, A \qquad \Sigma, A \Rightarrow \Pi}{\Gamma, \Sigma \Rightarrow \Delta, \Pi}(Cut). \end{align*} [/definition] Cut formalises the use of an intermediate lemma $A$. First prove $A$ from $\Gamma$, possibly among other classical alternatives in LK, then continue a derivation that uses $A$ together with $\Sigma$. [example: Cut as Lemma Use] Let $\mathcal D_1$ be a derivation of $\Gamma \Rightarrow A \to B$ and let $\mathcal D_2$ be a derivation of $\Sigma \Rightarrow A$. To use the proved implication as a lemma, first combine $\mathcal D_2$ with the initial sequent $B \Rightarrow B$ by implication-left: \begin{align*} \frac{ \mathcal D_2:\Sigma \Rightarrow A \qquad B \Rightarrow B }{ \Sigma, A \to B \Rightarrow B }(\to L). \end{align*} This sequent says that, once $A \to B$ is available on the left and $A$ has been obtained from $\Sigma$, the conclusion $B$ is available. Now cut in the already proved lemma $\mathcal D_1:\Gamma \Rightarrow A \to B$: \begin{align*} \frac{ \mathcal D_1:\Gamma \Rightarrow A \to B \qquad \frac{ \mathcal D_2:\Sigma \Rightarrow A \qquad B \Rightarrow B }{ \Sigma, A \to B \Rightarrow B }(\to L) }{ \Gamma, \Sigma \Rightarrow B }(Cut). \end{align*} If a later derivation uses $B$, say $\mathcal E:\Pi, B \Rightarrow \Delta$, then one more cut substitutes the derived $B$ into that later argument: \begin{align*} \frac{ \frac{ \mathcal D_1:\Gamma \Rightarrow A \to B \qquad \frac{ \mathcal D_2:\Sigma \Rightarrow A \qquad B \Rightarrow B }{ \Sigma, A \to B \Rightarrow B }(\to L) }{ \Gamma, \Sigma \Rightarrow B }(Cut) \qquad \mathcal E:\Pi, B \Rightarrow \Delta }{ \Gamma, \Sigma, \Pi \Rightarrow \Delta }(Cut). \end{align*} Thus cut is the formal sequent-calculus step that replaces an invocation of an intermediate lemma by a derivation of the formula that the later proof needs. [/example] The example isolates cut as lemma use, but the surrounding calculus also depends on how freely contexts may be managed. Before studying the harder problem of eliminating cut, it is useful to know which structural operations are merely admissible conveniences in the standard systems. Structural rules determine whether contexts behave like ordinary finite collections of assumptions. If weakening, contraction, and exchange are admissible, then adding unused hypotheses, reusing an assumption, or reordering a context can be treated as harmless proof management rather than as extra logical content. The point is to know when these operations must be primitive rules and when they can be recovered from the logical rules already present. The following result supplies that baseline for the standard sequent calculi before cut is treated as the genuinely difficult structural rule. [quotetheorem:4643] [citeproof:4643] Admissibility is weaker than being primitive: it says that any derivation using the operation can be transformed into one without using it as a rule. The hypotheses matter because this is a theorem about the standard LJ and LK presentations; in substructural calculi such as linear logic, weakening or contraction may fail precisely because unused or duplicated assumptions are meant to carry information. A boundary case is a calculus with ordered contexts and no exchange rule: the sequents $A,B \Rightarrow C$ and $B,A \Rightarrow C$ need not have the same derivations unless exchange is built in or proved admissible from the rules. This result therefore justifies flexible context notation for the ordinary propositional systems, but it does not license the same flexibility in every sequent calculus. The cut elimination theorem in Chapter 7 is stronger and more delicate because cut is not merely a notational convenience: it changes the way a proof can pass through intermediate formulas. ## How Are Sequent Proofs Built in Practice? The last step in this chapter is to see the calculus at work. The most useful habit is to build derivations from the desired end sequent upward: decompose the main connective of a goal on the right, or decompose an available compound assumption on the left. [example: Commutativity of Conjunction] We derive $A \wedge B \Rightarrow B \wedge A$. To prove a conjunction on the right, it is enough to prove each conjunct on the right from the same antecedent, so the two required sequents are $A \wedge B \Rightarrow B$ and $A \wedge B \Rightarrow A$. For the first conjunct, start with the initial sequent $B \Rightarrow B$, add the unused assumption $A$ on the left by weakening, and then use $\wedge L$ to package the two left assumptions as $A \wedge B$: \begin{align*} \frac{ \frac{B \Rightarrow B}{A, B \Rightarrow B}(WL) }{ A \wedge B \Rightarrow B }(\wedge L). \end{align*} For the second conjunct, start with the initial sequent $A \Rightarrow A$, add the unused assumption $B$ on the left by weakening, and again use $\wedge L$: \begin{align*} \frac{ \frac{A \Rightarrow A}{A, B \Rightarrow A}(WL) }{ A \wedge B \Rightarrow A }(\wedge L). \end{align*} Combining these two derivations by $\wedge R$ gives the full derivation \begin{align*} \frac{ \frac{ \frac{B \Rightarrow B}{A, B \Rightarrow B}(WL) }{ A \wedge B \Rightarrow B }(\wedge L) \qquad \frac{ \frac{A \Rightarrow A}{A, B \Rightarrow A}(WL) }{ A \wedge B \Rightarrow A }(\wedge L) }{ A \wedge B \Rightarrow B \wedge A }(\wedge R). \end{align*} Thus the assumption $A \wedge B$ is used twice, once to obtain $B$ and once to obtain $A$, and the right rule then assembles those two conclusions into $B \wedge A$. [/example] This example mirrors the natural deduction proof of $A \wedge B \to B \wedge A$, but the sequent proof makes every use of the assumption visible as a left-rule step. [example: Transitivity of Implication] We derive $A \to B, B \to C \Rightarrow A \to C$ by first proving the premise required by $\to R$, namely $A \to B, B \to C, A \Rightarrow C$. The inner implication $A \to B$ gives $B$ from the available $A$: start with the initial sequents $A \Rightarrow A$ and $B \Rightarrow B$, weaken the second by adding the unused assumption $A$, and apply $\to L$: \begin{align*} \frac{ A \Rightarrow A \qquad \frac{B \Rightarrow B}{A, B \Rightarrow B}(WL) }{ A, A \to B \Rightarrow B }(\to L). \end{align*} By exchange, this is the same context as \begin{align*} A \to B, A \Rightarrow B. \end{align*} Now use $B \to C$ on the left. Its first premise is the sequent just derived, and its second premise says that once $C$ has been obtained, the goal $C$ follows; the extra assumptions $A$ and $A \to B$ are added by weakening: \begin{align*} \frac{ \frac{ A \Rightarrow A \qquad \frac{B \Rightarrow B}{A, B \Rightarrow B}(WL) }{ A, A \to B \Rightarrow B }(\to L) \qquad \frac{ \frac{C \Rightarrow C}{A, C \Rightarrow C}(WL) }{ A \to B, A, C \Rightarrow C }(WL) }{ A \to B, A, B \to C \Rightarrow C }(\to L). \end{align*} Exchanging the last two assumptions gives $A \to B, B \to C, A \Rightarrow C$, so $\to R$ discharges the temporary assumption $A$: \begin{align*} \frac{ A \to B, B \to C, A \Rightarrow C }{ A \to B, B \to C \Rightarrow A \to C }(\to R). \end{align*} Thus the sequent proof records the two-stage composition: $A$ and $A \to B$ yield $B$, then $B$ and $B \to C$ yield $C$, so from $A$ we obtain $C$. [/example] The proof search pattern in the second example is the sequent version of chaining two functions: from $A$ and $A \to B$ we obtain $B$, and from $B$ and $B \to C$ we obtain $C$. The calculus records each stage as a local sequent transformation rather than as a linear prose argument. [remark: Proof Search and Cut] Cut is useful for writing human proofs because it permits intermediate claims. Cut-free proof search is more disciplined: it decomposes only formulas already present in the goal sequent. The cut elimination theorem studied later says that, for Gentzen systems, this discipline does not reduce what can ultimately be proved. [/remark] Sequent calculus therefore gives a second presentation of the same propositional logics while making structural behaviour explicit. The next chapter uses this explicit structure to formulate cut elimination and to analyse why proofs with intermediate lemmas can be transformed into proofs that only decompose the formulas appearing in the final sequent. Chapter 6 makes the internal structure of proofs visible at the level of sequents. Chapter 7 uses that structure to study cut elimination, showing how proofs with intermediate lemmas can be transformed into proofs that decompose only the formulas in the final sequent. # 7. Cut Elimination This chapter assumes the sequent calculi LJ and LK from Chapter 6, the structural rules, and the analogy from Chapter 3 between natural-deduction detours and sequent-calculus cuts. The goals are to state the cut rule precisely, explain the local reductions that remove it, and extract the metatheoretic consequences: subformula property, consistency, and propositional decidability. Cut elimination is the structural theorem saying that proofs which use intermediate lemmas can be transformed into proofs which do not. In the previous chapters, normalization removed detours from natural deduction; cut elimination is the corresponding theorem for sequent calculus. The central question is how a derivation using a formula $C$ as a temporary bridge can be reorganized so that the proof of $C$ and the use of $C$ are fused away. The payoff is substantial: once cuts are eliminated, every formula appearing in a proof is controlled by the end-sequent, giving consistency, the subformula property, and decision procedures for propositional fragments. ## The Cut Rule as an Intermediate Lemma How should sequent calculus express the ordinary mathematical act of proving a lemma and then using it? A derivation may first establish a formula $C$, then continue under the assumption that $C$ is available. The cut rule says that this intermediate formula may be passed from the right side of one sequent to the left side of another. [definition: Cut Rule] In LK, the cut rule is the inference \begin{align*} \frac{\Gamma \Rightarrow \Delta, C \qquad C, \Pi \Rightarrow \Lambda}{\Gamma, \Pi \Rightarrow \Delta, \Lambda}\,\mathrm{Cut}. \end{align*} In LJ, where the succedent contains at most one formula, the corresponding form is \begin{align*} \frac{\Gamma \Rightarrow C \qquad C, \Pi \Rightarrow D}{\Gamma, \Pi \Rightarrow D}\,\mathrm{Cut}. \end{align*} The formula $C$ is called the cut formula. [/definition] The left premise is a derivation of the lemma $C$, possibly alongside other alternatives in the classical succedent. The right premise is a derivation in which $C$ is available as an extra assumption. The conclusion removes $C$ from view, just as ordinary prose suppresses a lemma after it has been used. [example: Modus Ponens as Cut] Work in LJ, and suppose we are given derivations \begin{align*} \mathcal D_1 &: \Gamma \Rightarrow A,\\ \mathcal D_2 &: \Pi \Rightarrow A \to B. \end{align*} From the initial sequents $A \Rightarrow A$ and $B \Rightarrow B$, the implication-left rule gives \begin{align*} \frac{A \Rightarrow A \qquad B \Rightarrow B}{A \to B, A \Rightarrow B}\,\to L. \end{align*} Now cut $\mathcal D_2$ against this sequent, using $A \to B$ as the cut formula: \begin{align*} \frac{\Pi \Rightarrow A \to B \qquad A \to B, A \Rightarrow B} {\Pi, A \Rightarrow B}\,\mathrm{Cut}. \end{align*} The formula $A \to B$ has disappeared from the conclusion, but the antecedent $A$ remains. Cutting $\mathcal D_1$ against that remaining antecedent, with $A$ as the cut formula, gives \begin{align*} \frac{\Gamma \Rightarrow A \qquad \Pi, A \Rightarrow B} {\Gamma,\Pi \Rightarrow B}\,\mathrm{Cut}. \end{align*} Thus the sequent-calculus form of modus ponens is a two-step use of cut: first the proved implication $A \to B$ is used, and then the proved antecedent $A$ is substituted into the open assumption left by $\to L$. [/example] This example is the sequent-calculus version of applying a proved antecedent to an implication. The obstruction is that the derivation has introduced intermediate formulas, such as $A\to B$ and then $A$, that need not be visible in the final sequent. Those formulas make the proof depend on lemmas whose shape is not controlled by the conclusion. Cut elimination asserts that this detour through intermediate formulas can always be removed, although the resulting derivation may be longer and more intricate. To state that removal precisely, the proof system needs a syntactic class of derivations in which no such intermediate-lemma step occurs. [definition: Cut-Free Derivation] A derivation in LK or LJ is cut-free if no inference in the derivation is an instance of the cut rule. [/definition] Cut-free proofs are syntactically constrained in a way arbitrary proofs are not. The logical rules introduce or decompose the connectives already visible in the conclusion, while cut may introduce a formula unrelated to the final sequent. [remark: Lemmas and Proof Length] Cut elimination does not say that intermediate lemmas are bad mathematical practice. Lemmas compress proofs and reveal structure. The theorem says that, as far as derivability is concerned, their use is eliminable from the formal derivation. [/remark] ## Principal and Non-Principal Cut Reductions What local transformation removes a cut without changing the end-sequent? The answer depends on how the cut formula occurs in the final inference above each premise. If both premises have just introduced the cut formula, the cut is principal; if the cut formula is merely carried along as context in at least one premise, the cut is non-principal. [definition: Principal Cut] A cut is principal if the cut formula is the principal formula of the last inference in both cut premises. [/definition] A cut can fail to be principal because the cut formula is merely being transported through one of the premises rather than introduced by the last inference there. This is the obstruction handled by commuting the cut upward past that unrelated inference. [definition: Non-Principal Cut] A cut is non-principal if the cut formula is not the principal formula of the last inference in at least one cut premise. [/definition] The distinction is the engine of the proof. Non-principal reductions commute the cut upward past an inference, decreasing the height at which the cut occurs. Principal reductions replace one cut on a compound formula by cuts on its immediate subformulas, decreasing the complexity of the cut formula. [example: Eliminating a Principal Cut on Conjunction] Suppose the left premise of the cut is obtained by $\wedge R$ from derivations of $\Gamma \Rightarrow A$ and $\Gamma \Rightarrow B$, and suppose the right premise is obtained by the first conjunction-left rule from a derivation of $A,\Pi \Rightarrow C$: \begin{align*} \frac{A,\Pi \Rightarrow C}{A \wedge B,\Pi \Rightarrow C}\,\wedge L_1. \end{align*} Then the principal cut on $A \wedge B$ has the form \begin{align*} \frac{ \frac{\Gamma \Rightarrow A \qquad \Gamma \Rightarrow B}{\Gamma \Rightarrow A \wedge B}\,\wedge R \qquad \frac{A,\Pi \Rightarrow C}{A \wedge B,\Pi \Rightarrow C}\,\wedge L_1 }{ \Gamma,\Pi \Rightarrow C }\,\mathrm{Cut}. \end{align*} The reduction removes the introduction of $A \wedge B$ on both sides and cuts only the component actually used by $\wedge L_1$: \begin{align*} \frac{ \Gamma \Rightarrow A \qquad A,\Pi \Rightarrow C }{ \Gamma,\Pi \Rightarrow C }\,\mathrm{Cut}. \end{align*} Both derivations have the same end-sequent $\Gamma,\Pi \Rightarrow C$, but the new cut formula is $A$ instead of $A \wedge B$. Since $A$ is a proper subformula of $A \wedge B$, this principal reduction lowers the cut rank; the unused derivation of $\Gamma \Rightarrow B$ disappears because the chosen left conjunction rule never appeals to the $B$ component. [/example] The previous example fixes one test case for the idea. The next example, Eliminating a Principal Cut on Implication, changes the setting so the same mechanism can be recognized from another angle. [example: Eliminating a Principal Cut on Implication] In LJ, assume the derivation of the left cut premise ends by implication right-introduction: \begin{align*} \frac{A,\Gamma \Rightarrow B}{\Gamma \Rightarrow A \to B}\,\to R. \end{align*} Assume also that the right cut premise ends by implication left-introduction, with one derivation proving the antecedent and the other using the consequent: \begin{align*} \frac{\Pi \Rightarrow A \qquad B,\Sigma \Rightarrow C}{A \to B,\Pi,\Sigma \Rightarrow C}\,\to L. \end{align*} The principal cut on $A \to B$ therefore has the form \begin{align*} \frac{ \frac{A,\Gamma \Rightarrow B}{\Gamma \Rightarrow A \to B}\,\to R \qquad \frac{\Pi \Rightarrow A \qquad B,\Sigma \Rightarrow C}{A \to B,\Pi,\Sigma \Rightarrow C}\,\to L }{ \Gamma,\Pi,\Sigma \Rightarrow C }\,\mathrm{Cut}. \end{align*} The reduction removes the two introductions of $A \to B$ and replaces the one cut on the compound formula by two cuts on its immediate subformulas. First cut the derivation of $\Pi \Rightarrow A$ against the open $A$-assumption in $A,\Gamma \Rightarrow B$: \begin{align*} \frac{ \Pi \Rightarrow A \qquad A,\Gamma \Rightarrow B }{ \Pi,\Gamma \Rightarrow B }\,\mathrm{Cut}. \end{align*} By exchange of antecedent contexts, this is the same sequent as $\Gamma,\Pi \Rightarrow B$. Then cut that result against the derivation that uses $B$: \begin{align*} \frac{ \Gamma,\Pi \Rightarrow B \qquad B,\Sigma \Rightarrow C }{ \Gamma,\Pi,\Sigma \Rightarrow C }\,\mathrm{Cut}. \end{align*} Thus the reduced derivation has the same end-sequent $\Gamma,\Pi,\Sigma \Rightarrow C$, but the cut formula $A \to B$ has been replaced by the smaller cut formulas $A$ and $B$. [/example] These examples show why the proof needs a double induction. Commuting a cut upward may duplicate or rearrange derivations, so height alone is not enough. Reducing a principal cut lowers the formula rank, while reducing a non-principal cut lowers the relevant derivation height without increasing the formula rank. [definition: Cut Rank] The cut rank of an instance of cut is the number of logical connectives and quantifiers occurring in its cut formula. [/definition] The exact numerical convention is not important; what matters is that every proper subformula has smaller rank. For first-order logic, quantifier rules add the usual eigenvariable side conditions, and the reductions must preserve those side conditions by renaming bound variables when needed. The local reductions suggest an elimination procedure, but a theorem is needed to guarantee that the procedure terminates for arbitrary LK derivations. The rank-and-height analysis is what turns those local transformations into a global result. [quotetheorem:4644] [citeproof:4644] The hypotheses are tied to the exact LK rules. If cut is allowed, even the simple sequent $A \Rightarrow A$ can have a derivation mentioning an arbitrary unrelated formula $B$: weaken $A \Rightarrow A$ to put $B$ on the right, weaken another initial sequent to make $B$ usable on the left, cut on $B$, and contract back to the original sequent. The theorem does not say the cut-free proof is shorter or canonical; it only says that some cut-free derivation of the same end-sequent exists. Its forward use is that LK proofs become analytic after cut removal, which is what makes the subformula and consistency arguments possible. [quotetheorem:4645] [citeproof:4645] The single-succedent hypothesis is essential. Classical LK proves sequents such as $\Rightarrow A \vee (A \to \bot)$, while LJ does not, so an LK cut-elimination argument cannot simply be reinterpreted as an intuitionistic one. The theorem does not say that classical principles become intuitionistically valid, nor does it give a polynomial bound on proof size. Its forward role is to connect LJ with normalization: removing cuts is the sequent-calculus counterpart of substituting proofs for discharged assumptions in natural deduction. ## Transforming Proofs Using Intermediate Implications How does cut elimination change a proof that uses an implication as a reusable lemma? Such a proof often has the form: prove $A \to B$, prove $A$, then infer $B$. The cut-free version substitutes the proof of $A$ into the proof of $B$ at the point where the implication had used its temporary assumption. [example: Removing an Intermediate Implication] Suppose the derivation of $\Gamma \Rightarrow A \to B$ ends by implication right-introduction from a derivation \begin{align*} \mathcal D &: A,\Gamma \Rightarrow B, \end{align*} so that \begin{align*} \frac{A,\Gamma \Rightarrow B}{\Gamma \Rightarrow A \to B}\,\to R. \end{align*} Suppose also that \begin{align*} \mathcal E &: \Pi \Rightarrow A. \end{align*} If the proved implication is used by cut, then the cut formula is $A \to B$: \begin{align*} \frac{ \frac{A,\Gamma \Rightarrow B}{\Gamma \Rightarrow A \to B}\,\to R \qquad A \to B,\Pi \Rightarrow B }{ \Gamma,\Pi \Rightarrow B }\,\mathrm{Cut}. \end{align*} The right premise $A \to B,\Pi \Rightarrow B$ is obtained by using the implication-left rule with $\mathcal E$ as the proof of the antecedent and $B \Rightarrow B$ as the initial use of the consequent: \begin{align*} \frac{ \Pi \Rightarrow A \qquad B \Rightarrow B }{ A \to B,\Pi \Rightarrow B }\,\to L. \end{align*} The principal implication reduction removes the introduced formula $A \to B$ from both sides. Instead of first forming $\Gamma \Rightarrow A \to B$ and then using $A \to B$ on the left, cut the proof of $A$ directly against the open $A$-assumption in $\mathcal D$: \begin{align*} \frac{ \Pi \Rightarrow A \qquad A,\Gamma \Rightarrow B }{ \Pi,\Gamma \Rightarrow B }\,\mathrm{Cut}. \end{align*} By exchange of antecedents, $\Pi,\Gamma \Rightarrow B$ is the same sequent as $\Gamma,\Pi \Rightarrow B$. Thus the cut on the compound formula $A \to B$ is replaced by a cut on the smaller formula $A$, so the transformation is exactly the sequent-calculus form of substituting the proof of $A$ into the places where the derivation of $B$ used the temporary assumption $A$. [/example] This is the same conceptual move as beta-reduction in natural deduction: an introduction of implication followed by an elimination of implication is replaced by substitution of the argument proof for the discharged assumption. Sequent calculus expresses the move through cut reductions rather than through proof terms. [remark: Why Cut Elimination Is Not Merely Erasure] Removing cut does not mean deleting the derivation of the cut formula. The content of that derivation is pushed into the places where the formula was used. This is why cut elimination can increase proof length even though it reduces the logical vocabulary of the proof. [/remark] ## Consequences of Cut Elimination What can be read from a proof once all cuts have been removed? The major gain is that every logical inference in a cut-free derivation is tied to the formulas already present in the conclusion. No hidden lemma can introduce an unrelated formula and then disappear. [quotetheorem:4646] [citeproof:4646] The cut-free hypothesis is necessary. With cut present, the sequent $A \Rightarrow A$ can contain a completely unrelated cut formula $B$, which is not a subformula of the end-sequent, before the final contractions restore the original sequent. The theorem does not say that every subformula-built search branch succeeds, and in first-order logic the phrase "up to eigenvariable substitutions" still permits infinitely many term instances. Its forward use is analytic control: proof search and consistency arguments can inspect only the vocabulary forced by the end-sequent. The first place this analytic control pays off is the consistency of the calculus itself. Consistency means that the empty sequent $\Rightarrow$, which expresses the bare contradiction, has no derivation at all. Without cut elimination this is difficult to see, because a derivation could pass through arbitrarily complicated cut formulas before arriving at $\Rightarrow$. Once cuts are removed, however, any purported derivation of $\Rightarrow$ must end in some logical or structural rule, and the subformula property sharply constrains which rule that could be. The next theorem turns this observation into a proof that no derivation of the empty sequent exists. [quotetheorem:4647] [citeproof:4647] The formulation of contradiction as the empty sequent matters. If the calculus were extended by an axiom $\Rightarrow$, then $\Rightarrow$ would have a derivation immediately, so the last-inference argument would fail. The theorem does not prove consistency for arbitrary extensions of LK, nor does it replace semantic soundness when nonlogical axioms are added. Its forward connection is that cut elimination reduces consistency to a finite syntactic inspection of possible last rules. A second payoff is decidability. The question now is whether one can mechanically decide, for a given propositional formula, whether it is provable. The obstruction in the full calculus is again cut: a backward search may have to guess cut formulas of unbounded complexity, so the space of candidate derivations is unbounded. After cut elimination, every formula occurring on a search branch is a subformula of the goal, and in the propositional case there are only finitely many such subformulas. This bounds the search space and makes the following decidability result possible. [quotetheorem:4648] [citeproof:4648] The propositional restriction is essential. In first-order logic, backward quantifier rules can require searching through infinitely many terms, and first-order validity is not decidable in general. The theorem does not say that proof search is efficient; the finite search space may still be exponentially large. Its forward use is methodological: after cut elimination, proof search can be made complete by exploring only the finite closure of propositional subformulas. [example: Analytic Search After Cut Elimination] To search backward for a cut-free LJ proof of $\Rightarrow (A \wedge B) \to A$, inspect the outermost connective of the succedent. Since the target formula is an implication, the backward use of $\to R$ replaces the goal by its premise: \begin{align*} \frac{A \wedge B \Rightarrow A}{\Rightarrow (A \wedge B) \to A}\,\to R. \end{align*} The remaining antecedent has conjunction as its outermost connective. Using the conjunction-left rule backward replaces the assumption $A \wedge B$ by its two components: \begin{align*} \frac{A,B \Rightarrow A}{A \wedge B \Rightarrow A}\,\wedge L. \end{align*} The sequent $A,B \Rightarrow A$ is reached from the initial sequent $A \Rightarrow A$ by one left weakening: \begin{align*} \frac{A \Rightarrow A}{A,B \Rightarrow A}\,\mathrm{Weak}_L. \end{align*} Combining the three displayed steps gives the cut-free derivation \begin{align*} \frac{ \frac{ \frac{A \Rightarrow A}{A,B \Rightarrow A}\,\mathrm{Weak}_L }{ A \wedge B \Rightarrow A }\,\wedge L }{ \Rightarrow (A \wedge B) \to A }\,\to R. \end{align*} Every formula appearing in this derivation is one of \begin{align*} A,\qquad B,\qquad A \wedge B,\qquad (A \wedge B) \to A, \end{align*} so the search uses only subformulas of the end-formula $(A \wedge B) \to A$. [/example] Cut elimination is therefore the bridge between proof transformation and metatheory. It turns sequent calculus from a permissive formalism with lemmas into an analytic system whose derivations can be inspected, searched, and used to establish consistency results. Chapters 10-12 refine this idea in arithmetic, ordinal analysis, and computability: formal theories can code proofs, ordinal measures can prove termination of reductions, and computational interpretations read algorithms from proof structure. Cut elimination clarifies why proof systems are both syntactic and semantic tools: they can be simplified, analysed, and used to prove consistency. Chapter 8 turns back toward semantics and asks whether these proof systems capture all logical consequence, leading to completeness, compactness, and related metatheorems. # 8. Completeness and Compactness from Proof Systems This chapter turns the natural-deduction and sequent-calculus proof systems developed in Chapters 2-7 back toward semantics. The guiding question is whether syntactic derivability captures all semantic consequence: if every structure satisfying a set of assumptions also satisfies a sentence, must there be a formal derivation? The answer for first-order logic is Gödel's completeness theorem, and the proof proceeds by turning consistent syntax into a model. Compactness and the downward Löwenheim-Skolem theorem then appear as consequences of the same proof-theoretic construction. ## Consistency as the Starting Point for Model Building How can a proof system build a model when all it seems to contain is formulas and derivations? The key move is to start with a theory that has no contradiction and enlarge it until it decides every sentence while preserving consistency. Such an enlarged theory behaves like the complete diagram of a possible structure. [definition: Theory] A theory $T$ in a first-order language $L$ is a set of $L$-sentences. [/definition] A theory records assumptions rather than a single formula. In proof-theoretic arguments, $T \vdash \varphi$ means that there is a finite derivation of $\varphi$ from assumptions drawn from $T$. The model-building argument needs to know which sets of assumptions are still viable before any model has been constructed. A set of assumptions that proves both a sentence and its negation has already collapsed, so it cannot be extended into the diagram of a classical structure. We need a condition that is therefore a purely syntactic substitute for possible satisfiability. It lets the completeness proof track exactly which theories may be enlarged without forcing contradiction. [definition: Consistent Theory] A theory $T$ is consistent if there is no sentence $\varphi$ such that $T \vdash \varphi$ and $T \vdash \neg \varphi$. [/definition] For classical first-order logic with falsity, this is equivalent to saying $T \nvdash \bot$. The finite character of derivations is the main structural feature used below: every derivation mentions only finitely many assumptions. [example: A Consistent Diagram Fragment] Let $L$ contain a binary relation symbol $<$ and constants $c_1,c_2,c_3$. Consider the $L$-structure $\mathcal M$ with domain $\{1,2,3\}$, where $<^{\mathcal M}$ is the usual strict order on $\{1,2,3\}$ and $c_i^{\mathcal M}=i$. We verify that $\mathcal M$ satisfies each sentence in \begin{align*} T_0=\{c_1<c_2,\ c_2<c_3,\ \forall x\neg(x<x),\ \forall x\forall y\forall z((x<y\wedge y<z)\to x<z)\}. \end{align*} First, \begin{align*} \mathcal M\models c_1<c_2 &\iff c_1^{\mathcal M}<^{\mathcal M}c_2^{\mathcal M}\\ &\iff 1<2, \end{align*} which is true. Similarly, \begin{align*} \mathcal M\models c_2<c_3 &\iff c_2^{\mathcal M}<^{\mathcal M}c_3^{\mathcal M}\\ &\iff 2<3, \end{align*} which is true. For irreflexivity, take any $a\in\{1,2,3\}$. The possible cases are \begin{align*} 1<1&\text{ is false},\\ 2<2&\text{ is false},\\ 3<3&\text{ is false}. \end{align*} Hence $\mathcal M\models \neg(a<a)$ for each $a\in\{1,2,3\}$, so \begin{align*} \mathcal M\models \forall x\neg(x<x). \end{align*} For transitivity, take $a,b,d\in\{1,2,3\}$ and suppose $a<b$ and $b<d$. Since the domain has only three elements, the only strictly increasing triple is \begin{align*} a=1,\qquad b=2,\qquad d=3, \end{align*} and then $1<3$ is true. Therefore \begin{align*} \mathcal M\models \forall x\forall y\forall z((x<y\wedge y<z)\to x<z). \end{align*} Thus every sentence of $T_0$ is true in $\mathcal M$, so $T_0$ has a model and is therefore consistent by soundness of the usual proof system for first-order logic. The example shows that even a short finite list of formulas can already specify a concrete fragment of an ordered structure. [/example] The completeness proof does not assume that a consistent theory already has a model. Instead, it extends the theory syntactically until the interpretation of connectives and quantifiers can be read directly from membership in the theory. A merely consistent theory may leave some sentence undecided, and then membership in the theory cannot yet behave like a truth predicate. The next notion adds enough decisions to make the later truth lemma possible while still forbidding contradiction. [definition: Maximally Consistent Theory] A theory $T$ is maximally consistent if $T$ is consistent and, for every sentence $\varphi$ in its language, either $\varphi\in T$ or $\neg\varphi\in T$. [/definition] Maximal consistency combines two properties: no contradiction has been introduced, and no sentence remains undecided. The second property is what allows the truth lemma later to prove, by induction on formulas, that truth in the constructed model matches membership in the theory. [quotetheorem:4649] [citeproof:4649] The countability assumption keeps the construction sequential. For arbitrary languages, the same argument is carried out with Zorn's lemma or with a transfinite enumeration of sentences. The theorem is a syntactic completion step, not yet a model construction: it decides every sentence while preserving consistency, but it does not by itself provide witnesses for existential statements. That missing witness property is exactly why the next refinement adds Henkin constants before the term model is built. ## Henkin Constants for Witnessing Existentials What goes wrong if a maximally consistent theory contains $\exists x\,\varphi(x)$ but contains no named element witnessing it? The term model built from syntax has elements represented by closed terms, so existential formulas must be matched by constants or terms. Henkin's idea is to expand the language by adding new constants that serve as formal witnesses. [definition: Henkin Theory] A theory $T$ in a first-order language $L$ is Henkin if, for every $L$-formula $\varphi(x)$ with at most $x$ free, there is a closed $L$-term $t$ such that \begin{align*} T\vdash \exists x\,\varphi(x)\to \varphi(t). \end{align*} [/definition] A Henkin theory has enough names for existential claims. This does not mean that every element already has a special constant; it means that every provable existential sentence has some term that can serve as a witness. [example: Adding a Henkin Constant] Suppose $L$ contains a unary predicate $P$, $T$ is consistent, and $\exists x\,P(x)\in T$. Expand the language to $L'=L\cup\{c_P\}$ with $c_P$ fresh, and set \begin{align*} T'=T\cup\{\exists x\,P(x)\to P(c_P)\}. \end{align*} We show that adding this one Henkin axiom does not introduce a contradiction. Assume, toward a contradiction, that $T'$ is inconsistent. Then some finite $\Gamma\subset T$ satisfies \begin{align*} \Gamma,\ \exists x\,P(x)\to P(c_P)\vdash \bot. \end{align*} By the deduction rule for implication and classical negation, this gives \begin{align*} \Gamma&\vdash \neg(\exists x\,P(x)\to P(c_P)),\\ \Gamma&\vdash \exists x\,P(x),\\ \Gamma&\vdash \neg P(c_P). \end{align*} The constant $c_P$ is fresh, so it does not occur in any sentence of $\Gamma$. Replacing the fresh constant by a variable $y$ not occurring in $\Gamma$ gives \begin{align*} \Gamma\vdash \neg P(y). \end{align*} Since $y$ is not free in $\Gamma$, universal generalization gives \begin{align*} \Gamma\vdash \forall y\,\neg P(y). \end{align*} From $\Gamma\vdash \exists x\,P(x)$ and $\Gamma\vdash \forall y\,\neg P(y)$, instantiate the universal sentence at the witness variable used in the existential argument: \begin{align*} \forall y\,\neg P(y)&\vdash \neg P(x),\\ \exists x\,P(x),\ \forall y\,\neg P(y)&\vdash \bot. \end{align*} Hence $\Gamma\vdash\bot$, contradicting the consistency of $T$ because $\Gamma\subset T$. Therefore $T'$ is consistent. The new constant $c_P$ is not asserted to be the only object satisfying $P$; it is only a syntactic name that lets the existential sentence have a witness inside the expanded language. [/example] Adding one witness constant is harmless only if the process can be repeated for all existential formulas without creating inconsistency. The completion argument therefore needs a combined extension step: enlarge the language by enough formal names, preserve consistency, and end with a theory whose existential consequences have syntactic witnesses. [quotetheorem:4650] [citeproof:4650] Henkin constants are formal devices. They do not add semantic information by themselves; they make the later term model rich enough to interpret existential quantifiers correctly. Their role is to make existential truth visible inside the syntax of closed terms, so that the later model does not have to search outside the language for unnamed elements. The construction also separates naming from choice: a constant witnesses an existential formula only relative to the extended theory and its proof relation, not because the original language already singled out a canonical object. ## The Term Model and the Truth Lemma Once a theory is maximally consistent and Henkin, how is a structure extracted from it? The model uses closed terms as names for objects, identifying two terms when the theory proves that they are equal. Relations and functions are then interpreted by membership of the corresponding atomic sentences in the theory. [definition: Term Equivalence] Let $T$ be a theory with equality in a language $L$. For closed $L$-terms $s,t$, define $s\sim_T t$ if $T\vdash s=t$. [/definition] The equality rules ensure that $\sim_T$ is an equivalence relation and that functions and relations respect it. This is the syntactic substitute for quotienting by equality in an ordinary algebraic construction. With equality classes available, the construction can now turn syntax into an actual structure. Closed terms supply the objects, while membership of atomic sentences in the theory supplies the interpretations of relation symbols. [definition: Henkin Term Model] Let $T$ be a maximally consistent Henkin theory in a first-order language $L$ with equality. The Henkin term model $\mathcal M_T$ has domain the set of $\sim_T$-equivalence classes $[t]$ of closed $L$-terms. For each constant $c$, set $c^{\mathcal M_T}=[c]$. For each $n$-ary function symbol $f$, set \begin{align*} f^{\mathcal M_T}([t_1],\dots,[t_n])=[f(t_1,\dots,t_n)]. \end{align*} For each $n$-ary relation symbol $R$, define \begin{align*} \mathcal M_T\models R([t_1],\dots,[t_n]) \end{align*} when $R(t_1,\dots,t_n)\in T$. [/definition] Well-definedness is the main technical check. If $T$ proves $s_i=t_i$ for each $i$, the equality substitution rules give the same value for functions and the same truth value for relation formulas. Once the structure is defined, the central question is whether it satisfies exactly the sentences selected by the theory. This is what connects the syntactic construction to semantics rather than merely producing a formal quotient of terms. [quotetheorem:4651] [citeproof:4651] The truth lemma is the bridge from proof theory to model theory. It says that, after the Henkin preparation, the maximally consistent set is not merely a formal object; it is exactly the theory true in its term model. The atomic case depends on the definition of the term model, while the Boolean and quantifier cases use maximal consistency and the Henkin witness property. This is why both earlier preparations are needed: maximality controls negation and disjunction, and Henkin witnesses make existential formulas match closed terms in the domain. ## Completeness for First-Order Logic Why should semantic consequence be captured by derivability? If $T\models\varphi$ but no proof of $\varphi$ from $T$ exists, then $T\cup\{\neg\varphi\}$ should be consistent. The Henkin construction then produces a model of this enlarged theory, contradicting the assumed semantic consequence. [definition: Semantic Consequence] For a theory $T$ and sentence $\varphi$ in a language $L$, write $T\models\varphi$ if every $L$-structure satisfying all sentences in $T$ also satisfies $\varphi$. [/definition] This relation is semantic because it quantifies over structures. Completeness asserts that the proof relation $\vdash$ reaches exactly the same consequences. The obstruction is the apparent gap between an infinite class of models and a finite formal derivation. The Henkin construction closes that gap by showing that any consistent failure of derivability can be turned into a countermodel. [quotetheorem:4652] [citeproof:4652] Completeness is not the same as decidability. It says that valid consequences have finite proofs, but it does not provide a terminating method that always decides whether an arbitrary first-order sentence is valid. [example: A Validity Detected by Completeness] Let $T=\{\forall x(P(x)\to Q(x)),\ \forall xP(x)\}$. We show first why every model of $T$ satisfies $\forall xQ(x)$. Let $\mathcal M\models T$, and let $a$ be any element of the domain of $\mathcal M$. Since $\mathcal M\models \forall x(P(x)\to Q(x))$, universal instantiation gives \begin{align*} \mathcal M\models P(a)\to Q(a). \end{align*} Since $\mathcal M\models \forall xP(x)$, universal instantiation also gives \begin{align*} \mathcal M\models P(a). \end{align*} By the truth condition for implication, from $\mathcal M\models P(a)\to Q(a)$ and $\mathcal M\models P(a)$ we get \begin{align*} \mathcal M\models Q(a). \end{align*} Because $a$ was arbitrary, $\mathcal M\models \forall xQ(x)$. Hence \begin{align*} T\models \forall xQ(x). \end{align*} By *Gödel Completeness Theorem*, there is a formal derivation of $\forall xQ(x)$ from $T$. In natural deduction, the derivation has the same shape: choose a variable $y$ not occurring in any open undischarged assumption, instantiate both universal assumptions, \begin{align*} \forall x(P(x)\to Q(x))&\vdash P(y)\to Q(y),\\ \forall xP(x)&\vdash P(y), \end{align*} then apply implication elimination to obtain \begin{align*} \forall x(P(x)\to Q(x)),\ \forall xP(x)\vdash Q(y). \end{align*} Since $y$ was arbitrary, universal introduction yields \begin{align*} \forall x(P(x)\to Q(x)),\ \forall xP(x)\vdash \forall xQ(x). \end{align*} Thus completeness turns the semantic fact $T\models\forall xQ(x)$ into an explicit syntactic derivation from the two assumptions in $T$. [/example] ## Compactness from Finite Proofs What model-theoretic information is hidden in the fact that formal proofs are finite objects? Since any derivation uses only finitely many assumptions, inconsistency of an infinite theory must already appear in a finite fragment. Completeness converts that proof-theoretic fact into the compactness theorem. [definition: Finitely Satisfiable Theory] A theory $T$ is finitely satisfiable if every finite subset $T_0\subset T$ has a model. [/definition] Finite satisfiability is weaker than immediately having a model for all of $T$. The remaining problem is whether infinitely many individually compatible requirements can fail only when imposed all at once. Compactness answers that problem by using completeness and the finiteness of derivations: if the whole theory were unsatisfiable, a finite fragment would already contain the contradiction. This turns an infinite semantic question into a family of finite checks. The theorem is needed because finite satisfiability alone only gives separate models for separate finite fragments. Compactness is the principle that assembles those compatible finite fragments into one model of the entire theory. [quotetheorem:4290] [citeproof:4290/proof-theory] Compactness is often used by designing an infinite theory whose finite pieces can be interpreted directly. The theorem then supplies a single model satisfying all requirements at once. [example: A Finitely Satisfiable Theory Is Satisfiable] Let $L$ contain a binary relation symbol $<$ and constants $c_n$ for $n\in\mathbb N$. Let $T$ consist of the linear order axioms for $<$ together with the sentences $c_i<c_j$ for all $i<j$. We verify finite satisfiability explicitly. Let $T_0\subset T$ be finite. Only finitely many order requirements $c_i<c_j$ occur in $T_0$, so there is some $m\in\mathbb N$ such that every constant occurring in those requirements is among $c_1,\dots,c_m$. Define an $L$-structure $\mathcal M_0$ with domain $\mathbb Q$, interpret $<$ as the usual strict order on $\mathbb Q$, and set \begin{align*} c_k^{\mathcal M_0} = \begin{cases} k, & 1\le k\le m,\\ 0, & k>m. \end{cases} \end{align*} The usual order on $\mathbb Q$ is a linear order, so $\mathcal M_0$ satisfies every linear order axiom in $T_0$. If $c_i<c_j$ is one of the remaining sentences in $T_0$, then $i<j$ and $i,j\le m$, hence \begin{align*} \mathcal M_0\models c_i<c_j &\iff c_i^{\mathcal M_0}<c_j^{\mathcal M_0}\\ &\iff i<j, \end{align*} which is true by the choice of the sentence $c_i<c_j$. Thus every finite $T_0\subset T$ has a model. By *Compactness Theorem for First-Order Logic*, the whole theory $T$ has a model $\mathcal M$. Since $c_i<c_j\in T$ for every $i<j$, this model satisfies \begin{align*} \mathcal M\models c_i<c_j \end{align*} for every $i<j$. Therefore the interpretations of the constants form an infinite strictly increasing sequence in $\mathcal M$. [/example] The previous example fixes one test case for the idea. The next example, Nonstandard Large Finite Sets, changes the setting so the same mechanism can be recognized from another angle. [example: Nonstandard Large Finite Sets] Work in the first-order language with equality, and for each $n\in\mathbb N$ let \begin{align*} \sigma_n=\exists x_1\dots\exists x_n\bigwedge_{1\le i<j\le n}x_i\ne x_j. \end{align*} Let \begin{align*} T=\{\sigma_n:n\in\mathbb N\}. \end{align*} We verify that every finite subset of $T$ is satisfiable. If $T_0\subset T$ is finite, then there are finitely many indices $n_1,\dots,n_r$ such that \begin{align*} T_0=\{\sigma_{n_1},\dots,\sigma_{n_r}\}. \end{align*} Choose \begin{align*} m=\max\{n_1,\dots,n_r\}. \end{align*} Let $\mathcal M_0$ be the structure whose domain is \begin{align*} M_0=\{1,2,\dots,m\}, \end{align*} with equality interpreted as actual equality on $M_0$. For each $\sigma_{n_\ell}\in T_0$, we have $n_\ell\le m$, so the elements \begin{align*} 1,2,\dots,n_\ell \end{align*} belong to $M_0$. If $1\le i<j\le n_\ell$, then $i$ and $j$ are different natural numbers, hence \begin{align*} \mathcal M_0\models i\ne j. \end{align*} Therefore \begin{align*} \mathcal M_0\models \bigwedge_{1\le i<j\le n_\ell}x_i\ne x_j \end{align*} under the assignment $x_i\mapsto i$ for $1\le i\le n_\ell$, and the existential quantifiers give \begin{align*} \mathcal M_0\models \sigma_{n_\ell}. \end{align*} Since this holds for every $\sigma_{n_\ell}\in T_0$, the finite set $T_0$ has a model. By *Compactness Theorem for First-Order Logic*, the whole theory $T$ has a model $\mathcal M$. For every $n\in\mathbb N$, \begin{align*} \mathcal M\models \sigma_n, \end{align*} so for each $n$ the domain of $\mathcal M$ contains at least $n$ pairwise distinct elements. If the domain had exactly $r$ elements, then $\sigma_{r+1}$ would require $r+1$ pairwise distinct elements in a set of size $r$, which is impossible. Hence $\mathcal M$ is infinite. Thus infinitude is forced by the infinite theory $T$, even though no single first-order sentence expresses infinitude over all structures. [/example] ## Löwenheim-Skolem Consequences How much control does the Henkin proof give over the size of the model it builds? Because the term model has as many elements as there are closed terms, the cardinality of the language bounds the cardinality of the constructed model. This gives the downward Löwenheim-Skolem theorem as a by-product of completeness. [quotetheorem:4272] [citeproof:4272/proof-theory] The theorem can feel paradoxical when applied to theories with very large intended models, such as set theory. The resolution is that first-order axioms control membership and satisfaction internally, but the external cardinality of a model is measured from outside the model. [remark: Skolem Phenomenon] A countable first-order theory may have a countable model even when it proves that uncountable sets exist, provided the phrase "uncountable" is interpreted inside the model. The external observer sees only countably many elements, while the model may contain no internal bijection between its version of $\mathbb N$ and the set it calls uncountable. [/remark] The compactness and Löwenheim-Skolem theorems show that first-order proof systems have strong semantic reach but also strict expressive limits. Completeness turns consistency into satisfiability, compactness reflects the finitary nature of derivations, and Löwenheim-Skolem reflects the syntactic size of the language used to build term models. Chapter 8 shows that first-order proof systems are strong enough to match semantic consequence, but also finitary in a way that yields compactness and model-theoretic consequences. Chapter 9 isolates the finite content hidden inside first-order proofs by turning them into Herbrand-style term expansions and quantifier-free certificates. # 9. Herbrand's Theorem Herbrand's theorem is the point in the course where proof theory meets the finite combinatorics hidden inside first-order logic. Chapters 7 and 8 developed cut elimination, completeness, and compactness as structural tools for proofs and models; here we use those tools to isolate the quantifier-free core of first-order validity. The main question is: when a first-order formula is valid, can its validity be witnessed by finitely many ground instances? The prerequisites for this chapter are the syntax and semantics of first-order logic, especially terms, formulas, structures, satisfaction, and validity. We also use prenex normal form, propositional compactness, and the basic proof-search idea that validity of $F$ may be studied through unsatisfiability of $\neg F$. No model theory beyond the construction of term models is needed, but the reader should be comfortable distinguishing semantic satisfiability from propositional satisfiability of a finite set of ground atoms. ## Reducing Quantifiers to a Standard Shape How can we compare different first-order formulas when their quantifiers occur in different places? Herbrand's theorem is easiest to state after every formula has been converted into a form where all quantifiers stand at the front and the remaining part contains no quantifiers. This section records the syntactic reductions used before the finite Herbrand analysis begins. [definition: Prenex Formula] A first-order formula is in prenex form if it has the shape \begin{align*} Q_1x_1\,Q_2x_2\cdots Q_nx_n\,A(x_1,\dots,x_n), \end{align*} where each $Q_i$ is either $\forall$ or $\exists$, the variables $x_i$ are distinct, and $A$ is quantifier-free. [/definition] The quantifier-free formula $A$ is called the matrix of the prenex formula. Before moving quantifiers, bound variables are renamed so that no variable becomes accidentally captured. The definition would be of limited use unless arbitrary formulas could actually be brought into this standard shape. The needed result is an equivalence-preserving normalization theorem, with variable-renaming conditions preventing the syntactic rearrangement from changing meaning. [quotetheorem:4653] [citeproof:4653] Prenex normal form separates the order of quantifier choices from the propositional structure of the matrix. The distinct-variable hypothesis and the avoidance of free-variable capture are essential: without them, moving a quantifier can change which objects a variable ranges over inside a subformula. The theorem is purely syntactic and preserves logical equivalence in the original language, unlike Skolemization below, which expands the language and preserves satisfiability rather than equivalence. Herbrand's theorem then studies the finitely many ground instances needed to witness the matrix. [example: Prenexing A Mixed Formula] Consider the formula $(\forall x\,P(x)) \to \exists y\,Q(y)$. We first remove the implication using $A\to B \equiv \neg A\lor B$: \begin{align*} (\forall x\,P(x)) \to \exists y\,Q(y) &\equiv \neg(\forall x\,P(x)) \lor \exists y\,Q(y). \end{align*} Pushing the negation through the universal quantifier gives \begin{align*} \neg(\forall x\,P(x)) \lor \exists y\,Q(y) &\equiv \exists x\,\neg P(x) \lor \exists y\,Q(y). \end{align*} Since $x$ is not free in $\exists y\,Q(y)$, the first existential quantifier may be moved across the disjunction: \begin{align*} \exists x\,\neg P(x) \lor \exists y\,Q(y) &\equiv \exists x\,\bigl(\neg P(x) \lor \exists y\,Q(y)\bigr). \end{align*} Since $y$ is not free in $\neg P(x)$, the second existential quantifier may then be moved to the front: \begin{align*} \exists x\,\bigl(\neg P(x) \lor \exists y\,Q(y)\bigr) &\equiv \exists x\,\exists y\,\bigl(\neg P(x) \lor Q(y)\bigr). \end{align*} Thus a prenex equivalent is \begin{align*} \exists x\,\exists y\,\bigl(\neg P(x) \lor Q(y)\bigr), \end{align*} whose matrix $\neg P(x)\lor Q(y)$ records the propositional pattern left after the quantifier choices have been exposed. [/example] The next reduction removes existential quantifiers in a way suited to satisfiability and validity arguments. Instead of choosing an existential witness directly, we add a function symbol that names the witness as a function of the preceding universal variables. [definition: Skolemization] Fix a first-order language $L$. Skolemization is the transformation sending a prenex $L$-sentence \begin{align*} Q_1x_1\cdots Q_nx_n\,A(x_1,\dots,x_n) \end{align*} to a universal sentence over an expanded language $L'$. For each existentially quantified variable $x_i$, introduce a new function symbol $f_i$ whose arity is the number of universally quantified variables $u_1,\dots,u_k$ preceding $x_i$ in the prefix, replace $x_i$ by the term $f_i(u_1,\dots,u_k)$ throughout the remaining matrix, and delete the existential quantifier. [/definition] After Skolemization, the resulting formula is usually not logically equivalent to the original in the same language, because the language has been expanded by new symbols. Its role is instead semantic: it preserves satisfiability in the direction needed for Herbrand's theorem. The next point is to make that preservation precise. Without such a theorem, replacing existential quantifiers by fresh function symbols would be only a suggestive notation change, not a justified reduction for satisfiability and validity arguments. [quotetheorem:4654] [citeproof:4654] The expansion of the language is a real limitation, not a cosmetic change. For instance, $\exists y\,R(y)$ cannot be replaced inside the original language by $R(c)$ unless $c$ is already a symbol with the intended interpretation; Skolemization instead adds a fresh constant and asks only about satisfiability in the expanded language. The dependence on preceding universal variables is also necessary: replacing $\forall x\,\exists y\,R(x,y)$ by $\forall x\,R(x,c)$ would require one fixed witness for every $x$, while the original formula allows the witness to vary with $x$. For validity questions, we usually apply Skolemization to the negation of the formula, so that $F$ is valid exactly when $\neg F$ is unsatisfiable, and the Skolemized form of $\neg F$ lets us test unsatisfiability by looking at ground instances. [example: Skolemizing A Simple Dependency] For the prenex formula $\forall x\,\exists y\,R(x,y)$, the variable $y$ is existentially quantified after the universal variable $x$. Therefore the Skolem symbol for $y$ must take the preceding universal variable as an argument. Introduce a fresh unary function symbol $f$ and replace every occurrence of $y$ in the matrix $R(x,y)$ by $f(x)$: \begin{align*} R(x,y) &\rightsquigarrow R(x,f(x)). \end{align*} After deleting the existential quantifier, the Skolemized universal form is \begin{align*} \forall x\,R(x,f(x)). \end{align*} The unary term $f(x)$ records that the witness for $y$ may be different for different values of $x$; using a constant $c$ instead would give $\forall x\,R(x,c)$, which would require one fixed witness for all $x$. [/example] The ground terms generated by the language provide the possible substitutions used in Herbrand instances. After Skolemization, these terms are the syntactic names for the possible witnesses and their dependencies. To make the later finite-instance tests unambiguous, we need a fixed supply of all closed terms available in the language. That supply is called the Herbrand universe. [definition: Herbrand Universe] Given a first-order language $L$, its Herbrand universe $H_L$ is the set of all closed terms built from the constant symbols and function symbols of $L$. [/definition] If $L$ has no constant symbol, a fresh constant is added so that the Herbrand universe is non-empty. Predicate symbols do not create terms; they only form atomic formulas from terms. [example: Computing A Herbrand Universe] For the Skolemized language of $\forall x\,\exists y\,R(x,y)$, use the constant symbol $a$ and the unary Skolem function symbol $f$. A closed term is built by starting with a constant and then applying function symbols finitely many times. Since $a$ is the only constant and $f$ is the only function symbol, every closed term is obtained by repeatedly applying $f$ to $a$. Define \begin{align*} t_0 &= a,\\ t_1 &= f(t_0)=f(a),\\ t_2 &= f(t_1)=f(f(a)),\\ t_3 &= f(t_2)=f(f(f(a))), \end{align*} and in general set $t_{k+1}=f(t_k)$ for $k\ge 0$. Thus the Herbrand universe is \begin{align*} H_L=\{t_k:k\in\mathbb N\cup\{0\}\} =\{a,f(a),f(f(a)),f(f(f(a))),\dots\}. \end{align*} The Skolemized sentence is $\forall x\,R(x,f(x))$, so a ground instance is obtained by replacing $x$ with a closed term $t_k$: \begin{align*} R(x,f(x))[x:=t_k] &=R(t_k,f(t_k))\\ &=R(t_k,t_{k+1}). \end{align*} Therefore the ground instances are exactly \begin{align*} R(t_k,t_{k+1})\quad\text{for }k\in\mathbb N\cup\{0\}. \end{align*} The first three are \begin{align*} R(t_0,t_1)&=R(a,f(a)),\\ R(t_1,t_2)&=R(f(a),f(f(a))),\\ R(t_2,t_3)&=R(f(f(a)),f(f(f(a)))). \end{align*} The example shows that even a language with one constant and one unary function can have infinitely many ground terms, so the Herbrand universe may be infinite. [/example] ## Herbrand Disjunctions Once all terms are available, what finite object should replace a quantified formula? A Herbrand disjunction collects finitely many ground instances of the matrix. Herbrand's theorem says that validity of the original first-order formula is equivalent to the existence of such a finite quantifier-free valid disjunction. [definition: Herbrand Instance] Let $A(x_1,\dots,x_n)$ be a quantifier-free formula and let $t_1,\dots,t_n$ be ground terms from the Herbrand universe. The formula $A(t_1,\dots,t_n)$ is a Herbrand instance of $A$. [/definition] A Herbrand instance contains no variables and no quantifiers. It is therefore evaluated like a propositional formula once each ground atomic formula is regarded as a propositional atom. A single instance usually cannot represent the behavior of a quantified formula, because different ground terms may be needed for different possible witnesses. We need a finite certificate that packages the relevant ground instances into one quantifier-free formula whose truth can be tested propositionally. [definition: Herbrand Disjunction] Let $A(x_1,\dots,x_n)$ be quantifier-free. A Herbrand disjunction for $A$ is a finite disjunction \begin{align*} A(t_{1,1},\dots,t_{1,n}) \lor \cdots \lor A(t_{m,1},\dots,t_{m,n}), \end{align*} where all $t_{i,j}$ are ground terms from the Herbrand universe. [/definition] The disjunction is quantifier-free. Its validity is propositional validity relative to the atomic formulas that appear in the displayed finite expression. Because the Herbrand disjunction has no quantifiers left, its truth no longer depends on ranging over arbitrary first-order structures. What remains is a finite propositional question about the ground atoms that occur in the disjunction. [definition: Quantifier-Free Validity] A quantifier-free sentence is valid if every truth assignment to its ground atomic subformulas makes the sentence true. [/definition] This notion is decidable by finite truth-table analysis. Herbrand's theorem reduces first-order validity to the search for a finite quantifier-free validity certificate. The remaining difficulty is that first-order quantifiers range over arbitrary domains, while truth tables only inspect finitely many atomic cases. Herbrand's insight is that, after Skolemization, validity can be detected by finitely many ground instances when a valid certificate exists. [quotetheorem:4655] [citeproof:4655] The theorem explains why quantifier reasoning can be replaced by systematic enumeration of ground terms. Its hypotheses encode several choices: we work with sentences, use a Skolem expansion of the language, and judge the final expression by propositional truth assignments to its ground atoms. If the Skolemization step is skipped, existential dependencies can be lost; if the Herbrand universe is not fixed, the phrase "ground instance" has no definite meaning. The price is that the search space may be infinite even though a successful certificate, when it exists, is finite; Chapter 12 returns to this as the distinction between decidability and semi-decidability. [example: Extracting A Herbrand Disjunction] Consider \begin{align*} F=\bigl(\exists x\,\forall y\,P(x,y)\bigr)\to \exists u\,P(u,u). \end{align*} To extract a Herbrand witness, work with the negation of $F$: \begin{align*} \neg F &\equiv \neg\bigl(\neg(\exists x\,\forall y\,P(x,y))\lor \exists u\,P(u,u)\bigr)\\ &\equiv \exists x\,\forall y\,P(x,y)\land \neg\exists u\,P(u,u)\\ &\equiv \exists x\,\forall y\,P(x,y)\land \forall u\,\neg P(u,u). \end{align*} Since $x$ is not free in $\forall u\,\neg P(u,u)$, and $u$ is not free in $P(x,y)$, this is equivalent to the prenex sentence \begin{align*} \exists x\,\forall y\,\forall u\,\bigl(P(x,y)\land \neg P(u,u)\bigr). \end{align*} Skolemizing the leading existential quantifier introduces a fresh constant $a$, because no universal variables precede $x$. Replacing $x$ by $a$ gives the universal sentence \begin{align*} \forall y\,\forall u\,\bigl(P(a,y)\land \neg P(u,u)\bigr). \end{align*} Now take the ground instance with $y=a$ and $u=a$: \begin{align*} P(a,y)\land \neg P(u,u)\,[y:=a,u:=a] &=P(a,a)\land \neg P(a,a). \end{align*} This ground instance is propositionally unsatisfiable, since no truth assignment can make both $P(a,a)$ and $\neg P(a,a)$ true. Equivalently, the corresponding Herbrand disjunction for the original valid sentence is \begin{align*} \neg\bigl(P(a,a)\land \neg P(a,a)\bigr) &\equiv \neg P(a,a)\lor P(a,a), \end{align*} which is quantifier-free valid by the propositional law of excluded middle. The single ground term $a$ already exposes the finite contradiction in the Skolemized negation, so it yields the Herbrand witness for the validity of $F$. [/example] The example also points to a boundary of the idea. The following remark, Form Of The Theorem, records that interpretation before the construction is used again. [remark: Form Of The Theorem] Different textbooks state Herbrand's theorem either for existential valid formulas or for universal unsatisfiable formulas. These are the same statement under negation, prenex conversion, and Skolemization. In proof search, the unsatisfiable universal form is often more convenient; in proof extraction, the valid existential disjunction form is often more visible. [/remark] ## Herbrand Consistency How can consistency of a first-order theory be tested by finite syntactic data? Herbrand's consistency criterion says that a universal theory is consistent exactly when every finite set of its ground instances is propositionally satisfiable. This is the form of Herbrand's theorem most directly connected with proof search. [definition: Universal Theory] A first-order theory $T$ is universal if each axiom of $T$ has the form \begin{align*} \forall x_1\cdots\forall x_n\,A(x_1,\dots,x_n), \end{align*} where $A$ is quantifier-free. [/definition] The ground instances of the axioms are obtained by substituting closed terms from the Herbrand universe for the universally quantified variables. For a universal theory, these instances are the quantifier-free constraints that a Herbrand model must satisfy. The consistency test therefore asks whether any finite batch of those constraints already forces a propositional contradiction. If no finite batch does, the theory has passed the Herbrand-style consistency condition. [definition: Herbrand Consistency] A universal theory $T$ is Herbrand consistent if every finite set of ground instances of axioms of $T$ is propositionally satisfiable. [/definition] Herbrand consistency is a finite condition scheme rather than a single finite test. Each individual finite check is propositional, but there may be infinitely many checks. We need a criterion explaining why this finite scheme captures ordinary first-order consistency for universal theories. The point is to construct a genuine Herbrand model from the absence of finite propositional contradictions among ground instances. [quotetheorem:4656] [citeproof:4656] The criterion gives a model-construction reading of consistency. The universal hypothesis is essential because the Herbrand model checks universal axioms by checking all closed-term substitutions; formulas with leading existential quantifiers require Skolemization before this argument applies. The equality qualification is also essential: built-in equality imposes reflexivity, symmetry, transitivity, and congruence conditions that are not captured by arbitrary propositional truth assignments to atoms of the form $s=t$. If finite propositional contradictions never appear among the correctly formed ground instances, the Herbrand structure supplies a model. [example: A Universal Theory With A Herbrand Model] Let $T$ contain the universal axiom $\forall x\,R(x,f(x))$ in a language whose only constant symbol is $a$ and whose only function symbol is the unary symbol $f$. Define closed terms by \begin{align*} t_0&=a,\\ t_{k+1}&=f(t_k)\quad\text{for }k\ge 0. \end{align*} Thus the first few closed terms are \begin{align*} t_0&=a,\\ t_1&=f(a),\\ t_2&=f(f(a)),\\ t_3&=f(f(f(a))). \end{align*} Since every closed term must start with the only constant $a$ and then apply the only function symbol $f$ finitely many times, the Herbrand universe is \begin{align*} H_L=\{t_k:k\in\mathbb N\cup\{0\}\}. \end{align*} A ground instance of $\forall x\,R(x,f(x))$ is obtained by replacing $x$ with a closed term $t_k$. For each $k\ge 0$, \begin{align*} R(x,f(x))[x:=t_k] &=R(t_k,f(t_k))\\ &=R(t_k,t_{k+1}), \end{align*} because $t_{k+1}=f(t_k)$. Hence the ground instances are \begin{align*} R(t_k,t_{k+1})\quad\text{for }k\in\mathbb N\cup\{0\}. \end{align*} Now take any finite set of ground instances, say \begin{align*} \{R(t_{k_1},t_{k_1+1}),\dots,R(t_{k_m},t_{k_m+1})\}. \end{align*} Assign truth value true to each of the finitely many atoms displayed in this set. Then every formula in the finite set is true, so every finite set of ground instances is propositionally satisfiable. The corresponding Herbrand structure has domain $H_L$ and interprets $R$ by \begin{align*} R^{\mathcal H}=\{(t_k,t_{k+1}):k\in\mathbb N\cup\{0\}\}. \end{align*} For every element $t_k$ of the domain, \begin{align*} f^{\mathcal H}(t_k)=t_{k+1}, \end{align*} so \begin{align*} R^{\mathcal H}(t_k,f^{\mathcal H}(t_k)) &=R^{\mathcal H}(t_k,t_{k+1}) \end{align*} is true by the definition of $R^{\mathcal H}$. Therefore $\mathcal H\models \forall x\,R(x,f(x))$, and this universal theory has a Herbrand model. [/example] ## Automated Theorem Proving And Proof Search Why is Herbrand's theorem central to automated theorem proving? It turns first-order proof search into a search through ground terms plus propositional reasoning. This is the basis of resolution, unification-based search, and many completeness arguments for automated provers. [explanation: From Quantifiers To Search] To prove a sentence $F$, an automated prover often tries to refute $\neg F$. After prenexing and Skolemizing $\neg F$, the prover obtains a universal set of clauses. Herbrand's theorem says that if $F$ is valid, then some finite collection of ground instances of these clauses is already propositionally contradictory. A naive procedure enumerates ground terms, generates more and more instances, and checks propositional unsatisfiability. This is semidecision rather than decision: if $F$ is valid, the procedure eventually reaches a finite Herbrand certificate; if $F$ is not valid, the search may continue indefinitely. [/explanation] The raw Herbrand search is wasteful because it may generate many ground instances before finding the ones that interact. We need a mechanism for keeping variables in the clauses and computing exactly the substitutions that make complementary atoms match. [definition: Unifier] Fix a first-order language $L$. A substitution is a map $\sigma$ from variables to $L$-terms, extended recursively to all $L$-terms and atomic $L$-formulas. A unifier for two terms or atomic formulas $s$ and $t$ is a substitution $\sigma$ such that $s\sigma = t\sigma$. [/definition] Unification is the mechanism that lets a prover represent many Herbrand instances at once. A single clause with variables stands for all of its ground instances, and a unifier selects the instances needed for a resolution step. With this mechanism available, Herbrand's theorem becomes an operational completeness statement for automated proof search. The theorem below isolates the finite certificate that a complete search procedure is trying to uncover. [quotetheorem:4657] [citeproof:4657] This theorem does not say that search is efficient. It assumes the preceding transformations have produced a correct Skolemized clause form and that the propositional refutation system used at the ground level is complete. The limitation is important: Herbrand's theorem guarantees existence of a finite ground contradiction for valid inputs, but it gives no computable bound on how far the term search must go. It says that proof search is complete in the sense that a finite certificate exists whenever the input sentence is valid. [example: Ground Search Pattern] Suppose the Skolemized clause set contains the ground clauses $P(a)$ and $\neg Q(a)$, together with the clause with one variable \begin{align*} \neg P(x)\lor Q(x). \end{align*} Substituting the ground term $a$ for $x$ gives the Herbrand instance \begin{align*} (\neg P(x)\lor Q(x))[x:=a] &=\neg P(a)\lor Q(a). \end{align*} Thus the finite ground set under consideration is \begin{align*} \{\,P(a),\ \neg P(a)\lor Q(a),\ \neg Q(a)\,\}. \end{align*} To see that this set is propositionally unsatisfiable, let $v$ be any truth assignment to the ground atoms $P(a)$ and $Q(a)$. If all three displayed clauses were true under $v$, then \begin{align*} v(P(a))&=\text{true},\\ v(\neg Q(a))&=\text{true}, \end{align*} so $v(Q(a))=\text{false}$. Hence \begin{align*} v(\neg P(a))&=\text{false},\\ v(Q(a))&=\text{false}, \end{align*} and therefore \begin{align*} v(\neg P(a)\lor Q(a))=\text{false}\lor\text{false}=\text{false}, \end{align*} contradicting the assumption that the middle clause is true. So no truth assignment satisfies the finite ground set. The example shows the Herbrand search pattern: the contradiction appears only after choosing the ground instance $x:=a$. [/example] The example also points to a boundary of the idea. The following remark, Computational Meaning, records that interpretation before the construction is used again. [remark: Computational Meaning] Herbrand's theorem gives a bridge between semantic validity and finite syntactic certificates. The certificate is a finite list of terms plus a propositional tautology or contradiction. This is why the theorem remains central in proof theory, automated deduction, and the study of constructive content hidden inside classical first-order proofs. [/remark] Herbrand's theorem makes explicit the finite syntactic core of first-order reasoning. Chapter 10 then raises the stakes by moving to arithmetic, where proof theory can talk about proofs, computations, and formal derivations inside the object language itself. # 10. Arithmetic and Formal Theories Proof theory becomes sharper when the object language is strong enough to talk about finite syntactic objects. Chapters 1-7 studied derivations, normalization, and cut elimination from the outside; arithmetic lets us internalize part of that discussion inside a formal theory. This chapter introduces Peano Arithmetic as a first-order theory, explains how computable operations of a basic kind are represented by formulas, and works through elementary formal proofs about addition, multiplication, and induction. The guiding question is: how much ordinary reasoning about natural numbers can be carried out as a formal derivation? The answer is strong enough to support metamathematical applications, but it is achieved by very concrete means: a fixed language, finitely many algebraic axioms, and an infinite induction schema. ## The Language and Axioms of Peano Arithmetic To formalize arithmetic, we first need a language in which numerals, addition, multiplication, and order-like relations can be expressed without appealing to informal number theory. The language of Peano Arithmetic is deliberately small: it has just enough structure to build the usual natural-number calculations, while keeping formulas and proofs syntactic objects of the same kind studied earlier in the course. [definition: Language of Peano Arithmetic] The first-order language of Peano Arithmetic, denoted $\mathcal L_{\mathrm{PA}}$, has equality, a constant symbol $0$, a unary function symbol $S$, binary function symbols $+$ and $\cdot$, and the usual logical symbols and variables. [/definition] The term $Sx$ is read as the successor of $x$. The standard numeral for $n \in \mathbb N$ is the closed term $\overline{n}$ obtained by applying $S$ to $0$ exactly $n$ times, so $\overline{3}$ is $SSS0$. [example: Numerals and Closed Terms] In $\mathcal L_{\mathrm{PA}}$, the expression $S(S0)+S0$ is a closed term: $0$ is a closed term, so $S0$ and $S(S0)$ are closed terms, and then the binary function symbol $+$ forms the closed term $S(S0)+S0$ from those two closed terms. Under the intended interpretation in $\mathbb N$, $0$ denotes $0$ and $S$ denotes the successor function $n\mapsto n+1$. Hence \begin{align*} S0 &\text{ denotes } 0+1=1,\\ S(S0) &\text{ denotes } 1+1=2,\\ S(S0)+S0 &\text{ denotes } 2+1=3. \end{align*} Thus $S(S0)+S0$ denotes the natural number $3$ in the intended interpretation, even though the decimal symbol $3$ is not primitive in PA; the PA numeral for $3$ is the closed term $SSS0$. [/example] The language alone only gives symbols for arithmetic; proof theory also needs a fixed list of axioms governing those symbols. The central choice is to keep arithmetic first-order while adding enough recursive equations and induction instances to formalize ordinary numerical reasoning. [definition: Peano Arithmetic] Peano Arithmetic, denoted $\mathrm{PA}$, is the first-order theory in $\mathcal L_{\mathrm{PA}}$ with the following non-logical axioms: \begin{align*} &\forall x\, \neg(Sx = 0),\\ &\forall x\forall y\,(Sx = Sy \to x = y),\\ &\forall x\,(x + 0 = x),\\ &\forall x\forall y\,(x + Sy = S(x+y)),\\ &\forall x\,(x \cdot 0 = 0),\\ &\forall x\forall y\,(x \cdot Sy = x\cdot y + x), \end{align*} together with, for each $\mathcal L_{\mathrm{PA}}$-formula $\varphi(x, z_1,\dots,z_k)$, the induction axiom \begin{align*} \forall z_1\cdots\forall z_k\,\bigl((\varphi(0,z_1,\dots,z_k) \land \forall x(\varphi(x,z_1,\dots,z_k) \to \varphi(Sx,z_1,\dots,z_k))) \to \forall x\,\varphi(x,z_1,\dots,z_k)\bigr). \end{align*} [/definition] The induction part is not a single axiom but a schema: every formula $\varphi$ gives a separate axiom. This is why PA remains a first-order theory while still supporting induction for formulas with quantifiers and parameters. [remark: First-Order Induction] The induction schema ranges over formulas of the object language, not over arbitrary subsets of $\mathbb N$. Second-order arithmetic has a stronger-looking induction principle because it can quantify over sets of numbers directly. PA instead has one first-order instance for each formula. [/remark] The axioms for $+$ and $\cdot$ are recursive equations in the second argument. This asymmetry matters in formal proofs: facts such as $0+x=x$ or $x+y=y+x$ are not axioms and must be derived by induction. We need the first metatheorem about PA to package the induction schema into a usable proof rule. It explains when a base case and a uniform successor step are enough to derive a universal arithmetic statement inside PA. [quotetheorem:4658] [citeproof:4658] This rule form is the version used in ordinary arithmetic proofs. The hypothesis that the step is proved universally is essential: PA may not pass from a proof of one isolated implication $\varphi(\overline n)\to\varphi(S\overline n)$ to induction over all $x$. The limitation is also important: the rule applies only to formulas of $\mathcal L_{\mathrm{PA}}$, so it does not quantify over arbitrary external sets of natural numbers. In later formalizations, this admissible rule is what lets PA verify recursively defined syntactic predicates by induction on code length, proof length, or formula complexity. ## Primitive Recursive Functions and Representability The next problem is to connect informal computation with formal arithmetic. If a numerical function is given by an elementary recursive definition, can PA express its graph and prove the correct input-output equations? Representability is the bridge from computation outside the theory to formulas inside the theory. [definition: Primitive Recursive Function] The class of primitive recursive functions is the smallest class of functions $\mathbb N^k\to\mathbb N$, for varying $k\ge 1$, containing the zero functions, successor function, and projection functions, and closed under composition and primitive recursion. [/definition] For primitive recursion, closure means that if $g:\mathbb N^k\to\mathbb N$ and $h:\mathbb N^{k+2}\to\mathbb N$ are already in the class, then the function $f:\mathbb N^{k+1}\to\mathbb N$ determined by \begin{align*} f(0,x_1,\dots,x_k) &= g(x_1,\dots,x_k),\\ f(Sn,x_1,\dots,x_k) &= h(n,f(n,x_1,\dots,x_k),x_1,\dots,x_k) \end{align*} is also primitive recursive. [example: Addition as Primitive Recursion] To view addition as a primitive recursive function, take the recursion variable to be the second input. Define $A(y,x)$ by primitive recursion from \begin{align*} g(x) &= x,\\ h(y,u,x) &= Su. \end{align*} The primitive-recursion clauses then give \begin{align*} A(0,x) &= g(x)\\ &= x, \end{align*} and, for every $y$, \begin{align*} A(Sy,x) &= h(y,A(y,x),x)\\ &= S(A(y,x)). \end{align*} If we write $x+y$ for $A(y,x)$, these two equations become \begin{align*} x+0 &= x,\\ x+Sy &= S(x+y). \end{align*} Thus addition is primitive recursive with initial function the projection $g(x)=x$ and step function $(y,u,x)\mapsto Su$. The same two recursive clauses are exactly the PA axioms for addition, so PA defines addition by recursion on the second argument. [/example] Arithmetic can only talk about computation after numerical input-output behavior has been translated into formulas. The first representability notion asks for the weakest concrete guarantee: PA should prove the correct formula for each actual tuple of numerals and refute the incorrect outputs. [definition: Numeralwise Representability] A function $f:\mathbb N^k\to\mathbb N$ is numeralwise represented in PA by a formula $F(x_1,\dots,x_k,y)$ if for all $n_1,\dots,n_k,m\in\mathbb N$: \begin{align*} f(n_1,\dots,n_k)=m &\implies \mathrm{PA}\vdash F(\overline{n_1},\dots,\overline{n_k},\overline m),\\ f(n_1,\dots,n_k)\ne m &\implies \mathrm{PA}\vdash \neg F(\overline{n_1},\dots,\overline{n_k},\overline m). \end{align*} [/definition] This notion asks PA to decide each concrete instance of the graph of $f$. A stronger version, often called functional representability, also asks PA to prove existence and uniqueness of the output for every input. [definition: Functional Representability] A function $f:\mathbb N^k\to\mathbb N$ is functionally represented in PA by a formula $F(x_1,\dots,x_k,y)$ if PA proves \begin{align*} \forall x_1\cdots\forall x_k\,\exists!y\,F(x_1,\dots,x_k,y), \end{align*} and $F$ numeralwise represents $f$. [/definition] The important test case is not an isolated arithmetic function such as addition, but the large family of mechanical syntactic operations needed to code formal proofs. Once formulas and derivations are replaced by natural numbers, PA must be able to recognize the corresponding primitive recursive checks inside its own language. The following representability theorem supplies exactly that bridge: every primitive recursive computation has an arithmetical formula whose behaviour PA can verify on numerals. [quotetheorem:4659] [citeproof:4659] This theorem is the technical reason arithmetic can talk about syntax. The primitive recursive hypothesis is essential because PA needs a formula whose finite verification steps can be mirrored by formal derivations; an arbitrary numerical function need not come with such a uniform finite recipe. The theorem is limited to functions and relations whose computation is primitive recursive, although many syntactic predicates needed for proof theory fall exactly into this class once a coding scheme has been fixed. Once formulas, terms, and derivations are coded by numbers, the operations "is a formula", "is an axiom", and "is a proof of" become representable, which is the bridge to incompleteness and formal consistency statements. [remark: Why Coding Enters] The representability theorem does not say that PA contains functions as objects. It says that the graph of a computable numerical operation can be expressed by a formula whose behaviour on numerals PA can verify. Gödel numbering turns syntactic operations into numerical operations, and representability then brings them into arithmetic. [/remark] ## Formal Proofs of Elementary Arithmetic The final problem is practical: what does a proof in PA look like when the statement is an ordinary arithmetic identity? The recursive axioms give immediate facts about the second argument of $+$ and $\cdot$, while facts about the first argument often require induction. [quotetheorem:4660] [citeproof:4660] Although this theorem is immediate, it is useful as a baseline. Its hypothesis-free character comes from the direction chosen in the recursive definition of addition: the axiom handles the second argument being $0$ directly. The limitation is that no corresponding axiom handles the first argument being $0$, so the superficially similar statement $\forall x\,(0+x=x)$ requires induction. This contrast is the first place where the formal asymmetry of the axioms produces a genuine proof obligation. [quotetheorem:4661] [citeproof:4661] This proof illustrates how PA turns ordinary recursive calculation into formal derivation. The induction hypothesis is needed because the recursive axiom for addition only rewrites terms whose second argument is a successor, so it gives no direct information about all terms of the form $0+x$. The result is limited to the particular identity proved; commutativity and associativity still require separate inductions. The same pattern will recur for multiplication, where identities about the first argument must be built from the right-recursive defining equations. [example: Deriving a Concrete Sum] PA proves $\overline{2}+\overline{2}=\overline{4}$. Since $\overline{2}=SS0$ and $\overline{4}=SSSS0$, it is enough to derive $SS0+SS0=SSSS0$. Apply the addition axiom $x+Sy=S(x+y)$ first with $x=SS0$ and $y=S0$, and then with $x=SS0$ and $y=0$: \begin{align*} SS0+SS0 &= SS0+S(S0)\\ &= S(SS0+S0)\\ &= S(S(SS0+0)). \end{align*} Now apply the addition axiom $x+0=x$ with $x=SS0$: \begin{align*} S(S(SS0+0)) &= S(S(SS0))\\ &= SSSS0. \end{align*} Combining the displayed equalities gives $SS0+SS0=SSSS0$, hence $\mathrm{PA}\vdash \overline{2}+\overline{2}=\overline{4}$. [/example] To prove associativity, it is helpful to isolate the exact formula used for induction. Since addition recurses on the second argument, the clean induction is on the third variable. [quotetheorem:4662] [citeproof:4662] The induction on $z$ is forced by the way addition was axiomatized: the defining equation directly controls the second input, so the outermost addition in $(x+y)+z$ can be unfolded along $z$. The theorem does not yet give commutativity, cancellation, or ordered arithmetic; it supplies only the reassociation rule needed to manage nested sums. Its importance is structural, since later multiplication proofs repeatedly reduce to sums where parentheses must be moved without changing the represented number. [example: Using Associativity Inside a Formal Derivation] Suppose a PA-derivation has already proved the instance of *Associativity of Addition in PA* \begin{align*} (x+y)+z=x+(y+z). \end{align*} By symmetry of equality, PA also derives \begin{align*} x+(y+z)=(x+y)+z. \end{align*} Substituting this equality into the context $u+0$ gives \begin{align*} (x+(y+z))+0=((x+y)+z)+0. \end{align*} Now combine this with the given line $((x+y)+z)+0=(x+y)+z$ and the associativity instance again: \begin{align*} (x+(y+z))+0 &=((x+y)+z)+0\\ &=(x+y)+z\\ &=x+(y+z). \end{align*} By transitivity of equality, PA derives $(x+(y+z))+0=x+(y+z)$. Thus a proved identity such as associativity can be reused inside later derivations by applying the ordinary equality rules of first-order logic. [/example] Multiplication follows the same pattern but depends on addition. Since multiplication is introduced recursively by $x\cdot 0=0$ and $x\cdot Sy=x\cdot y+x$, the immediate theorem is the right-zero law supplied directly by the defining axiom. [quotetheorem:4663] [citeproof:4663] As with addition, the theorem depends on the direction of the recursive definition: multiplication is specified by recursion in the second argument. It gives no immediate proof of $0\cdot x=0$, because that identity varies the recursive argument while fixing the first input. The next theorem shows how multiplication facts inherit earlier addition facts, and it marks the point where the hierarchy of formal arithmetic lemmas begins to matter. [quotetheorem:4664] [citeproof:4664] These examples reveal the proof-theoretic role of the recursive axioms. The induction hypothesis is necessary because the defining multiplication equation reduces $0\cdot Sx$ to $0\cdot x+0$, so the proof must already know the preceding case and must also use addition facts to simplify the resulting sum. The theorem is still only a zero law; distributivity, associativity, and commutativity of multiplication require further inductions and additional addition lemmas. This layered dependence is exactly what later arithmetization uses: complicated syntactic checks are reduced to primitive recursive clauses, and PA verifies them by repeated formal induction. ## Arithmetic as a Base Theory for Proof Theory The reason PA appears in proof theory is not only that it formalizes arithmetic. It is strong enough to formalize substantial pieces of syntax, so questions about proofs can be translated into questions about numbers. [definition: Arithmetization of Syntax] Let $\operatorname{Syn}$ be a specified set of syntactic objects, such as variables, terms, formulas, finite sequences of formulas, and derivations. An arithmetization of syntax is an injective map \begin{align*} \ulcorner\cdot\urcorner : \operatorname{Syn} \to \mathbb N \end{align*} together with numerical relations on $\mathbb N$ expressing the formation rules and proof rules for the chosen syntax. [/definition] The assignment is usually called a Gödel numbering. The exact coding is less important than its effectiveness: decoding immediate subformulas, checking whether a sequence is a derivation, and identifying the last formula of a proof must be primitive recursive or reducible to primitive recursive relations. [example: Proof Predicates] Fix a Gödel numbering of formulas and derivations, and let $\operatorname{Proof}_{\mathrm{PA}}(p,q)$ mean that $p$ codes a finite PA-derivation whose final formula has code $q$. For a fixed proof format, decoding $p$ gives a finite sequence of formula codes \begin{align*} \langle a_0,\dots,a_{n-1}\rangle. \end{align*} The relation $\operatorname{Proof}_{\mathrm{PA}}(p,q)$ is then the conjunction of the following numerical conditions: \begin{align*} &\operatorname{Seq}(p),\\ &\operatorname{Len}(p)=n \text{ for some } n>0,\\ &\operatorname{Entry}(p,n-1)=q,\\ &\forall i<n\,\operatorname{LineOK}(p,i). \end{align*} Here $\operatorname{LineOK}(p,i)$ says that the $i$-th line is justified. Writing $a_i=\operatorname{Entry}(p,i)$, this means \begin{align*} \operatorname{LineOK}(p,i) \end{align*} holds exactly when at least one of the following holds: \begin{align*} &\operatorname{LogicalAxiom}(a_i),\\ &\operatorname{PAAxiom}(a_i),\\ &\exists j<i\,\exists k<i\,\operatorname{MP}(a_j,a_k,a_i), \end{align*} where $\operatorname{MP}(r,s,t)$ expresses that $s$ codes the formula whose antecedent has code $r$ and whose consequent has code $t$. Since the bounds $i<n$, $j<i$, and $k<i$ are part of the coded finite sequence, checking the whole derivation is a finite numerical verification: decode the sequence, inspect its last entry, and verify each earlier line by one of the displayed clauses. The coding functions $\operatorname{Len}$ and $\operatorname{Entry}$, the syntactic predicates for formulas and axiomhood, and the bounded search over earlier lines are primitive recursive once the Gödel numbering and proof system are fixed. Therefore the relation $\operatorname{Proof}_{\mathrm{PA}}(p,q)$ is primitive recursive, and the *Basic Representability Theorem for Primitive Recursive Functions* gives an $\mathcal L_{\mathrm{PA}}$-formula representing it inside PA. Thus the external statement “$p$ is a PA-proof of the formula coded by $q$” becomes an arithmetic formula about the two numbers $p$ and $q$. [/example] The example also points to a boundary of the idea. The following remark, From Formal Arithmetic to Metatheorems, records that interpretation before the construction is used again. [remark: From Formal Arithmetic to Metatheorems] Arithmetization is the entry point to incompleteness and consistency results. A statement about the existence of a proof becomes an arithmetic statement of the form $\exists p\,\operatorname{Proof}_{\mathrm{PA}}(p,q)$. Chapters 11 and 12 analyze what PA and related theories can prove about such statements using the proof-theoretic tools developed earlier in the course. [/remark] The chapter main lesson is that PA is both a mathematical theory of the natural numbers and a formal environment for reasoning about proofs. Its induction schema gives controlled access to infinite reasoning, while representability turns finite computation and syntactic verification into arithmetic formulas. This combination is what makes arithmetic the standard base theory for modern proof-theoretic metamathematics. Arithmetic gives proof theory an internal language for syntax, computation, and induction. Chapter 11 uses that setting to revisit Gentzen's consistency proof, connecting cut elimination and transfinite induction to the question of why arithmetic is reliable. # 11. Ordinal Analysis and Gentzen's Consistency Proof This chapter connects the structural transformations of earlier chapters with the foundational question that motivated much of Hilbert's programme: can arithmetic justify its own reliability? It assumes familiarity with formal arithmetic from Chapter 10, sequent calculi from Chapter 6, cut elimination from Chapter 7, and Gödel's incompleteness theorems, which are recalled again in Chapter 12. The goal is to understand how Gentzen assigns ordinal measures to proof reductions, why the ordinal $\varepsilon_0$ appears, and how transfinite induction below $\varepsilon_0$ yields a consistency proof for Peano Arithmetic. Cut elimination and normalization showed that proofs can be simplified by local reductions, but Peano Arithmetic is strong enough to encode those reductions internally. Gentzen's insight was to measure proof reductions by ordinals below $\varepsilon_0$, and to prove termination using transfinite induction that goes beyond what Peano Arithmetic itself can justify. ## The Limit Imposed by Gödel's Second Incompleteness Theorem The first question is why a consistency proof for arithmetic cannot simply be formalized inside arithmetic. If Peano Arithmetic can reason about syntax, derivations, and primitive recursive proof checking, it can also express the statement that no derivation of contradiction exists. Gödel's second incompleteness theorem says that, assuming Peano Arithmetic is consistent, this internally expressed consistency statement is not provable in Peano Arithmetic. [definition: Arithmetized Consistency Statement] Let $\operatorname{Proof}_{\mathrm{PA}} \subset \mathbb N \times \mathbb N$ be a primitive recursive relation such that $\operatorname{Proof}_{\mathrm{PA}}(n,m)$ holds precisely when $n$ codes a Peano Arithmetic proof of the formula with Gödel number $m$. Let $\ulcorner 0=1\urcorner \in \mathbb N$ be the Gödel number of $0=1$. The arithmetized consistency statement for Peano Arithmetic is \begin{align*} \operatorname{Con}(\mathrm{PA}) := \forall n\, \neg \operatorname{Proof}_{\mathrm{PA}}(n,\ulcorner 0=1\urcorner). \end{align*} [/definition] This is not a semantic assertion written outside the system; it is a sentence of arithmetic. The point of arithmetization is that syntactic facts about proofs become number-theoretic facts about codes. In the form needed here, Gödel's second incompleteness theorem says: if Peano Arithmetic is consistent and the usual arithmetization of PA-provability is used, then PA does not prove $\operatorname{Con}(\mathrm{PA})$. More generally, a sufficiently strong, consistent, recursively axiomatized theory satisfying the standard derivability conditions cannot prove its own appropriately formalized consistency statement. This is the exact obstruction Gentzen's proof must avoid: the consistency argument cannot be one that Peano Arithmetic can formalize as a proof of its own arithmetized consistency statement. [remark: Meaning Of The Obstruction] Gödel's theorem does not say that Peano Arithmetic has no consistency proof in any sense. It says that no proof formalizable in Peano Arithmetic can establish the usual arithmetized consistency statement, provided Peano Arithmetic is consistent. A consistency proof may still be possible in a stronger metatheory, or in a framework using principles not reducible to Peano Arithmetic. [/remark] Gentzen's proof occupies exactly this space. It is finitistic in its manipulation of proof trees, but it invokes transfinite induction up to $\varepsilon_0$, a principle whose full strength is not provable in Peano Arithmetic. [example: Consistency As Absence Of A Coded Proof] Suppose the proof system for Peano Arithmetic has a Gödel coding, so each natural number $n$ is either decoded as a finite sequence \begin{align*} (\varphi_0,\varphi_1,\dots,\varphi_{k-1}) \end{align*} or rejected as not coding such a sequence. Define $\operatorname{Proof}_{\mathrm{PA}}(n,m)$ to hold exactly when the decoded sequence has final formula with Gödel number $m$ and every line is justified. More explicitly, for each $i<k$, the check requires one of the following: $\varphi_i$ is an axiom of PA, or there are earlier indices $j_1,\dots,j_\ell<i$ such that $\varphi_i$ follows from $\varphi_{j_1},\dots,\varphi_{j_\ell}$ by one of the finitely many inference rules. For the contradiction formula $0=1$, let $\ulcorner 0=1\urcorner$ be its Gödel number. Then the assertion that $n$ is not a PA-proof of contradiction is \begin{align*} \neg \operatorname{Proof}_{\mathrm{PA}}(n,\ulcorner 0=1\urcorner). \end{align*} Saying this for every possible code gives \begin{align*} \forall n\,\neg \operatorname{Proof}_{\mathrm{PA}}(n,\ulcorner 0=1\urcorner), \end{align*} which is precisely $\operatorname{Con}(\mathrm{PA})$. Thus the informal global claim “there is no PA-derivation of contradiction” becomes a single universal arithmetical sentence about natural-number codes. [/example] ## Transfinite Induction Below Epsilon Nought The next problem is how to justify termination of proof reductions when the reductions are not measured by ordinary natural numbers. Cut reduction may replace one proof by another whose local height is larger, so a simple induction on proof height is not enough. Gentzen's solution is to measure proofs by ordinals below a particular countable ordinal, then prove that every reduction strictly decreases that measure. [definition: Transfinite Induction Along A Well-Ordering] Let $(A,<)$ be a well-ordered set, and let $P(a)$ be a property of elements $a \in A$. Transfinite induction along $(A,<)$ is the principle \begin{align*} \left(\forall a \in A\,\left((\forall b<a\, P(b)) \implies P(a)\right)\right) \implies \forall a \in A\, P(a). \end{align*} [/definition] For $A=\mathbb N$, this is ordinary induction. For ordinal notations below $\varepsilon_0$, it permits induction over nested exponential patterns such as $\omega^{\omega^2}+\omega^5\cdot 3+7$. [definition: Epsilon Nought] The ordinal $\varepsilon_0$ is the least ordinal $\alpha$ satisfying \begin{align*} \omega^\alpha = \alpha. \end{align*} [/definition] Equivalently, $\varepsilon_0$ is the supremum of the sequence \begin{align*} \omega,\quad \omega^\omega,\quad \omega^{\omega^\omega},\quad \omega^{\omega^{\omega^\omega}},\quad \dots . \end{align*} The ordinals below $\varepsilon_0$ are exactly those obtained from $0$, addition, and exponentiation base $\omega$ after finitely many steps. This finite notation system is what makes Gentzen's argument computationally meaningful rather than a vague appeal to all countable ordinals. [definition: Cantor Normal Form Below Epsilon Nought] An ordinal $\alpha<\varepsilon_0$ is in Cantor normal form if it is written as \begin{align*} \alpha = \omega^{\alpha_1}c_1 + \omega^{\alpha_2}c_2 + \dots + \omega^{\alpha_k}c_k, \end{align*} where $k \in \mathbb N$, $c_1,\dots,c_k \in \mathbb N$, $c_i>0$, and \begin{align*} \alpha_1>\alpha_2>\dots>\alpha_k\geq 0. \end{align*} [/definition] Because each exponent $\alpha_i$ is again below $\varepsilon_0$, this definition is recursive. The recursion stops because only finitely many exponentiations and sums occur in any displayed notation. [quotetheorem:4665] [citeproof:4665] This normal form lets us compute comparisons effectively: compare leading exponents, then coefficients, then the remaining tail. The restriction to ordinals below $\varepsilon_0$ is essential here, because the exponents appearing in the notation are themselves governed by the same finite grammar and the recursion remains finitary. The theorem does not provide a notation system for all countable ordinals, nor does it say that every well-ordering relevant to proof theory has such a simple representation. Its role in Gentzen's argument is more specific: it supplies a canonical symbolic language in which proof reductions can be assigned measures and those measures can be compared by finite calculations. [example: Comparing Cantor Normal Forms] Consider \begin{align*} \alpha &= \omega^{\omega^2} + \omega^5\cdot 4 + \omega^2,\\ \beta &= \omega^{\omega^2} + \omega^5\cdot 3 + \omega^4. \end{align*} Both are in Cantor normal form, and their first term is the same: \begin{align*} \omega^{\omega^2}=\omega^{\omega^2}. \end{align*} The next exponent in both expressions is $5$, so the comparison moves to the corresponding finite coefficients: \begin{align*} 4>3. \end{align*} Equivalently, \begin{align*} \omega^5\cdot 4+\omega^2 &=\omega^5\cdot 3+\omega^5+\omega^2,\\ \omega^5\cdot 3+\omega^5+\omega^2 &>\omega^5\cdot 3+\omega^4, \end{align*} because $\omega^5>\omega^4$. Hence \begin{align*} \alpha>\beta. \end{align*} The lower terms $\omega^2$ and $\omega^4$ matter only after all earlier exponents and coefficients agree, so this example shows the lexicographic character of comparison in Cantor normal form. [/example] The comparison procedure is useful only because it is attached to a well-ordering. The obstruction in a termination proof is the possibility of an infinite chain of reductions with ever-smaller measures. The theorem below rules out exactly that possibility for ordinal notations below $\varepsilon_0$, turning strict ordinal decrease into a proof-theoretic termination argument. [quotetheorem:1460] [citeproof:1460] The phrase "standard ordering" matters: the theorem is about the intended ordering of the ordinal notation system, not about an arbitrary syntactic ordering of strings. The limitation to notations below $\varepsilon_0$ also matters, because Gentzen's assignment is designed so that every measure produced by the arithmetic reduction procedure lies inside this initial segment. Once these two facts are fixed, termination of reductions becomes a consequence of well-foundedness rather than a separate combinatorial argument. ## Ordinal Measures For Proof Reductions The final problem is to connect these ordinal calculations to actual derivations in arithmetic. A cut in a proof is an intermediate formula introduced and then immediately used, so cut elimination removes detours. In Peano Arithmetic, however, induction formulas and quantified cuts interact in ways that can increase proof height while reducing the logical complexity of the cut. [definition: Cut Rank] In a sequent calculus proof, the cut rank of a cut is the logical complexity of its cut formula, measured by the number and nesting depth of logical connectives and quantifiers in that formula. The cut rank of a proof is the maximum cut rank among cuts occurring in the proof. [/definition] The relevant measure cannot be just the number of cuts. A reduction may replace one cut by several simpler cuts, so the proof needs a well-founded measure in which a decrease in formula complexity outweighs a possible increase in proof size. [definition: Ordinal Assignment To A Proof] Let $\mathcal P$ be the set of proof trees in a fixed sequent calculus, and let $\mathcal O_{<\varepsilon_0}$ be the set of ordinal notations below $\varepsilon_0$ equipped with its standard ordering. An ordinal assignment for a proof reduction procedure $\rightsquigarrow$ on $\mathcal P$ is a map \begin{align*} o: \mathcal P \to \mathcal O_{<\varepsilon_0} \end{align*} such that every permitted reduction step $\pi\rightsquigarrow \pi'$ satisfies \begin{align*} o(\pi')<o(\pi). \end{align*} [/definition] Gentzen's construction assigns ordinals so that the outer exponent records high-level cut complexity, while lower terms record subsidiary height and multiplicity information. This mirrors the way Cantor normal form makes leading exponents dominate coefficients and later terms. [example: Informal Ordinal Descent In A Cut Reduction] Suppose a proof has a cut of rank $r+1$, where $r\in\mathbb N$, and its assigned ordinal measure begins with the dominant term $\omega^{r+1}$. If the reduction replaces that cut by five cuts of rank at most $r$, a typical new measure has the form $\omega^r\cdot 5+\beta$ with $\beta<\omega^r$. The decrease is visible from the ordinal calculation \begin{align*} \omega^r\cdot 5+\beta &< \omega^r\cdot 5+\omega^r && \text{because } \beta<\omega^r,\\ &= \omega^r\cdot 6,\\ &< \omega^r\cdot \omega && \text{because } 6<\omega,\\ &= \omega^{r+1}. \end{align*} Thus the reduced proof may contain more cuts, but all of them lie below the former dominant rank component. The example shows why an ordinal measure can decrease even when an ordinary natural-number count of cuts increases. [/example] The remaining issue is to know that this kind of local decrease can be arranged uniformly for every possible reduction step in a full PA proof. Cut elimination is not a single move, and some reductions duplicate subproofs or raise ordinary proof height, so a naive size measure cannot control the process. Gentzen's ordinal assignment is designed to survive exactly these complications: each permitted reduction must lower the assigned ordinal even when some finite features of the proof become larger. [quotetheorem:4666] [citeproof:4666] This theorem is the technical engine of the consistency proof. It is not a general theorem about every sequent calculus for arithmetic; it depends on the chosen presentation of induction, the precise reduction steps, and the matching ordinal assignment. Those choices are coordinated so that increases in proof height are always paid for by decreases in a more dominant ordinal component. The theorem therefore converts the syntactic process of reducing proofs into a descending sequence of ordinal notations, and the absence of infinite descending sequences supplies termination. ## Gentzen's Consistency Proof For Peano Arithmetic The central question is how termination of reductions yields consistency. If Peano Arithmetic had a proof of contradiction, then Gentzen's reductions would transform it until no cuts remained. A cut-free proof has the subformula property, and no cut-free proof of the empty or contradictory sequent exists from the arithmetic axioms in the relevant calculus. The result does not evade Gödel's theorem: it establishes consistency relative to a transfinite induction principle whose full uniform form is stronger than what Peano Arithmetic can prove. [quotetheorem:4667] [citeproof:4667] Thus the result is not an internal PA proof of $\operatorname{Con}(\mathrm{PA})$, but a metatheoretic reduction of PA consistency to the well-foundedness of the ordinal notation system below $\varepsilon_0$. The hypothesis about well-founded ordinal notation is doing real work: it rules out the infinite reduction path that would otherwise undermine the termination argument. This also explains why the theorem is compatible with incompleteness, since the consistency claim is obtained only after moving to a stronger metatheory. The distinction is exactly what makes the next question meaningful: whether $\varepsilon_0$ is merely sufficient for the argument, or whether it measures the exact proof-theoretic strength of Peano Arithmetic. [quotetheorem:4668] [citeproof:4668] This result gives a numerical summary of the strength of Peano Arithmetic. The ordinal $\varepsilon_0$ is not just a convenient bound for Gentzen's proof; it measures exactly how far ordinary induction over natural numbers can be iterated in arithmetically meaningful ways. [remark: What Ordinal Analysis Measures] Ordinal analysis assigns to a formal theory an ordinal that calibrates the transfinite induction principles needed to justify its proof reductions. For weak arithmetic theories the ordinals are smaller; for stronger theories of analysis and set existence the ordinals become much larger and require richer notation systems. The method turns consistency strength into a precise comparison problem. [/remark] For Peano Arithmetic, this calibration has a concrete form: any single ordinal notation below $\varepsilon_0$ can be analyzed by finitely many nested inductions, but the whole notation system cannot be mastered uniformly inside PA itself. [example: Why Peano Arithmetic Reaches All Fixed Levels Below Epsilon Nought] Let $\alpha=\omega^3+\omega\cdot 2+5$, and let $P(\xi)$ be an arithmetical property. To prove transfinite induction below this fixed $\alpha$, PA only has to follow the finite shape of the notation. Every ordinal below $\omega^3$ has the form \begin{align*} \xi=\omega^2 a+\omega b+c \end{align*} with $a,b,c\in\mathbb N$, and comparison is lexicographic in these coordinates: \begin{align*} \omega^2 a+\omega b+c<\omega^2 a'+\omega b'+c' \end{align*} exactly when either $a<a'$, or $a=a'$ and $b<b'$, or $a=a'$, $b=b'$, and $c<c'$. Thus PA can prove $P(\xi)$ for all $\xi<\omega^3$ by three nested ordinary inductions: \begin{align*} &\text{induct on }a,\\ &\quad \text{inside that, induct on }b,\\ &\quad\quad \text{inside that, induct on }c. \end{align*} At the stage $\omega^2 a+\omega b+c$, the transfinite induction hypothesis supplies $P(\eta)$ for every \begin{align*} \eta<\omega^2 a+\omega b+c, \end{align*} which means precisely the earlier cases \begin{align*} &\eta=\omega^2 a'+\omega b'+c' &&\text{with } a'<a,\\ &\eta=\omega^2 a+\omega b'+c' &&\text{with } b'<b,\\ &\eta=\omega^2 a+\omega b+c' &&\text{with } c'<c. \end{align*} These are exactly the hypotheses delivered by the outer, middle, and inner ordinary inductions. After $\omega^3$, the remaining part of $\alpha$ is \begin{align*} \omega\cdot 2+5. \end{align*} The block below $\omega^3+\omega\cdot 2$ consists of the two $\omega$-blocks \begin{align*} \omega^3+r \quad\text{and}\quad \omega^3+\omega+r \end{align*} with $r\in\mathbb N$. PA handles each block by one ordinary induction on $r$. Finally, the finite tail consists of the five cases \begin{align*} \omega^3+\omega\cdot 2,\quad \omega^3+\omega\cdot 2+1,\quad \omega^3+\omega\cdot 2+2,\quad \omega^3+\omega\cdot 2+3,\quad \omega^3+\omega\cdot 2+4, \end{align*} and these are checked one after another, each using the previously established cases as its induction hypotheses. The important point is that the notation $\omega^3+\omega\cdot 2+5$ is fixed, so this whole proof uses only finitely many ordinary inductions; PA can carry out that finite pattern, even though it cannot prove one uniform induction principle covering all notations below $\varepsilon_0$ at once. [/example] Gentzen's proof is therefore both a consistency proof and a boundary theorem. It shows that Peano Arithmetic can be justified from a transfinite induction principle just beyond its own internal reach, and it explains why $\varepsilon_0$ is the exact ordinal at which this justification stabilizes. Gentzen's argument shows that consistency can be measured by ordinal strength rather than by semantic intuition alone. Chapter 12 closes the course by linking proof theory to computability, asking what formal systems can decide, what they cannot, and how proof structure reflects computational limits. # 12. Proof Theory and Computability This final chapter brings together the proof-theoretic material developed earlier in the course with the computability-theoretic question of what formal systems can decide. We assume the preceding chapters on natural deduction, sequent calculus, soundness, completeness, normalization, and cut elimination, and we now ask what those structural theorems imply about algorithms. The central distinction is between finding a proof when one exists and recognizing in finite time that no proof exists. ## Proof Search, Decidability, and Semi-Decidability Can proof be found by mechanical search? Once derivations are finite syntactic objects, a proof system gives an immediate search space: enumerate candidate derivation trees, check whether each is correctly formed, and stop when a derivation of the target formula appears. The subtle question is whether failure can also be detected in finite time. [definition: Decision Procedure] A decision procedure for a set $S \subset \mathbb N$ is an algorithm which, on input $n \in \mathbb N$, halts and returns yes if $n \in S$, and halts and returns no if $n \notin S$. [/definition] A decision procedure gives two-sided information: both membership and non-membership are finitely recognizable. We need a separate notion for the one-sided situation produced by proof search, where finding a derivation is finite evidence for success but failing to find one so far is not finite evidence of failure. [definition: Semi-Decision Procedure] A semi-decision procedure for a set $S \subset \mathbb N$ is an algorithm which, on input $n \in \mathbb N$, halts and returns yes if $n \in S$, and does not halt or returns no without a uniform halting guarantee if $n \notin S$. [/definition] Semi-decidability is exactly the situation produced by naive proof search in a sound and complete proof system. If the formula is valid, completeness says that some finite derivation exists, and systematic enumeration will eventually find it. If the formula is invalid, the search may continue forever. [example: Enumerating Derivations] Fix a Hilbert, natural deduction, or sequent calculus presentation of first-order logic whose rule-checking relation is decidable. Choose an effective coding of finite labelled trees by natural numbers. On input a sentence $\varphi$, run through $0,1,2,\ldots$ in order. For each number $n$, first decide whether $n$ decodes to a finite labelled tree. If it does not, reject this $n$ and move to $n+1$. If it does, check, line by line or node by node, that every leaf is an allowed axiom or open assumption, every internal node follows from its immediate predecessors by one of the rules, and the root is labelled by $\varphi$. This gives a semi-decision procedure for derivability. If $\varphi$ is derivable, then there is some finite derivation tree $D$ with conclusion $\varphi$. Since the coding lists every finite tree, $D$ has some code $m \in \mathbb N$. When the enumeration reaches $m$, the decoding test succeeds, the rule checks succeed at every node of $D$, and the root check confirms that the conclusion is $\varphi$, so the procedure halts and answers yes. If $\varphi$ is not derivable, then no finite tree is a correct derivation of $\varphi$; hence each number either fails to decode as a derivation tree or decodes to a tree failing at least one axiom, rule, or root-label check. In that case the search has no successful code to find, so it may continue forever. [/example] The propositional case is better behaved because truth tables give a finite semantic search. We need to state why a formula with atoms $p_1,\dots,p_n$ can be decided by checking its $2^n$ valuations and comparing the result with validity. [quotetheorem:4669] [citeproof:4669] This theorem marks a boundary. The finiteness hypothesis is doing the essential work: a propositional formula mentions only finitely many atoms, and each atom has only two possible truth values. If formulas allowed infinitely many independent atoms in a single input, or if valuations ranged over infinite structures with quantifiers, the truth-table argument would no longer be a finite decision procedure. Thus propositional proof search can be replaced by finite semantic checking, while first-order quantifiers range over arbitrary domains and introduce an infinite semantic dimension. The bridge from truth in all structures to existence of a finite proof depends on completeness. Soundness is also essential: without it, the search might halt on invalid sentences because the proof system could derive false conclusions. The result does not give a decision procedure, because the absence of a proof is not detected by finite search; invalidity would require a uniform finite refutation method, and no such method exists for full first-order logic. [quotetheorem:4670] [citeproof:4670] After this theorem, first-order validity should be viewed as recursively enumerable rather than decidable. The finite object being searched for is a derivation, not a countermodel, and completeness guarantees only that such an object exists in the valid case. The limitation is therefore conceptual as well as practical: exhaustive proof search has a success condition, but it has no uniform stopping condition for invalid inputs. This semi-decision procedure leaves a serious asymmetry. When a sentence is valid, proof search eventually finds a derivation; when it is invalid, the same search may simply run forever with no signal that failure is permanent. One might hope to repair the situation by replacing proof search with a more clever semantic or syntactic algorithm, but the obstruction is deeper than the incompleteness of that particular search method. [quotetheorem:4671] [citeproof:4671] Church's theorem explains why complete proof systems do not make first-order logic decidable. Completeness gives eventual success on valid inputs, but the theorem says there is no algorithm which also settles all invalid inputs. The effectiveness of the translation from machines to sentences is essential: a non-computable assignment of sentences would not transfer undecidability. The result is also specific to sufficiently expressive first-order validity; restricted fragments, such as propositional logic or some monadic fragments, can still be decidable. [remark: Validity Versus Derivability] For a fixed recursively axiomatized complete proof system for first-order logic, validity and derivability define the same set of sentences. The set is semi-decidable because derivations are finite checkable objects. It is not decidable because the semantic problem of validity cannot be separated from invalidity by an algorithm. [/remark] ## Extracting Algorithms from Constructive Proofs When does a proof of existence tell us how to find the object whose existence is proved? In constructive proof systems, the rules are designed so that proving $\exists y\,R(x,y)$ requires enough information to produce a witness, and proving an implication gives a transformation from proofs of the antecedent to proofs of the consequent. [definition: Constructive Existence Proof] A constructive existence proof of $\exists y\,A(y)$ is a proof whose final existential introduction step provides a term $t$ and a proof of $A(t)$. [/definition] The important point is not merely the last step of a finished proof, since a proof may contain detours before normalization. The theorem below uses normalization to expose the final introduction form, making the computational witness visible. [quotetheorem:4672] [citeproof:4672] This property fails for classical logic in this direct form. A classical proof may establish $\exists y\,A(y)$ by contradiction without constructing any particular $y$; for example, it may prove $\neg\forall y\,\neg A(y)$ and then use double-negation principles to obtain the existential statement. The closedness assumption is also necessary, since open assumptions may contain parameters on which a witness depends. Constructive systems avoid that loss of information by restricting the use of principles such as excluded middle and double-negation elimination, so the next extraction results can read witnesses from normalized proofs. [example: Extracting a Witness Function] Suppose a closed intuitionistic natural-deduction derivation $\Pi$ proves \begin{align*} \forall x\,\exists y\,R(x,y), \end{align*} where $R$ is decidable. For an input term $a$, apply universal elimination to $\Pi$; the resulting derivation $\Pi_a$ has conclusion \begin{align*} \exists y\,R(a,y). \end{align*} Normalize $\Pi_a$. Normalization preserves the conclusion and introduces no new open assumptions, so the normalized derivation is still a closed proof of $\exists y\,R(a,y)$. Since a normal intuitionistic proof of an existential formula must end with existential introduction, its last step has the form \begin{align*} \frac{\Delta_a : R(a,t(a))}{\exists y\,R(a,y)}\ \exists I, \end{align*} for some term $t(a)$ and some derivation $\Delta_a$ of $R(a,t(a))$. Thus the proof determines the rule \begin{align*} a \longmapsto t(a). \end{align*} Define $f(a)=t(a)$. For each input $a$, the extracted subderivation $\Delta_a$ proves \begin{align*} R(a,f(a)), \end{align*} because $f(a)$ is exactly the witness term displayed in the final existential-introduction step. Decidability of $R$ is not what produces the witness; it lets the extracted output be checked against the specification $R(a,f(a))$. [/example] Program extraction needs a vocabulary for the computational evidence carried by a proof. Instead of saying only that a sentence is provable, realizability records which computational objects count as evidence for each logical form. [definition: Realizer] For a fixed constructive language and a fixed domain of computational objects $D$, a realizability interpretation is an assignment \begin{align*} A \longmapsto \operatorname{Real}(A) \subseteq D \end{align*} from formulas to sets of computational objects, defined by recursion on the logical form of $A$. An element $r \in \operatorname{Real}(A)$ is called a realizer of $A$. [/definition] The recursive clauses specify the computational shape of evidence: pairs realize conjunctions, tagged data realize disjunctions, functions realize implications, and witnesses together with realizers realize existential formulas. This gives a precise way to state when a normalized constructive proof actually computes the promised data. [quotetheorem:4673] [citeproof:4673] The theorem is a bridge between proof theory and computability. Normalization is needed because the computational witness may be hidden behind eliminations before the proof is reduced. Decidability of $R$ is not the source of the witness, but it ensures that the extracted output can be checked against the represented specification in the intended domain. The theorem does not say that every classical proof of a universal-existential sentence yields such an algorithm; classical principles may prove existence without giving uniform witnesses. This is why constructive mathematics is especially well suited to verified algorithm design: the proof object contains both a specification and a program meeting it. ## Normalization as Computation Why does normalization look like evaluation? In natural deduction, a detour occurs when a proof introduces a connective and then immediately eliminates it. In computation, the analogous situation is applying a freshly constructed function, pair, or case split to its consumer. [definition: Proof Reduction] For a fixed natural deduction system, a proof reduction is a partial map \begin{align*} \rho : \mathcal D \rightharpoonup \mathcal D \end{align*} from derivations to derivations, defined on derivations containing a specified introduction-elimination detour, such that $\rho(\Pi)$ has the same conclusion and the same undischarged assumptions as $\Pi$. [/definition] For implication, the detour has the same shape as beta-reduction. If a proof of $A \to B$ was obtained by assuming $A$ and deriving $B$, and it is immediately applied to a proof of $A$, reduction substitutes the proof of $A$ for the discharged assumption inside the derivation of $B$. [example: Implication Reduction and Function Application] Suppose the last two rules of a derivation have the form \begin{align*} \frac{ \frac{ [A]^u \quad \cdots \quad B }{ A \to B }\ \to I,u \qquad \Pi_A : A }{ B }\ \to E . \end{align*} Here $u$ names the temporary assumption $A$ discharged by $\to I$, and $\Pi_A$ is the supplied derivation of $A$. The reduction removes the introduction-elimination detour by substituting $\Pi_A$ for every open occurrence of the discharged assumption $u$ inside the derivation of $B$: \begin{align*} \frac{ \frac{ [A]^u \quad \cdots \quad B }{ A \to B }\ \to I,u \qquad \Pi_A : A }{ B }\ \to E \quad\rightsquigarrow\quad \bigl(\text{derivation of }B\text{ with each occurrence of }[A]^u\text{ replaced by }\Pi_A\bigr). \end{align*} The conclusion remains $B$, and the discharged assumption $u$ is no longer open; the only open assumptions left are those already open in the subderivation of $B$ other than $u$, together with the open assumptions of $\Pi_A$. Under the Curry-Howard reading, the subderivation from assumption $A$ to conclusion $B$ is represented by a term $M$ with free variable $x:A$, implication introduction is represented by $\lambda x.M$, and the derivation $\Pi_A$ is represented by a term $N:A$. The corresponding term reduction is \begin{align*} (\lambda x.M)N &\rightsquigarrow M[N/x], \end{align*} where $M[N/x]$ is obtained by replacing each free occurrence of $x$ in $M$ by $N$. Thus implication reduction is exactly beta-reduction at the level of proof terms: applying a freshly introduced implication immediately executes the substitution that the implication introduction had abstracted. [/example] The lambda-calculus comparison is not an analogy added after the fact; it is a precise correspondence between proof normalization and program evaluation. To use that correspondence systematically, one must specify how formulas become types, proofs become typed terms, and proof reductions become computation steps. [definition: Curry-Howard Correspondence] For a fixed intuitionistic proof system and a corresponding typed lambda calculus, the Curry-Howard correspondence consists of assignments \begin{align*} A &\longmapsto \tau_A,\\ \Pi : A &\longmapsto M_\Pi : \tau_A,\\ \Pi \rightsquigarrow \Pi' &\longmapsto M_\Pi \to M_{\Pi'} \end{align*} from formulas to types, proofs of $A$ to terms of type $\tau_A$, and proof-reduction steps to term-evaluation steps. [/definition] Under this correspondence, conjunction corresponds to product types, disjunction to sum types, implication to function types, truth to the unit type, and falsity to the empty type. Quantifiers correspond to dependent products and dependent sums in richer type theories. Once proofs have been translated into typed terms, normalization becomes a statement about evaluation. The theorem below gives the promised computational reading: normal proofs correspond to terms with no remaining reduction steps. [quotetheorem:4674] [citeproof:4674] This result explains the computational content of normalization theorems. The restriction to intuitionistic natural deduction is important because its introduction and elimination rules match the constructors and eliminators of typed lambda calculus. Adding unrestricted classical principles changes the computational interpretation, usually requiring control operators, continuations, or double-negation translations rather than the direct reading above. A normal proof is therefore a program in evaluated form only relative to the chosen proof-term calculus: it has no pending redexes corresponding to logical detours in that calculus. [example: Normalizing a Pair Projection] Suppose $\Pi_A$ is a derivation of $A$ and $\Pi_B$ is a derivation of $B$. First form the conjunction by $\wedge I$, and then immediately eliminate it by the second projection: \begin{align*} \frac{ \frac{ \Pi_A : A \qquad \Pi_B : B }{ A \wedge B }\ \wedge I }{ B }\ \wedge E_2 . \end{align*} The elimination rule $\wedge E_2$ uses only the right component of the conjunction, so the proof reduction deletes the introduced conjunction and leaves precisely the derivation that supplied the $B$-component: \begin{align*} \frac{ \frac{ \Pi_A : A \qquad \Pi_B : B }{ A \wedge B }\ \wedge I }{ B }\ \wedge E_2 \quad\rightsquigarrow\quad \Pi_B : B . \end{align*} Under the Curry-Howard reading, $\Pi_A$ is represented by a term $M:A$, $\Pi_B$ by a term $N:B$, conjunction introduction is represented by pairing, and second-conjunction elimination is represented by the second projection. Thus the corresponding proof-term reduction is \begin{align*} \pi_2(M,N) \rightsquigarrow N. \end{align*} The normalized proof has the same conclusion $B$, but it no longer contains the redundant step of constructing a pair only to project its second component. [/example] ## Undecidability, Incompleteness, and the Limits of Formal Proof What do undecidability and incompleteness say about the project of formalizing mathematics? They do not say that formal proof is unreliable; soundness and normalization results show the opposite for well-designed systems. They say that sufficiently expressive formal systems cannot simultaneously be computably axiomatized, consistent, and complete for all arithmetical truth. [definition: Recursively Axiomatized Theory] A theory $T$ is recursively axiomatized if there is an algorithm which decides whether a given sentence is an axiom of $T$. [/definition] For such a theory, derivability from $T$ is semi-decidable: enumerate finite derivations and check whether each line is either a logical axiom, a $T$-axiom, or follows by a rule. To ask whether the theory settles every sentence, we need a separate notion saying that each sentence or its negation is derivable. [definition: Syntactic Completeness] A theory $T$ is syntactically complete if, for every sentence $\varphi$ in its language, either $T \vdash \varphi$ or $T \vdash \neg \varphi$. [/definition] Syntactic completeness is a proof-theoretic property of a theory, not the same as semantic completeness of first-order logic. First-order semantic completeness says that validity coincides with derivability in pure logic. Gödel incompleteness says that particular effective theories of arithmetic cannot decide every arithmetical sentence without becoming inconsistent. The obstruction comes from combining enough arithmetic to encode computation with an effective list of axioms, because those two features let the theory speak about its own derivations. [quotetheorem:1506] [citeproof:1506] The theorem identifies a limit of proof search inside arithmetic. The set of theorems of $T$ is semi-decidable, but if $T$ is consistent and strong enough, it cannot decide every sentence of its language. The hypotheses are important: recursive axiomatizability makes the proof-search problem effective, while the strength assumption ensures that the theory can represent the relevant coding of syntax and computation. The conclusion is not that arithmetic is chaotic, but that no single consistent effective theory of sufficient strength captures every arithmetical truth by deciding each sentence or its negation. For Peano Arithmetic specifically, the second incompleteness theorem says that, if $\mathrm{PA}$ is consistent, then $\mathrm{PA}$ does not prove its usual arithmetized consistency sentence $\operatorname{Con}(\mathrm{PA})$. Gentzen's consistency proof for Peano Arithmetic is therefore proof-theoretic rather than contradictory to Gödel's theorem: it proves consistency using transfinite induction up to an ordinal not formalizable in the same way inside Peano Arithmetic itself. [example: Gentzen Consistency and the Second Incompleteness Theorem] Gentzen's argument proves $\operatorname{Con}(\mathrm{PA})$ from a principle stronger than Peano Arithmetic itself. To each proof $P$ in the chosen sequent calculus for $\mathrm{PA}$, Gentzen assigns an ordinal notation $o(P)$ with \begin{align*} o(P) &< \varepsilon_0. \end{align*} The reduction step for eliminating cuts is arranged so that whenever $P \rightsquigarrow P'$, the assigned ordinal strictly decreases: \begin{align*} P \rightsquigarrow P' \quad\Longrightarrow\quad o(P') < o(P) < \varepsilon_0. \end{align*} If $\mathrm{PA}$ were inconsistent, there would be a proof $P_0$ of contradiction. Repeated cut-reduction would then produce a sequence of proofs \begin{align*} P_0 \rightsquigarrow P_1 \rightsquigarrow P_2 \rightsquigarrow \cdots, \end{align*} and hence a strictly descending sequence of ordinal notations \begin{align*} o(P_0) &> o(P_1) > o(P_2) > \cdots,\\ o(P_i) &< \varepsilon_0 \quad \text{for every } i. \end{align*} Transfinite induction up to $\varepsilon_0$, equivalently the well-foundedness of the ordinal notations below $\varepsilon_0$, says that no such infinite descending sequence exists. Therefore the assumed proof of contradiction cannot exist, so the external argument proves \begin{align*} \operatorname{Con}(\mathrm{PA}). \end{align*} The point is that the needed well-foundedness principle for $\varepsilon_0$ is not available inside $\mathrm{PA}$ in the strength required to formalize the whole reduction argument. Thus Gentzen's proof establishes the consistency of $\mathrm{PA}$ from a stronger external standpoint, while *Gödel's Second Incompleteness Theorem* says that, if $\mathrm{PA}$ is consistent, $\mathrm{PA}$ itself does not prove $\operatorname{Con}(\mathrm{PA})$. [/example] This resolves a common misunderstanding: incompleteness is not a ban on consistency proofs. We need one final theorem to turn the same phenomenon into an algorithmic limitation on theoremhood itself: for strong effective theories, proof search cannot be converted into a total decision procedure. [quotetheorem:4675] [citeproof:4675] This theorem is different from the earlier semi-decidability statement. Recursive axiomatizability guarantees that proofs can be found by search, but consistency and arithmetic strength prevent this search from being upgraded to a total decision procedure. The strength hypothesis matters: weak decidable theories and finite fragments can have decidable theoremhood. The final lesson is that proof theory gives both positive and negative information. Normalization and cut elimination show that proofs have structure and computational content; undecidability and incompleteness show that no single effective formal calculus exhausts all mathematical truth in strong enough languages. [remark: The Course-Level Picture] Natural deduction made assumptions and discharge explicit. Sequent calculus made structural rules and cut visible. Normalization and cut elimination turned proofs into reducible objects. In this final chapter, those same transformations explain why constructive proofs compute, why proof search semi-decides validity, and why formal proof has principled limits. [/remark]