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.
Best Answer
I’m struggling to figure out what is it that you actually want. You can consider induction on an arbitrary well-founded relation instead of an ordinal (and only on well-founded relations, as induction actually implies that the relation is well-founded). (This covers all the various special cases like transfinite induction, structural induction, $\in$-induction, and whatnot.) If the relation is reasonably encoded, its induction scheme should have the same proof-theoretic strength as induction on the ordinal which is the rank of the relation. Thus, the only thing you can achieve is to have ordinals represented nonuniquely by elements of a fancy, more complicated structure. As a matter of fact, this is what you do anyway, since e.g. in the usual representation of ordinals below $\varepsilon_0$ in arithmetic using Cantor normal form, ordinals are identified with certain trees. So the answer to your question appears to be “yes, just call them trees instead of ordinals”.