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)

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 proof-theoretically weaker than ZF. Interpretable in Martin-Löf type theory. IZF equiconsistent with ZF. Realizability models exist. No choice or excluded middle derivable. Ordinal analysis possible.

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

Limitations. Weaker than ZF — some classical results unavailable. Requires constructive reasoning habits. Multiple systems (CZF, IZF, etc.) — no single standard. Less familiar than ZFC. Proof-theoretic analysis technical.

© 2026 Lingenic LLC