Independence results around constructive ZF

DOI10.1016/J.APAL.2004.08.002MaRDI QIDQ1765158zbMATH OpenOpenAlexFDO

Authors Robert S. Lubarsky

Publication date 23 February 2005

Published in Annals of Pure and Applied Logic (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1510.00465

zbMATH Keywords

exponentiationintuitionistic set theoryKripke modelpower setsubset collection

Mathematics Subject Classification ID

Consistency and independence results (03E35) Nonclassical and second-order set theories (03E70)

Abstract: Using Kripke models, it is shown that CZF does not prove Power Set, and that CZF with Subset Collection substituted by Exponentiation does not prove Subset Collection.

Recommendations

• Kripke models for subtheories of \textsf{CZF}
• Constructive Zermelo-Fraenkel Set Theory, Power Set, and the Calculus of Constructions
• Axiom ``collection independence of ``DC principle in intuitionistic set theory
• Replacement versus collection and related topics in constructive Zermelo-Fraenkel set theory
• On the Constructive Dedekind Reals: Extended Abstract

Cites work

• scientific article; zbMATH DE number 3839951 (Why is no real title available?)
• scientific article; zbMATH DE number 3910392 (Why is no real title available?)
• scientific article; zbMATH DE number 4012604 (Why is no real title available?)
• scientific article; zbMATH DE number 3754682 (Why is no real title available?)
• scientific article; zbMATH DE number 3521950 (Why is no real title available?)
• scientific article; zbMATH DE number 1136111 (Why is no real title available?)
• scientific article; zbMATH DE number 2247250 (Why is no real title available?)
• CZF and second order arithmetic
• Constructive set theory
• The lack of definable witnesses and provably recursive functions in intuitionistic set theories
• The strength of some Martin-Löf type theories

Cited in

(20)

• The associated sheaf functor theorem in algebraic set theory
• On the Constructive Dedekind Reals: Extended Abstract
• On adopting Kripke semantics in set theory
• Are there enough injective sets?
• Lawvere–Tierney sheaves in Algebraic Set Theory
• Binary refinement implies discrete exponentiation
• Logics of intuitionistic Kripke-Platek set theory
• Constructive toposes with countable sums as models of constructive set theory
• On constructing completions
• On the constructive Dedekind reals
• A cumulative hierarchy of sets for constructive set theory
• CZF and second order arithmetic
• Forcing in intuitionistic systems without power-set
• Kripke models for subtheories of \textsf{CZF}
• Axiom of power set in \(L^{\mathrm{re}}\)
• The generalised type-theoretic interpretation of constructive set theory
• Replacement versus collection and related topics in constructive Zermelo-Fraenkel set theory
• scientific article; zbMATH DE number 956477 (Why is no real title available?)
• Realizability Models Separating Various Fan Theorems
• Separating the fan theorem and its weakenings. II

This page was built for publication: Independence results around constructive ZF

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1765158)