http://math.andrej.com/2008/02/02/the-hydra-game/

My question actually is this: can Goodstein sequence to be proven to stop in a lambda calculus? Naively, it should be.

And another question: can set theory be modeled in lambda? (Or should I reread Dana Scott's works?)