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?



Is there a polynomial equation whose solution over the integers is independent of ZFC
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.


