Transfinite induction requires a second order induction hypothesis. So, that can not be defined as axiom scheme in FOL. However, if I look to Goodstein's theorem en the Hydra games, then they have to do with tree structures. Suppose we have in FOL a binary tree. This has an element 0 and a predicate that makes a pair P(x,y). We have the expected definitions on these tree like structures. Now, is it possible to define an axiom scheme on this binary tree structure, that is strong enough for transfinite induction (to proof Goodstein's theorem)? Or, is a second order induction hypothesis always necessary, even when when we start to make schemes on tree structures? And why? Lucas