Proof — Gödel's incompleteness theorems

Statement

First incompleteness: In any consistent formal system F that can express elementary arithmetic, there exists a true statement G that is not provable in F. Second incompleteness: F cannot prove its own consistency (if F is consistent). This established fundamental limits on formal systems and paved the way for computability theory.

Formula

Consistent F ⊇ PA ⇒ ∃G (True(G) ∧ ¬Prov_F(G))

Equation

Con(F) not provable in F

Proof sketch

Gödel constructed a self-referential sentence G that asserts its own unprovability. If G were provable, F would be inconsistent; if ¬G were provable, G would be false but provable. Hence G is true and unprovable. The proof uses Gödel numbering to arithmetize syntax.