Imagine we have a consistent
formal system F for proving theorems about
Turing machines. We implement F in a Turing machine that churns out its proofs in
lexicographic order.
Some of these proofs will be proofs that such and such a Turing machine will halt. We adapt our machine so that when it proves that a particular Turing machine halts, it outputs that proof together with an integer, which is incremented for each successive proof. We call this machine E, since it enumerates the proofs that particular Turing machines halt.
We now construct another machine, M, so that it expects a number on its input - call this n - and then runs E until the nth proof is encountered. Let's say this nth proof has established that the machine T will
halt (all the output consists of proofs that particular machines will halt, so it shouldn't be too hard to extract T.)
M now runs T, giving it n as input. We know T will halt - our formal system has proven it - so when T halts, M takes T's ouput, adds one, outputs the result, and halts.
Since M has output that differs by one from the ouput of all machines proven to halt by E, the proof that M will halt is never given by E, and yet from an analysis of the way in which E is constructed it seems to follow quite straightforwardly that M will halt.
The set of provably halting Turing machines
seems to be both enumerable and non-enumerable.
The author of the paradox has this to say
Conclusion and interpretation: No consistent formal system can prove its own correctness. This is not a new result -- it's essentially Loeb's Theorem (a variant of Godel's second incompleteness theorem) in the context of rigorous mathematical logic: "If you can show that (if you can show it then it's true) then you can show anything." I like to think of it as an analysis of religious (or academic)
fanatics: If you don't accept the possibility that your way of thinking is wrong, then you are, with certainty, wrong.
But still, intuitively, there is a strong suspicion that the formal system
F implies that
M will halt (as Winfree himself agrees.
I found this paradox at:
http://www.gg.caltech.edu/~winfree/old_html/logic.html.
The author of that page (which has other interesting stuff) is Erik Winfree, who is pleased to call the paradox
Winfree's Paradox.