On Some Doubts Concerning the Formal Correctness of Gödel's Incompleteness Theorem

Similar to Russell's antinomy, Gödel's Incompleteness Theorem involves some kind of negative self-reference. For verifying the formal correctness, a complete formalization of the proof is required. Its formulation in the standard work on higher-order logic by Peter B. Andrews (and also in set-theoretic works) reveals a weakness in the proof unknown before. Unlike mathematics in general, this theorem cannot be proven in Andrews' logical system by syntactical means only, which raises questions on the theorem's necessity. The problem of negative self-reference in mathematics, the rôle of metamathematics in general and of the semantic approach (model theory) in detail is discussed.