51 found
Sort by:
  1. Michael Rathjen (forthcoming). 2010 European Summer Meeting of the Association for Symbolic Logic Logic Colloquium'10. Bulletin of Symbolic Logic.
     
    My bibliography  
     
    Export citation  
  2. Michael Rathjen (forthcoming). Recent Advances in Ordinal Analysis. Bulletin of Symbolic Logic.
    Ordinal-theoretic proof theory came into existence in 1936, springing forth from Gentzen's head in the course of his consistency proof of arithmetic. Gentzen fostered hopes that with sufficiently large constructive ordinals one could establish the consistency of analysis, i.e., second order arithmetic. The purpose of the present paper is, in general, the report the state of the art of ordinal analysis and, in particular, the recent success in obtaining an ordinal analysis for a strong subsystem of second order arithmetic, which (...)
    Direct download  
     
    My bibliography  
     
    Export citation  
  3. Michael Rathjen (2014). Constructive Zermelo–Fraenkel Set Theory and the Limited Principle of Omniscience. Annals of Pure and Applied Logic 165 (2):563-572.
    Direct download (2 more)  
     
    My bibliography  
     
    Export citation  
  4. Michael Rathjen (2014). Relativized Ordinal Analysis: The Case of Power Kripke–Platek Set Theory. Annals of Pure and Applied Logic 165 (1):316-339.
    Direct download (2 more)  
     
    My bibliography  
     
    Export citation  
  5. Sy-David Friedman, Michael Rathjen & Andreas Weiermann (2013). Slow Consistency. Annals of Pure and Applied Logic 164 (3):382-393.
    Direct download (4 more)  
     
    My bibliography  
     
    Export citation  
  6. Bahareh Afshari & Michael Rathjen (2012). Ordinal Analysis and the Infinite Ramsey Theorem. In. In S. Barry Cooper (ed.), How the World Computes. 1--10.
    No categories
    Direct download  
     
    My bibliography  
     
    Export citation  
  7. Ray-Ming Chen & Michael Rathjen (2012). Lifschitz Realizability for Intuitionistic Zermelo–Fraenkel Set Theory. Archive for Mathematical Logic 51 (7-8):789-818.
    A variant of realizability for Heyting arithmetic which validates Church’s thesis with uniqueness condition, but not the general form of Church’s thesis, was introduced by Lifschitz (Proc Am Math Soc 73:101–106, 1979). A Lifschitz counterpart to Kleene’s realizability for functions (in Baire space) was developed by van Oosten (J Symb Log 55:805–821, 1990). In that paper he also extended Lifschitz’ realizability to second order arithmetic. The objective here is to extend it to full intuitionistic Zermelo–Fraenkel set theory, IZF. The machinery (...)
    Direct download (4 more)  
     
    My bibliography  
     
    Export citation  
  8. Graham E. Leigh & Michael Rathjen (2012). The Friedman—Sheard Programme in Intuitionistic Logic. Journal of Symbolic Logic 77 (3):777-806.
    This paper compares the roles classical and intuitionistic logic play in restricting the free use of truth principles in arithmetic. We consider fifteen of the most commonly used axiomatic principles of truth and classify every subset of them as either consistent or inconsistent over a weak purely intuitionistic theory of truth.
    Direct download (5 more)  
     
    My bibliography  
     
    Export citation  
  9. Michael Rathjen (2012). From the Weak to the Strong Existence Property. Annals of Pure and Applied Logic 163 (10):1400-1418.
    Direct download (4 more)  
     
    My bibliography  
     
    Export citation  
  10. Michael Rathjen & Andreas Weiermann (2011). Reverse Mathematics and Well-Ordering Principles. In S. B. Cooper & Andrea Sorbi (eds.), Computability in Context: Computation and Logic in the Real World. World Scientific.
    No categories
    Direct download  
     
    My bibliography  
     
    Export citation  
  11. Bahareh Afshari & Michael Rathjen (2010). A Note on the Theory of Positive Induction, {{Rm ID}^*_1}. Archive for Mathematical Logic 49 (2):275-281.
    The article shows a simple way of calibrating the strength of the theory of positive induction, ${{\rm ID}^{*}_{1}}$ . Crucially the proof exploits the equivalence of ${\Sigma^{1}_{1}}$ dependent choice and ω-model reflection for ${\Pi^{1}_{2}}$ formulae over ACA 0. Unbeknown to the authors, D. Probst had already determined the proof-theoretic strength of ${{\rm ID}^{*}_{1}}$ in Probst, J Symb Log, 71, 721–746, 2006.
    No categories
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  12. Graham Emil Leigh & Michael Rathjen (2010). An Ordinal Analysis for Theories of Self-Referential Truth. Archive for Mathematical Logic 49 (2):213-247.
    The first attempt at a systematic approach to axiomatic theories of truth was undertaken by Friedman and Sheard (Ann Pure Appl Log 33:1–21, 1987). There twelve principles consisting of axioms, axiom schemata and rules of inference, each embodying a reasonable property of truth were isolated for study. Working with a base theory of truth conservative over PA, Friedman and Sheard raised the following questions. Which subsets of the Optional Axioms are consistent over the base theory? What are the proof-theoretic strengths (...)
    No categories
    Direct download (4 more)  
     
    My bibliography  
     
    Export citation  
  13. Bahareh Afshari & Michael Rathjen (2009). Reverse Mathematics and Well-Ordering Principles: A Pilot Study. Annals of Pure and Applied Logic 160 (3):231-237.
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  14. Robert S. Lubarsky & Michael Rathjen (2008). On the Constructive Dedekind Reals. Logic and Analysis 1 (2):131-152.
    In order to build the collection of Cauchy reals as a set in constructive set theory, the only power set-like principle needed is exponentiation. In contrast, the proof that the Dedekind reals form a set has seemed to require more than that. The main purpose here is to show that exponentiation alone does not suffice for the latter, by furnishing a Kripke model of constructive set theory, Constructive Zermelo–Fraenkel set theory with subset collection replaced by exponentiation, in which the Cauchy (...)
    Direct download (6 more)  
     
    My bibliography  
     
    Export citation  
  15. Michael Rathjen (2008). The Natural Numbers in Constructive Set Theory. Mathematical Logic Quarterly 54 (1):83-97.
    No categories
    Direct download (4 more)  
     
    My bibliography  
     
    Export citation  
  16. Matthew Foreman, Su Gao, Valentina Harizanov, Ulrich Kohlenbach, Michael Rathjen, Reed Solomon, Carol Wood & Marcia Groszek (2007). New Orleans Marriott and Sheraton New Orleans New Orleans, Louisiana January 7–8, 2007. Bulletin of Symbolic Logic 13 (3).
    Direct download  
     
    My bibliography  
     
    Export citation  
  17. Michael Rathjen (2006). A Note on Bar Induction in Constructive Set Theory. Mathematical Logic Quarterly 52 (3):253-258.
    No categories
    Direct download (4 more)  
     
    My bibliography  
     
    Export citation  
  18. Michael Rathjen (2006). Theories and Ordinals in Proof Theory. Synthese 148 (3):719 - 743.
    How do ordinals measure the strength and computational power of formal theories? This paper is concerned with the connection between ordinal representation systems and theories established in ordinal analyses. It focusses on results which explain the nature of this connection in terms of semantical and computational notions from model theory, set theory, and generalized recursion theory.
    Direct download (6 more)  
     
    My bibliography  
     
    Export citation  
  19. Michael Rathjen & Sergei Tupailo (2006). Characterizing the Interpretation of Set Theory in Martin-Löf Type Theory. Annals of Pure and Applied Logic 141 (3):442-471.
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  20. John Baldwin, Lev Beklemishev, Michael Hallett, Valentina Harizanov, Steve Jackson, Kenneth Kunen, Angus J. MacIntyre, Penelope Maddy, Joe Miller & Michael Rathjen (2005). Carnegie Mellon University, Pittsburgh, PA May 19–23, 2004. Bulletin of Symbolic Logic 11 (1).
    Direct download  
     
    My bibliography  
     
    Export citation  
  21. Michael Rathjen (2005). The Disjunction and Related Properties for Constructive Zermelo-Fraenkel Set Theory. Journal of Symbolic Logic 70 (4):1233 - 1254.
    This paper proves that the disjunction property, the numerical existence property. Church's rule, and several other metamathematical properties hold true for Constructive Zermelo-Fraenkel Set Theory. CZF. and also for the theory CZF augmented by the Regular Extension Axiom. As regards the proof technique, it features a self-validating semantics for CZF that combines realizability for extensional set theory and truth.
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  22. Michael Rathjen (2005). An Ordinal Analysis of Parameter Free Π1 2-Comprehension. Archive for Mathematical Logic 44 (3):263-362.
    No categories
    Direct download (4 more)  
     
    My bibliography  
     
    Export citation  
  23. Michael Rathjen (2005). An Ordinal Analysis of Stability. Archive for Mathematical Logic 44 (1):1-62.
    No categories
    Direct download (4 more)  
     
    My bibliography  
     
    Export citation  
  24. Michael Rathjen (2005). Replacement Versus Collection and Related Topics in Constructive Zermelo–Fraenkel Set Theory. Annals of Pure and Applied Logic 136 (1-2):156-174.
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  25. Michael Rathjen (2005). The Constructive Hilbert Program and the Limits of Martin-Löf Type Theory. Synthese 147 (1):81 - 120.
    No categories
    Direct download (5 more)  
     
    My bibliography  
     
    Export citation  
  26. Robert S. Lubarsky & Michael Rathjen (2003). On the Regular Extension Axiom and its Variants. Mathematical Logic Quarterly 49 (5):511.
    No categories
    Direct download (5 more)  
     
    My bibliography  
     
    Export citation  
  27. Michael Rathjen (2003). Realizing Mahlo Set Theory in Type Theory. Archive for Mathematical Logic 42 (1):89-101.
    After introducing the large set notion of Mahloness, this paper shows that constructive set theory with an axiom asserting the existence of a Mahlo set has a realizability interpretation in an extension of Martin-Löf type theory developed by A. Setzer.
    No categories
    Direct download (4 more)  
     
    My bibliography  
     
    Export citation  
  28. Michael Möllerfeld & Michael Rathjen (2002). A Note on the Σ1 Spectrum of a Theory. Archive for Mathematical Logic 41 (1):33-34.
    No categories
    Direct download (5 more)  
     
    My bibliography  
     
    Export citation  
  29. Michael Rathjen (2001). The Strength of Martin-Löf Type Theory with a Superuniverse. Part II. Archive for Mathematical Logic 40 (3):207-233.
    Universes of types were introduced into constructive type theory by Martin-Löf [3]. The idea of forming universes in type theory is to introduce a universe as a set closed under a certain specified ensemble of set constructors, say ?. The universe then “reflects”?.This is the second part of a paper which addresses the exact logical strength of a particular such universe construction, the so-called superuniverse due to Palmgren (cf.[4–6]).It is proved that Martin-Löf type theory with a superuniverse, termed MLS, is (...)
    No categories
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  30. Michael Rathjen (2000). The Strength of Martin-Löf Type Theory with a Superuniverse. Part I. Archive for Mathematical Logic 39 (1):1-39.
    Universes of types were introduced into constructive type theory by Martin-Löf [12]. The idea of forming universes in type theory is to introduce a universe as a set closed under a certain specified ensemble of set constructors, say $\mathcal{C}$ . The universe then “reflects” $\mathcal{C}$ .This is the first part of a paper which addresses the exact logical strength of a particular such universe construction, the so-called superuniverse due to Palmgren (cf. [16, 18, 19]).It is proved that Martin-Löf type theory (...)
    No categories
    Direct download (5 more)  
     
    My bibliography  
     
    Export citation  
  31. Michael Rathjen (1999). Explicit Mathematics with the Monotone Fixed Point Principle. II: Models. Journal of Symbolic Logic 64 (2):517-550.
    This paper continues investigations of the monotone fixed point principle in the context of Feferman's explicit mathematics begun in [14]. Explicit mathematics is a versatile formal framework for representing Bishop-style constructive mathematics and generalized recursion theory. The object of investigation here is the theory of explicit mathematics augmented by the monotone fixed point principle, which asserts that any monotone operation on classifications (Feferman's notion of set) possesses a least fixed point. To be more precise, the new axiom not merely postulates (...)
    Direct download (6 more)  
     
    My bibliography  
     
    Export citation  
  32. Michael Rathjen (1998). Explicit Mathematics with the Monotone Fixed Point Principle. Journal of Symbolic Logic 63 (2):509-542.
    The context for this paper is Feferman's theory of explicit mathematics, a formal framework serving many purposes. It is suitable for representing Bishop-style constructive mathematics as well as generalized recursion, including direct expression of structural concepts which admit self-application. The object of investigation here is the theory of explicit mathematics augmented by the monotone fixed point principle, which asserts that any monotone operation on classifications (Feferman's notion of set) possesses a least fixed point. To be more precise, the new axiom (...)
    Direct download (6 more)  
     
    My bibliography  
     
    Export citation  
  33. Michael Rathjen, Edward R. Griffor & Erik Palmgren (1998). Inaccessibility in Constructive Set Theory and Type Theory. Annals of Pure and Applied Logic 94 (1-3):181-200.
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  34. Thomas Glaß, Michael Rathjen & Andreas Schlüter (1997). On the Proof-Theoretic Strength of Monotone Induction in Explicit Mathematics. Annals of Pure and Applied Logic 85 (1):1-46.
    Direct download (2 more)  
     
    My bibliography  
     
    Export citation  
  35. Thomas Glass, Michael Rathjen & Andreas Schlüter (1997). On the Proof-Theoretic Strength of Monotone Induction in Explicit Mathematics. Annals of Pure and Applied Logic 85 (1):1-46.
    Direct download  
     
    My bibliography  
     
    Export citation  
  36. Michael Rathjen (1996). Monotone Inductive Definitions in Explicit Mathematics. Journal of Symbolic Logic 61 (1):125-146.
    The context for this paper is Feferman's theory of explicit mathematics, T 0 . We address a problem that was posed in [6]. Let MID be the principle stating that any monotone operation on classifications has a least fixed point. The main objective of this paper is to show that T 0 + MID, when based on classical logic, also proves the existence of non-monotone inductive definitions that arise from arbitrary extensional operations on classifications. From the latter we deduce that (...)
    Direct download (6 more)  
     
    My bibliography  
     
    Export citation  
  37. Michael Rathjen (1996). Review: Richard Sommer, Transfinite Induction Within Peano Arithmetic. [REVIEW] Journal of Symbolic Logic 61 (4):1388-1388.
    Direct download (2 more)  
     
    My bibliography  
     
    Export citation  
  38. Michael Rathjen (1996). The Recursively Mahlo Property in Second Order Arithmetic. Mathematical Logic Quarterly 42 (1):59-66.
    No categories
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  39. Michael Rathjen (1995). Recent Advances in Ordinal Analysis: Π 21-CA and Related Systems. Bulletin of Symbolic Logic 1 (4):468 - 485.
    Direct download (4 more)  
     
    My bibliography  
     
    Export citation  
  40. Michael Rathjen (1995). Recent Advances in Ordinal Analysis: $Pi _{2}^{1}-Text{CA}$ and Related Systems. Bulletin of Symbolic Logic 1 (4):468-485.
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  41. Michael Rathjen (1995). State of the Art of Ordinal Analysis and, in Particular, the Recent Success in Obtaining an Ordinal Analysis for the System of Π1 2-Analysis, Which is the Subsystem of Formal Second Order Arithmetic, Z2, with Comprehension Confined to Π1. [REVIEW] Bulletin of Symbolic Logic 1 (4).
    Direct download  
     
    My bibliography  
     
    Export citation  
  42. Michael Rathjen (1995). X1. 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 Π1 2-Analysis, Which is the Subsystem of Formal Second Order Arithmetic, Z2, with Comprehension. [REVIEW] Bulletin of Symbolic Logic 1 (4).
    Direct download  
     
    My bibliography  
     
    Export citation  
  43. Edward Griffor & Michael Rathjen (1994). The Strength of Some Martin-Löf Type Theories. Archive for Mathematical Logic 33 (5):347-385.
    One objective of this paper is the determination of the proof-theoretic strength of Martin-Löf's type theory with a universe and the type of well-founded trees. It is shown that this type system comprehends the consistency of a rather strong classical subsystem of second order arithmetic, namely the one with Δ 2 1 comprehension and bar induction. As Martin-Löf intended to formulate a system of constructive (intuitionistic) mathematics that has a sound philosophical basis, this yields a constructive consistency proof of a (...)
    No categories
    Direct download (4 more)  
     
    My bibliography  
     
    Export citation  
  44. Michael Rathjen (1994). Collapsing Functions Based on Recursively Large Ordinals: A Well-Ordering Proof for KPM. [REVIEW] Archive for Mathematical Logic 33 (1):35-55.
    It is shown how the strong ordinal notation systems that figure in proof theory and have been previously defined by employing large cardinals, can be developed directly on the basis of their recursively large counterparts. Thereby we provide a completely new approach to well-ordering proofs as will be exemplified by determining the proof-theoretic ordinal of the systemKPM of [R91].
    No categories
    Direct download (4 more)  
     
    My bibliography  
     
    Export citation  
  45. Michael Rathjen (1994). Proof Theory of Reflection. Annals of Pure and Applied Logic 68 (2):181-224.
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  46. Michael Rathjen (1993). How to Develop Proof‐Theoretic Ordinal Functions on the Basis of Admissible Ordinals. Mathematical Logic Quarterly 39 (1):47-54.
    No categories
    Direct download (5 more)  
     
    My bibliography  
     
    Export citation  
  47. Michael Rathjen & Andreas Weiermann (1993). Proof-Theoretic Investigations on Kruskal's Theorem. Annals of Pure and Applied Logic 60 (1):49-88.
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  48. Michael Rathjen (1992). A Proof-Theoretic Characterization of the Primitive Recursive Set Functions. Journal of Symbolic Logic 57 (3):954-969.
    Let KP- be the theory resulting from Kripke-Platek set theory by restricting Foundation to Set Foundation. Let G: V → V (V:= universe of sets) be a ▵0-definable set function, i.e. there is a ▵0-formula φ(x, y) such that φ(x, G(x)) is true for all sets x, and $V \models \forall x \exists!y\varphi (x, y)$ . In this paper we shall verify (by elementary proof-theoretic methods) that the collection of set functions primitive recursive in G coincides with the collection of (...)
    Direct download (6 more)  
     
    My bibliography  
     
    Export citation  
  49. Michael Rathjen (1991). Proof-Theoretic Analysis of KPM. Archive for Mathematical Logic 30 (5-6):377-403.
    KPM is a subsystem of set theory designed to formalize a recursively Mahlo universe of sets. In this paper we show that a certain ordinal notation system is sufficient to measure the proof-theoretic strength ofKPM. This involves a detour through an infinitary calculus RS(M), for which we prove several cutelimination theorems. Full cut-elimination is available for derivations of $\Sigma (L_{\omega _1^c } )$ sentences, whereω 1 c denotes the least nonrecursive ordinal. This paper is self-contained, at least from a technical (...)
    No categories
    Direct download (4 more)  
     
    My bibliography  
     
    Export citation  
  50. Michael Rathjen (1991). The Role of Parameters in Bar Rule and Bar Induction. Journal of Symbolic Logic 56 (2):715-730.
    For several subsystems of second order arithmetic T we show that the proof-theoretic strength of T + (bar rule) can be characterized in terms of T + (bar induction) □ , where the latter scheme arises from the scheme of bar induction by restricting it to well-orderings with no parameters. In addition, we demonstrate that ACA + 0 , ACA 0 + (bar rule) and ACA 0 + (bar induction) □ prove the same Π 1 1 -sentences.
    Direct download (6 more)  
     
    My bibliography  
     
    Export citation  
1 — 50 / 51