show/hide this revision's text 2 added 1472 characters in body

The simplest example I can think of is Goodstein's theorem. This, as the name suggest, is provable (in the standard ZFC theory of sets) but is not provable in Peano arithmeticarithmetics.

I don't want to duplicate Wikipedia, but briefly here is how it goes. Take a number, say $47$ and write it in base $2$, so you get $$47 = 1 \cdot 2^5 + 1 \cdot 2^3 + 1 \cdot 2^2 + 1 \cdot 2^1 + 1 \cdot 2^0.$$ Write each exponent in base $2$, rinse and repeat until you cannot simplify anymore. In our case you get$$47 = 1 \cdot 2^{1 \cdot 2^{1\cdot 2^{1 \cdot 2^0}} + 1 \cdot 2^0} + 1 \cdot 2^{1 \cdot 2^{1 \cdot 2^0} + 1 \cdot 2^0} + 1 \cdot 2^{2^{1 \cdot 2^0}} + 1 \cdot 2^{1 \cdot 2^0} + 1 \cdot 2^0.$$

After that subtitute each $2$ with a $3$ and subtract $1$, to get$$1 \cdot 3^{1 \cdot 3^{1\cdot 3^{1 \cdot 3^0}} + 1 \cdot 3^0} + 1 \cdot 3^{1 \cdot 3^{1 \cdot 3^0} + 1 \cdot 3^0} + 1 \cdot 3^{3^{1 \cdot 3^0}} + 1 \cdot 3^{1 \cdot 3^0} + 1 \cdot 3^0 - 1 = 3^{28} + 81 + 27 + 3.$$

Write this number again in expanded base $3$ (in our case we already have it), change each $3$ with a $4$ and subtract $1$ (this time the expanded form will change a bit since we do not have a final $1$).

Proceed in this way and you get a sequence (called the Goodstein sequence of $n$) which becomes abnormously big at a really fast rate and... well, this sequence is eventually $0$. Just subtracting that small $1$ at each step eventually becomes preponderant over the base substitution.

The fact that the Goodstein sequence of $n$ is eventually $0$ is really easy to prove using ordinals, but it turns out it is an unprovable statement with only Peano arithmetics.

show/hide this revision's text 1

The simplest example I can think of is Goodstein's theorem. This, as the name suggest, is provable (in the standard ZFC theory of sets) but is not provable in Peano arithmetic.