20

We can define a sound proof system as a computable function $\Pi$ which maps strings (proofs) to strings (statements proved), with the following property: if $\Pi(\pi) = p$, then $p$ encodes a true statement. We think of $\pi$ as a proof of $p$. (If $\pi$ is not a valid proof, then $\Pi$ outputs some fixed true statement.) We consider sound proof systems ...


9

Your program P may halt if the proof system it is using is inconsistent, allowing it to prove a self-contradictory statement. The fact that no (sufficiently expressive) proof system can prove its own consistency is exactly what is shown by Gödel's second incompleteness theorem (which, not coincidentally, is in many ways analogous to Turing's halting theorem)....


6

Succinctly, your argument (that there is no such proof that P does not halt) is a proof but not in the same proof system that P is using to search for proofs! In fact, this very kind of computability-based argument can be used to great effect to prove the generalized incompleteness theorems, even the Rosser strengthening.


3

The problem is decidable. You can enumerate the (finitely many) programs that use at most $b$ bytes. For each such candidate program $P$, you can check whether $P$ is valid program (for any reasonable representation) and execute it for up to $t$ time steps. Eventually you either find a program that prints $s$ (and accept) or you run out of programs (and ...


1

There is an efficient way of detecting infinite loop, with no practical drawbacks (even if it is impossible in theory): Let's says you have a cryptographic hash function like sha256, delivering a 256 bit's "imprint" of whatever input you give, with a probability of collision of 2^-128 (due to birthday problem). Let's use an integer counter of 128 ...


Only top voted, non community-wiki answers of a minimum length are eligible