[srcreigh]

Obligatory mention that although Halt doesn’t exist for arbitrary P, there are Halt_N for every natural N where Halt_N works on empty-input TMs with at most N states.

Undecidability is more about compression than it is about whether we can determine if TMs halt.

[snarkconjecture]

For sufficiently large N, it's impossible to prove Halt_N correct.

(The N required depends on your axioms.)