Is ZFC set theory a satisfactory foundation for mathematics?

Question

The conventional wisdom seems to be that it is, but there are problematic mismatches. Some are well-known: the use of first-order logic, and the many different implementations of the axioms, neither of which has any impact on mainstream mathematical practice. In fact almost all of the sophisticated development in set theory in the last hundred years seems to be irrelevant to mainstream practice. The concern here is that it doesn't always do the job of justifying mainstream methods. In particular, most implementations of ZFC do not justify a standard mainstream union operation.

The union operation is: suppose $S$ is a set, and $A_s$ is a collection of sets indexed by $S$. Then the union $\cup_{s\in S} A_s$ is a set. For example suppose $S$ is a set of objects in a category. Then $(a,b)\mapsto \text{morph}(a,b)$ is a collection of sets indexed by $S\times S$. That the union of these morphism sets is again a set is a basic ingredient of category theory.

The ostensible justification in ZFC requires some notation. Let $U$ denote the universe (of all possible elements) and, as usual, $\in$ the element-of operation. Sets are subcollections of $U$ of the form $\{y\mid y\in x\}$, for some $x\in U$. The union axiom in ZFC asserts that if $z$ is a set then the collection of elements of sets corresponding to elements of $z$ is a set. In symbols, $\{x\mid (\exists y)\mid (x\in y)\&(y\in z)\}$. To connect the standard operation with this, note that since each $A_s$ is assumed to be a (ZFC) set, there are elements $y_s\in U$ so that $A_s=\{x\mid x\in y_s\}$. We need to see that the collection of $y_s$ with $s\in S$ is a set. The assignment $s\mapsto y_s$ gives an obvious bijection from $S$ to this collection. $S$ is assumed to be a set, and the replacement axiom of ZFC asserts that the image of a set under a function is again a set. Now the problem. The replacement axiom only applies to ZFC functions, ie.~given by some sort of first-order formula, and we have no reason to believe the "obvious bijection" has this form. This is not just hypothetical. Every ZFC theory, with the exception of a few maximal ones, has a set $S$ and a bijection (in the mainstream sense) to a subcollection of $U$ that is not a set.

It seems to me that if we want to take the idea of "foundation" serously, then we need a new one.

Answer 1

This is a long comment, but it might also be an answer, so I'm posting it as such.

Work in the formal system ZFC. Let $\mathbb{N}$ be the meta collection of informal natural numbers, and let $\omega$ be the formal set in ZFC that is the first infinite ordinal.

From a meta point of view, we have a nice map $f\colon \mathbb{N}\to \omega$ given by the rule $n\mapsto \underline{n}$ where we recursively define $$ \underline{0}=\emptyset\text{ and } \underline{n+1}=\underline{n}\cup\{\underline{n}\}. $$ In this way, we can encode our meta numbers into our formal system (just like we can encode numbers into computer hardware, or any other formal foundational system).

Now, from the metatheoretical perspective, we can form the union of the meta numbers and get $\mathbb{N}$ as a completed collection. From the formal side, there is no such set as $f(\mathbb{N})$ because we have no way to uniformly define the images of the meta numbers. In other words, even though $\omega$ is a formal set we have no way of knowing whether or not $f$ is a bijection.

Does this mean ZFC is a lousy foundation? Not really. When viewed in a certain light, it just reveals a limitation of language. There are always limitations to any encoding of a metatheoretical idea in a formal language system; see Tarski's theorem on truth for one example of such phenomena.