51 found
Sort by:
  1. 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  
  2. Michael Rathjen (2014). Constructive Zermelo–Fraenkel Set Theory and the Limited Principle of Omniscience. Annals of Pure and Applied Logic 165 (2):563-572.
    In recent years the question of whether adding the limited principle of omniscience, LPO, to constructive Zermelo–Fraenkel set theory, CZF, increases its strength has arisen several times. As the addition of excluded middle for atomic formulae to CZF results in a rather strong theory, i.e. much stronger than classical Zermelo set theory, it is not obvious that its augmentation by LPO would be proof-theoretically benign. The purpose of this paper is to show that CZF+RDC+LPO has indeed the same strength as (...)
    Direct download (2 more)  
     
    My bibliography  
     
    Export citation  
  3. Michael Rathjen (2014). Relativized Ordinal Analysis: The Case of Power Kripke–Platek Set Theory. Annals of Pure and Applied Logic 165 (1):316-339.
    The paper relativizes the method of ordinal analysis developed for Kripke–Platek set theory to theories which have the power set axiom. We show that it is possible to use this technique to extract information about Power Kripke–Platek set theory, KP.As an application it is shown that whenever KP+AC proves a ΠP2 statement then it holds true in the segment Vτ of the von Neumann hierarchy, where τ stands for the Bachmann–Howard ordinal.
    Direct download (2 more)  
     
    My bibliography  
     
    Export citation  
  4. Sy-David Friedman, Michael Rathjen & Andreas Weiermann (2013). Slow Consistency. Annals of Pure and Applied Logic 164 (3):382-393.
    The fact that “natural” theories, i.e. theories which have something like an “idea” to them, are almost always linearly ordered with regard to logical strength has been called one of the great mysteries of the foundation of mathematics. However, one easily establishes the existence of theories with incomparable logical strengths using self-reference . As a result, PA+Con is not the least theory whose strength is greater than that of PA. But still we can ask: is there a sense in which (...)
    Direct download (4 more)  
     
    My bibliography  
     
    Export citation  
  5. Bahareh Afshari & Michael Rathjen (2012). Ordinal Analysis and the Infinite Ramsey Theorem. In S. Barry Cooper (ed.), How the World Computes. 1--10.
    Direct download  
     
    My bibliography  
     
    Export citation  
  6. 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  
  7. 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  
  8. 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  
  9. 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  
  10. 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.
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  11. 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 (...)
    Direct download (4 more)  
     
    My bibliography  
     
    Export citation  
  12. Bahareh Afshari & Michael Rathjen (2009). Reverse Mathematics and Well-Ordering Principles: A Pilot Study. Annals of Pure and Applied Logic 160 (3):231-237.
    The larger project broached here is to look at the generally sentence “if X is well-ordered then f is well-ordered”, where f is a standard proof-theoretic function from ordinals to ordinals. It has turned out that a statement of this form is often equivalent to the existence of countable coded ω-models for a particular theory Tf whose consistency can be proved by means of a cut elimination theorem in infinitary logic which crucially involves the function f. To illustrate this theme, (...)
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  13. 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  
  14. Michael Rathjen (2008). The Natural Numbers in Constructive Set Theory. Mathematical Logic Quarterly 54 (1):83-97.
    Constructive set theory started with Myhill's seminal 1975 article [8]. This paper will be concerned with axiomatizations of the natural numbers in constructive set theory discerned in [3], clarifying the deductive relationships between these axiomatizations and the strength of various weak constructive set theories.
    Direct download (4 more)  
     
    My bibliography  
     
    Export citation  
  15. 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  
  16. Michael Rathjen (2006). A Note on Bar Induction in Constructive Set Theory. Mathematical Logic Quarterly 52 (3):253-258.
    Bar Induction occupies a central place in Brouwerian mathematics. This note is concerned with the strength of Bar Induction on the basis of Constructive Zermelo-Fraenkel Set Theory, CZF. It is shown that CZF augmented by decidable Bar Induction proves the 1-consistency of CZF. This answers a question of P. Aczel who used Bar Induction to give a proof of the Lusin Separation Theorem in the constructive set theory CZF.
    Direct download (4 more)  
     
    My bibliography  
     
    Export citation  
  17. 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  
  18. 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.
    Constructive Zermelo–Fraenkel set theory, CZF, can be interpreted in Martin-Löf type theory via the so-called propositions-as-types interpretation. However, this interpretation validates more than what is provable in CZF. We now ask ourselves: is there a reasonably simple axiomatization of the set-theoretic formulae validated in Martin-Löf type theory? The answer is yes for a large collection of statements called the mathematical formulae. The validated mathematical formulae can be axiomatized by suitable forms of the axiom of choice.The paper builds on a self-interpretation (...)
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  19. 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  
  20. 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  
  21. Michael Rathjen (2005). An Ordinal Analysis of Parameter Free Π1 2-Comprehension. Archive for Mathematical Logic 44 (3):263-362.
    Direct download (4 more)  
     
    My bibliography  
     
    Export citation  
  22. Michael Rathjen (2005). An Ordinal Analysis of Stability. Archive for Mathematical Logic 44 (1):1-62.
  23. 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.
    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 (...)
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  24. 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  
  25. Robert S. Lubarsky & Michael Rathjen (2003). On the Regular Extension Axiom and its Variants. Mathematical Logic Quarterly 49 (5):511.
    The regular extension axiom, REA, was first considered by Peter Aczel in the context of Constructive Zermelo-Fraenkel Set Theory as an axiom that ensures the existence of many inductively defined sets. REA has several natural variants. In this note we gather together metamathematical results about these variants from the point of view of both classical and constructive set theory.
    Direct download (5 more)  
     
    My bibliography  
     
    Export citation  
  26. 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.
    Direct download (4 more)  
     
    My bibliography  
     
    Export citation  
  27. Michael Möllerfeld & Michael Rathjen (2002). A Note on the Σ1 Spectrum of a Theory. Archive for Mathematical Logic 41 (1):33-34.
    Direct download (5 more)  
     
    My bibliography  
     
    Export citation  
  28. Michael Rathjen & Samuel R. Buss (2002). The Superjump in Martin-Löf Type Theory. Bulletin of Symbolic Logic 8 (4):538-538.
     
    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 (...)
    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 (...)
    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.
    This paper is the first in a series whose objective is to study notions of large sets in the context of formal theories of constructivity. The two theories considered are Aczel's constructive set theory and Martin-Löf's intuitionistic theory of types. This paper treats Mahlo's π-numbers which give rise classically to the enumerations of inaccessibles of all transfinite orders. We extend the axioms of CZF and show that the resulting theory, when augmented by the tertium non-datur, is equivalent to ZF plus (...)
    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.
    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 (...)
    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 (3 more)  
     
    My bibliography  
     
    Export citation  
  38. Michael Rathjen (1996). The Recursively Mahlo Property in Second Order Arithmetic. Mathematical Logic Quarterly 42 (1):59-66.
    The paper characterizes the second order arithmetic theorems of a set theory that features a recursively Mahlo universe; thereby complementing prior proof-theoretic investigations on this notion. It is shown that the property of being recursively Mahlo corresponds to a certain kind of β-model reflection in second order arithmetic. Further, this leads to a characterization of the reals recursively computable in the superjump functional.
    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.
  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 (...)
    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].
    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.
    The paper contains proof-theoretic investigation on extensions of Kripke-Platek set theory, KP, which accommodate first-order reflection. Ordinal analyses for such theories are obtained by devising cut elimination procedures for infinitary calculi of ramified set theory with Пn reflection rules. This leads to consistency proofs for the theories KP+Пn reflection using a small amount of arithmetic and the well-foundedness of a certain ordinal system with respect to primitive decending sequences. Regarding future work, we intend to avail ourselves of these new cut (...)
    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.
    In ordinal analysis of impredicative theories so-called collapsing functions are of central importance. Unfortunately, the definition procedure of these functions makes essential use of uncountable cardinals whereas the notation system that they call into being corresponds to a recursive ordinal. It has long been claimed that, instead, one should manage to develop such functions directly on the basis of admissible ordinals. This paper is meant to show how this can be done. Interpreting the collapsing functions as operating directly on admissible (...)
    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.
    In this paper we calibrate the exact proof-theoretic strength of Kruskal's theorem, thereby giving, in some sense, the most elementary proof of Kruskal's theorem. Furthermore, these investigations give rise to ordinal analyses of restricted bar induction.
    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 (...)
    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