Switch to: Citations

Add references

You must login to add references.
  1. Extending constructive operational set theory by impredicative principles.Andrea Cantini - 2011 - Mathematical Logic Quarterly 57 (3):299-322.
    We study constructive set theories, which deal with operations applying both to sets and operations themselves. Our starting point is a fully explicit, finitely axiomatized system ESTE of constructive sets and operations, which was shown in 10 to be as strong as PA. In this paper we consider extensions with operations, which internally represent description operators, unbounded set quantifiers and local fixed point operators. We investigate the proof theoretic strength of the resulting systems, which turn out to be impredicative . (...)
    Download  
     
    Export citation  
     
    Bookmark   3 citations  
  • (1 other version)Explicit mathematics and operational set theory: Some ontological comparisons.Gerhard Jäger & Rico Zumbrunnen - 2017 - Association for Symbolic Logic: The Bulletin of Symbolic Logic.
    We discuss several ontological properties of explicit mathematics and operational set theory: global choice, decidable classes, totality and extensionality of operations, function spaces, class and set formation via formulas that contain the definedness predicate and applications.
    Download  
     
    Export citation  
     
    Bookmark   3 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  
  • On Feferman’s operational set theory OST.Gerhard Jäger - 2007 - Annals of Pure and Applied Logic 150 (1-3):19-39.
    We study and some of its most important extensions primarily from a proof-theoretic perspective, determine their consistency strengths by exhibiting equivalent systems in the realm of traditional set theory and introduce a new and interesting extension of which is conservative over.
    Download  
     
    Export citation  
     
    Bookmark   14 citations  
  • Operational closure and stability.Gerhard Jäger - 2013 - Annals of Pure and Applied Logic 164 (7-8):813-821.
    In this article we introduce and study the notion of operational closure: a transitive set d is called operationally closed iff it contains all constants of OST and any operation f∈d applied to an element a∈d yields an element fa∈d, provided that f applied to a has a value at all. We will show that there is a direct relationship between operational closure and stability in the sense that operationally closed sets behave like Σ1 substructures of the universe. This leads (...)
    Download  
     
    Export citation  
     
    Bookmark   3 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  
  • About the Strength of Operational Regularity.Gerhard Jäger & Rico Zumbrunnen - 2012 - In Ulrich Berger, Hannes Diener, Peter Schuster & Monika Seisenberger (eds.), Logic, Construction, Computation. De Gruyter. pp. 305-324.
    Download  
     
    Export citation  
     
    Bookmark   3 citations  
  • Operational set theory and small large cardinals.Solomon Feferman with with R. L. Vaught - manuscript
    “Small” large cardinal notions in the language of ZFC are those large cardinal notions that are consistent with V = L. Besides their original formulation in classical set theory, we have a variety of analogue notions in systems of admissible set theory, admissible recursion theory, constructive set theory, constructive type theory, explicit mathematics and recursive ordinal notations (as used in proof theory). On the face of it, it is surprising that such distinctively set-theoretical notions have analogues in such disaparate and (...)
    Download  
     
    Export citation  
     
    Bookmark   2 citations  
  • Constructive Set Theory with Operations.Andrea Cantini & Laura Crosilla - 2007 - In Alessandro Andretta, Keith Kearnes & Domenico Zambella (eds.), Logic Colloquium 2004: Proceedings of the Annual European Summer Meeting of the Association for Symbolic Logic, Held in Torino, Italy, July 25-31, 2004. Cambridge: Cambridge University Press.
    We present an extension of constructive Zermelo{Fraenkel set theory [2]. Constructive sets are endowed with an applicative structure, which allows us to express several set theoretic constructs uniformly and explicitly. From the proof theoretic point of view, the addition is shown to be conservative. In particular, we single out a theory of constructive sets with operations which has the same strength as Peano arithmetic.
    Download  
     
    Export citation  
     
    Bookmark   3 citations  
  • Power types in explicit mathematics?Gerhard Jager - 1997 - Journal of Symbolic Logic 62 (4):1142-1146.
    In this note it is shown that in explicit mathematics the strong power type axiom is inconsistent with (uniform) elementary comprehension and discuss some general aspects of power types in explicit mathematics.
    Download  
     
    Export citation  
     
    Bookmark   6 citations  
  • Full operational set theory with unbounded existential quantification and power set.Gerhard Jäger - 2009 - Annals of Pure and Applied Logic 160 (1):33-52.
    We study the extension of Feferman’s operational set theory provided by adding operational versions of unbounded existential quantification and power set and determine its proof-theoretic strength in terms of a suitable theory of sets and classes.
    Download  
     
    Export citation  
     
    Bookmark   9 citations  
  • Systems of explicit mathematics with non-constructive μ-operator. Part II.Solomon Feferman & Gerhard Jäger - 1996 - Annals of Pure and Applied Logic 79 (1):37-52.
    This paper is mainly concerned with proof-theoretic analysis of some second-order systems of explicit mathematics with a non-constructive minimum operator. By introducing axioms for variable types we extend our first-order theory BON to the elementary explicit type theory EET and add several forms of induction as well as axioms for μ. The principal results then state: EET plus set induction is proof-theoretically equivalent to Peano arithmetic PA <0).
    Download  
     
    Export citation  
     
    Bookmark   28 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  
  • Elementary Constructive Operational Set Theory.Andrea Cantini & Laura Crosilla - 2010 - In Ralf Schindler (ed.), Ways of Proof Theory. De Gruyter. pp. 199-240.
    We introduce an operational set theory in the style of [5] and [16]. The theory we develop here is a theory of constructive sets and operations. One motivation behind constructive operational set theory is to merge a constructive notion of set ([1], [2]) with some aspects which are typical of explicit mathematics [14]. In particular, one has non-extensional operations (or rules) alongside extensional constructive sets. Operations are in general partial and a limited form of self{application is permitted. The system we (...)
    Download  
     
    Export citation  
     
    Bookmark   3 citations