Can transfinite induction be defined as axiom scheme in FOL on bin-tree structures? 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.
 A: 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”.
A: Not sure whether I understand what exactly you mean. But transfinite induction is formally almost the same as "finite" induction, the only difference lies in the limit-ordinal-case. I.e. "finite" induction is $\varphi(0)\rightarrow\forall n(\varphi(n)\rightarrow\varphi(n+1))\rightarrow\forall n\varphi(n)$ while transfinite induction is $\varphi(0)\rightarrow\forall n(\varphi(n)\rightarrow\varphi(n+1))\rightarrow (n\in \mbox{Lim}\rightarrow\forall m \lt n (\varphi(m))\rightarrow\varphi(n))\rightarrow\forall n\varphi(n)$ (or just $\varphi(0)\rightarrow\forall n (\forall m\lt n(\varphi(m))\rightarrow\varphi(n))\rightarrow\forall n\varphi(n)$).
Of course, in higher order logic, you can quantify over $\varphi$. In first order logic, you will just put in infinitely many induction axioms, with $\varphi$ ranging over all formulas with one free variable. Thats why it is called "axiom scheme" rather than just "axiom", its a scheme to produce infinitely many axioms.
I hope I got your question right.
A: Assuming I understand your comment right, I don't know that binary trees are enough to get there, but arbitrary finite trees should certainly be.  One natural induction-esque principle on trees would be the Konig's lemmas; the weak version (WKL0) simply states that every infinite binary tree has an infinite path, while the strong version makes the same claim for an infinite tree where the nodes can have arbitrary (finite) degree.  According to Reverse Mathematics (or at least the Wikipedia page on it!), the 'proof ordinal' for WKL0 is just ωω, whereas that for ACA0 (which full Konig's lemma is equivalent to) is ε0.  So you may be able to derive a proof based on Konig's lemma, but it seems likely that binary trees may not have 'enough strength' to get you there.
A: Does the wiki article http://en.wikipedia.org/wiki/Structural_induction help?
