Switch to: Citations

Add references

You must login to add references.
  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 (5 more)  
     
    Export citation  
     
    Bookmark   7 citations  
  • Constructive set theory.John Myhill - 1975 - Journal of Symbolic Logic 40 (3):347-382.
    Direct download (8 more)  
     
    Export citation  
     
    Bookmark   78 citations  
  • Independence results around constructive ZF.Robert S. Lubarsky - 2005 - Annals of Pure and Applied Logic 132 (2-3):209-225.
    CZF is an intuitionistic set theory that does not contain Power Set, substituting instead a weaker version, Subset Collection. In this paper a Kripke model of CZF is presented in which Power Set is false. In addition, another Kripke model is presented of CZF with Subset Collection replaced by Exponentiation, in which Subset Collection fails.
    Direct download (6 more)  
     
    Export citation  
     
    Bookmark   19 citations  
  • CZF and second order arithmetic.Robert S. Lubarsky - 2006 - Annals of Pure and Applied Logic 141 (1):29-34.
    Constructive ZF + full separation is shown to be equiconsistent with Second Order Arithmetic.
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   9 citations  
  • Heyting-valued interpretations for constructive set theory.Nicola Gambino - 2006 - Annals of Pure and Applied Logic 137 (1-3):164-188.
    We define and investigate Heyting-valued interpretations for Constructive Zermelo–Frankel set theory . These interpretations provide models for CZF that are analogous to Boolean-valued models for ZF and to Heyting-valued models for IZF. Heyting-valued interpretations are defined here using set-generated frames and formal topologies. As applications of Heyting-valued interpretations, we present a relative consistency result and an independence proof.
    Direct download (5 more)  
     
    Export citation  
     
    Bookmark   17 citations  
  • 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