Hacker News new | ask | show | jobs
by ProfHewitt 1862 days ago
Your statement 1 of Gödel's first result is not quite correct.

Suppose that Halt[e] means that expression e halts.

The predicate Halt is algorithmically undecidable. That is,

there is no algorithm that decides Halt.

But this does not directly say that Halt is inferentially

undecidable. That is, Halt[e] can always be proved or

disproved.