CZF and second order arithmetic

DOI10.1016/J.APAL.2005.07.002MaRDI QIDQ2498896zbMATH OpenOpenAlexFDO

Authors Robert S. Lubarsky

Publication date 16 August 2006

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

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

zbMATH Keywords

equiconsistencyintuitionistic set theoryrecursive realizability

Mathematics Subject Classification ID

Nonclassical and second-order set theories (03E70) Second- and higher-order arithmetic and fragments (03F35) Intuitionistic mathematics (03F55)

Abstract: CZF + Separation is shown to be equiconsistent with second-order arithmetic, using realizability.

Cites work

• Algebraic set theory and the effective topos
• Constructive set theory
• scientific article; zbMATH DE number 3839951 (Why is no real title available?)
• scientific article; zbMATH DE number 3900744 (Why is no real title available?)
• scientific article; zbMATH DE number 4012604 (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?)
• Independence results around constructive ZF
• Iterated inductive definitions and subsystems of analysis: recent proof-theoretical studies
• Metamathematical investigation of intuitionistic arithmetic and analysis. With contributions by C. A. Smorynski, J. I. Zucker and W. A. Howard
• The strength of some Martin-Löf type theories

Cited in

(13)

• Independence results around constructive ZF
• Kripke models for subtheories of \textsf{CZF}
• On Tarski’s fixed point theorem
• Extending constructive operational set theory by impredicative principles
• On the existence of Stone-Čech compactification
• Topological inductive definitions
• scientific article; zbMATH DE number 6983478 (Why is no real title available?)
• Constructive Zermelo-Fraenkel Set Theory, Power Set, and the Calculus of Constructions
• Aspects of predicative algebraic set theory. II: Realizability
• Choice and independence of premise rules in intuitionistic set theory
• The proof-theoretic strength of constructive second-order set theories
• Very large set axioms over constructive set theories
• Aspects of predicative algebraic set theory. I: Exact completion

This page was built for publication: CZF and second order arithmetic

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