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 (...)
    Direct download (6 more)  
     
    Export citation  
     
    Bookmark   6 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 (...)
    Direct download (5 more)  
     
    Export citation  
     
    Bookmark   3 citations  
  • From the Weak to the Strong Existence Property.Michael Rathjen - 2012 - Annals of Pure and Applied Logic 163 (10):1400-1418.
  • 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 (...)
    No categories
    Direct download (4 more)  
     
    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.
  • 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 (...)
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark  
  • Approximating beppo levi’s principio di approssimazione.Riccardo Bruni & Peter Schuster - 2014 - Bulletin of Symbolic Logic 20 (2):141-169.
    Direct download (3 more)  
    Translate
     
     
    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 (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   1 citation