Constructive Set Theory

Origin. Myhill and Aczel developed Constructive Zermelo-Fraenkel (CZF) set theory (1970s-80s). Intuitionistic set theory preserving constructive meaning. Alternative: Intuitionistic ZF (IZF). Foundation for constructive mathematics without choice or excluded middle.

Models. Sets without classical axioms. ZFC: classical, includes choice and excluded middle. CZF: constructive, no choice, restricted separation. Existence claims require construction. Proof-theoretic strength calibrated. Models in realizability and type theory.

Formalism.

CZF axioms:

1. Extensionality: ∀x.(x ∈ a ↔ x ∈ b) → a = b
2. Pairing: ∃c.∀x.(x ∈ c ↔ x = a ∨ x = b)
3. Union: ∃c.∀x.(x ∈ c ↔ ∃y ∈ a. x ∈ y)
4. Restricted separation: ∃c.∀x.(x ∈ c ↔ x ∈ a ∧ φ(x)) for restricted φ
5. Strong collection: ∀x ∈ a.∃y.φ(x,y) → ∃b.∀x ∈ a.∃y ∈ b.φ(x,y) ∧ ∀y ∈ b.∃x ∈ a.φ(x,y)
6. Infinity: ω exists
7. Set induction: (∀x.(∀y ∈ x.φ(y)) → φ(x)) → ∀x.φ(x)
8. Subset collection: a predicative surrogate for power set; implies exponentiation (the class of functions a → b is a set)

Restricted formulas: Δ₀: bounded quantifiers only (∀x ∈ a, ∃x ∈ a). Full separation with arbitrary φ is too strong constructively.

IZF vs CZF: IZF: intuitionistic logic + ZF axioms (full separation, powerset). CZF: weaker, avoids impredicativity. CZF ⊂ IZF proof-theoretically.

No excluded middle: ¬¬∃x.φ(x) does not imply ∃x.φ(x). Must construct witness.

Symbols.

Metatheory. CZF is predicative in a precise sense: Aczel (1978) interpreted it in Martin-Löf type theory with one universe and W-types, and Rathjen's ordinal analysis puts its proof-theoretic ordinal at the Bachmann–Howard ordinal, so CZF, Kripke–Platek set theory with infinity and ID₁ are all of the same strength — far below ZF, and below second-order arithmetic. IZF is a different animal: Friedman (1973) showed it is equiconsistent with ZF, since the double-negation translation interprets ZF inside it, so intuitionistic logic alone brings no reduction in strength, and CZF's weakness comes from restricted separation and the absence of power set. Adding excluded middle to CZF yields ZF. Choice is not simply absent but excluded: the Diaconescu–Goodman–Myhill argument derives excluded middle from full AC in the presence of separation and extensionality, so only weak choice principles (countable choice, dependent choice, the presentation axiom) are compatible. Rathjen (2005) proved CZF has the disjunction and numerical existence properties, whereas Friedman and Ščedrov (1985) showed IZF lacks the existence property outright. Strengthening CZF by the regular extension axiom raises it to the strength of Kripke–Platek with one recursively inaccessible.

Applies to. Constructive mathematics foundations. Type theory connections. Proof assistants (Coq, Agda foundations). Predicative mathematics. Formal topology. Bishop-style analysis.

Limitations. CZF has no power set. It cannot prove that the subsets of a singleton form a set, so the truth values are a proper class and Cantor's theorem has no statement in its usual form; the Dedekind reals are recovered only through subset collection, and even then the classical ordinal and cardinal arithmetic built on power set is unavailable. Excluded middle is not merely unassumed but incompatible with the intended reading: trichotomy for the reals, the decidability of equality on ℝ, the law of trichotomy for cardinals, Zorn's lemma and any well-ordering of ℝ all fail, and full AC would restore excluded middle. Restricted separation means a subclass of a set carved out by an unbounded formula — the halting indices inside ω, for instance — is not delivered as a set at all. CZF cannot prove Con(CZF), and being far weaker than ZF it cannot prove Con(ZF) or the consistency of any impredicative theory. The intuitionistic logic removes no consistency strength by itself: IZF is exactly as strong as ZF and, by Friedman and Ščedrov, does not even deliver the existence property that motivates it.

© 2026 Lingenic LLC