nLab Mostowski set theory

Redirected from "constructive Mostowski set theory".

Context

Foundations

foundations

The basis of it all

 Set theory

set theory

Foundational axioms

foundational axioms

Removing axioms

Contents

Idea

Mostowski set theory is a well-founded material set theory which is equivalent in strength to the structural set theories of ETCS and bounded SEAR with choice.

 Definition

In classical logic

We assume that we are working in full classical logic. Mostowski set theory has the following axioms and axiom schemata:

  1. Extensionality: for any set xx and yy, x=yx = y if and only if for all zz, zxz \in x if and only if zyz \in y.

  2. Empty set: there is a set ={}\varnothing = \{\}.

  3. Pairing: for all sets xx and yy, there is a set {x,y}\{x, y\}

  4. Union: for all sets xx, there is a set {z|yx.zy}\{z \vert \exists y \in x.z \in y\}

  5. Schema of Δ 0 \Delta_0 -separation: for any Δ 0\Delta_0-formula ϕ(x)\phi(x) and for any set aa, there is a set {xa|ϕ(x)}\{x \in a \vert \phi(x)\}

  6. Schema of limited Δ 0\Delta_0-replacement: for any Δ 0\Delta_0-formula ϕ(x,y)\phi(x, y), for all sets aa and bb, if for any set xax \in a there is a unique set yy such that ϕ(x,y)\phi(x, y), and for all zyz \in y, zbz \subseteq b, then there is a set {y|xa.ϕ(x,y)}\{y \vert \exists x \in a.\phi(x, y)\}

  7. Power sets: for any set xx, there is a set 𝒫(x)={y|yx}\mathcal{P}(x) = \{y \vert y \subseteq x\}

  8. Infinity: there is a set ω\omega such that for all sets xx, xωx \in \omega if and only if x=x = \emptyset or there exists a set yωy \in \omega such that y{y}=xy \cup \{y\} = x.

  9. Choice: for any set aa, if for all xax \in a there is a set yxy \in x, then there is a function ff from aa to a\bigcup a such that f(x)xf(x) \in x for all xax \in a.

  10. Regularity: if there is a set yxy \in x, then there is a set yxy \in x such that xy=x \cap y = \emptyset

  11. Transitive closure: every set is a subset of a smallest transitive set

  12. Mostowski's principle: every well-founded extensional relation is isomorphic to a transitive set equipped with the relation \in.

This implies that Mostowski set theory is equivalent in strength to ETCS, a well-pointed topos with natural numbers object and the axiom of choice.

Variations of Mostowski set theory in classical logic

By removing axiom 9 from Mostowski set theory, one gets Mostowski set theory without choice, which is equivalent in strength to a well-pointed Boolean topos with natural numbers object and the axiom of well-founded materialization.

By removing axiom 7 from Mostowski set theory, one gets predicative Mostowski set theory, which is equivalent in strength to a well-pointed Boolean pretopos with natural numbers object and the axiom of choice.

By removing axiom 8 from Mostowski set theory, one gets weakly finitist Mostowski set theory, which is equivalent in strength to a well-pointed Boolean topos with the axiom of choice.

If one replaces axiom 8 with the axiom of finiteness (for any formula ϕ\phi, if ϕ()\phi(\emptyset) and for all sets xx, ϕ(x)\phi(x) implies that ϕ(x{x})\phi(x \cup \{x\}), then for all sets xx, ϕ(x)\phi(x)), one gets strongly finitist Mostowski set theory, which is equivalent in strength to the category FinSet. Axioms 7 and 9 are redundant in this formulation, since both are implied by the axiom of finiteness.

Thus, the most general variation of Mostowski set theory in classical logic is weakly finitist predicative Mostowski set theory without choice, which consists of axioms 1-6 and 10-12, and is equivalent in strength to a general well-pointed Boolean pretopos with the axiom of well-founded materialization.

In intuitionisitc logic

Now, we assume that we are working in intuitionistic logic. Then Δ 0\Delta_0-classical Mostowski set theory has the following axioms and axiom schemata:

  1. Extensionality: for any set xx and yy, x=yx = y if and only if for all zz, zxz \in x if and only if zyz \in y.

  2. Empty set: there is a set ={}\varnothing = \{\}.

  3. Pairing: for all sets xx and yy, there is a set {x,y}\{x, y\}

  4. Union: for all sets xx, there is a set {z|yx.zy}\{z \vert \exists y \in x.z \in y\}

  5. Schema of Δ 0 \Delta_0 -separation: for any Δ 0\Delta_0-formula ϕ(x)\phi(x) and for any set aa, there is a set {xa|ϕ(x)}\{x \in a \vert \phi(x)\}

  6. Schema of limited Δ 0\Delta_0-replacement: for any Δ 0\Delta_0-formula ϕ(x,y)\phi(x, y), for all sets aa and bb, if for any set xax \in a there is a unique set yy such that ϕ(x,y)\phi(x, y), and for all zyz \in y, zbz \subseteq b, then there is a set {y|xa.ϕ(x,y)}\{y \vert \exists x \in a.\phi(x, y)\}

  7. Power sets: for any set xx, there is a set 𝒫(x)={y|yx}\mathcal{P}(x) = \{y \vert y \subseteq x\}

  8. Infinity: there is a set ω\omega such that for all sets xx, xωx \in \omega if and only if x=x = \emptyset or there exists a set yωy \in \omega such that y{y}=xy \cup \{y\} = x.

  9. Choice: for any set aa, if for all xax \in a there is a set yxy \in x, then there is a function ff from aa to a\bigcup a such that f(x)xf(x) \in x for all xax \in a.

  10. Regularity: if there is a set yxy \in x, then there is a set yxy \in x such that xy=x \cap y = \emptyset

  11. Transitive closure: every set is a subset of a smallest transitive set

  12. Mostowski's principle: every well-founded extensional relation is isomorphic to a transitive set equipped with the relation \in.

This implies that Mostowski set theory is equivalent in strength to ETCS in intuitionistic logic, a constructively well-pointed topos with natural numbers object and the axiom of choice.

The name Δ 0\Delta_0-classical Mostowski set theory comes from the fact that the law of excluded middle is only valid for Δ 0\Delta_0-formulas in the theory, being a consequence of the axiom of choice, rather than for all formulas in the theory, as in the case for Mostowski set theory in classical logic.

Variations of Mostowski set theory in intuitionistic logic

By removing axiom 9 from Δ 0\Delta_0-classical Mostowski set theory, one gets intuitionistic Mostowski set theory, which is equivalent in strength to a constructively well-pointed topos with natural numbers object and the axiom of well-founded materialization.

By replacing axiom 7 by the axiom of fullness (for all sets aa and bb, the set of entire relations from aa to bb exists) in intuitionistic Mostowski set theory, one gets constructive Mostowski set theory.

By removing axiom 7 from Δ 0\Delta_0-classical Mostowski set theory, one gets predicative Δ 0\Delta_0-classical Mostowski set theory, which is equivalent in strength to a constructively well-pointed Heyting pretopos with natural numbers object and the axiom of choice.

By removing axiom 7 from intuitionistic Mostowski set theory, one gets strongly predicative constructive Mostowski set theory, which is equivalent in strength to a constructively well-pointed Heyting pretopos with a natural numbers object and the axiom of well-founded materialization.

By replacing axiom 7 by the axiom of exponentiation (for all sets aa and bb, the set b ab^a of functions from aa to bb exists) in intuitionistic Mostowski set theory, one gets (neutral) weakly predicative constructive Mostowski set theory, which is equivalent in strength to a constructively well-pointed ΠW-pretopos with the axiom of well-founded materialization.

By removing axiom 8 from any XX Mostowski set theory, with XX being one of (Δ 0\Delta_0-classical, intuitionistic, predicative Δ 0\Delta_0-classical, weakly predicative constructive, strongly predicative constructive), one gets weakly finitist XX Mostowski set theory, which is equivalent in strength to a constructively well-pointed CC, where CC is one of (Boolean topos with the axiom of choice, elementary topos with the axiom of well-founded materialization, Boolean pretopos with the axiom of choice, Π-pretopos with the axiom of well-founded materialization, Heyting pretopos with the axiom of well-founded materialization).

If one replaces axiom 8 in any of the above with the axiom of finiteness (for any formula ϕ\phi, if ϕ()\phi(\emptyset) and for all sets xx, ϕ(x)\phi(x) implies that ϕ(x{x})\phi(x \cup \{x\}), then for all sets xx, ϕ(x)\phi(x)), one gets strongly finitist Mostowski set theory, which is equivalent in strength to the category FinSet. Axioms 7 and 9 are redundant in this formulation, since both are implied by the axiom of finiteness.

Thus, the most general variation of Mostowski set theory in intuitionistic logic is weakly finitist, strongly predicative, constructive Mostowski set theory, which consists of axioms 1-6 and 10-12, and is equivalent in strength to a general constructively well-pointed Heyting pretopos with the axiom of well-founded materialization.

Material-structural adjunctions

Given any material set theory VV which satisfies axioms 1-6. Then one could construct the category 𝕊𝕖𝕥(V)\mathbb{Set}(V) of sets and functions in VV, and 𝕊𝕖𝕥(V)\mathbb{Set}(V) is a constructively well-pointed Heyting pretopos.

Given any constructively well-pointed Heyting pretopos \mathcal{E}, we can construct the type 𝕍()\mathbb{V}(\mathcal{E}) as the type of well-founded extensional accessible pointed graph objects in \mathcal{E}. 𝕍()\mathbb{V}(\mathcal{E}) is a model of material set theory satisfying axioms 1-6 and 10-12.

 See also

 References

Last revised on February 8, 2024 at 15:36:24. See the history of this page for a list of all contributions to it.