An Introduction to Proof Theory: Normalization, Cut-Elimination, and Consistency Proofs

Oxford: Oxford University Press. Edited by Sergio Galvan & Richard Zach (2021)
  Copy   BIBTEX

Abstract

An Introduction to Proof Theory provides an accessible introduction to the theory of proofs, with details of proofs worked out and examples and exercises to aid the reader's understanding. It also serves as a companion to reading the original pathbreaking articles by Gerhard Gentzen. The first half covers topics in structural proof theory, including the Gödel-Gentzen translation of classical into intuitionistic logic, natural deduction and the normalization theorems, the sequent calculus, including cut-elimination and mid-sequent theorems, and various applications of these results. The second half examines ordinal proof theory, specifically Gentzen's consistency proof for first-order Peano Arithmetic. The theory of ordinal notations and other elements of ordinal theory are developed from scratch, and no knowledge of set theory is presumed. The proof methods needed to establish proof-theoretic results, especially proof by induction, are introduced in stages throughout the text. Mancosu, Galvan, and Zach's introduction will provide a solid foundation for those looking to understand this central area of mathematical logic and the philosophy of mathematics.

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 91,349

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

Similar books and articles

A Simple Proof that Super-Consistency Implies Cut Elimination.Gilles Dowek & Olivier Hermant - 2012 - Notre Dame Journal of Formal Logic 53 (4):439-456.
A note on the proof theory the λII-calculus.David J. Pym - 1995 - Studia Logica 54 (2):199 - 230.
An Analytic Calculus for the Intuitionistic Logic of Proofs.Brian Hill & Francesca Poggiolesi - 2019 - Notre Dame Journal of Formal Logic 60 (3):353-393.
Canonical proof nets for classical logic.Richard McKinley - 2013 - Annals of Pure and Applied Logic 164 (6):702-732.
A Formalization Of Sambins's Normalization For Gl.Edward Hauesler & Luiz Carlos Pereira - 1993 - Mathematical Logic Quarterly 39 (1):133-142.
Reprint of: A more general general proof theory.Heinrich Wansing - 2017 - Journal of Applied Logic 25:23-46.
Identity of proofs based on normalization and generality.Kosta Došen - 2003 - Bulletin of Symbolic Logic 9 (4):477-503.
Gentzen's proof systems: byproducts in a work of genius.Jan von Plato - 2012 - Bulletin of Symbolic Logic 18 (3):313-367.
Cut-elimination and proof-search for bi-intuitionistic logic using nested sequents.Rajeev Goré, Linda Postniece & Alwen Tiu - 1998 - In Marcus Kracht, Maarten de Rijke, Heinrich Wansing & Michael Zakharyaschev (eds.), Advances in Modal Logic. CSLI Publications. pp. 43-66.

Analytics

Added to PP
2021-08-03

Downloads
77 (#211,098)

6 months
21 (#122,177)

Historical graph of downloads
How can I increase my downloads?

Author Profiles

Richard Zach
University of Calgary
Paolo Mancosu
University of California, Berkeley

References found in this work

No references found.

Add more references