This question is about whether every mathematical theorem can be reduced to the question of whether a single Turing machine halts. In particular, I'm interested in conjectures that are currently unproven.
For example: Wikipedia says that it's currently unknown whether there are any odd perfect numbers. Since it's decidable whether a given number is perfect, one could write a Turing machine that checks each odd number in turn and halts if it finds one that's perfect. (This Turing machine does not take any input.) If we knew whether that Turing machine halts, then we would know whether the conjecture is true, and vice versa.
However, as another example, what about the twin primes conjecture? It's decidable whether a given number is the first prime in a twin pair, but in this case we can't just halt when we find the first one, because the question is about whether there are an infinite number. It's not clear to me whether it's possible to make a Turing machine that halts if and only if the twin primes conjecture is true.
We can surely make a Turing machine that halts if and only if the twin primes conjecture is provable within Peano arithmetic or some other formal system, but that's a different question, since it might be true but not provable in the particular system we choose.
So my questions are
- Is it possible to make a Turing machine that halts if and only if the twin primes conjecture is true? (And if so, how?)
- Is it possible, in general, to make a Turing machine that halts if and only if some given mathematical statement is true? Can this Turing machine be constructed algorithmically from the formal statement?
- If it's not possible in general, is there some way to classify mathematical statements into whether they're equivalent to the halting of a single Turing machine, or a turing machine with an oracle, etc.? If so, is this classification decidable for a given statement?