Is ZFC's Wikipedia article accurate about the redundancy of the axiom schema of specification?

Question

I have a question about the redundancy of the axiom schema of specification that mentioned in the Wikipedia article Zermelo–Fraenkel set theory. I am sure that in some formulations of ZFC, this axiom actually follows from the axiom schema of replacement and the axiom of the empty set. However, in the formulation in the article above, it seems not to be true, contrary to what is stated in the article. I cannot prove that my suspicion is true because it is too difficult for me. I found one related article but it doesn't completely prove my suspicion. Let me explain in detail.

In the article, the axiom schema of specification is written as:

$$\textsf{SPE}\ \forall z \forall w_1 \forall w_2 \dots \forall w_n \exists y \forall x [ x \in y \Leftrightarrow ((x \in z) \land \varphi(x, w_1, w_2, \dots, w_n, z))]$$

where $\varphi$ is any formula in the language of ZFC with all free variables among $x, y, w_1, \dots, w_n$ ($y$ is not free in $\varphi$),

and the axiom schema of replacement is written as:

$$\textsf{REP}\ \forall A \forall w_1 \forall w_2 \dots \forall w_n[\forall x (x \in A \Rightarrow \exists ! y\ \varphi) \Rightarrow \exists B \forall x(x \in A \Rightarrow \exists y (y \in B \land \varphi))]$$

where $\varphi$ is any formula in the language of ZFC whose free variables are $x, y, A, w_1,\dots, w_n$ so that in particular $B$ is not free in $\varphi$.

And the axiom of the empty set is not formulated in the article, but it should be written as:

$$\textsf{EMP}\ \exists X \forall x [\lnot(x \in X)].$$

For the discussion below, I want to introduce another formulation of the axiom schema of replacement. Let the following formulation written as $\textsf{REP'}$, the apodosis of which is different from that of $\textsf{REP}$:

$$\textsf{REP'}\ \forall A \forall w_1 \forall w_2 \dots \forall w_n[\forall x (x \in A \Rightarrow \exists ! y\ \varphi) \Rightarrow \exists B \forall y(\exists x (x \in A \land \varphi) \Leftrightarrow y \in B)],$$

where $\varphi$ is any formula in the language of ZFC whose free variables are $x, y, A, w_1,\dots, w_n$ so that in particular $B$ is not free in $\varphi$.

Also let the axioms other than $\textsf{SPE}$ and $\textsf{REP}$ in the article (Axiom of extensionality, Axiom of pairing, Axiom of union, Axiom of infinity, Axiom of power set, Axiom of well-ordering ($\textsf{AC}$)) written as $\textsf{ZFC'}$.

Now we can move to the point of my question. I am sure that all the axioms which $\textsf{SPE}$ generates are theorems of $\textsf{ZFC'} + \textsf{REP'}$. One can prove it in the almost same way as in the Wikipedia article Axiom schema of replacement. However, I suspect that $\textsf{SPE}$ is indepent from $\textsf{ZFC'} + \textsf{REP}$ (more accurately, "some of the axioms which $\textsf{SPE}$ generates are"), in contrast to what is stated in the article:

In some other axiomatizations of ZF, this axiom is redundant in that it follows from the axiom schema of replacement and the axiom of the empty set.

(With the limitation of "In some other axiomatizations of ZF", I should not say that it is clearly incorrect even if my suspicion is true, but I think that it should be replaced by more accurate explanation.) The reason is that essentially, the proof of $\textsf{REP} \vdash \textsf{REP'}$ seems to depend on $\textsf{SPE}$.

It exceed my capability to prove that a proposition or propositions are independent from an axiom system. Then I would like someone to prove or disprove this. I would like to know it is related to whether $\textsf{AC}$ is assumed (I think it is unrelated).

Also I found an article which seems to present an result which almost proves my suspicion. In IN PRAISE OF REPLACEMENT, it is stated that

Levy showed that Extensionality, Empty Set, Pairing, Union, Power Set, a parameter-free version of Separation, and $\text{R}^\leftarrow$ together do not imply Replacement.

where $\text{R}^\leftarrow$ refers what is almost same as $\textsf{REP}$. However, I cannot prove my original question even with this fact (in other words, I cannot prove that the axiom of infinity and axiom of choice are unrelated), so I would like help.

If my suspicion is true, I believe that the explanation of the redundancy should be replaced by something like "$\textsf{SPE}$ is redundant if $\textsf{REP}$ was $\textsf{REP'}$ and $\textsf{EMP}$ was also assumed".

Thank you.

Answer 1

Using $\sf{ZFC}$ as a metatheory, we can construct a model of $\sf{ZF}$ minus Specification, where Replacement is formulated as in $\sf{REP}$ which does not immediately imply Specification. Moreover, the model we construct will be such that every infinite set contains $\emptyset$ as a member, and this clearly violates Specification. Consequently, it is proven that Separation is independent of the other axioms of $\sf{ZF}$, provided we are using the weaker $\sf{REP}$ schema to axiomatize Replacement. This model is constructed as follows

• For each set $S$, let $\operatorname{Cl}(S)$ denote the closure of $S$ under the adjunction operation, which is the operation $(x,y) \mapsto x\cup\{y\}$.
• Via transfinite recursion, define $M_0=\emptyset$, and generally $M_{\alpha+1} = \operatorname{Cl}(M_\alpha\cup\{M_\alpha\})$, using $M_\alpha = \bigcup_{\beta<\alpha} M_\beta$ whenever $\alpha$ is a limit.
• Define our model $M = M_{\omega_1}$ where $\omega_1$ is the first uncountable ordinal.

There are a few things to notice about this hierarchy. Firstly, we generally have $\beta<\alpha \implies (M_\beta\in M_\alpha \land M_\beta\subseteq M_\alpha)$. Using that, we easily show that each $M_\alpha$ set is closed under Adjunction, where the successor case is immediate by definition of $\operatorname{Cl}$. A simple induction then proves that each $M_\alpha$ is a transitive set. This follows after noting that $\operatorname{Cl}(T)$ is transitive for any transitive $T$, and that $M_\alpha\cup\{M_\alpha\}$ is transitive whenever $M_\alpha$ is transitive.

The final observation is that each $S\in M_\alpha$ takes the form $S=M_\beta \cup Z$ for some $\beta<\alpha$ and some finite $Z\subseteq M_\alpha$. By consequence, it also follows that we always have $|M_\alpha| = \max\{\aleph_0, |\alpha|\}$ for any $\alpha>0$. Indeed, the latter claim follows since we can repeatedly decompose $S$ using the former claim, and this results in representing $S$ by a finite wellfounded tree where each branch eventually ends in a leaf labeled by some $M_\beta$ for $\beta<\alpha$. Since the set of unlabeled finite trees is countable, then the set of finite trees labeled by the members of some set $X$ will have cardinality $|\mathbb{N}\times X^\mathbb{N}| = |\mathbb{N}\times X| = \max\{\aleph_0, |X|\}$, which works so long as $|X|\neq 0$. In our case, $X=\{M_\beta : \beta<\alpha\}$ which clearly obeys $|X|=\alpha$, giving the desired cardinality.

---

Now, we claim that our model $M_{\omega_1}$ satisfies all the required properties. As previously, we see that each $M_\alpha$ is a transitive set, and thus models both Extensionality and Regularity. For $\alpha>0$ we also get the axiom of Empty Set, since then $M_0=\emptyset \in M_\alpha$. We also get $M_\alpha$ closed under pairing, since generally $\{x,y\} = (\emptyset\cup\{x\})\cup\{y\} \in M_\alpha$ whenever $x,y\in M_\alpha$.

Next, we get Infinity so long as $\alpha>1$. The Infinity axiom demands some $W\in M_\alpha$ such that $\emptyset\in W \land \forall(x\in W), x\cup\{x\}\in W$, and the set $M_1=W$ satisfies here, where $M_1\in M_\alpha$ so long as $\alpha>1$.

Whenever $\alpha$ is a limit, then it also models the Union axiom. This works since each $S\in M_\alpha$ admits $\beta<\alpha$ obeying $S\in M_\beta$, and then we see $M_\beta\in M_\alpha$ and also $\forall(x\in S), x\subseteq M_\beta$ as required by the Union axiom.

Likewise, $M_\alpha$ models the Powerset axiom whenever $\alpha$ is a limit. In particular for each $\beta<\alpha$, the model $M_\alpha$ thinks that the powerset of $M_\beta$ is simply $M_{\beta+1}$. This works since each $S\in M_\alpha$ having $S\subseteq M_\beta$ can be decomposed as $S=M_\gamma\cup Z$, for some $\gamma<\alpha$ and some finite set $Z\subseteq M_{\alpha}$. Since we require $S\subseteq M_\beta$ then necessarily $\gamma\leq \beta<\beta+1$ so that $M_\gamma\in M_{\beta+1}$, and likewise $Z\subseteq M_\beta\subseteq M_{\beta+1}$, and this proves $S\in M_{\beta+1}$ simply because $M_{\beta+1}$ is closed under Adjunction. More generally, each $X\in M_\alpha$ admits $\beta<\alpha$ having $X\subseteq M_\beta$, and then all $S\in M_\alpha$ having $S\subseteq X$ will also obey $S\subseteq M_\beta$ and thus $S\in M_{\beta+1}$, which proves the Powerset principle.

Finally, in case $\alpha$ is an uncountable regular cardinal such as $\alpha=\omega_1$, then $M_\alpha$ will model the axiom of Replacement. Indeed, for any $X\in M_\alpha$ and any function $F:X\to M_\alpha$, we can find some $Y\in M_\alpha$ such that $\forall(x\in X), F(x)\in Y$. To do this, consider the function $G(x)=\min\{\beta : F(x)\in M_\beta\}$, then we see $G:X\to \alpha$ which obeys $F(x)\in M_{G(x)}$. Next, after finding $\beta<\alpha$ such that $X\in M_\beta$, we observe $X\subseteq M_\beta$ and thus $|X|\leq |M_\beta| = \max\{\aleph_0, |\beta|\} < |\alpha| = \alpha$. Since $\alpha$ is regular and the domain $X$ has cardinality lesser than $\alpha$, then the image of $G$ is bounded in $\alpha$. It follows that there's $\gamma<\alpha$ where $\forall(x\in X), G(x)<\gamma$. Consequently $F(x)\in M_{G(x)} \subseteq M_\gamma \in M_\alpha$, proving Replacement.

---

So, we see that our model $M_{\omega_1}$ obeys all the ordinary axioms of $\sf{ZF}$, except possibly Specification. To prove Specification fails, just notice that all the infinite sets in our model must include $M_1$ as a subset, and thus include $M_0=\emptyset$ as an element. So, even an operation as simple as $S \mapsto S\setminus\{\emptyset\}$ is not total in our model, and so Specification fails very badly.

Something worth mentioning is that, because we have a set model of this theory ($\sf{ZF}$ without Specification), it follows that $\sf{ZFC}$ proves this theory consistent. This implies that the proof power of this theory is strictly weaker than $\sf{ZFC}$, which is a more telling result than merely showing Specification is independent. In fact, it should be possible to construct a class model of $M_{\omega_1}$ from within Second-Order Arithmetic ($Z_2$), in the sense that $Z_2$ has an interpretation of $\sf{ZF}-\sf{SPE}$. This implies the proof power of $\sf{ZF}-\sf{SPE}$ is not stronger than $Z_2$, which is dramatically weaker than the full $\sf{ZF}$.