Consistency of T isn’t enough, is it? For example the theory (PA + “The program that searches for a contradiction in PA halts”) is consistent, even though that program doesn’t halt.
I don’t follow. I agree that (PA + “PA is inconsistent”) is consistent. How does it follow that consistency of T isn’t enough? The way I use consistency there is “If T proves that a program halts, then that program does halt and we can safely run it.”.
I’m arguing that, for a theory T and Turing machine P, “T is consistent” and “T proves that P halts” aren’t together enough to deduce that P halts. And as I counter example I suggested T = PA + “PA is inconsistent” and P = “search for an inconsistency in PA”. This P doesn’t halt even though T is consistent and proves it halts.
So if it doesn’t work for that T and P, I don’t see why it would work for the original T and P.
I thought of that before but I was a bit worried about it because Löb’s Theorem says that a theory can never prove this axiom schema about itself. But I think we’re safe here because we’re assuming “If T proves φ, then φ” while not actually working in T.
Consistency of T isn’t enough, is it? For example the theory (PA + “The program that searches for a contradiction in PA halts”) is consistent, even though that program doesn’t halt.
I don’t follow. I agree that (PA + “PA is inconsistent”) is consistent. How does it follow that consistency of T isn’t enough? The way I use consistency there is “If T proves that a program halts, then that program does halt and we can safely run it.”.
I’m arguing that, for a theory T and Turing machine P, “T is consistent” and “T proves that P halts” aren’t together enough to deduce that P halts. And as I counter example I suggested T = PA + “PA is inconsistent” and P = “search for an inconsistency in PA”. This P doesn’t halt even though T is consistent and proves it halts.
So if it doesn’t work for that T and P, I don’t see why it would work for the original T and P.
Right. Perhaps the axiom schema “If T proves φ, then φ.”?
Yeah, I think that’s probably right.
I thought of that before but I was a bit worried about it because Löb’s Theorem says that a theory can never prove this axiom schema about itself. But I think we’re safe here because we’re assuming “If T proves φ, then φ” while not actually working in T.