65 found
Order:
  1.  81
    The strength of some Martin-Löf type theories.Edward Griffor & Michael Rathjen - 1994 - 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 (3 more)  
     
    Export citation  
     
    Bookmark   48 citations  
  2. Proof-theoretic analysis of KPM.Michael Rathjen - 1991 - 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)  
     
    Export citation  
     
    Bookmark   42 citations  
  3.  56
    Handbook of Constructive Mathematics.Douglas Bridges, Hajime Ishihara, Michael Rathjen & Helmut Schwichtenberg (eds.) - 2023 - Cambridge: Cambridge University Press.
    Constructive mathematics – mathematics in which ‘there exists’ always means ‘we can construct’ – is enjoying a renaissance. Fifty years on from Bishop’s groundbreaking account of constructive analysis, constructive mathematics has spread out to touch almost all areas of mathematics and to have profound influence in theoretical computer science. This handbook gives the most complete overview of modern constructive mathematics, with contributions from leading specialists surveying the subject’s myriad aspects. Major themes include: constructive algebra and geometry, constructive analysis, constructive topology, (...)
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  4.  50
    Proof theory of reflection.Michael Rathjen - 1994 - 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 (4 more)  
     
    Export citation  
     
    Bookmark   37 citations  
  5.  45
    Proof-theoretic investigations on Kruskal's theorem.Michael Rathjen & Andreas Weiermann - 1993 - 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 (4 more)  
     
    Export citation  
     
    Bookmark   34 citations  
  6.  26
    Admissible extensions of subtheories of second order arithmetic.Gerhard Jäger & Michael Rathjen - 2024 - Annals of Pure and Applied Logic 175 (7):103425.
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  7.  44
    Constructing the constructible universe constructively.Michael Rathjen - 2024 - Annals of Pure and Applied Logic 175 (3):103392.
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  8. An ordinal analysis for theories of self-referential truth.Graham Emil Leigh & Michael Rathjen - 2010 - 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)  
     
    Export citation  
     
    Bookmark   14 citations  
  9. An ordinal analysis of parameter free Π12-comprehension.Michael Rathjen - 2005 - Archive for Mathematical Logic 44 (3):263-362.
    Abstract.This paper is the second in a series of three culminating in an ordinal analysis of Π12-comprehension. Its objective is to present an ordinal analysis for the subsystem of second order arithmetic with Δ12-comprehension, bar induction and Π12-comprehension for formulae without set parameters. Couched in terms of Kripke-Platek set theory, KP, the latter system corresponds to KPi augmented by the assertion that there exists a stable ordinal, where KPi is KP with an additional axiom stating that every set is contained (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   18 citations  
  10. Ordinal notations based on a weakly Mahlo cardinal.Michael Rathjen - 1990 - Archive for Mathematical Logic 29 (4):249-263.
  11.  69
    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 (...)
    Direct download (8 more)  
     
    Export citation  
     
    Bookmark   17 citations  
  12.  77
    Slow consistency.Sy-David Friedman, Michael Rathjen & Andreas Weiermann - 2013 - 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)  
     
    Export citation  
     
    Bookmark   9 citations  
  13.  90
    On the constructive Dedekind reals.Robert S. Lubarsky & Michael Rathjen - 2008 - 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)  
     
    Export citation  
     
    Bookmark   11 citations  
  14.  31
    Derivatives of normal functions in reverse mathematics.Anton Freund & Michael Rathjen - 2021 - Annals of Pure and Applied Logic 172 (2):102890.
  15. From the weak to the strong existence property.Michael Rathjen - 2012 - Annals of Pure and Applied Logic 163 (10):1400-1418.
  16. A proof-theoretic characterization of the primitive recursive set functions.Michael Rathjen - 1992 - 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 (8 more)  
     
    Export citation  
     
    Bookmark   11 citations  
  17. An ordinal analysis of stability.Michael Rathjen - 2005 - Archive for Mathematical Logic 44 (1):1-62.
    Abstract.This paper is the first in a series of three which culminates in an ordinal analysis of Π12-comprehension. On the set-theoretic side Π12-comprehension corresponds to Kripke-Platek set theory, KP, plus Σ1-separation. The strength of the latter theory is encapsulated in the fact that it proves the existence of ordinals π such that, for all β>π, π is β-stable, i.e. Lπ is a Σ1-elementary substructure of Lβ. The objective of this paper is to give an ordinal analysis of a scenario of (...)
    Direct download (5 more)  
     
    Export citation  
     
    Bookmark   12 citations  
  18.  47
    The disjunction and related properties for constructive Zermelo-Fraenkel set theory.Michael Rathjen - 2005 - 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 (4 more)  
     
    Export citation  
     
    Bookmark   12 citations  
  19.  45
    How to develop Proof‐Theoretic Ordinal Functions on the basis of admissible ordinals.Michael Rathjen - 1993 - 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 (2 more)  
     
    Export citation  
     
    Bookmark   11 citations  
  20.  77
    Reverse mathematics and well-ordering principles: A pilot study.Bahareh Afshari & Michael Rathjen - 2009 - 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 (4 more)  
     
    Export citation  
     
    Bookmark   8 citations  
  21.  58
    Inaccessibility in constructive set theory and type theory.Michael Rathjen, Edward R. Griffor & Erik Palmgren - 1998 - 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 (5 more)  
     
    Export citation  
     
    Bookmark   10 citations  
  22.  47
    Relativized ordinal analysis: The case of Power Kripke–Platek set theory.Michael Rathjen - 2014 - 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 (4 more)  
     
    Export citation  
     
    Bookmark   5 citations  
  23.  87
    The strength of Martin-Löf type theory with a superuniverse. Part I.Michael Rathjen - 2000 - 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)  
     
    Export citation  
     
    Bookmark   10 citations  
  24.  27
    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 (...)
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark   9 citations  
  25. Lifschitz realizability for intuitionistic Zermelo–Fraenkel set theory.Ray-Ming Chen & Michael Rathjen - 2012 - 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 (5 more)  
     
    Export citation  
     
    Bookmark   5 citations  
  26.  43
    Intuitionistic sets and numbers: small set theory and Heyting arithmetic.Stewart Shapiro, Charles McCarty & Michael Rathjen - forthcoming - Archive for Mathematical Logic.
    It has long been known that (classical) Peano arithmetic is, in some strong sense, “equivalent” to the variant of (classical) Zermelo–Fraenkel set theory (including choice) in which the axiom of infinity is replaced by its negation. The intended model of the latter is the set of hereditarily finite sets. The connection between the theories is so tight that they may be taken as notational variants of each other. Our purpose here is to develop and establish a constructive version of this. (...)
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark  
  27.  40
    An order-theoretic characterization of the Howard–Bachmann-hierarchy.Jeroen Van der Meeren, Michael Rathjen & Andreas Weiermann - 2017 - Archive for Mathematical Logic 56 (1-2):79-118.
    In this article we provide an intrinsic characterization of the famous Howard–Bachmann ordinal in terms of a natural well-partial-ordering by showing that this ordinal can be realized as a maximal order type of a class of generalized trees with respect to a homeomorphic embeddability relation. We use our calculations to draw some conclusions about some corresponding subsystems of second order arithmetic. All these subsystems deal with versions of light-face Π11\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\varPi ^1_1$$\end{document}-comprehension.
    No categories
    Direct download (5 more)  
     
    Export citation  
     
    Bookmark   3 citations  
  28.  57
    A note on the theory of positive induction, $${{\rm ID}^*_1}$$.Bahareh Afshari & Michael Rathjen - 2010 - 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)  
     
    Export citation  
     
    Bookmark   6 citations  
  29.  98
    The Friedman—Sheard programme in intuitionistic logic.Graham E. Leigh & Michael Rathjen - 2012 - 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 (6 more)  
     
    Export citation  
     
    Bookmark   5 citations  
  30.  45
    Constructive Zermelo–Fraenkel set theory and the limited principle of omniscience.Michael Rathjen - 2014 - 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 (6 more)  
     
    Export citation  
     
    Bookmark   4 citations  
  31.  55
    Characterizing the interpretation of set theory in Martin-Löf type theory.Michael Rathjen & Sergei Tupailo - 2006 - 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 (5 more)  
     
    Export citation  
     
    Bookmark   7 citations  
  32.  45
    Indefiniteness in semi-intuitionistic set theories: On a conjecture of Feferman.Michael Rathjen - 2016 - Journal of Symbolic Logic 81 (2):742-754.
    The paper proves a conjecture of Solomon Feferman concerning the indefiniteness of the continuum hypothesis relative to a semi-intuitionistic set theory.
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark   3 citations  
  33.  29
    Remarks on Barr’s Theorem: Proofs in Geometric Theories.Michael Rathjen - 2016 - In Peter Schuster & Dieter Probst (eds.), Concepts of Proof in Mathematics, Philosophy, and Computer Science. Boston: De Gruyter. pp. 347-374.
    Direct download  
     
    Export citation  
     
    Bookmark   3 citations  
  34.  68
    The role of parameters in bar rule and bar induction.Michael Rathjen - 1991 - 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 (8 more)  
     
    Export citation  
     
    Bookmark   7 citations  
  35. Explicit mathematics with the monotone fixed point principle. II: Models.Michael Rathjen - 1999 - 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 (8 more)  
     
    Export citation  
     
    Bookmark   6 citations  
  36.  36
    Well-partial-orderings and the big Veblen number.Jeroen Van der Meeren, Michael Rathjen & Andreas Weiermann - 2015 - Archive for Mathematical Logic 54 (1-2):193-230.
    In this article we characterize a countable ordinal known as the big Veblen number in terms of natural well-partially ordered tree-like structures. To this end, we consider generalized trees where the immediate subtrees are grouped in pairs with address-like objects. Motivated by natural ordering properties, extracted from the standard notations for the big Veblen number, we investigate different choices for embeddability relations on the generalized trees. We observe that for addresses using one finite sequence only, the embeddability coincides with the (...)
    No categories
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark   3 citations  
  37.  64
    The Constructive Hilbert Program and the Limits of Martin-Löf Type Theory.Michael Rathjen - 2005 - Synthese 147 (1):81-120.
  38.  40
    The natural numbers in constructive set theory.Michael Rathjen - 2008 - 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  
     
    Export citation  
     
    Bookmark   5 citations  
  39.  30
    Reverse mathematics and well-ordering principles.Michael Rathjen & Andreas Weiermann - 2011 - In S. B. Cooper & Andrea Sorbi (eds.), Computability in Context: Computation and Logic in the Real World. World Scientific.
  40.  48
    Ordinal notation systems corresponding to Friedman’s linearized well-partial-orders with gap-condition.Michael Rathjen, Jeroen Van der Meeren & Andreas Weiermann - 2017 - Archive for Mathematical Logic 56 (5-6):607-638.
    In this article we investigate whether the following conjecture is true or not: does the addition-free theta functions form a canonical notation system for the linear versions of Friedman’s well-partial-orders with the so-called gap-condition over a finite set of n labels. Rather surprisingly, we can show this is the case for two labels, but not for more than two labels. To this end, we determine the order type of the notation systems for addition-free theta functions in terms of ordinals less (...)
    No categories
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  41.  46
    Theories and Ordinals in Proof Theory.Michael Rathjen - 2006 - 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 (4 more)  
     
    Export citation  
     
    Bookmark   5 citations  
  42.  34
    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 (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   5 citations  
  43.  65
    A note on Bar Induction in Constructive Set Theory.Michael Rathjen - 2006 - 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 (2 more)  
     
    Export citation  
     
    Bookmark   4 citations  
  44.  64
    The strength of Martin-Löf type theory with a superuniverse. Part II.Michael Rathjen - 2001 - 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)  
     
    Export citation  
     
    Bookmark   4 citations  
  45.  49
    On the regular extension axiom and its variants.Robert S. Lubarsky & Michael Rathjen - 2003 - 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 (2 more)  
     
    Export citation  
     
    Bookmark   4 citations  
  46.  37
    The Recursively Mahlo Property in Second Order Arithmetic.Michael Rathjen - 1996 - 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  
     
    Export citation  
     
    Bookmark   4 citations  
  47. Kripke-Platek Set Theory and the Anti-Foundation Axiom.Michael Rathjen - 2001 - Mathematical Logic Quarterly 47 (4):435-440.
    The paper investigates the strength of the Anti-Foundation Axiom, AFA, on the basis of Kripke-Platek set theory without Foundation. It is shown that the addition of AFA considerably increases the proof theoretic strength.
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark   3 citations  
  48.  55
    Monotone inductive definitions in explicit mathematics.Michael Rathjen - 1996 - 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 (8 more)  
     
    Export citation  
     
    Bookmark   3 citations  
  49.  67
    Realizing Mahlo set theory in type theory.Michael Rathjen - 2003 - 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)  
     
    Export citation  
     
    Bookmark   3 citations  
  50. Proof Theory of Constructive Systems: Inductive Types and Univalence.Michael Rathjen - 2017 - In Gerhard Jäger & Wilfried Sieg (eds.), Feferman on Foundations: Logic, Mathematics, Philosophy. Cham: Springer.
    No categories
     
    Export citation  
     
    Bookmark   1 citation  
1 — 50 / 65