Why does Cantor's diagonalization argument fail for definable real numbers?

Question

Apologies if these are not typical definitions - I'm new to set theory, but one thing has been really confusing me for a while.

Define a real number $x$ to be definable if it can be uniquely specified in ZFC. In other words, there is some finite string of symbols in ZFC which is satisfied by $x$ and only $x$. Since there are only a countable number of finite strings in ZFC, cardinality of the definable real numbers is countable. Suppose that $(x_1, x_2, x_3 \dots)$ is the list of all definable real numbers ordered by the shortest equation that defines them.

Now, apply Cantor's diagonalization argument: let $d_i$ be $1$ if the $i^{th}$ digit of $x_i$ after the decimal point is $0$, and $1$ otherwise, and let $x = 0.d_1d_2d_3\dots$. Since for every $i$, $x$ and $x_i$ differ in at least one digit, $x$ is not a definable real number. On the other hand, I've just given an explicit, uniquely defining description of $x$. So $x$ should be definable.

What's going on here?

Answer 1

This is rather subtle. The short answer is that “$x$ is definable in ZFC” cannot be defined in ZFC (unless ZFC is inconsistent - let’s assume ZFC is consistent). In fact, you can’t even define “$\phi$ is a true statement” within ZFC. This goes back to Tarski’s undefinability of truth.

Within ZFC, you can come up with the set $Pred$ of unary predicates in the language of ZFC. From here, you’d like to be able to come up with some relation $holds \subseteq Pred \times \mathbb{R}$ such that for all predicates $P$, we have can prove in ZFC that $holds(\ulcorner P \urcorner, x)$ if and only if $P(x)$. From here, you could define $definable(x) = \exists P (holds(P, x) \land \forall y (holds(P, y) \to x = y))$.

However, defining $holds$ is not possible.