Proof — Halting problem (undecidability)

Statement

There is no algorithm that, given a program and its input, can decide whether the program will halt. The halting problem is undecidable. This result, with Gödel's incompleteness theorems, established fundamental limits on what can be computed and proved.

Formula

No Turing machine can decide if M(x) halts

Equation

HALT(M, x) is undecidable

Proof sketch

Proof by diagonalization: assume a halting decider H exists. Construct a machine D that, given M, runs H(M,M) and halts iff H says M does not halt on M. Then D(D) halts iff D(D) does not halt—contradiction.