There is a natural analogy between the theories PA and ZFC. See the linked question by Gro-Tsen here.

Peano arithmetic (PA) is a first order approximation to the natural numbers. As is well known, there are true facts about the natural numbers that we cannot prove in PA, but we can prove them in stronger systems that seem to be entailed by philosophical assumptions about the natural numbers.

Informally, my question is: Does this aspect of the analogy extend to ZFC?

In a **trivial** way, the answer to my question is yes. Since we (supposedly) believe the axioms of ZFC, we accept the statement Con(ZFC) that asserts ZFC is consistent, and also Con(ZFC+Con(ZFC)), and so forth. My question then is whether or not there are **non-trivial** examples of higher order considerations giving us theorems about sets that are not provable in ZFC, just as the Paris-Harrington theorem is true but not provable in PA.

To attempt motivating an example, consider the following: The "axiom of union" in ZFC is a first order approximation of the philosophical assertion that putting collections together results in a new collection. (The classic paradoxes show that we have to be careful what we mean by a collection, but let's ignore that issue for now.) In particular, if we have some collection $S$ of subsets of the natural numbers, then we have no problem asserting the existence of $\bigcup S$ as a subset of $\mathbb{N}$.

If we have a first order, recursively enumerable theory $T$, extending ZFC, we can define a truth predicate $P_n$ for the formulas cut off at level $\Sigma_n$. Philosophically, we thus expect the existence of a full truth predicate---not one definable in any first order way in $T$ (that would be impossible by Tarski's theorem), but one that "exists" nonetheless. Can we leverage this fact, or other facts like it, to make philosophical advances in understanding "true" set theory?

1more comment