Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. Join them; it only takes a minute:

Sign up
Here's how it works:
  1. Anybody can ask a question
  2. Anybody can answer
  3. The best answers are voted up and rise to the top

What impact would a device (ie super-computer or relativistic computer or other method) that solves the halting problem have on math?

Would there be any mathematical problems left to solve?

What would be the greatest mathematical challenges left?

Could we compute if our axiom system is is consistent?

Could we find "the one true and final" complete set theory?

share|cite|improve this question
The existence of a halting oracle would disprove the Church-Turing thesis. Breaking it open and studying it would lead to new physics since none of the physics we currently have is super-Turing. It would also count as a constructive proof of the law of excluded middle. – quanta Apr 7 '11 at 18:50
Why is this tagged [physics]? – Rahul Apr 7 '11 at 21:34

Well, a means to solve the halting problem itself would do nothing for us if it would take $2^{1000}$ steps to test whether even a small program halted or not. But let us suppose we have a magical oracle that can do this for us quickly. For instance, imagine that you had a scroll with Chaitin's constant inscribed on it.

Then we could certainly compute whether the axiom system (which I'll assume to be recursively enumerable in the standard sense) is consistent or not. Simply define a machine $M$ as follows: for each $n$, $M$ enumerates all possible proofs of length $n$ (in our language and using our fixed set of axioms) and checks whether a contradiction (that is, $p \cap \not p$) can be derived. If at some point a contradiction is derived, it halts. So whether this program halts or not is equivalent to the consistency of the given axiom scheme. By a variant of this, we would be able to determine whether any statement of interest (e.g. the Riemann hypothesis, the P versus NP problem, etc.) is provable from our axiom scheme.

share|cite|improve this answer
If we were in possession of such an oracle, then we could tell whether or not any given theorem can be proven within a given effectively generated axiom scheme. But then we would want a stronger axiom scheme in which it can be proven whether not any program halts. Godel's incompleteness theorem (or a generalisation) would still apply to that axiom scheme. – George Lowther Apr 7 '11 at 22:17
@George: Dear George, thanks for the correction. – Akhil Mathew Apr 7 '11 at 22:19

There is a subtle point here that should be noted: We have to know which halting problem we are talking about. If we are referring to the halting problem for Turing machines, that would mean that we can decide the consistency of today's axiomatic systems only. That is, mathematics may radically evolve if an algorithm that solves the halting problem for Turing machines was invented.

The reason why can be found in the definition of an axiomatic system. What we want is a set of axioms such that an algorithm decide whether a sentence is an axiom or not. Therefore new algorithmic processes may allow us to create new, more expressive axiomatic systems that cannot be coded in Turing machines.

And maybe this new class of algorithms will have similar properties to Turing machines and won't be able to solve its own halting problem. Then these new mathematics will likewise have uncertainties and require ingenuity in the discovery of theorems.

share|cite|improve this answer

Such a device would only solve problems low down in the hierarchy. For example, let $T$ be the set of sentences in the usual language of number theory that are TRUE in the natural numbers (so I am asking about truth, not provability from say the usual axioms). Our hypothetical device would be hopelessly inadequate for determining whether or not a sentence is in $T$. Admittedly, it would be able to deal with most of the interesting sentences.

share|cite|improve this answer
Is "hopelesly inadequate for determining" the same as "unable to determine"? – jva Aug 19 '11 at 7:23
Yes. Say lowest level, recursive sets in many variables, then existential quantification on recursive sets (r.e.), then universal quantification on existential quantification on recursive sets, and so on, alternating $\forall$ and $\exists$. Each level is of provably higher level of undecidability as the next lower level. The set of sentences true in $\mathbb{N}$ provably belongs to none of those levels. This is a result of Tarski (undefinability of truth). A machine that checked $n=1$ in $1$ millisecond, $n=2$ in $1/10$, $n=3$ in $1/100$, and so on could solve the halting problem. (cont) – André Nicolas Aug 19 '11 at 9:00
(cont) It could not solve the $\forall\exists$ class, let alone $\exists\forall\exists$ and so on. Truth in $\mathbb{N}$ is "harder" than any level in this hierarchy. Thus an "oracle" that settles the Halting Problem would be an infinite chain of levels too weak to settle truth. Not that one should complain. An oracle for level $\exists$ would take care of a number of the classical open problems, a (strictly stronger) oracle for the $\forall\exists$ would take care of probably the rest. But it would not begin to settle truth in general. – André Nicolas Aug 19 '11 at 9:19

I think it would have to walk a careful line. If we had an oracle for the halting problem, we could essentially prove much of number theory with a machine, something like:

1) n=0

2) Test (in)equality of formula for n

If its true, continue.

If its false stop.

3) n= n+1

4) GOTO 1

and then we use the oracle on it. This would work for most theorems and conjectures in number theory.

It really gets right on the edge of Goedels incompleteness theorem, because in principal you can check most first order sentences about the integers.

share|cite|improve this answer
In principle. ${}$ – Mariano Suárez-Alvarez Apr 7 '11 at 22:54

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.