= Intuitionistic Zermelo–Fraenkel set theory
{title2=$\mathsf{IZF}$}
= IZF
{c}
{synonym}
Full intuitionistic Zermelo–Fraenkel set theory uses <intuitionistic first-order logic>, extensionality, pairing, union, infinity, full separation, power set, collection and <epsilon induction>. Collection is stronger than replacement intuitionistically. This is distinct from predicative constructive ZF, which restricts separation and replaces full power set. The full theory supports a <Boolean-valued inner universe over intuitionistic set theory>, giving the relative consistency of classical <ZF>.
Back to article page
