Switch to: References

Citations of:

Pure proof theory aims, methods and results

Wolfram Pohlers

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

Add citations

You must login to add citations.

Mathematical Infinity, Its Inventors, Discoverers, Detractors, Defenders, Masters, Victims, Users, and Spectators.Edward G. Belaga - manuscriptdetails "The definitive clarification of the nature of the infinite has become necessary, not merely for the special interests of the individual sciences, but rather for the honour of the human understanding itself. The infinite has always stirred the emotions of mankind more deeply than any other question; the infinite has stimulated and fertilized reason as few other ideas have ; but also the infinite, more than other notion, is in need of clarification." (David Hilbert 1925). Download Export citation Bookmark
Mathematical proof theory in the light of ordinal analysis.Reinhard Kahle - 2002 - Synthese 133 (1/2):237 - 255.details We give an overview of recent results in ordinal analysis. Therefore, we discuss the different frameworks used in mathematical proof-theory, namely "subsystem of analysis" including "reverse mathematics", "Kripke-Platek set theory", "explicit mathematics", "theories of inductive definitions", "constructive set theory", and "Martin-Löf's type theory". Download Export citation Bookmark
(1 other version)Proof theory for theories of ordinals II: Π3-reflection.Toshiyasu Arai - 2004 - Annals of Pure and Applied Logic 129 (1-3):39-92.details This paper deals with a proof theory for a theory T3 of Π3-reflecting ordinals using the system O of ordinal diagrams in Arai 1375). This is a sequel to the previous one 1) in which a theory for recursively Mahlo ordinals is analyzed proof-theoretically. Download Export citation Bookmark 12 citations
(1 other version)How is it that infinitary methods can be applied to finitary mathematics? Gödel's T: a case study.Andreas Weiermann - 1998 - Journal of Symbolic Logic 63 (4):1348-1370.details Inspired by Pohlers' local predicativity approach to Pure Proof Theory and Howard's ordinal analysis of bar recursion of type zero we present a short, technically smooth and constructive strong normalization proof for Gödel's system T of primitive recursive functionals of finite types by constructing an ε 0 -recursive function [] 0 : T → ω so that a reduces to b implies [a] $_0 > [b]_0$ . The construction of [] 0 is based on a careful analysis of the Howard-Schütte (...) Download Export citation Bookmark 7 citations
(1 other version)Proof theory for theories of ordinals II:< i> Π_< sub> 3-reflection.Toshiyasu Arai - 2004 - Annals of Pure and Applied Logic 129 (1):39-92.details Download Export citation Bookmark 6 citations
Ordinal diagrams for Π3-reflection.Toshiyasu Arai - 2000 - Journal of Symbolic Logic 65 (3):1375 - 1394.details In this paper we introduce a recursive notation system O(Π 3 ) of ordinals. An element of the notation system is called an ordinal diagram. The system is designed for proof theoretic study of theories of Π 3 -reflection. We show that for each $\alpha in O(Π 3 ) a set theory KP Π 3 for Π 3 -reflection proves that the initial segment of O(Π 3 ) determined by α is a well ordering. Proof theoretic study for such theories (...) will be reported in [4]. (shrink) Download Export citation Bookmark 7 citations
First Order Theories for Nonmonotone Inductive Definitions: Recursively Inaccessible and Mahlo.Gerhard Jäger - 2001 - Journal of Symbolic Logic 66 (3):1073-1089.details In this paper first order theories for nonmonotone inductive definitions are introduced, and a proof-theoretic analysis for such theories based on combined operator forms a la Richter with recursively inaccessible and Mahlo closure ordinals is given. Download Export citation Bookmark 6 citations

1