that CZF has the disjunction property and the numerical existence property. Most classical theories, such as Peano arithmetic and ZFC do not have the existence or disjunction property. Some classical theories, such as ZFC plus the axiom of constructibility, do have a weaker form of the existence property (Rathjen 2005). In topoi Freyd and Scedrov (1990) observed that the disjunction property holds in free Heyting algebras and free topoi. In categorical terms, in the free topos, that corresponds to the fact that the terminal object, , is not the join of two proper subobjects. Together with the existence property it translates to the assertion that is an indecomposable projective object—the functor it represents (the global-section functor) preserves epimorphisms and coproducts. Relationships There are several relationship between the five properties discussed above. In the setting of arithmetic, the numerical existence property implies the disjunction property. The proof uses the fact that a disjunction can be rewritten as an existential formula quantifying over natural numbers: . Therefore, if is a theorem of , so is . Thus, assuming the numerical existence property, there exists some such that is a theorem. Since is a numeral, one may concretely check the value of : if then is a theorem and if then is a theorem. Harvey Friedman (1974) proved that in any recursively enumerable extension of intuitionistic arithmetic, the disjunction property implies the numerical existence property. The proof uses self-referential sentences in way similar to the proof of Gödel's incompleteness theorems. The key step is to find a bound on the existential quantifier in a formula (∃x)A(x), producing a bounded existential formula (∃x<n)A(x). The bounded formula may then be written as a finite disjunction A(1)∨A(2)∨...∨A(n). Finally, disjunction elimination may be used to show that one of the disjuncts is provable. See also Constructive set theory Heyting arithmetic Law of excluded middle Realizability Existential quantifier References Peter J. Freyd and Andre Scedrov, 1990, Categories, Allegories. North-Holland. Harvey Friedman, 1975, The disjunction property implies the numerical existence property, State University of New York at Buffalo. Gerhard Gentzen, 1934, "Untersuchungen über das logische Schließen. I", Mathematische Zeitschrift v. 39 n. 2, pp. 176–210. Gerhard Gentzen, 1935, "Untersuchungen über das logische Schließen. II", Mathematische Zeitschrift v. 39 n. 3, pp. 405–431. Kurt Gödel, 1932, "Zum intuitionistischen Aussagenkalkül", Anzeiger der Akademie der Wissenschaftischen in Wien, v. 69, pp. 65–66. Stephen Cole Kleene, 1945, "On the interpretation of intuitionistic number