Introduction to Proof Theory

Foundations of Proof Theory Introduction Proof theory is a branch of mathematical logic that studies proofs themselves as mathematical objects. Rather than asking whether a statement is true in the real world, proof theory asks: how can we demonstrate truth by manipulating symbols according to precise, formal rules? This shift in perspective—treating proofs as things to be studied rather than just tools for establishing truth—opens up entirely new questions about the nature of reasoning itself. What is a Formal Proof? A formal proof is a finite sequence of formulas (logical statements) that ends with the statement we wish to prove. Each formula in this sequence must satisfy one of two conditions: it is either an axiom (a formula we accept as true without proof), or it follows from earlier formulas by applying an inference rule (a precise rule that allows us to derive new formulas from old ones). Think of it like building with blocks. You start with certain blocks that are given to you (your axioms), and then you can stack and combine them according to specific construction rules (your inference rules) until you've built the structure you wanted (your conclusion). The key difference between a formal proof and an informal mathematical proof is precision. In informal proofs, mathematicians often skip steps, appeal to intuition, or use language that isn't completely rigorous. In formal proofs, every single step must be justified by an axiom or an explicitly stated inference rule—there is no room for shortcuts. Formal Systems: The Framework for Proofs Before we can write formal proofs, we need a formal system—a precisely defined framework that tells us what symbols we're working with and what we're allowed to do with them. A formal system consists of four essential components: A set of symbols: These are the basic building blocks we use to write formulas (like the symbols for logical connectives: $\land$ for "and," $\lor$ for "or," $\neg$ for "not"). Formation rules: These rules tell us which sequences of symbols count as well-formed formulas. For example, "$p \land q$" is well-formed, but "$\land p$" is not. A set of axioms: These are formulas we accept as true starting points. They're the foundation upon which all proofs rest. A set of inference rules: These rules specify how we can transform one or more formulas into a new formula. For instance, an inference rule might say: "If you have both $p$ and $p \to q$, then you can derive $q$." Two classic formal systems are propositional logic (which deals with simple logical combinations of statements) and first-order predicate logic (which also allows quantifiers like "for all" and "there exists"). Multiple Ways to Prove the Same Thing: Proof Calculi Here's an important insight: any given formal system can be presented in multiple different ways. Each way is called a proof calculus, and each provides a different "style" for constructing proofs. Think of proof calculi like different notational systems for arithmetic. You can add two numbers using the standard algorithm, or using an abacus, or using your fingers—the underlying mathematics is the same, but the method of doing the calculation differs. Similarly, different proof calculi for the same logical system will all be capable of proving the same statements, but they give you different tools for doing so. Why does this matter? Different proof calculi are convenient for different purposes. Some are easy to use for actually writing out proofs. Others are better suited for mathematical analysis of proofs themselves. By studying multiple calculi, we get richer insights into the structure of logical reasoning. Natural Deduction: Reasoning Like a Mathematician Natural deduction is a proof calculus designed to mimic how mathematicians actually reason informally. It feels intuitive because it structures reasoning around the logical connectives themselves. The key idea is that for each logical connective ($\land$, $\lor$, $\to$, $\neg$, etc.), natural deduction provides: An introduction rule that tells you how to prove a statement using that connective An elimination rule that tells you how to use a statement containing that connective to derive something else For example, the introduction rule for conjunction ($\land$) says: if you can prove $p$ and you can prove $q$, then you can prove $p \land q$. The elimination rule says: if you have already proved $p \land q$, then you can use this to derive both $p$ and $q$ separately. This structure makes natural deduction feel natural—it matches how we think about logical reasoning. However, as we'll see later, other proof calculi have advantages for certain theoretical analyses. Sequent Calculus: A More Structural Approach Sequent calculus is another fundamental proof calculus, introduced by mathematician Gerhard Gentzen. It takes a more structural approach to reasoning. The basic object in sequent calculus is called a sequent, written as: $$\Gamma \Rightarrow \Delta$$ Here, $\Gamma$ is a sequence of formulas (the antecedents or premises), and $\Delta$ is a sequence of formulas (the consequents). The sequent expresses: "From the antecedents $\Gamma$, one can infer the consequents $\Delta$." The inference rules in sequent calculus operate on these sequents directly. For instance, there are rules that add formulas to the left side, rules that add formulas to the right side, and so on. While sequent calculus may initially seem more alien than natural deduction, it reveals deep structural properties of proofs that natural deduction can obscure. This makes it invaluable for theoretical analysis. The Cut Rule: Composing Proofs One of the most important features of sequent calculus is the cut rule. This rule allows you to compose two proofs by introducing an intermediate formula. Suppose you have: A proof of $\Gamma \Rightarrow A$ (showing that $A$ follows from $\Gamma$) A proof of $A, \Delta \Rightarrow \Phi$ (showing that $\Phi$ follows from $A$ and $\Delta$) The cut rule lets you combine these into a proof of $\Gamma, \Delta \Rightarrow \Phi$ by "cutting out" the intermediate formula $A$. This is very natural from a mathematical perspective—it's how we usually compose arguments. However, the presence of the cut rule creates a puzzle: it seems to require this intermediate step, but is that step really necessary? Cut-Elimination: A Surprising Theorem Here's one of the most elegant results in proof theory: Gentzen's cut-elimination theorem states that any proof using the cut rule can be transformed into a cut-free proof (a proof that doesn't use the cut rule at all). This is surprising because it means the cut rule, while convenient, is not actually necessary. Any statement provable with cut is also provable without it. The significance of this result cannot be overstated. Cut-elimination: Reveals hidden structure: The process of eliminating cuts often exposes combinatorial properties of proofs that would otherwise be hidden Simplifies theoretical arguments: Many consistency proofs and other meta-theoretical results become cleaner once we restrict to cut-free proofs Provides constructive consistency proofs: For arithmetic and other foundational systems, cut-elimination can give constructive proofs that the system is consistent (doesn't contain contradictions) The cut-elimination process essentially shows that the "shortcuts" the cut rule provides can always be replaced with more direct arguments—the long way around always exists. Key Theorems: Consistency and Completeness Two fundamental theorems in proof theory concern the relationship between our formal systems and the truths we care about. Consistency means that a formal system cannot prove both a statement and its negation. In other words, no contradiction can be derived. A consistent system is not "broken"—it doesn't prove everything, and it doesn't prove falsehoods. Completeness (in the proof-theoretic sense) means that if a statement is true in every possible interpretation or every possible model, then there exists a formal proof of it within our system. In other words, our proof rules are powerful enough to capture all the semantic truths. Gödel's completeness theorem (for first-order logic) is a landmark result showing that first-order logic is indeed complete: any statement that is semantically valid (true in all models) can be formally proved. This demonstrates a beautiful correspondence between what is syntactically provable (derivable using our formal rules) and what is semantically true (true in all interpretations). This relationship between syntax (the formal rules) and semantics (the meaning and truth conditions) is central to understanding what proofs really accomplish. The Curry–Howard Isomorphism: Proofs as Programs One of the most profound discoveries in logic is the Curry–Howard isomorphism, which establishes a deep correspondence between two seemingly unrelated areas: Proofs in logic (constructing formal derivations of statements) Programs in typed functional programming (writing code with specific type annotations) The isomorphism states that these are actually the same thing, viewed from different perspectives. Specifically: A logical formula corresponds to a type in a programming language A proof of that formula corresponds to a program (or "term") of that type The inference rules of logic correspond to the code construction rules of the language For example, a proof that "$A \land B$" follows from hypotheses corresponds to a function that, given inputs of type $A$ and type $B$, produces an output. The proof is the program; the program is the proof. Why is this important? This isomorphism bridges logic and computation: Proof assistants like Coq and Agda use this correspondence to allow mathematicians to write formal proofs that are simultaneously executable programs. This enables verification of both mathematical theorems and software correctness in a unified framework. Type system design in modern programming languages is informed by this correspondence, making type systems more expressive and reliable. Automated theorem proving harnesses proof-theoretic ideas to develop systems that can search for and verify proofs automatically. The Curry–Howard isomorphism reveals that proof theory is not just about abstract logical truth—it connects to computation, programming, and the foundations of computer science itself. Summary: Why Proof Theory Matters Proof theory asks fundamental questions: When does a proof exist for a given statement? How long must a proof be? Can one proof be transformed into another? What do the structural properties of proofs tell us about logic itself? By studying proofs as mathematical objects, proof theory reveals the deep architecture of reasoning. It connects syntax to semantics, logic to computation, and abstract mathematical principles to practical applications in computer science. Whether you're verifying software with proof assistants, understanding the foundations of mathematics, or designing better programming languages, proof theory provides the essential framework.