The Journal of Symbolic Logic

Research Article

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

Michael Rathjen

Department of Mathematics, Ohio State University, Columbus. OH 43210., USA, E-mail: rathjen@math.ohio-state.edu

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.

(Received September 28 2004)

(Revised May 23 2005)

Key words and phrases

  • Constructive set theory;
  • realizability;
  • metamathematical property