# Are there programs that never halt and have no non-termination proof?

Like black holes in computer science. We can only know they exist but when we have one of them we will never know it's one of them.

• Deciding the halting-problem is at least as hard as proving theorems (given a theorem $T$ you can simply write a program like if T is true then halt else loop forever, the program terminates if and only if the theorem is true). If there weren't such programs it would mean that you could prove all theorems, which is well known to be false. – Bakuriu Dec 24 '14 at 10:17
• @Bakuriu: How would you write if T is true? – ruakh Dec 24 '14 at 19:28
• @ruakh: The traditional method is For each string S in the (countable) universe of possible strings: If S is a syntactically valid proof of T, halt. – Quuxplusone Dec 25 '14 at 0:08
• @Quuxplusone: Well, yes, but that doesn't seem to fit into Bakuriu's construction . . . – ruakh Dec 25 '14 at 2:00
• This is interesting, but beyond my knowledge. Can you elaborate, please? – Evorlor Dec 25 '14 at 2:23

There are indeed programs like this. To prove this, let's suppose to the contrary that for every machine that doesn't halt, there is a proof it doesn't halt.

These proofs are strings of finite length, so we can enumerate all proofs of length less than $s$ for some integer $s$.

We can then use this to solve the halting problem as follows: Given a Turing Machine $M$ and an input $x$, we use the following algorithm:

s := 0
while (True)
test if machine M halts on input x in s steps
look at all proofs of length s and see if they prove M doesn't halt on input x
set s := s + 1


If $M$ halts on input $x$, then it halts in some finite number of steps $s$, so our algorithm terminates.

If $M$ doesn't halt on input $x$, then by our assumption, there's some proof length $s$ where there's a proof that $M$ doesn't halt. So in this case, our algorithm always terminates.

Thus, we have an algorithm deciding the Halting problem which always terminates. But we know this cannot exist, so our assumption that there's always a proof of non-halting must be false.

• I think a weaker form of godel's incompleteness theorem follows from this too. Basically that there exist things which are true but can't be proven. This is one of my new favorite thought experiments. – Jake Dec 24 '14 at 5:36
• Do you think trying to prove P = NP or trying to find an odd perfect number could be one of these programs? – Otakar Molnár López Dec 24 '14 at 5:46
• That doesn't quite make sense because non-terminating programs are not proofs nor are they numbers but the idea you are getting at has been brought up. Some say that PvsNP is unprovable – Jake Dec 24 '14 at 6:07
• @Jake I believe part of the motivation of Turing machines was a cleaner expression of the idea behind Godel's theorem. – cpast Dec 25 '14 at 3:52

For a somewhat more concrete example, let us assume that the theory we are using for our proofs has the following (quite reasonable, IMO) features:

1. It is is consistent; that is, it cannot prove a contradiction.
2. Its set of axioms is recursively enumerable.
3. Its proofs can be written down as finite bitstrings.
4. The question of whether a given string encodes a well-formed and correct proof in it is algorithmically decidable in finite time.
5. It is expressive enough to admit a proof of Gödel's second incompleteness theorem, which says that it cannot prove its own consistency.

With those assumptions, the following program will never halt, but cannot be proved (within the scope of the theory we are using) not to halt:

let k := 0;
repeat:
let k := k + 1;
let s := binary expansion of k, excluding leading 1 bit;
while s does not encode a proof of a contradiction;
halt.


The key detail here is the first assumption above, namely that the theory we are using for our proofs is consistent. Obviously, we need to assume this, for our proofs to be worth anything, but Gödel's second incompleteness theorem says that, for any reasonably expressive and effectively axiomatized theory, we cannot actually prove this (except possibly in some other theory, whose consistency we then need to assume, etc. etc.).