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?
On
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.
On
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.
On
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.
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.