First order logic and set theory: who comes first?

[jordi]

Goldrei's Propositional and Predicate Calculus states, in page 13:

"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?

 

[jedishrfu]

I don't think mathematicians would be happy with this state of affairs. It is possible that if you're reading different authors that one started from a predicate calculus foundation whereas another started from set theory which means you need to know that before you mix and match your understanding from the books.

The axiom of choice may actually be independent of either set theory or predicate calculus making this an okay thing to do.

https://en.wikipedia.org/wiki/Axiom_of_choice
Perhaps @fresh_42 can shed some light on this topic.

 

[fresh_42]

One needs sets to set up the first order logic, as it consists of symbols and rules. The symbols are logical symbols, variables, and symbols for constants $\mathcal{C}$, functions $\mathcal{F}$ and $relations$\mathcal{R}##. Those are taken from a set of them, possibly empty. In any case, if described this way, and I'm not saying it is the only way, then we need sets prior to the language.

The axiom of choice isn't part of standard set theory. It is an independent tool, which in case we needed it to prove theorems phrased in first order logic it should be added. So the order is: ZF > ZFC > 1st order logic > theorems. Of course you can object that we need first order logic to describe ZFC, so to some extend it is the question about hen and egg. As we only needed a basket for our symbols, we could as well follow the order: 1st order logic > ZF > ZFC > theorems, and define the basket otherwise. And again: hen and egg.

I would not sign

the most important result in predicate calculus depends on one of the axioms of set theory

since many results rely on AC. IMO those considerations only reflect the insufficiency of any language. Set theory as well as first order logic are only the best we could have done so far in our goal to setup a framework without contradictions.