Earlier quoted context omitted.
The undecidability property proven here doesn't imply that there exists at least one Diophantine equation for which we'll never know if it's solvable or not, does it?
In [0], Carl and Moroz give an explicit polynomial in 3639528+1 variables such that: a well-formed formula is a theorem in the first order predicate calculus if and only if the polynomial parametrized by the Diophantine coding of the formula (a single natural number) has a solution in N^{3639528}. From this, they get an explicit Diophantine equation such that: the Godel-Bernays set theory is consistent if and only if…
- there's no general algorithm that can solve an arbitrary problem from the set (the whole thing is undecidable)
- each problem in isolation _can_ be solved. there's no single problem that's impossible to solve