# On formal systems in which Gödel's first incompleteness theorem can be proved

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