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

intuitionistic set theoryrecursive realizabilityequiconsistency

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

• 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?)
• Algebraic set theory and the effective topos
• Constructive set theory
• 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

(11)

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

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)