On: Kurt Gödel and the Mechanization of Mathematics

[strbean]

Out of curiosity, could you give some examples of such theorems?

[xamuel → strbean]

1. The original example would be Goedel's own example, namely, the statement (formulated in the language of PA) that PA is consistent, i.e., that PA does not prove 1=0.

Less contrived examples are:

2. Goodstein's Theorem https://en.wikipedia.org/wiki/Goodstein%27s_theorem

3. A theorem stating that every computable strategy is a winning strategy in the hydra game (see https://faculty.baruch.cuny.edu/lkirby/accessible_independen...)

4. The strengthened finite Ramsey theorem, see https://en.wikipedia.org/wiki/Paris%E2%80%93Harrington_theor...

[strbean → xamuel]

Thanks!