Pure Proof Theory. Mathematicians are interested in structures. There is only one way to find the theorems of a structure. Start with an axiom system for the structure and deduce the theorems logically. These axiom systems are the objects of proof-theoretical research. Studying axiom systems there is a series of more [Book Review]

Bulletin of Symbolic Logic 2 (2):159-188 (1996)

Abstract

Apologies. The purpose of the following talk is to give an overview of the present state of aims, methods and results in Pure Proof Theory. Shortage of time forces me to concentrate on my very personal views. This entails that I will emphasize the work which I know best, i.e., work that has been done in the triangle Stanford, Munich and Münster. I am of course well aware that there are as important results coming from outside this triangle and I apologize for not displaying these results as well.Moreover the audience should be aware that in some points I have to oversimplify matters. Those who complain about that are invited to consult the original papers.1.1. General. Proof theory startedwithHilbert's Programme which aimed at a finitistic consistency proof for mathematics.By Gödel's Theorems, however, we know that we can neither formalize all mathematics nor even prove the consistency of formalized fragments by finitistic means. Inspite of this fact I want to give some reasons why I consider proof theory in the style of Gentzen's work still as an important and exciting field of Mathematical Logic. I will not go into applications of Gentzen's cut-elimination technique to computer science problems—this may be considered as applied proof theory—but want to concentrate on metamathematical problems and results. In this sense I am talking about Pure Proof Theory.Mathematicians are interested in structures. There is only one way to find the theorems of a structure. Start with an axiom system for the structure and deduce the theorems logically. These axiom systems are the objects of proof-theoretical research. Studying axiom systems there is a series of more or less obvious questions.

Other Versions

PhilArchive

Upload a copy of this work     Papers currently archived: 95,443

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

Similar books and articles

Pure proof theory aims, methods and results.Wolfram Pohlers - 1996 - Bulletin of Symbolic Logic 2 (2):159-188.
x1. Aims.Wolfram Pohlers - 1996 - Bulletin of Symbolic Logic 2 (2):159-188.
The strength of extensionality I—weak weak set theories with infinity.Kentaro Sato - 2009 - Annals of Pure and Applied Logic 157 (2-3):234-268.
Direct Proofs of Lindenbaum Conditionals.René Gazzari - 2014 - Logica Universalis 8 (3-4):321-343.
Determinate logic and the Axiom of Choice.J. P. Aguilera - 2020 - Annals of Pure and Applied Logic 171 (2):102745.
Structural Proof Theory.Sara Negri, Jan von Plato & Aarne Ranta - 2001 - New York: Cambridge University Press. Edited by Jan Von Plato.
A relative consistency proof.Joseph R. Shoenfield - 1954 - Journal of Symbolic Logic 19 (1):21-28.
An Introduction to Proof Theory: Normalization, Cut-Elimination, and Consistency Proofs.Paolo Mancosu, Sergio Galvan & Richard Zach - 2021 - Oxford: Oxford University Press. Edited by Sergio Galvan & Richard Zach.
Cut-Elimination for Simple Type Theory with an Axiom of Choice.G. Mints - 1999 - Journal of Symbolic Logic 64 (2):479-485.

2014-01-21

37 (#435,018)

6 months
2 (#1,505,662)

Author's Profile

Wolfram Pohlers
University of Muenster

Citations of this work

Proof theory for theories of ordinals II: Π3-reflection.Toshiyasu Arai - 2004 - Annals of Pure and Applied Logic 129 (1-3):39-92.

References found in this work

Systems of predicative analysis.Solomon Feferman - 1964 - Journal of Symbolic Logic 29 (1):1-30.
Proof theory of reflection.Michael Rathjen - 1994 - Annals of Pure and Applied Logic 68 (2):181-224.
Proof theory and ordinal analysis.W. Pohlers - 1991 - Archive for Mathematical Logic 30 (5-6):311-376.