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

Edit: I think my question was not fully clear yet.

If you have the natural numbers with the ordinals, you can make an axiom scheme as schoppenhauer suggests in the answer.

However, this requires definitions of ordinal. If you encode the ordinals in the natural numbers (using FOL + PA + addition and multiplication), you can not proof that these numbers are well ordered (I assume this base on the results of reverse mathematics). You need second order logic for that. So, the only option here is to define the ordinals as is and not base it on PA.

If we do so, we have defined the ordinals and the axiom scheme of transfinite induction and with that we should be able to prove Goodstein's theorem.

But, I am not so font on ordinals. So, my question is if it is possible to make a kind of induction axiom scheme on binary trees (instead of ordinal numbers), that is stronger than normal induction. FOL + these binary trees + binary tree induction axiom scheme, should be capable of proving Goodstein theorem.

I would like this, because I consider a binary tree as a much more simpler concept than ordinals.

I think this should be possible, based on the observation of the Hydra games which are based on Goodstein.