The disjunction and related properties for constructive Zermelo-Fraenkel set theory

Journal of Symbolic Logic 70 (4):1233-1254 (2005)
  Copy   BIBTEX

Abstract

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.

Categories

Keywords

Reprint years

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 93,296

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

My notes

Similar books and articles

A note on Bar Induction in Constructive Set Theory.Michael Rathjen - 2006 - Mathematical Logic Quarterly 52 (3):253-258.
Extensional Realizability and Choice for Dependent Types in Intuitionistic Set Theory.Emanuele Frittaion - 2023 - Journal of Symbolic Logic 88 (3):1138-1169.
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 and the limited principle of omniscience.Michael Rathjen - 2014 - Annals of Pure and Applied Logic 165 (2):563-572.
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.
The first-order logic of CZF is intuitionistic first-order logic.Robert Passmann - 2024 - Journal of Symbolic Logic 89 (1):308-330.
Realizability models for constructive set theories with restricted induction principles.Laura Crosilla - unknown
Inaccessible set axioms may have little consistency strength.L. Crosilla & M. Rathjen - 2002 - Annals of Pure and Applied Logic 115 (1-3):33-70.
CZF does not have the existence property.Andrew W. Swan - 2014 - Annals of Pure and Applied Logic 165 (5):1115-1147.
Lifschitz realizability as a topological construction.Michael Rathjen & Andrew W. Swan - 2020 - Journal of Symbolic Logic 85 (4):1342-1375.

Analytics

Added to PP
2010-08-24

Downloads
30 (#550,897)

6 months
12 (#243,143)

Historical graph of downloads
How can I increase my downloads?

Author's Profile

Michael Rathjen
University of Leeds

Citations of this work

From the weak to the strong existence property.Michael Rathjen - 2012 - Annals of Pure and Applied Logic 163 (10):1400-1418.
Set theory: Constructive and intuitionistic ZF.Laura Crosilla - 2010 - Stanford Encyclopedia of Philosophy.

View all 12 citations / Add more citations

References found in this work

Formal systems for some branches of intuitionistic analysis.G. Kreisel - 1970 - Annals of Mathematical Logic 1 (3):229.
The strength of some Martin-Löf type theories.Edward Griffor & Michael Rathjen - 1994 - Archive for Mathematical Logic 33 (5):347-385.
Realizability and recursive set theory.Charles McCarty - 1986 - Annals of Pure and Applied Logic 32:153-183.
Inaccessible set axioms may have little consistency strength.L. Crosilla & M. Rathjen - 2002 - Annals of Pure and Applied Logic 115 (1-3):33-70.

View all 6 references / Add more references