From a wikipedia page:
One can write down a concrete polynomial p ∈ Z[x1, …, x9] such that
the statement "there are integers m1, …, m9 with p(m1, …, m9) = 0"
can neither be proven nor disproven in ZFC (assuming ZFC is
consistent). This follows from Yuri Matiyasevich's resolution of
Hilbert's tenth problem; the polynomial is constructed so that it has
an integer root if and only if ZFC is inconsistent.
So I opened the paper, and what I understood is that there exists a universal polynomial, such that
$$x\in W_v \iff \exists m_1\ldots m_9, U(x,v,m_1\ldots m_9) = 0$$
where $W_v$ is a recursively enumerable set indexed by $v$, and $x$ is a binary number or whatever output format we prescribe of our Turing machines.
Now if we select $v$ such that $W_v$ is non-recursive but r.e., then the set $X = \{ x : x\in W_v \} $ is undecidable. That doesn't mean that for every particular $x$, $x \in W_v$ is undecidable in ZFC, right?
For instance let $W_v$ is the set of all Turing machines (no input) that halt, this is a recognisable but not decidable set, and let $x$ be a Turing machine that halts on instantiation, then we can prove $x\in W_v$
Basically I'm having trouble proving the statement in the blockquotes from wikipedia, do let me know how to go about it.
Best Answer
Let me elaborate my comment a bit: the fact that a set $X$ is not decidable doesn't mean that we cannot decide membership for any element. It is the converse actually. Namely, for every $X\subset \mathbb{N}$ (let us remain in the context of classical computability) and every $x$, there is a computable function $\varphi=\varphi_{x,X}$ s.t. $\varphi(x) = \chi_X(x)$ where $\chi_X$ is the characteristic function of $X$. This is easy to see: if $x\in X$ let $\varphi$ be the map constantly $1$, otherwise let it be constantly $0$. This clearly proves the claim, albeit in a trivial and non-satisfactory way.
When it comes to provability the focus is slightly different: you want to prove that a certain statement is true or false. In the case of the diophantine polynomial, the claim is "there are $m_1,...,m_9$ s.t. $U(x,m_1,...,m_9)=0$". Now, the set of theorems in ZFC (or in any theory with a r.e. set of axioms) is a r.e. set. This means that $x$ is a theorem in ZFC iff there are $m_1,...m_9$ as above. Now take $x$ to be (index for) the Gödel formula (or any other statement independent of ZFC). Once $x$ is fixed, the polynomial $U$ is just a polynomial of $m_1,...,m_9$ ($x$ is now a parameter). If ZFC could prove (or disprove) that such $m_1,...,m_9$ exist, it could prove (or disprove) Gödel formula, and we know this is not the case.
Here's another (explicit) example of a Turing machine whose behavior eludes ZFC: https://www.scottaaronson.com/blog/?p=2725