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 undec

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.