Realizability for constructive Zermelo-Fraenkel set theory
Michael Rathjen · Cambridge University Press eBooks · 2017
Constructive Zermelo-Fraenkel Set Theory, CZF, has emerged as a standard reference theory that relates to constructive predicative mathematics as ZFC relates to classical Cantorian mathematics. A hallmark of this theory is that it possesses a type-theoretic model. Aczel showed that it has a formulae-as-types interpretation in Martin-Löf’s intuitionist theory of types [14, 15]. This paper, though, is concerned with a rather different interpretation. It is shown that Kleene realizability provides a self-validating semantics for CZF, viz. this notion of realizability can be formalized in CZF and demonstrably in CZF it can be verified that every theorem of CZF is realized. This semantics, then, is put to use in establishing several equiconsistency results. Specifically, augmenting CZF by well-known principles germane to Russian constructivism and Brouwer’s intuitionism turns out to engender theories of equal proof-theoretic strength with the same stock of provably recursive functions.