>>11809203I really like this characterization. Let be the set of true sentences of arithmetic. Take any recursively enumerable subset of , that is closed under logical deductions. For example, modus ponens is a rule of inference so if , then . Godels first theorem says that there is a sentence , that is, there is a true statement about arithmetic that is not provable from . In fact, this can be strengthen, you can in fact take to be not just recursively enumerable, but any set definable in . Godel's second theorem says that the sentence that asserts the consistency of is one of these sentences. The halting problem states there is no Turing machine that decides, answers a yes or no answer, on a given input , whether the Turing machine with code , halts or goes into an infinite loop on input .
Of course there are a lot of details to check. The halting problem proof is not too bad. You are not going to understand these theorems unless yo go through the details.
