Is there a polynomial equation whose solution over the integers is independent of ZFC - MathOverflow

Is there a polynomial equation whose solution over the integers is independent of ZFC

2012-04-28T13:23:14Z

Consider the algorithm that goes over all proofs in peano arithmetic. Allegedly, for a given multivariate polynomial equation we should find a proof or disproof of existence of an integer solution. Therefore, given the negaative solution of Hilbert's 10th problem, there should be a polynomial for which we could neither prove or disprove existence of an integer solution. Is this argument valid? It seems strange, can anyone explain to me this anomaly? It seems to indicate that there are models in which there is a solution and others in which there is no solution. I dont really understand how that can happen?

Answer by Joel David Hamkins for Is there a polynomial equation whose solution over the integers is independent of ZFC

2012-04-28T13:48:00Z

Yes, your description of the situation is essentially correct. The way it can happen is this.

On the one hand, if a given diophantine equation does have a solution in the integers, then it will be easy to prove in PA that this solution is indeed a solution, since the proof amounts to checking that that particular solution is indeed a solution.

But on the other side of the coin, when a diophatine equation has no integer solution, there seems to be no reason for us to expect that there should be an easy proof that there is no solution. And indeed, because of the MRDP solution of Hilbert's 10th problem, we know that there are diophatine equations having no integer solution, but for which we cannot prove this in PA. The way to understand what is going on is to realize that this situation arises when the diophatine equation has no solution in the standard integers, but there is some nonstandard model of PA, with nonstandard integers, in which there is a solution using the arithmetic of that nonstandard model. The solution in that model must necessarily involve some of the infinite nonstandard integers, since the standard part of a nonstandard model of arithmetic has the standard arithmetic.

Answer by Johannes Hahn for Is there a polynomial equation whose solution over the integers is independent of ZFC

2012-04-28T13:49:45Z

Hi Daniel.

The point with Hilbert's 10th problem is that diophantine equations are complex enough to encode Turing machines and other complicated stuff that has some kind of no-can-do-theorem. In particular: To each Turing machine there is a polynomial $p\in\mathbb{Z}[X_1,\ldots,X_n]$ such that $p$ has a solution in $\mathbb{N}$ iff the machine halts (lets consider only turing machines with empty input for simplicity).

Now lets look at the machine that lists all PA-proofs and halts iff it finds a proof of a given PA-statement $\psi$. If PA could prove the existence or non-existence of solutions to every diophantine equation, then it could decide this in particular for those equations that encode Turing machines, i.e. this algorithm would effectively decide the halting problem which is impossible.

There are other things that you can encode with diophantine equations. For example it is possible to translate a statement like $con(PA)$ into a diophantine equation. Now PA cannot prove the existence of solutions of such an equation because that would mean that PA proves $con(PA)$ which is also impossible. It can't disprove the existence of solutions either because then PA would prove $\neg con(PA)$ which is also impossible because PA is consistent.

Now about the models... There isn't that much to say about it. If PA cannot decide the existence of solutions of $p=0$, then the standard model $\mathbb{N}$ won't contain a solution (because if it would, this solution could be explicitely written down and it could be checked by calculation that it is indeed a solution thus giving a formal PA-proof of its existence). But there will be many non-standard models with solutions. Those solutions are of course non-standard numbers, so you can't write them down or do any kind of explicit computations with them. In particular: You won't be able to squeeze an existence proof out of them like you can with a standard solution.

I hope that answers your questions.