Gödel’s incompleteness theorems have many variants: semantic vs. syntactic versions, which specific theory is taken as basic, what model of computability is used, which logical system is assumed to underlie the provability relation, how syntax is arithmetized, what hypotheses the theorem itself uses (soundness, consistency, \(\omega\)-consistency, etc.). These result in trade-offs regarding simplicity of the proof, but also scope of application and consequences that can be drawn.

There are two new(ish) and super-useful surveys of proofs of Gödel’s incompleteness theorem that review these versions and their limitations and scope. The first is by Lev Beklemishev:

Л.Д. Беклемишев (2010). Теоремы Гёделя о неполноте и границы их применимости. I., Успехи Математических Наук 65(5) 61-104. PDF.

English translation:

L. D. Beklemishev (2010). Gödel incompleteness theorems and the limits of their applicability. I.*,* *Russian Mathematical Surveys * 65(5) 857-898. PDF

The second is by Bernd Buldt:

B. Buldt (2014). The scope of Gödel’s first incompleteness theorem, *Logica Universalis*. forthcoming. PDF preprint

Lev’s is mathematically more exhaustive and more technical; Bernd’s is less technical and also goes into philosophically relevant aspects such as Gödel’s theorems for system with non-classical underlying logics.