# What is the first order formulation of Zorn's lemma in the language of set theory?

Very often in notes of courses in set theory you find the assertion that in ZF the Axiom of choice (AC) is equivalent to Zorn's Lemma (ZL) (which is equivalent to Well Ordering Principle which it equivalent to Cardinality Tricotomy etc). Some proof of the statement might follow, or at least of the easy part, namely $\text{ZL}\rightarrow\text{AC}$. And still, regardless of having mentioned that the equivalence is a theorem of ZF, little is said about the syntax behind the statement and the proof. I'm finding it difficult finding even the formulation of Zorn's lemma in the language of set theory $\mathcal{L}=\{\in\}$.

The formulation of AC would be the following. Let's assume that we are familiar with the formulas "$f$ is a functions whose domain is $A$" and "$y$ is the image of $x$ by $f$" (namely $f(x)=y$), AC can be written as $$\forall A \exists f ((f \text{ is a formula whose domain is } A)\wedge \forall x (x\in A \rightarrow \exists y (f(x)=y \wedge y\in x))).$$

My question would be what is the formulation of Zorn's Lemma in the language of set theory.

Since this question deals with my incapability of finding a pertinent standard source, the mentioning of any such source is welcomed.

Bonus question Consider a language $\mathcal{L}=\{\leq\}$ with a binary relation and the theory $T$ of partial orders in said language. Consider a formulation of ZL given by the following second order formula $\phi$: $$(\forall X (X \text{ is a chain } \rightarrow \exists c \forall x (x\in X\rightarrow x\leq c))\rightarrow \exists m\, (m \text{ is a maximal element)}.$$

If $\phi$ a theorem of $T$?

• ??? Why would you imagine there's any problem formulating Zorn's lemma in forst order ZF? It's just a statement about sets. And sets of sets and mappings and chains and partial orders, all of which are just sets. – David C. Ullrich Jan 17 '16 at 19:04
• @DavidC.Ullrich well I've read a proof of AC using ZL where the set of partial choice functions is taken as the partial ordered set in ZL, the symbol $\in$ however does not order said functions by extension, and I assume in a formulation in $\mathcal{L}=\{\leq \}$ of ZL the only relation in the language must act as the partial ordering. – Anguepa Jan 17 '16 at 19:13
• I just think reading for once said sentence or knowing where to find it would help me. – Anguepa Jan 17 '16 at 19:14
• I seriously doubt that seeing ZL literally formulated in the language of ZF would be any help. It would probably be a page or so. Nobody ever actually writes anything non-trivial in that language, they just convince themselves that they could if they had to. – David C. Ullrich Jan 17 '16 at 19:20
• While in the application of proving AC using ZL you mention, there are sets (partial choice functions) which are partially ordered by set-inclusion ($\subseteq$, not $\in$), a general formulation of ZL (cf. the Wikipedia article) will make no assumption other than that there exists a partially-ordered set $(P,\le)$ satisfying existence of an upper bound (in $P$) for any totally-ordered subset (chain) of $P$. – hardmath Jan 17 '16 at 19:20

This is probably going to be very unilluminating, but here goes:

"If, in a partial order $P$, every chain $C$ has an upper bound, then $P$ has a maximal element."

Let's start with the obvious bit: how do we talk about partial orders in set theory? Note that we could also ask, "How do we talk about groups in set theory?" or rings, or fields, or . . . and the answers will be basically the same.

Definition 1. A partial order is an ordered pair $(P, L)$, where

• $P$ is a set,

• $L$ is a binary relation on $P$, and

• $L$ satisfies the axioms of a partial order: transitivity, reflexivity (I'm viewing $L$ as $\le$, not $<$, here), antisymmetry.

This might seem non-set-theory-ish, but remember: we have ordered pairs and powersets! This means that all the above can be formalized in set theory with little difficulty:

Definition 2 (all ZF). A partial order is a set $x$ such that

• $x=\{a, \{a, b\}\}$ for some sets $a, b$ (this is the Kuratowski ordered pair); and these $a, b$ satisfy

• $b\subseteq a^2$ (note that "$a^2$", the set of Kuratowski ordered pairs of elements of $a$, can be constructed via repeated powerset and separation),

• $\forall x, y, z\in a, [(x, y), (y, z)\in b\implies (x, z)\in b]$ (this is transitivity - for simplicity I've written "$(\cdot, \cdot)$" instead of the full Kuratowski ordered pair),

• $\forall x\in a, [(x, x)\in b]$ (reflexivity), and

• $\forall x, y\in a[(x, y)\in b\wedge (y, x)\in b\implies x=y]$ (antisymmetry).

So this lets us talk about partial orders.

Similarly, if $(a, b)$ is a partial order, then a chain is a set $x\subseteq a$ such that $\forall y, z\in x[(y, z)\in b\vee (z, y)\in b]$. And maximal elements and upper bounds of chains are similarly straightforwardly definable.

All of this, when spelled out formally, yields a perfectly normal first order sentence. Birds-eye view, it has the form $$\forall x[P(x)\wedge\forall zQ(x,z)\implies \exists w M(x,w)]$$ where $P$, $Q$, and $M$ are abbreviations for the formulas defining "is a partial order," "is either not a chain in -, or which is a chain in - and has an upper bound," and "is a maximal element in -" respectively. Written out entirely, it's quite long; if you really want to you can easily write it out for yourself, but I'd think for a while first about exactly what it is you're hoping to see.

As to your bonus question: sorry to disappoint, but second-order logic is terrible.

There is no nice proof system for second-order logic (at least, not with the standard semantics - with Henkin semantics there is, but then with Henkin semantics it's just first-order logic in disguise). This can be made precise and proved in a variety of ways. Just to get started, note that set-theoretic questions can get folded in. For instance, the $\varphi$ you mention is a second-order consequence of the definition of partial order iff the axiom of choice is true! Another good example is that we can write an explicit second-order sentence which is a tautology iff the continuum hypothesis holds.

So in order for us to answer your question, you need to tell us what set-theoretic assumptions you're making - in particular, whether you assume AC; and I believe at that point the answer won't really be interesting. :)

I believe I've written more about the general terribleness of second-order logic elsewhere, for instance, in my answer to Complete and correct deductive axiom for SOL

• There's no need to refer to powerset and separation; "$b\subseteq a^2$" can be written $\forall x\in b\exists y,z\in a[x=(y,z)]$, regardless of whether you know that the set $a^2$ actually exists. – Eric Wofsey Jan 18 '16 at 3:04
• @EricWofsey Quite right. I didn't mean to imply that those axioms were necessary to write "$b\subseteq a^2$," I just thought that it would be a good thing to mention as context. – Noah Schweber Jan 18 '16 at 3:06
• Interesting side note: my definition of the Kuratowski ordered pair is slightly incorrect - historically, the right definition is $(a, b)=\{\{a\},\{a, b\}\}$, and what I wrote is apparently called the short Kuratowski pairing. There's no real difference - unless you care about the axiom of foundation, which is required to show that the short Kuratowski pairing is actually injective (the long one, though, is fine). – Noah Schweber Jan 18 '16 at 3:09
• If the definition of ordered pairs is not the Kuratowski definition you shouldn't call it that. – Asaf Karagila Jan 18 '16 at 7:02
• thank you your answer did help me, since my doubt had to do with the failure at understanding the way structures are represented in models of ZF (upfront I thought a partial order would be a set where the relation $\in$ acted as the partial order relation). I can now see I overlooked the capabilities of set theory. – Anguepa Jan 18 '16 at 12:07