Switch to: References

Add citations

You must login to add citations.
  1. 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  
  • 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   1 citation  
  • The Generalised Type-Theoretic Interpretation of Constructive Set Theory.Nicola Gambino & Peter Aczel - 2006 - Journal of Symbolic Logic 71 (1):67 - 103.
    We present a generalisation of the type-theoretic interpretation of constructive set theory into Martin-Löf type theory. The original interpretation treated logic in Martin-Löf type theory via the propositions-as-types interpretation. The generalisation involves replacing Martin-Löf type theory with a new type theory in which logic is treated as primitive. The primitive treatment of logic in type theories allows us to study reinterpretations of logic, such as the double-negation translation.
    Direct download (5 more)  
     
    Export citation  
     
    Bookmark   8 citations  
  • The associated sheaf functor theorem in algebraic set theory.Nicola Gambino - 2008 - Annals of Pure and Applied Logic 156 (1):68-77.
    We prove a version of the associated sheaf functor theorem in Algebraic Set Theory. The proof is established working within a Heyting pretopos equipped with a system of small maps satisfying the axioms originally introduced by Joyal and Moerdijk. This result improves on the existing developments by avoiding the assumption of additional axioms for small maps and the use of collection sites.
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   3 citations