|
|
|
|
|
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. |
|