Switch to: References

Add citations

You must login to add citations.
  1. 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 (...)
    Download  
     
    Export citation  
     
    Bookmark   7 citations  
  • From the weak to the strong existence property.Michael Rathjen - 2012 - Annals of Pure and Applied Logic 163 (10):1400-1418.
    Download  
     
    Export citation  
     
    Bookmark   8 citations  
  • 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 (...)
    Download  
     
    Export citation  
     
    Bookmark   5 citations  
  • Refinement is equivalent to Fullness.Albert Ziegler - 2010 - Mathematical Logic Quarterly 56 (6):666-669.
    In the article [4], a new constructive set theoretic principle called Refinement was introduced and analysed. While it seemed to be significantly weaker than its alternative, the more established axiom of Fullness , it was shown to suffice to imply many of the mathematically important consequences. In this article, we will define for each set A a set of truth values which measures the complexity of the equality relation on A. Using these sets we will show that Refinement is actually (...)
    Download  
     
    Export citation  
     
    Bookmark  
  • Derived rules for predicative set theory: an application of sheaves.Benno van den Berg & Ieke Moerdijk - 2012 - Annals of Pure and Applied Logic 163 (10):1367-1383.
    Download  
     
    Export citation  
     
    Bookmark   4 citations  
  • Set theory: Constructive and intuitionistic ZF.Laura Crosilla - 2010 - Stanford Encyclopedia of Philosophy.
    Constructive and intuitionistic Zermelo-Fraenkel set theories are axiomatic theories of sets in the style of Zermelo-Fraenkel set theory (ZF) which are based on intuitionistic logic. They were introduced in the 1970's and they represent a formal context within which to codify mathematics based on intuitionistic logic. They are formulated on the basis of the standard first order language of Zermelo-Fraenkel set theory and make no direct use of inherently constructive ideas. In working in constructive and intuitionistic ZF we can thus (...)
    Download  
     
    Export citation  
     
    Bookmark   4 citations  
  • Choice and independence of premise rules in intuitionistic set theory.Emanuele Frittaion, Takako Nemoto & Michael Rathjen - 2023 - Annals of Pure and Applied Logic 174 (9):103314.
    Download  
     
    Export citation  
     
    Bookmark  
  • Realisability for infinitary intuitionistic set theory.Merlin Carl, Lorenzo Galeotti & Robert Passmann - 2023 - Annals of Pure and Applied Logic 174 (6):103259.
    Download  
     
    Export citation  
     
    Bookmark  
  • Kripke models for subtheories of CZF.Rosalie Iemhoff - 2010 - Archive for Mathematical Logic 49 (2):147-167.
    In this paper a method to construct Kripke models for subtheories of constructive set theory is introduced that uses constructions from classical model theory such as constructible sets and generic extensions. Under the main construction all axioms except the collection axioms can be shown to hold in the constructed Kripke model. It is shown that by carefully choosing the classical models various instances of the collection axioms, such as exponentiation, can be forced to hold as well. The paper does not (...)
    Download  
     
    Export citation  
     
    Bookmark   2 citations  
  • Numerical Existence Property and Categories with an Internal Copy.Samuele Maschio - 2020 - Logica Universalis 14 (3):383-394.
    We define here a notion of internal copy and of weak internal copy of a category. We will then determine some families of categories having an internal copy or a weak internal copy. We will consider categories of definable classes of first-order theories and we will see that the notion of internal copy is related to the notion of numerical existence property.
    Download  
     
    Export citation  
     
    Bookmark  
  • CZF does not have the existence property.Andrew W. Swan - 2014 - Annals of Pure and Applied Logic 165 (5):1115-1147.
    Constructive theories usually have interesting metamathematical properties where explicit witnesses can be extracted from proofs of existential sentences. For relational theories, probably the most natural of these is the existence property, EP, sometimes referred to as the set existence property. This states that whenever ϕϕ is provable, there is a formula χχ such that ϕ∧χϕ∧χ is provable. It has been known since the 80s that EP holds for some intuitionistic set theories and yet fails for IZF. Despite this, it has (...)
    Download  
     
    Export citation  
     
    Bookmark   1 citation  
  • (1 other version)Approximating beppo levi’s principio di approssimazione.Riccardo Bruni & Peter Schuster - 2014 - Bulletin of Symbolic Logic 20 (2):141-169.
    We try to recast in modern terms a choice principle conceived by Beppo Levi, who called it the Approximation Principle. Up to now, there was almost no discussion about Levi’s contribution, due to the quite obscure formulation of AP the author has chosen. After briefly reviewing the historical and philosophical surroundings of Levi’s proposal, we undertake our own attempt at interpreting AP. The idea underlying the principle, as well as the supposed faithfulness of our version to Levi’s original intention, are (...)
    Download  
     
    Export citation  
     
    Bookmark