# Do we only need Choice for higher order-statements (Zorn’s lemma as example)?

In this earlier post, I asked why the axiom of choice, which is an axiom in set theory, is used in areas that are not set theory, such as group theory. The answer was that, whenever choice is used, it is used to prove something about the set of models of group theory, and hence is a statement about sets rather than about groups.

Now I’m trying to understand this for Zorn’s lemma specifically. Zorn’s lemma says:

Zorn’s Lemma — Suppose a partially ordered set $$P$$ has the property that every chain in $$P$$ has an upper bound in $$P$$. Then the set $$P$$ contains at least one maximal element.

The axiom of choice is used in the proof of Zorn’s lemma. This at first sight confused me, since Zorn’s lemma seems like a theorem about partial orders, not about sets in general. But then I realized that it is a second-order statement, rather than first order, since it is about subsets of $$P$$. I don’t fully understand the proof of Zorn’s lemma, since I’m somewhat confused still by the axiom of choice, so let me ask a question to clarify:

Question 1. Is it true that the proof of Zorn’s lemma uses the axiom of choice on totally ordered subsets of $$P$$, rather than on $$P$$ itself?

This gives me the more general conjecture:

Question 2. Is it true that whenever we have a first-order statement about a structure (such as posets), we never need the axiom of choice to prove it, but if the statement is higher-order, we may need it?

Note that (in the context of partial orders) I’m talking about first-order statements within the theory of partial orders, not e.g. first-order statements about the set of models of the theory of partial orders, or e.g. about the category of posets.

• What does the question even mean? Higher order statements? Extend your language to be multisorted and everything becomes first-order. Jun 2, 2019 at 7:55
• The existence of a maximal element is a first-order statement. Yes, the condition on upper bounds is not first-order in the language of orders, but it is not what we want to prove anyway. Jun 2, 2019 at 7:57

For example, if ZFC proves that every group satisfies some first-order sentence $$\varphi$$, then so does ZF - the point being that the language $$\langle e,*,{}^{-1}\rangle$$ of groups is well-orderable (indeed, finite).
• @user56834 Re: your first question, remember that a first-order language is just a set of symbols of appropriate type. If choice fails, there are some sets which are non-well-orderable; well, this leads to sets of symbols which are non-well-orderable. For example, consider the language consisting of an $n$-ary function symbol for each $n$-ary function on $\mathbb{R}$ (this language shows up in nonstandard analysis, for example). This set of symbols is incredibly huge; it has size $2^{2^{\aleph_0}}$. So if the powerset of the reals isn't well-orderable, neither is this language. (cont'd) Jun 3, 2019 at 13:10
• @user56834 Re: your first question, remember that a first-order language is just a set of symbols of appropriate type. If choice fails, there are some sets which are non-well-orderable; well, this leads to sets of symbols which are non-well-orderable. For example, consider the language consisting of an $n$-ary function symbol for each $n$-ary function on $\mathbb{R}$ (this language shows up in nonstandard analysis, for example). This set of symbols is incredibly huge; it has size $2^{2^{\aleph_0}}$. So if the powerset of the reals isn't well-orderable, neither is this language. (cont'd) Jun 3, 2019 at 13:10
• Of course such languages actually occur only very rarely in practice; basically every first-order language you actually use is even finite! But they do crop up from time to time. Re: your second question, model existence is "dual" to entailment: "$T$ entails $\varphi$" is equivalent to "There is no model of $T\cup\{\neg\varphi\}$." Showing that choice plays no role in model existence arguments of a certain kind also shows that it plays no role in semantic entailment arguments of that same kind. Jun 3, 2019 at 13:12