My favourite proof of the (Second) Incompleteness Theorem is the semantic proof due to Jech/Woodin: https://andrescaicedo.files.wordpress.com/2010/11/2ndincompl

My favourite proof of the (Second) Incompleteness Theorem is the semantic proof due to Jech/Woodin: https://andrescaicedo.files.wordpress.com/2010/11/2ndincompleteness1.pdf https://andrescaicedo.files.wordpress.com/2010/11/2ndincompl... It is easiest to think about in terms of set theory, but it is possible to formalize it in a fragment of second-order arithmetic that is conservative over PA (and this conservativity is provable in PA itself). The beauty of this proof is that it first establishes semantic incompleteness without formalizing a proof system; the connection to syntactic incompleteness only uses the Completeness Theorem, which is of independent interest.