# Understanding ZFC

I initially thought that ZFC was something like a collection of axioms or formation rules, defined in terms of primitive notions, which when successively combined with each other, produced all of the sets that are taken as the ingredients of mathematics. I thought that all mathematical concepts were just names we had given to particular sets generated cumulatively by these axioms, for example, functions were defined as sets of pairs of elements, and the natural numbers the set of all sets generated by recursively taking the power set, starting on the empty set. I had been exploring ways to "interpret" particular classes of sets as things like quantifiers, or the logical connective $$\rightarrow$$ ('if-then'). Thus, I thought ZFC was like a formal language, which generated a "theory" (the collection of all expressions it generates).

I am now revising my understanding of this in many ways and trying to update my view. First of all, ZFC is a collection of axioms, written in first-order logic. First order logic is defined in terms of primitive notions: constants, variables, functions, predicates, and equality. I would like to consider that it could be possible to enumerate all possible strings of first order logic, but I don't know what further conceptual issues there may be in trying to do so.

This means that the theory generated by ZFC is a subset of the theory generated by first order logic. My guess is that if you find some way to interpret the expressions of first-order logic (a model), you realize that the collection of all possible expressions doesn't have good properties. For example, consider the desire for a theory that does not contain both $$\phi$$ and $$\neg \phi$$, "consistency". How can you modify FOL to try to achieve that? You could try to change the formation rules of FOL.

The condition $$\forall x (\phi(x) \vee \neg \phi(x))$$ is itself a sentence of first-order logic. I am not sure how we can formally "interpret" this as being about expressions in FOL, that is, that variable x can be substituted with expressions from FOL. I am not sure if we should seek a consistent theory by changing the formation rules or imposing conditions on the theory. If we change the formation rules, we may no longer be able to express the concept of "consistency" itself. If we declare that we want to consider expressions meeting a certain condition, how do we stop our formation rules from generating those expressions that we want excluded from our theory?

The von Neumann hierarchy of sets is supposed to generate all pure, well-founded sets, and it only requires the concept of power set and of union. So, I guess ZFC is not an attempt to generate all sets, but to express properties of a collection of sets we would like to have. As I understand it, ZFC does not determine a unique collection of sets or model, but there are actually infinitely many distinct models (How many countable models of ZFC are there?).

If one is to do mathematics rigorously, they would like every concept they mention, such as a function or relation, to have a precise definition. How can we do that with ZFC if ZFC does not determine a unique universe of sets? Is the general idea that one does not enumerate all possible sets, but can prove the existence of a particular set they would like to use, in any model of ZFC?

ZFC does generate a “theory”. Formally speaking, a theory is simply a set of sentences in the given formal language. Any set of axioms generates a theory, namely the collection of sentences provable from this collection of axioms. In terms of ZFC, this theory describes the properties of sets, and that include what sets can be constructed or otherwise proven to exist under the axioms of ZFC. It is, of course, possible to enumerate all sentences provable from ZFC. Just run a computer program that enumerates all possible formal proofs from ZFC axioms, say. This is true of any “reasonable” collection of axioms, not just ZFC.

As for “the theory generated by ZFC is a subset of the theory generated by first order logic”, this is false, at least when “theory” is interpreted in the formal way I mentioned above. There is a conceptual issue here: first order logic and ZFC are simply not two things at the same level. First order logic is a system of logic, which includes a collection of logical axioms and deduction rules, while ZFC is a collection of axioms written in terms of first order language. Any axiomatic system in first order logic is considered to automatically incorporate all the logical axioms of the first order logic, so ZFC contains more axioms, so to speak, and therefore can prove more things. The theory generated by logical axioms of first order logic is simply things that should be true regardless of what mathematical structures you are studying, insofar as the said structures can be characterized in terms of first order logic, while ZFC is supposed to generate a theory describing the universe of sets. Of course, if a statement is true for all mathematical structures, then it must be in particular true for the universe of sets.

Variables in first order logic cannot be substituted with first order expressions (or collection of objects, for that matter). If you want to do that, you need second order logic.

Finally, yes, ZFC does not determine a unique universe of sets. In fact, that is simply impossible - Löwenheim-Skolem theorem implies that ZFC, or any possible (and consistent) set theory axiomatic system admits models of arbitrary infinite cardinalities, as long as you want to study a universe of sets that is infinite. Furthermore, Gödel’s incompleteness theorem means that it’s not even possible for any “reasonable” axiomatic system to be complete, that is, there are always statements that cannot be proved or disproved using the axioms. This isn’t really an obstruction to doing mathematics rigorously. Basically, when we say we can prove the existence of certain sets, we mean that these sets exist in all models of ZFC. More generally, when we prove a theorem with a given construction of the relevant objects from sets, we mean that this construction can be carried out in all models of ZFC and the corresponding theorem is true for such constructions in all models of ZFC. This is possible because every statement provable from ZFC is true in all models of ZFC. There are also parts of mathematics that study the consequences of other axiomatic systems, or statements independent from ZFC. These can be formalized in a similar manner.