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

Question

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.

Answer 1

There is certainly a strong sense in which the answer to your question is yes: namely, model-existence - and hence semantic entailment in general - doesn't depend on choice (unless our language is quite weird, namely non-well-orderable).

The completeness theorem in its full glory is indeed not provable in ZF alone, but this is only because complicated languages are permitted. As long as the language of the theory in question is well-orderable (and it's hard to come up with a natural example which consistently isn't), the Henkin construction goes through without choice. Since choice doesn't affect syntactic consistency (the latter being all about finite sequences), this means that as long as the language in question is well-orderable we'll never need choice to tell whether a given semantic entailment holds.

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).