# proof theory > branch of mathematical logic **Wikidata**: [Q852732](https://www.wikidata.org/wiki/Q852732) **Wikipedia**: [English](https://en.wikipedia.org/wiki/Proof_theory) **Source**: https://4ort.xyz/entity/proof-theory ## Summary Proof theory is a branch of mathematical logic that studies the structure and properties of mathematical proofs, treating proofs themselves as mathematical objects subject to formal analysis. It focuses on understanding what can be proven, how proofs are constructed, and the relationships between different proof systems, playing a fundamental role in foundations of mathematics, automated reasoning, and theoretical computer science. ## Key Facts - **Field Classification**: Subfield of mathematics (parent: mathematical logic) - **Academic Discipline**: Mathematical logic (sitelink_count: 101) - **Instance Of**: Q11862829, Q4671286 (academic concepts) - **Subclass Of**: Q1166618 - **Wikipedia Title**: Proof theory - **Wikidata Description**: Branch of mathematical logic - **Sitelink Count**: 29 - **Aliases**: proof systems - **MathOverflow Tag**: https://mathoverflow.net/tags/proof-theory - **Library Classifications**: - LCC: QA9.54 - DDC: 511.36 - NLM: 4936 - **MSC Classification**: 03Fxx ## FAQs ### What is proof theory concerned with? Proof theory is concerned with analyzing the formal structure of mathematical proofs, treating proofs as syntactic objects that can be studied, compared, and transformed. It examines proof calculi, proof normalization, the relationship between different proof systems, and what theorems can be proved within given systems. ### Who are the key figures in proof theory? Foundational figures include Gerhard Gentzen (1909–1945), who developed sequent calculus and natural deduction; Jacques Herbrand (1908–1931), known for the Herbrand theorem; and Paul Lorenzen (1915–1994), who contributed to constructive proof theory. Later influential figures include Jean-Yves Girard (French logician), William Alvin Howard (American mathematician, known for the Curry-Howard correspondence), Georg Kreisel (1923–2015), Gaisi Takeuti (1926–2017), William Craig (1918–2016), T.M. Scanlon, and Sara Negri. ### How does proof theory relate to other fields? Proof theory is deeply connected to mathematical logic, theoretical computer science, and philosophy of mathematics. The Curry-Howard correspondence (Howard, Girard) establishes a fundamental link between proofs and programs, connecting proof theory to type theory and functional programming. It also relates to automated theorem proving, formal verification, and model theory. ### What are the main proof systems studied in proof theory? The main proof systems include natural deduction (developed by Gentzen), sequent calculus (Gentzen), Hilbert systems, and various specialized calculi. These systems are studied for their properties such as soundness, completeness, cut-elimination, and normalization. ### Is proof theory used in practical applications? Yes, proof theory underpins formal verification, automated theorem proving, proof assistants (like Coq, Lean, and Isabelle), and software verification. The theoretical foundations developed in proof theory enable rigorous checking of mathematical proofs and verification of hardware and software systems. ## Why It Matters Proof theory matters because it provides the foundational framework for understanding the nature of mathematical reasoning itself. By treating proofs as formal objects, it allows mathematicians and logicians to answer fundamental questions about what can be known, what assumptions are required to prove certain results, and how different mathematical theories relate to each other. The field has profound implications for the foundations of mathematics. Through results like Gödel's incompleteness theorems and Gentzen's consistency proofs, proof theory helped resolve fundamental questions about the limits of formal systems. The development of cut-elimination theorems and proof normalization procedures provided crucial insights into the constructive content of mathematical proofs. In computer science, proof theory has become indispensable through the Curry-Howard correspondence, which reveals that proofs and programs are two perspectives on the same underlying reality. This insight has revolutionized programming language theory, type systems, and formal verification. Modern proof assistants like Coq, Lean, and Agda directly apply proof-theoretic methods to verify complex mathematical theorems and ensure software correctness. The field also plays a critical role in philosophical debates about the foundations of mathematics, particularly regarding constructivism, finitism, and the nature of mathematical truth. Thinkers like Lorenzen contributed to constructive and dialogical approaches that view proofs as interactive processes rather than static objects. ## Notable For - **Foundational Contributions to Mathematical Logic**: Proof theory forms one of the four main pillars of mathematical logic alongside model theory, set theory, and recursion theory - **Curry-Howard Correspondence**: The fundamental insight connecting proofs to programs, independently discovered by William Alvin Howard and elaborated by Jean-Yves Girard - **Gentzen's Sequent Calculus**: A revolutionary proof formalism that enabled major advances in structural proof theory and automated reasoning - **Cut-Elimination Theorem**: A central result showing that proofs can be normalized without cuts, with profound implications for proof search and proof analysis - **Dialectica Interpretation**: Gödel's functional interpretation, developed by Kreisel, connecting intuitionistic arithmetic to primitive recursive functionals - **Proof Analysis**: Methods developed by Sara Negri and others for analyzing proofs in formal systems and extracting constructive content - **Substructural Logics**: Proof theory has driven the development of logics like linear logic (Girard) where structural rules can be controlled ## Body ### Historical Development Proof theory emerged as a distinct discipline in the early 20th century, primarily through the work of Gerhard Gentzen, whose 1934 doctoral dissertation introduced both natural deduction and sequent calculus. Gentzen's work provided new formalisms for representing logical inference that were more natural for human reasoning than the Hilbert-style axiomatic systems previously used. His consistency proof for elementary number theory, completed in 1936, represented a landmark achievement in the foundations of mathematics. Jacques Herbrand's work in the late 1920s and early 1930s laid crucial groundwork through the Herbrand theorem, which established a connection between first-order logic and propositional logic and became fundamental to automated theorem proving. Jan Śleszyński, a Polish mathematician, contributed to the early development of proof-theoretic ideas, particularly in the area of logical foundations. The post-war period saw significant expansion of the field. Paul Lorenzen developed dialogical logic and contributed to constructive proof theory, emphasizing the procedural aspects of mathematical reasoning. Georg Kreisel's work in the 1950s and 1960s advanced the understanding of proof interpretation and functional interpretations, including the famous Kreisel's interpretation. ### Key Figures and Their Contributions The development of proof theory has been driven by numerous influential mathematicians and logicians: **Gerhard Gentzen (1909–1945)**: Created natural deduction and sequent calculus, developed cut-elimination theorems, and produced consistency proofs for arithmetic. His work remains foundational to modern proof theory. **Jean-Yves Girard**: Developed linear logic, a substructural logic that refines classical and intuitionistic logic by controlling the use of structural rules. His work on proof theory and type theory has been enormously influential. **William Alvin Howard**: Formulated the Curry-Howard correspondence, demonstrating the deep connection between natural deduction and lambda calculus, between proofs and programs. **Gaisi Takeuti (1926–2017)**: Made fundamental contributions to proof theory, particularly in ordinal analysis and the study of proof-theoretic strength of mathematical theories. **William Craig (1918–2016)**: Known for the Craig interpolation theorem and work on proof theory and model theory. **T.M. Scanlon**: Contributed to proof theory and philosophical logic, particularly in areas connecting formal logic to moral and political philosophy. **Sara Negri**: Known for work on structural proof theory, proof analysis, and the development of methods for extracting constructive content from classical proofs. ### Theoretical Foundations Proof theory studies formal systems for representing logical inference. The main calculi include: **Natural Deduction**: Developed by Gentzen, it provides rules for each logical connective that mirror natural reasoning patterns. The system has introduction and elimination rules for each operator, with the property that proofs can be normalized. **Sequent Calculus**: Also developed by Gentzen, it uses sequents (assertions of the form Γ ⊢ Δ meaning "from premises Γ conclude conclusions Δ") and provides a symmetric treatment of conjunction and disjunction. The sequent calculus is particularly important for proof search and cut-elimination. **Hilbert Systems**: Traditional axiomatic systems using axiom schemes and modus ponens. While less natural for human use, they are important for foundational studies. The central meta-theoretic results include: - **Cut-Elimination**: The theorem that any proof can be transformed into a cut-free proof, showing that cuts are not essential for provability - **Normalization**: The property that proofs can be reduced to a canonical form - **Completeness**: Various completeness results connecting provability in formal systems to semantic notions of truth ### Connections to Other Fields **Mathematical Logic**: Proof theory is one of the four main areas of mathematical logic. It complements model theory (which studies the semantic interpretation of logical languages), set theory (which studies collections and infinity), and recursion theory (which studies computability). **Type Theory and Programming Languages**: The Curry-Howard correspondence establishes that types correspond to propositions and programs to proofs. This has driven developments in functional programming, type systems, and proof assistants. **Automated Reasoning**: Proof-theoretic methods underlie algorithms for automated theorem proving, including resolution, tableau methods, and proof search in sequent calculi. **Philosophy of Mathematics**: Proof theory contributes to debates about constructivism, finitism, and the foundations of mathematics. The proof-theoretic analysis of mathematical theories provides measures of their constructive content. ### Classification and Identifiers Proof theory is classified under multiple systems: - **Library of Congress Classification**: QA9.54 - **Dewey Decimal Classification**: 511.36 - **National Library of Medicine**: 4936 - **Mathematical Subject Classification**: 03Fxx - **Wikidata**: Q11862829 (academic concept), Q4671286 (formal science) - **Freebase**: /m/0191r1 - **GND**: 4145177-6 - **LCCN**: sh85107437 - **BNF**: 122670310 - **NDL**: 01190375 ### Modern Applications Contemporary proof theory finds application in: **Formal Verification**: Tools like Coq, Lean, Isabelle, and Agda use proof-theoretic foundations to verify mathematical theorems and software/hardware correctness. **Proof Assistants**: Modern proof assistants implement type theory based on the Curry-Howard correspondence, allowing users to write programs that double as mathematical proofs. **Software Verification**: Formal methods for verifying that software behaves correctly rely on proof-theoretic foundations to ensure that verification results are mathematically sound. **Mathematical Knowledge Management**: Proof theory provides frameworks for representing, checking, and transmitting mathematical knowledge in formal systems. ### Related Concepts and Fields Proof theory connects to numerous related areas within mathematics and computer science: - **Model Theory**: Studies the semantic interpretation of logical languages; complementary to proof-theoretic approaches - **Set Theory**: Provides foundational frameworks for mathematics; proof-theoretic analysis can measure the strength of set-theoretic axioms - **Recursion Theory**: Studies computability; connections to proof theory through Gödel's incompleteness theorems - **Category Theory**: Provides abstract frameworks for understanding mathematical structures, including those arising in proof theory - **Intuitionistic Logic**: A constructive logic that rejects certain classical principles; proof theory for intuitionistic systems is particularly well-developed - **Linear Logic**: A substructural logic developed by Girard where resources are tracked; exemplifies how proof-theoretic considerations drive logical development ## References 1. [Nuovo soggettario](https://thes.bncf.firenze.sbn.it/termine.php?id=4936) 2. Nuovo soggettario 3. Freebase Data Dumps. 2013 4. Integrated Authority File 5. YSO-Wikidata mapping project 6. National Library of Israel 7. KBpedia 8. [OpenAlex](https://docs.openalex.org/download-snapshot/snapshot-data-format)