An Introduction to Proof Theory: Normalization, Cut-Elimination, and Consistency Proofs
Paolo Mancosu, Sergio Galvan, and Richard Zach
Abstract
Proof theory is a central area of mathematical logic of special interest to philosophy. It has its roots in the foundational debate of the 1920s, in particular, in Hilbert’s program in the philosophy of mathematics, which called for a formalization of mathematics, as well as for a proof, using philosophically unproblematic, “finitary” means, that these systems are free from contradiction. Structural proof theory investigates the structure and properties of proofs in different formal deductive systems, including axiomatic derivations, natural deduction, and the sequent calculus. Central results ... More
Proof theory is a central area of mathematical logic of special interest to philosophy. It has its roots in the foundational debate of the 1920s, in particular, in Hilbert’s program in the philosophy of mathematics, which called for a formalization of mathematics, as well as for a proof, using philosophically unproblematic, “finitary” means, that these systems are free from contradiction. Structural proof theory investigates the structure and properties of proofs in different formal deductive systems, including axiomatic derivations, natural deduction, and the sequent calculus. Central results in structural proof theory are the normalization theorem for natural deduction, proved here for both intuitionistic and classical logic, and the cut-elimination theorem for the sequent calculus. In formal systems of number theory formulated in the sequent calculus, the induction rule plays a central role. It can be eliminated from proofs of sequents of a certain elementary form: every proof of an atomic sequent can be transformed into a “simple” proof. This is Hilbert’s central idea for giving finitary consistency proofs. The proof requires a measure of proof complexity called an ordinal notation. The branch of proof theory dealing with mathematical systems such as arithmetic thus has come to be called ordinal proof theory. The theory of ordinal notations is developed here in purely combinatorial terms, and the consistency proof for arithmetic presented in detail.
Keywords:
proof theory,
consistency proof,
proof transformation,
ordinal notation,
inductive proof,
formalization of mathematics,
philosophy of mathematics,
Hilbert’s program,
Gerhard Gentzen
Bibliographic Information
| Print publication date: 2021 |
Print ISBN-13: 9780192895936 |
| Published to Oxford Scholarship Online: October 2021 |
DOI:10.1093/oso/9780192895936.001.0001 |
Authors
Affiliations are at time of print publication.
Paolo Mancosu, author
Willis S. and Marion Slusser Professor of Philosophy, University of California at Berkeley
Sergio Galvan, author
Emeritus Professor of Logic, Catholic University of Milan
Richard Zach, author
Professor of Philosophy, University of Calgary
More
Less
