[FOM] Rapid growth functions and consistency of PA

[Andrej Bauer]

Dear FOMers,

an undergraduate student at our math department got interested in
Goodstein sequences and the Hydra game of Paris and Kirby. He is going
to present them in an upcoming local seminar. The easy part is not
problematic, namely how to use induction up to epsilon_0 to show that
the sequences stop and that all strategies are victorious. But the
difficult part, namely that these statements are beyond PA, is very
difficult at undergraduate level.

We decided he should not get into the hard part because it would
require too much work. However, there ought to be some easy
(artificial) examples that show how statements about rapidly-growing
functions are related to consistency of PA. I would be grateful if you
could suggest some such examples, as this is getting a bit out of my
area. Something that can be managed by a smart undergraduate student
would allow the student to nicely round up his presentation.

With kind regards,

Andrej Bauer