# How do proofs of program termination depend on strength of logical systems?

I'm looking for clarifying insights on the following topic. While there can be no general proof strategy to show that terminating Turing programs do, indeed, terminate, some specific programs can be shown to terminate as follows.

To show a program terminates, we pick a meta-theory (say ZFC or a dependent type theory), formalize the notion of Turing computation in it, and then prove a version of the statement $$\forall \mathrm{inputs}.\exists n \in \mathbb{N}. \mathrm{computation}(\mathrm{program},\mathrm{input},\text{step:} n) = \text{halting-state}$$

Are there examples of programs that can be shown to (not) terminate in one meta-theory but not in another? What is the general theoretical idea here? (Is it consistency strength?)

Here's an attempt: consider a logical system A, and the algorithm P that enumerates proofs in A and halts when it finds an inconsistency. Consider a stronger system B, that shows that A is consistent. Then B proves that P never terminates, a proof that cannot be supplied by A ... if A is consistent. (Are there concrete/better examples?)

I think my confusion arises a bit from the subject of computability theory usually not explicitly picking foundations (as evident e.g. in the Church-Turing hypothesis) so it takes P's termination as an objective (albeit potentially inaccessible) truth, not something that depends on the choice of logical system. Is the analog of this in the subject of logic, that consistency of a logical system is an objective (albeit potentially inaccessible) truth? And then to connect the two: would computability theorist happily accept any proof of termination in any logical system they deem consistent?

• You might be interested in this blog post by John Baez (and the related post by Joel David Hamkins) Jul 19, 2023 at 15:43

In the meantime, yes there are definitely turing machines that can be shown to halt in one metatheory, but not another. In fact, your idea to enumerate potential proofs of the consistency of $$A$$ is a great one! If $$A$$ is consistent (and strong enough), then it can never know that about itself, so $$A$$ cannot prove that such a machine halts. But in a stronger system $$B$$, maybe we can prove it!
For a "concrete example", take the Paris-Harrington Theorem. This says that if you give me natural numbers $$n,m,k$$, then I can find a natural number $$N$$ big enough to make some ramsey-theoretic statement true. It turns out that the function $$\mathsf{PH}(n,m,k)$$ outputting such an $$N$$ is computable! So now we can ask whether it provably halts.
In ZFC we can prove that $$\mathsf{PH}$$ halts on all inputs, because we can prove that the number $$N$$ always exists (so if we naively search for it, we'll always find it, and so $$\mathsf{PH}$$ will halt). However in PA we can't prove that it always halts! Formally this is because you can use Paris-Harrington to prove the consistency of PA. Informally this is because $$N$$ "grows so quickly" that PA can't guarantee the existence of an $$N$$ for each possible input.