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 `n`th proof is encountered. Let's say this `n`th 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*.