If you actually want to make the proof above as rigorous as Goedel’s original proof, you’ll find that it will be exactly as technical as the original. The techn

If you actually want to make the proof above as rigorous as Goedel’s original proof, you’ll find that it will be exactly as technical as the original. The technical difficulty in the proof above is hidden in the step 2 — what you need to show is that every statement of a form “the Turing machine T = {..., ..., ...} halts on input ...” is expressible in the language of first order arithmetic. To do that, you need to do exactly the same work as Goedel did, with all the finite string encoding etc.