5 ms·

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, do

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?

hackandthink 4y ago
My understanding: There's no algorithm to decide. But for any equation we can be lucky to find a solution or a proof that there's no solution. But this doesn't prove that there is an equation for which we'll never know if it's solvable or not.
- moefh 4y ago
  From my understanding, while that's is technically true, given a consistent axiomatic system (like ZFC[1], the foundation of mathematics we use) there exists a diophantine equation that can't be proven to have no solutions in that system (even though it has no solutions). This mathoverflow answer[2] gives the equation and a link to the paper that shows how to calculate the constants (the numbers are huge!). What that means in practice is that although what you wrote is true, for some diophantine equations we'd have to come up with new axioms to be able to write a proof of the inexistence of its solutions. But then, how can we be sure that the the new axioms are consistent? [1] I'm assuming ZFC is consistent; if it's not then it can prove anything, including the existence of solutions for any equations at all [2] https://mathoverflow.net/a/81986 https://mathoverflow.net/a/81986
  - hackandthink 4y ago
    Thanks. I'm somewhat lost, but it seems to work Gödel like. The statement is true (equation has no solution) but we can't prove it.
- layer8 4y ago
  See https://news.ycombinator.com/item?id=34384838 https://news.ycombinator.com/item?id=34384838, I think it disproves your last sentence — at least when assuming that all solutions and all proofs of non-existence of a solution are expressible in a shared formal language.
ykonstant 4y ago
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 that Diophantine equation has no solutions (and thus the same is true for ZFC, since NBG is a conservative extension of ZFC). [0] https://link.springer.com/article/10.1007/s10958-014-1830-2 https://link.springer.com/article/10.1007/s10958-014-1830-2
- najdan33 4y ago
  Does there exist a set of yes/no problems such that: - 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
  - layer8 4y ago
    I don’t think so, at least if you assume that each concrete solution can be expressed in finite length in a formal language with a finite alphabet, and can be mechanically checked (which is generally the case for mathematical proofs). Because then you could just enumerate all strings of that language until you find one that describes the solution to the given problem, which by your second item would be guaranteed to exist, and thus the procedure be guaranteed to terminate, contradicting your first item.
    - najdan33 4y ago
      Thanks for the answer, it helps piece together the puzzle. I believe there's a problem with this reasoning: > each concrete solution can be expressed in finite length in a formal language with a finite alphabet Suppose that's the case, the problem is that the resulting language of all the finite proofs can still be infinite and we again cannot enumerate and check all the solutions (since the final set is infinite). Therefore we're short of a method to decide yes/no for each question. This appears to be exactly the case in the example provided by @ykonstant > Consider the sequence of yes/no problems P_K = {Is there a solution to Q=0 in [-K,K]^n?} parametrized by a positive integer K. For each yes/no question, the workload is finite, but for the union of all yes/no questions, the workload is not finite.

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?

hackandthink 4y ago

My understanding: There's no algorithm to decide. But for any equation we can be lucky to find a solution or a proof that there's no solution. But this doesn't prove that there is an equation for which we'll never know if it's solvable or not.

moefh 4y ago
From my understanding, while that's is technically true, given a consistent axiomatic system (like ZFC[1], the foundation of mathematics we use) there exists a diophantine equation that can't be proven to have no solutions in that system (even though it has no solutions). This mathoverflow answer[2] gives the equation and a link to the paper that shows how to calculate the constants (the numbers are huge!). What that means in practice is that although what you wrote is true, for some diophantine equations we'd have to come up with new axioms to be able to write a proof of the inexistence of its solutions. But then, how can we be sure that the the new axioms are consistent? [1] I'm assuming ZFC is consistent; if it's not then it can prove anything, including the existence of solutions for any equations at all [2] https://mathoverflow.net/a/81986 https://mathoverflow.net/a/81986
- hackandthink 4y ago
  Thanks. I'm somewhat lost, but it seems to work Gödel like. The statement is true (equation has no solution) but we can't prove it.
layer8 4y ago
See https://news.ycombinator.com/item?id=34384838 https://news.ycombinator.com/item?id=34384838, I think it disproves your last sentence — at least when assuming that all solutions and all proofs of non-existence of a solution are expressible in a shared formal language.

ykonstant 4y ago

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 that Diophantine equation has no solutions (and thus the same is true for ZFC, since NBG is a conservative extension of ZFC). [0] https://link.springer.com/article/10.1007/s10958-014-1830-2 https://link.springer.com/article/10.1007/s10958-014-1830-2

najdan33 4y ago
Does there exist a set of yes/no problems such that: - 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
- layer8 4y ago
  I don’t think so, at least if you assume that each concrete solution can be expressed in finite length in a formal language with a finite alphabet, and can be mechanically checked (which is generally the case for mathematical proofs). Because then you could just enumerate all strings of that language until you find one that describes the solution to the given problem, which by your second item would be guaranteed to exist, and thus the procedure be guaranteed to terminate, contradicting your first item.
  - najdan33 4y ago
    Thanks for the answer, it helps piece together the puzzle. I believe there's a problem with this reasoning: > each concrete solution can be expressed in finite length in a formal language with a finite alphabet Suppose that's the case, the problem is that the resulting language of all the finite proofs can still be infinite and we again cannot enumerate and check all the solutions (since the final set is infinite). Therefore we're short of a method to decide yes/no for each question. This appears to be exactly the case in the example provided by @ykonstant > Consider the sequence of yes/no problems P_K = {Is there a solution to Q=0 in [-K,K]^n?} parametrized by a positive integer K. For each yes/no question, the workload is finite, but for the union of all yes/no questions, the workload is not finite.