Can we restrict schemata in ZFC as to only construct sets with clear cut membership?

Question

Lets examine the axiom schema of Separation in ZFC set theory. The formula is

$\forall A \exists x \forall y (y \in x \leftrightarrow y \in A \land \phi(y))$

Now per Godel incompletness theorem, there is a sentence $\theta$ such that ZFC neither prove nor disprove.

Now lets take the set

$\Omega= \{y \in A | y=y \land \theta \}$

Now ZFC proves $\Omega$ to exist via Separation. Also it proves it to be unique (for each $A$)! But what are exactly the members of $\Omega$???

The clear answer is that it doesn't have a clear membership!!! Its membership is model sensitive, i.e., it depends on adding further axioms, so for example if we add $\theta$ to the axioms of ZFC, then we'll have $\Omega=A$ in the resulting system, while if we add $\neg \theta$ to the axioms of ZFC, then we'll have $\Omega=\emptyset$ in the resulting system.

Of course ZFC itself cannot prove either case, nor can it prove $\Omega$ to be neither $A$ nor $\emptyset$ since this would contradict some consistent extensions of it. This means that the membership of $\Omega$ is undecided from the axioms of ZFC alone!

The problem is that $\Omega$ is not even a case of postponed membership, i.e. there is only one kind of membership of $\Omega$ after adding sufficient axioms to clear its identity. No! here even if we add axioms still the identity of $\Omega$ depends on those axioms, so it can differ with different extensions. So we can say that across extensions of ZFC, $\Omega$ doesn't have a fixed identity.

If the above is correct, then what's the rationale from having an axiom schema like Separation if it leads to defining and proving the existence of sets of undecided membership in it? Sets that are vague from its own perspective?

Can't we have a restriction on schemata of ZFC such that only sets with clear cut membership (or at least postponed) can be constructed? i.e. sets whose membership won't change with different extensions of ZFC?

Answer 1

ZFC is really a red herring here: the same phenomenon happens already in, say, PA. For example, PA proves

There is a number $n$ such that $n=0$ if the Goldbach conjecture is true and $n=1$ if the Goldbach conjecture is false.

More generally, we have:

$(*)\quad$ If $T$ is any incomplete theory with two formulas $\varphi,\psi$ which $T$ proves each define distinct elements then $T$ has an "ambiguous object."

Turning back to the original question, note that Separation need not be used here in the context of ZFC; for example, without using Separation ZFC proves that $$X:=\{\emptyset: CH\}$$ is a set while not determining whether $X=\{\emptyset\}$ or $X=\emptyset$. The way ZFC proves this is by cases: first showing that $\emptyset$ exists, then showing that $\{\emptyset\}$ exists, and then concluding that there is a unique $X$ with the above property.

And $(*)$ applies to basically every reasonable theory - the only way to avoid it is to either go ultraweak, to the level of theories not capable of defining two provably distinct objects, or to go to complete theories which entails either dropping computable axiomatizability or again losing almost all logical strength. So ultimately the answer to your question is: no, not without giving up absolutely fundamental properties of ZFC (namely its strength and its computable axiomatizability).

Answer 2

Each choice of $\phi$ gives its own axiom. Your proposal is to use a smaller schema in which the only $\phi$ used are those for which, for any set $A$, the same elements of $A$ satisfy $\phi$ in all models. An equivalent formulation, provided our new theory can prove each $x$ is the unique element of some singleton of $x$, is that we restrict to those $\phi$ for which models never disagree on what satisfies $\phi$.

Now, a given alternative to ZFC, whereby some $\phi$ are banned, may or may not have this enviable property. But it's a property of the theory, and we want to use that property to define which $\phi$ contribute axioms to the theory. The smaller the schema becomes, the less the new theory can prove, and you might discover a $\phi$ you used to think was OK no longer is. It's unclear what will survive this loop, and even less clear there's a unique $\phi$-choosing algorithm that achieves what we want. So unless you can prove a metatheorem that says which $\phi$ to choose to get this done, I can't see it getting off the ground. Ironically, the intent here to make separation's products "well-defined" has an ill-defined strategy.

Try not to be too disappointed, though. The responsibility of axioms as implicit definitions is to claim some meaning can be given to the symbols in those axioms under which they're true, i.e. that the axioms have a model. Their responsibility isn't to know which model is of interest. Indeed, if such axioms as these are incomplete (which they'll have to be if consistent), they can't narrow things down to one model. ZFC's axioms "define" what sets are, but only implicitly, and certainly not uniquely. And if multiple meanings of "set" are consistent with these axioms, one shouldn't mind if a specific set the theory defines is similarly subject to model-dependent details.