What fragment of ZFC do we need to prove Zorn's lemma?

Question

It is extremely well-known that Zorn's lemma is a theorem of ZFC. My interest is in a certain finitely-axiomatisable fragment of ZFC, sometimes called RZC (restricted Zermelo with choice) or ZBQC. The axioms of RZC are the following:

• Extensionality
• Empty set
• Pair set
• Union
• Power set
• Infinity
• Foundation
• Choice (in the sense that every surjection has a right inverse)
• Separation for $\Delta_0$-formulae

Adrian Mathias also defines an extension of RZC, called MAC (Mac Lane set theory), by adding the transitive containment axiom:

• Every set is contained in a transitive set.

(Apparently RZC and MAC are equiconsistent.)

Question. Is Zorn's lemma a theorem of RZC? If not, is it a theorem of MAC?

It is reasonably clear that well-founded induction is valid in RZC, but without the axiom of replacement it is not at all obvious to me whether Hartogs numbers exist. ($V_{\omega + \omega}$ is a model of RZC, but the only von Neumann ordinals in $V_{\omega + \omega}$ are precisely those below $\omega + \omega$, even though it has uncountable well-ordered sets.) Once we know that there are sufficiently large well-ordered sets, it seems to me that the usual proof of Zorn's lemma will go through in RZC.

Motivation. One can build a model of RZC out of any model of ETCS (elementary theory of the category of sets) and ETCS can be interpreted in any model of RZC. What I really want to know is whether ETCS proves that, say, every vector space has a basis, and it seems like a good first step would be to establish the claim for RZC.

Answer 1

This reformulation of the construction Hartogs number seems to work:

Lemma (Hartogs). If $X$ is a set, then there is a well-ordered set $Y$ for which there is no injection $Y \to X$.

Proof. Let $\overline{X}$ be any set containing $X$ as a proper subset. Let $\mathcal{F}$ be the set of all well-orderings of subsets of $\overline{X}$; this can be constructed using power sets, cartesian products, and $\Delta_0$-separation, and let $\mathcal{F}_0$ be the subset of $\mathcal{F}$ consisting of well-orderings of $X$. Let $Y$ be the set of isomorphism classes in $\mathcal{F}$; this can be constructed using power sets, function sets, and $\Delta_0$-separation. $Y$ has an obvious linear order (using induction over well-ordered sets), and in fact it is well-ordered.

• If $\mathbb{N}$ (in the sense of a set for which mathematical induction is valid) exists, we proceed by supposing $Y$ is not well-ordered: then by mathematical induction we could produce an $\mathbb{N}$-indexed strictly descending sequence $$y_0 > y_1 > y_2 > \cdots$$ in $Y$, but the sequence $y_1 > y_2 > \cdots$ can then be embedded in a representative of the class $y_0$, implying $y_0$ is not an isomorphism class of well-orderings – which is a contradiction. [Does this need choice? Embeddings of one well-ordered set as an initial segment of another are unique if they exist, so I'm inclined to believe this is choice-free...]

• If $\mathbb{N}$ does not exist, then [...?]

Once we have shown $Y$ is well-ordered, it is easy to prove that every member of $\mathcal{F}_0$ embeds as a proper initial segment of $Y$. A standard argument then shows there is no injection $Y \to X$: indeed, if there were, then $Y$ would embed as a proper initial segment of itself – an absurdity. 　◼

The standard proof of Zorn's lemma now goes through without problems:

Lemma (Zorn). If $X$ is a partially-ordered set such that every well-ordered chain in $X$ has an upper bound in $X$, then $X$ has a maximal element.

Proof. Let $\mathcal{G}$ be the set of well-ordered chains in $X$; this can be constructed using power sets and $\Delta_0$-separation. Using the axiom of choice, we may choose once and for all an upper bound for each well-ordered chain in $X$, so that we obtain a function $u : \mathcal{G} \to X$ such that $z < u(Z)$ for all $Z$ in $\mathcal{G}$ and all $z$ in $Z$. [I think the axiom of choice is only needed to construct $u$ and nowhere else.]

Let $Y$ be a well-ordered set so large that there is no injection $Y \to X$, and suppose for a contradiction that $X$ has no maximal elements. We define an injective monotone function $f : Y \to X$ by recursion:

• If $f (y)$ has been defined for all $y < z$ in $Y$, then define $f (z) = u(\{ f(y) : y < z \})$ (where $\{ f(y) : y < z \}$ is constructed using $\Delta_0$-separation instead of replacement).

This produces the desired contradiction. 　◼