Can sets be constructed in ZFC using possibly undecidable conditions?

Question

Let $P$ denote the set of all prime numbers, $E$ the set of even numbers greater than 2, and $$X:=\{e\in E \,\,|\,\, \exists x,y\in P: x+y=e \}.$$

Note that if Goldbach’s conjecture (that all even numbers are expressible as the sum of two primes) is true, then $X$ is the set of all evens greater than 2, and that otherwise, it is “missing” some evens.

Are sets like this “allowed” in ZFC, i.e., constructable using ZFC axioms? If yes, then what happens if Goldbach’s conjecture is undecidable? Wouldn’t that cause problems/paradoxes for set theory?

Answer 1

Yes, this set can be defined. The axiom schema of separation says that if $S$ is a set and $\varphi$ is any property that can be expressed in the first-order language of set theory, then $\{x\in S:\varphi(x)\}$ is a set. In particular, your set $X$ is trivial to define in this way starting from $S=E$ (or $S=\mathbb{N}$).

Note that being able to "construct" this set in ZFC in this context merely means that we can prove it exists: that is, we can prove there exists a set $X$ such that for all $x$, $x\in X$ if and only if $x$ is an even natural number that is a sum of two primes. It doesn't mean that we can explicitly figure out what all its elements are or anything else like that. So, there is nothing deep or paradoxical about being able to construct this set in ZFC. If Goldbach's conjecture were independent of ZFC, this would just mean that ZFC cannot prove $X=E$ and also cannot prove $X\neq E$, which in no way conflicts with being able to prove $X$ exists.

Answer 2

It is not a contradiction for something to be undecidable. Contradictions happen when you prove too much, whereas undecidability is about what you can't prove.

We can cut to the chase and define $X=\emptyset$ if the continuum hypothesis holds, otherwise $X=\{\emptyset\}.$ This is a perfectly valid definition in ZFC. We know for a fact that (if ZFC is consistent), it cannot decide whether $X$ is empty or not.

That's fine. ZFC can't decide a lot of things. Your example with the Goldbach conjecture is no different, except that it's not very likely that the Goldbach conjecture is actually undecidable in ZFC. If it were, ZFC would not decide whether your $X$ contains every even number or not. Again, this is fine. ZFC cant decide a lot of things. And again, it makes no difference that we've wrapped our undecidable proposition in a set definition.

In constructive math, things are different, and definitions like this are viewed as problematic. It's not so much that such a definition is paradoxical, but rather that such an object isn't considered to exist, since we can't actually produce it concretely, so it isn't considered a valid definition. See here.

Note it's possible to produce similarly problematic "definitions" classically. For instance, "the least ordinal with property P" sounds superficially like a good definition since the "the least" part guarantees uniqueness, but if it's not provable (or not known to be provable) in ZFC that there is any ordinal with property $P,$ then we can't show this object exists, so this isn't a valid definition in ZFC.