Take the 2-minute tour ×
MathOverflow is a question and answer site for professional mathematicians. It's 100% free, no registration required.

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?

share|improve this question
Related question: mathoverflow.net/questions/29365/… –  Joel David Hamkins Apr 28 '12 at 13:31
Also mildly related: mathoverflow.net/questions/32892/… –  Asaf Karagila Apr 28 '12 at 14:32
add comment

2 Answers

up vote 7 down vote accepted

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.

share|improve this answer
Given all of this, can you give an explicit example of a diophantine equation for which PA can't prove or disprove the existence of a solution? –  Paul Siegel Apr 28 '12 at 15:44
In principle I suppose I could. ;-) The polynomials that I and Joel David Hamkins describe are obtainable by algorithmic procedures. It's a very boring thing to do, but in principle possible, even by hand. A friend of mine told me he once calculated a "small" polynomial that encodes $con(ZFC)$ (or was it $con(PA)$ ?) for his diploma thesis. If I remember correctly he said that only [some two-digit number] variables were necessary and the polynomial would fit on [one-digit number] pages if printed. I could ask him if you like. –  Johannes Hahn Apr 29 '12 at 14:45
I just saw Asaf Karagila's comment. In one answer in that thread Merlin Carl is mentioned (which is the "friend of mine" I was talking about) and in another answer Vladimir Reshetnikov gives an explicit and (for me surprisingly) short polynomial. –  Johannes Hahn Apr 29 '12 at 14:56
add comment

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.

share|improve this answer
It is possible to construct such an equation? Does this mean that in more powerful systems we can solve the 10th problem? –  Daniel Bachmat Apr 28 '12 at 14:00
Yes, one can write down explicit diophantine equations with the property. For any computably axiomatizable formal system $T$, there is a diophantine equation whose solutions are the Goedel codes of a proof of a contradiction in $T$. If $T$ is consistent, this diophantine equation will have no solution, but $T$ will be unable to prove this. (About your inquiry about more powerful systems, follow the link in my comment to your question above, where this is discussed at length.) –  Joel David Hamkins Apr 28 '12 at 14:12
add comment

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.