Discussion about this post

User's avatar
lcamtuf's avatar

Note that most of the proofs cited in this article have something in common. They don't actually show the thing they claim to prove: they posit that there are only two choices and then rule out the other option.

This is the principle of the excluded middle (PEM): "it's either x or not x". Sometimes, before we use it, we ought to ask: can it be neither? Can it be something else? Maybe there's some third category between "stops in finite time" and "continues forever", and we just need a theory of that?

Although most mathematicians play fast and loose with PEM, there's a niche school of constructivist mathematics that treats many such proofs as suspect and tries to work without leaning on PEM.

Expand full comment
Iustin Pop's avatar

me → this article → (woosh). Or at least after the "A constrained-instruction computer" part.

Expand full comment
12 more comments...

No posts