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