Switch to: References

Add citations

You must login to add citations.
  1. (2 other versions)x1. Aims.Wolfram Pohlers - 1996 - Bulletin of Symbolic Logic 2 (2):159-188.
    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 (...)
    Download  
     
    Export citation  
     
    Bookmark   1 citation  
  • Systems of explicit mathematics with non-constructive μ-operator. Part I.Solomon Feferman & Gerhard Jäger - 1993 - Annals of Pure and Applied Logic 65 (3):243-263.
    Feferman, S. and G. Jäger, Systems of explicit mathematics with non-constructive μ-operator. Part I, Annals of Pure and Applied Logic 65 243-263. This paper is mainly concerned with the proof-theoretic analysis of systems of explicit mathematics with a non-constructive minimum operator. We start off from a basic theory BON of operators and numbers and add some principles of set and formula induction on the natural numbers as well as axioms for μ. The principal results then state: BON plus set induction (...)
    Download  
     
    Export citation  
     
    Bookmark   23 citations  
  • The strength of admissibility without foundation.Gerhard Jäger - 1984 - Journal of Symbolic Logic 49 (3):867-879.
    Download  
     
    Export citation  
     
    Bookmark   8 citations  
  • Hilbert's program relativized: Proof-theoretical and foundational reductions.Solomon Feferman - 1988 - Journal of Symbolic Logic 53 (2):364-384.
    Download  
     
    Export citation  
     
    Bookmark   64 citations  
  • Recent advances in ordinal analysis: Π 21-CA and related systems.Michael Rathjen - 1995 - Bulletin of Symbolic Logic 1 (4):468 - 485.
    §1. Introduction. The purpose of this paper is, in general, to report the state of the art of ordinal analysis and, in particular, the recent success in obtaining an ordinal analysis for the system of -analysis, which is the subsystem of formal second order arithmetic, Z2, with comprehension confined to -formulae. The same techniques can be used to provide ordinal analyses for theories that are reducible to iterated -comprehension, e.g., -comprehension. The details will be laid out in [28].Ordinal-theoretic proof theory (...)
    Download  
     
    Export citation  
     
    Bookmark   17 citations  
  • Mathematical proof theory in the light of ordinal analysis.Reinhard Kahle - 2002 - Synthese 133 (1/2):237 - 255.
    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  
  • Theories of Frege structure equivalent to Feferman's system T 0.Daichi Hayashi - 2025 - Annals of Pure and Applied Logic 176 (1):103510.
    Download  
     
    Export citation  
     
    Bookmark  
  • A new model construction by making a detour via intuitionistic theories I: Operational set theory without choice is Π 1 -equivalent to KP.Kentaro Sato & Rico Zumbrunnen - 2015 - Annals of Pure and Applied Logic 166 (2):121-186.
    Download  
     
    Export citation  
     
    Bookmark   6 citations  
  • Systems of explicit mathematics with non-constructive μ-operator and join.Thomas Glaß & Thomas Strahm - 1996 - Annals of Pure and Applied Logic 82 (2):193-219.
    The aim of this article is to give the proof-theoretic analysis of various subsystems of Feferman's theory T1 for explicit mathematics which contain the non-constructive μ-operator and join. We make use of standard proof-theoretic techniques such as cut-elimination of appropriate semiformal systems and asymmetrical interpretations in standard structures for explicit mathematics.
    Download  
     
    Export citation  
     
    Bookmark   10 citations  
  • (1 other version)Well-ordering proofs for Martin-Löf type theory.Anton Setzer - 1998 - Annals of Pure and Applied Logic 92 (2):113-159.
    We present well-ordering proofs for Martin-Löf's type theory with W-type and one universe. These proofs, together with an embedding of the type theory in a set theoretical system as carried out in Setzer show that the proof theoretical strength of the type theory is precisely ψΩ1Ω1 + ω, which is slightly more than the strength of Feferman's theory T0, classical set theory KPI and the subsystem of analysis + . The strength of intensional and extensional version, of the version à (...)
    Download  
     
    Export citation  
     
    Bookmark   10 citations  
  • Replacement versus collection and related topics in constructive Zermelo–Fraenkel set theory.Michael Rathjen - 2005 - Annals of Pure and Applied Logic 136 (1-2):156-174.
    While it is known that intuitionistic ZF set theory formulated with Replacement, IZFR, does not prove Collection, it is a longstanding open problem whether IZFR and intuitionistic set theory ZF formulated with Collection, IZF, have the same proof-theoretic strength. It has been conjectured that IZF proves the consistency of IZFR. This paper addresses similar questions but in respect of constructive Zermelo–Fraenkel set theory, CZF. It is shown that in the latter context the proof-theoretic strength of Replacement is the same as (...)
    Download  
     
    Export citation  
     
    Bookmark   5 citations  
  • Realization of constructive set theory into explicit mathematics: a lower bound for impredicative Mahlo universe.Sergei Tupailo - 2003 - Annals of Pure and Applied Logic 120 (1-3):165-196.
    We define a realizability interpretation of Aczel's Constructive Set Theory CZF into Explicit Mathematics. The final results are that CZF extended by Mahlo principles is realizable in corresponding extensions of T 0 , thus providing relative lower bounds for the proof-theoretic strength of the latter.
    Download  
     
    Export citation  
     
    Bookmark   8 citations  
  • On the proof-theoretic strength of monotone induction in explicit mathematics.Thomas Glaß, Michael Rathjen & Andreas Schlüter - 1997 - Annals of Pure and Applied Logic 85 (1):1-46.
    We characterize the proof-theoretic strength of systems of explicit mathematics with a general principle asserting the existence of least fixed points for monotone inductive definitions, in terms of certain systems of analysis and set theory. In the case of analysis, these are systems which contain the Σ12-axiom of choice and Π12-comprehension for formulas without set parameters. In the case of set theory, these are systems containing the Kripke-Platek axioms for a recursively inaccessible universe together with the existence of a stable (...)
    Download  
     
    Export citation  
     
    Bookmark   9 citations  
  • A theory of rules for enumerated classes of functions.Andreas Schlüter - 1995 - Archive for Mathematical Logic 34 (1):47-63.
    We define an applicative theoryCL 2 similar to combinatory logic which can be interpreted in classes of functions possessing an enumerating function. In contrast to the models of classical combinatory logic, it is not necessarily assumed that the enumerating function itself belongs to that function class. Thereby we get a variety of possible models including e. g. the classes of primitive recursive, recursive, elementary, polynomial-time comptable ofɛ 0-recursive functions.We show that inCL 2 a major part of the metatheory of enumerated (...)
    Download  
     
    Export citation  
     
    Bookmark   4 citations  
  • A new model construction by making a detour via intuitionistic theories II: Interpretability lower bound of Feferman's explicit mathematics T 0.Kentaro Sato - 2015 - Annals of Pure and Applied Logic 166 (7-8):800-835.
    Download  
     
    Export citation  
     
    Bookmark   5 citations  
  • Ordinal notations based on a hierarchy of inaccessible cardinals.Wolfram Pohlers - 1987 - Annals of Pure and Applied Logic 33 (C):157-179.
    Download  
     
    Export citation  
     
    Bookmark   3 citations  
  • (1 other version)Realization of analysis into explicit mathematics.Sergei Tupailo - 2001 - Journal of Symbolic Logic 66 (4):1848-1864.
    We define a novel interpretation R of second order arithmetic into Explicit Mathematics. As a difference from standard D-interpretation, which was used before and was shown to interpret only subsystems proof-theoretically weaker than T 0 , our interpretation can reach the full strength of T 0 . The R-interpretation is an adaptation of Kleene's recursive realizability, and is applicable only to intuitionistic theories.
    Download  
     
    Export citation  
     
    Bookmark   4 citations  
  • Ordinal diagrams for recursively Mahlo universes.Toshiyasu Arai - 2000 - Archive for Mathematical Logic 39 (5):353-391.
    In this paper we introduce a recursive notation system $O(\mu)$ of ordinals. An element of the notation system is called an ordinal diagram following G. Takeuti [25]. The system is designed for proof theoretic study of theories of recursively Mahlo universes. We show that for each $\alpha<\Omega$ in $O(\mu)$ KPM proves that the initial segment of $O(\mu)$ determined by $\alpha$ is a well ordering. Proof theoretic study for such theories will be reported in [9].
    Download  
     
    Export citation  
     
    Bookmark   8 citations  
  • (2 other versions)Pure proof theory aims, methods and results.Wolfram Pohlers - 1996 - Bulletin of Symbolic Logic 2 (2):159-188.
    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 (...)
    Download  
     
    Export citation  
     
    Bookmark   8 citations  
  • Upper Bounds for metapredicative mahlo in explicit mathematics and admissible set theory.Gerhard Jager & Thomas Strahm - 2001 - Journal of Symbolic Logic 66 (2):935-958.
    In this article we introduce systems for metapredicative Mahlo in explicit mathematics and admissible set theory. The exact upper proof-theoretic bounds of these systems are established.
    Download  
     
    Export citation  
     
    Bookmark   17 citations  
  • Reflections on reflections in explicit mathematics.Gerhard Jäger & Thomas Strahm - 2005 - Annals of Pure and Applied Logic 136 (1-2):116-133.
    We give a broad discussion of reflection principles in explicit mathematics, thereby addressing various kinds of universe existence principles. The proof-theoretic strength of the relevant systems of explicit mathematics is couched in terms of suitable extensions of Kripke–Platek set theory.
    Download  
     
    Export citation  
     
    Bookmark   7 citations  
  • Extending the system T0 of explicit mathematics: the limit and Mahlo axioms.Gerhard Jäger & Thomas Studer - 2002 - Annals of Pure and Applied Logic 114 (1-3):79-101.
    In this paper we discuss extensions of Feferman's theory T 0 for explicit mathematics by the so-called limit and Mahlo axioms and present a novel approach to constructing natural recursion-theoretic models for systems of explicit mathematics which is based on nonmonotone inductive definitions.
    Download  
     
    Export citation  
     
    Bookmark   13 citations  
  • Ordinal diagrams for Π3-reflection.Toshiyasu Arai - 2000 - Journal of Symbolic Logic 65 (3):1375 - 1394.
    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 (...)
    Download  
     
    Export citation  
     
    Bookmark   7 citations  
  • A new model construction by making a detour via intuitionistic theories III: Ultrafinitistic proofs of conservations of Σ 1 1 collection. [REVIEW]Kentaro Sato - 2023 - Annals of Pure and Applied Logic 174 (3):103207.
    Download  
     
    Export citation  
     
    Bookmark   1 citation  
  • Relativizing operational set theory.Gerhard Jäger - 2016 - Bulletin of Symbolic Logic 22 (3):332-352.
    We introduce a way of relativizing operational set theory that also takes care of application. After presenting the basic approach and proving some essential properties of this new form of relativization we turn to the notion of relativized regularity and to the system OST that extends OST by a limit axiom claiming that any set is element of a relativized regular set. Finally we show that OST is proof-theoretically equivalent to the well-known theory KPi for a recursively inaccessible universe.
    Download  
     
    Export citation  
     
    Bookmark  
  • 1999 European Summer Meeting of the Association for Symbolic Logic.Wilfrid Hodges - 2000 - Bulletin of Symbolic Logic 6 (1):103-137.
    Download  
     
    Export citation  
     
    Bookmark  
  • First Order Theories for Nonmonotone Inductive Definitions: Recursively Inaccessible and Mahlo.Gerhard Jäger - 2001 - Journal of Symbolic Logic 66 (3):1073-1089.
    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