# Can we hope to solve all Diophantine equations?

According to Godel result, neither ZFC nor other particular theory is strong enough to resolve all questions about, say, Diophantine equations. But maybe we can hope that a sequence of theories will help? It is known that ZFC-1 theory (ZFC + Cons(ZFC) ) is much stronger than ZFC, in sense that now there are theorems with extremely shorter proofs, and many new theorem are now decidable. If we continue this to ZFC-2, .., ZFC-n, ... then ZFC-w which is union of all, ZFC-(w+1) and so on, we can continue to extremely large sets of theories, about all of them we have no doubts, and maybe now for every natural Diophantine equation we can choose a theory witch resolve it? Moreover, if we would be able to imagine non-enumerable set of such theories, may be we could hope that for EVERY Diophantine equation has a corresponding theory from this set in which it can be resolved? Or this is trivially incorrect “conjecture”? It seems that this does not contradict to Godel Theorem, which consider one theory, not a sequence of theories.

Another way of thinking about the same idea is to take only axioms from ZFC but add a new derivation rule, which would say that "from any set of axioms A it follows that A is consistent". With this derivation rule we would derive Cons(ZFC) in one step! So, for some reasons (by the way, I do not understand why) Godel theorem is not applicable here. May we hope that with ZFC extended with such a new derivation rule we can, say, solve all Diophantine equations?

-
Am I missing something here? I'd have said it was Matijasevich's theorem, proved in 1970 relying on earlier work of Putnam, Davis, and Robinson, that says you can't "resolve all questions about Diophantine equations". –  Michael Hardy Jun 24 '10 at 15:52
See also this related question and my answer there - mathoverflow.net/questions/12865/… –  François G. Dorais Jun 24 '10 at 16:36
2 Michael Herdy Matijasevich's theorem states that there is no single algorithm for all equations, or, equivalently, no single theory can resolve all of them. My question is that may be the sequence of theories can help. But, as noted by Prof. Joel David Hamkins, this particular sequence is inside a single theory ZFC+Inaccessible, so it will no work. But may be other sequences may help? –  Bogdan Grechuk Jun 27 '10 at 13:10

On the one hand, no consistent theory $T$ that we can describe by giving a computable enumeration of its axioms can settle all Diophantine equations. The reason is that for any such theory $T$, we can construct an integer polynomial $p_T(\vec x)$ that has a solution in the integers if and only if $T$ is inconsistent. Thus, since $T$ is consistent, $p_T$ will have no solutions, but $T$ will not prove this.

One may construct $p_T$ by understanding the MRDP solution to Hilbert's 10th problem. In that argument, for any Turing machine program, one may construct a polynomial whose solutions correspond to halting instances of the program. But consider the program that searches for a proof of a contradiction in $T$, halting only when one is found. The corresponding polynomial $p_T$ for this program will have a solution if and only if the program halts, which is if and only if $T$ is inconsistent, as desired.

So we cannot hope to settle all Diophantine equations with respect to one computably enumerable theory.

Nevertheless, we can describe theories that solve all Diophantine equations in other ways. For example, the theory TA known as True Arithmetic, extends PA and consists precisely of the first order assertions that are true in the standard model $\langle \mathbb{N},+,\cdot,0,1,\lt\rangle$. (One could use $\mathbb{Z}$ in place of $\mathbb{N}$ here, or just realize that $\mathbb{Z}$ is interpretable in $\mathbb{N}$.) Our background theory ZFC proves that TA is consistent and complete, and it certainly correctly settles all the Diophantine equations, proving of exactly those polynomials that have solutions that they do have solutions and of the others that they do not. So this theory is the kind of limit theory you requested. But the difficulty with TA and with any of the non-enumerable limit theories that you seek, is that it is too difficult to recognize the axioms. We cannot tell if a proof from TA is legitimate, because we cannot even recognize the axioms.

For the purpose of settling Diophantine equations, it would suffice to use $TA_1$, consisting just of the true $\Pi_1$ assertions. But recognizing whether a given $\Pi_1$ assertion is true or not (that is, recognizing it as an axiom of $TA_1$) is exactly as difficult as recognizing whether a given Diophantine equation has solutions in the integers or not.

This last difficulty is inherent in the problem, since any theory correctly proving whether the polynomials have solutions or not will prove all the instances of $TA_1$. So $TA_1$ a minimal instance of the theory you seek, but it is not clear how useful it is for your purpose, since it is as difficult to recognize the axioms of this theory as it is to solve the problems you intend to solve with it.

-
Yes, I agree with you, but I am asking not about one theory T but about the whole sequence of theories: ZFC1 consisting of "ZFC+(ZFC is consistent)", ZFC2 is "ZFC1+(ZFC1 is consistent)", etc, and for any ordinal $\alpha$ we get theory $ZFC_\alpha$. If we try to say that union of all this theories is T and apply your argument, that your polynomial $p_T$ will be resolved by next theory in a sequence: "T+(T is consistent)"! So, no particular theory T will help for ALL equations, but for every particular equation we can hope to find a corresponding theory in sequence which will resolve it. –  Bogdan Grechuk Jun 24 '10 at 13:29
It is important, that all the axioms are easy to recognize here, and the problem "We cannot tell if a proof is legitimate, because we cannot even recognize the axioms" do not arise with this sequence. –  Bogdan Grechuk Jun 24 '10 at 13:30
A uniform description of the tower of theories $T_n$ leads to a description of the union theory $\bigcup_n T_n$, to which the $p_T$ objection still applies. And if you can't describe the tower of theories, then it seems you can't (uniformly) recognize your axioms, and so the other objection applies. –  Joel David Hamkins Jun 24 '10 at 15:13
You don't need to work above ZFC, since as I explained $TA_1$ suffices, and this is provably the minimal theory to do so. This theory is a tower of finitely axiomatizabble theories $T_n$, where one adds the answer for one polynomial in each step. In this way, each $T_n$ is c.e., and we can prove that we can recognize the axioms of each individual $T_n$ separately, and the union settles all Diophantine equations. So this tower satisfies your properties. But we cannot uniformly describe the tower, and similarly for any such tower of theories that succeeds. –  Joel David Hamkins Jun 24 '10 at 15:21
The point being that there are single theories, such as ZFC+Inaccessible which are thought likely to be consistent and that imply the entire tower of consistency statements in the tower you mention. So the $p_T$ for these theories $T$ will be Diophantine equations not settled by your tower. –  Joel David Hamkins Jun 24 '10 at 18:11