I'm looking for an effective theory $T$ that solves the halting problem, in the sense that for every Turing machine $M$, $T$ either proves that $M$ halts, or that it does not halt.
On the face of it, this would violate Turing's theorem that you can not solve the halting problem. The trick is that $T$ would not actually be sound, i.e., there would be at least one Turing machine $M$ such that $T$ proves that $M$ halts, but it really doesn't. (So it would not actually solve the halting problem.) (For example $PA+\lnot Con(PA)$ proves that the Turing machine that looks for a contradiction in $PA$ halts, when it in fact this machine does not.)
As to avoid trivial answers (such as a theory that simply asserts that every turing machine halts), I'm also going to require that $T$ proves all the axioms of PA, and is consistient.
- Since Turing's theorem can be internalized to $T$ (since it can in $PA$), $T$ can proves that $T$ does not solve the halting problem. This is okay though, since $T$ is not sound.
- This implies that in any model of $T$, there would be a nonstandard Turing machine $M$ such that $T$ cannot prove whether or not $M$ halts.
- $T$ proves that $T$ is inconsistent, since it would proves that the machine that looks for a contradiction in $T$ halts (otherwise, it would need to prove that this machine does not halt, proving itself consistent, in violation of Goedel's second incompleteness theorem).