"The countable union of countable sets is countable (...) This result is needed to prove our major result, the completeness theorem in Chapter 5. It depends on a principle called the axiom of choice."

In other words: the most important result in predicate calculus depends on one of the axioms of set theory.

I am surprised, since I thought that predicate calculus comes first, and set theory later. Of course, predicate calculus uses massively the concept of set, and its notation, but I always thought that this usage of set was in the metalanguage (in other words, we were using the concept set informally, as "grouping of things").

But if a (contrived) axiom of set theory is needed to prove the most important result in predicate calculus, then it means that set theory is not being used in the metalanguage, but as "axiomatic set theory".

Thinking about it, there seems to be a way out: we define first order logic with sets in the metalanguage. We do not prove (yet) the completeness theorem of predicate calculus (as a consequence, we do not need the axiom of choice, so we do not need axiomatic set theory). Then, we define axiomatic set theory using predicate calculus. So, we say the axioms of set theory are true. In particular, the axiom of choice is true. Now, we go back to predicate calculus and we use the axiom of choice to prove the completeness theorem in predicate calculus. The loop is closed.

Is it really this way???