Gödel’s first incompleteness theorem says (excerpted from Wikipedia):
For any consistent, effectively generated formal theory that proves certain basic arithmetic truths, there is an arithmetical statement that is true, but not provable in the theory.
Now we consider a formal system A in which Gödel’s first incompleteness theorem(G_1) can be proved.
If A is effectively generated, consistent and includes Peano arithmetic(PA), then G_1 explicitly gives a proposition P, and asserts P is both true and unprovable inside A. Because we can prove G_1 inside A, we can prove P is true. Also, we can prove P is unprovable inside A. But this is a contradiction.
Therefore, a formal system cannot possess all of the four properties below:
- effectively generated
- includes Peano arithmetic
- in which Gödel’s first incompleteness theorem can be proved
Since Property 1 and 3 are usually satisfied for ordinary systems, it may sound more elegant when reformulated as:
For any formal system A, which is effectively generated and includes Peano arithmetic, if Gödel’s first incompleteness theorem can be proved inside A, then A must be inconsistent.