> The computer theory version of Godel's result is the halting problem
I am not sure that I agree with this. Of course if you can solve the halting problem, then you can decide some propositions. Like you have two Turing machines, one that enumerates proofs and the other that enumerates counterexamples, and they stop after finding the first one. Prove that one or them halts and you have decided the proposition.
On the other hand, there are "highly undecidable" problems which you cannot solve even if you had an oracle for the halting problem.
The Halting Problem Theorem is an intuitive way to prove inferential incompleteness for strongly-typed theories in which Gödel’s proposition I'mUnprovable does not exist.
Using Orders on propositions, the construction of Gödel’s proposition I'mUnprovable is blocked because the mapping Ψ↦⊬Ψ has no fixed point because ⊬Ψ has order one greater than the order of Ψ since Ψ is a propositional variable.
I am not sure that I agree with this. Of course if you can solve the halting problem, then you can decide some propositions. Like you have two Turing machines, one that enumerates proofs and the other that enumerates counterexamples, and they stop after finding the first one. Prove that one or them halts and you have decided the proposition.
On the other hand, there are "highly undecidable" problems which you cannot solve even if you had an oracle for the halting problem.