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