# 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.

-
Transfinite induction up to a given ordinal can be added to FOL as an axiom scheme; certainly, enough induction to prove Goodstein's theorem can be added as an axiom. Therefore I expect that the answer to your question is certainly yes; if you're willing to do it really awkwardly, you could encode numbers in trees, then copy over all the axioms you'd need to prove Goodstein's theorem in an extension of PA. As for finding a more natural way, I don't see an easy way to do that using binary trees, but that doesn't mean there isn't one. –  Henry Towsner Oct 22 '10 at 1:36
The deeper reason for my question is that I consider a pair operator (which makes bin-trees possible) more natural than PA with addition and multiplication. I do not object against ordinal numbers, but I consider them even less natural. So, I am curious if simple logic (FOL) can be build up in a different way, using pairs and if this is even stronger, because it can prove Goodstein. –  Lucas K. Oct 28 '10 at 19:22

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”.

-

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.

-
Schoppenhauer, Very much thanks for the answer, but unfortunately this was not what I was looking for. I made an edit to the question. I hope it is more clear now. Once you have defined ordinals, you can add the axiom scheme as you suggested. This gives a FOL that is stronger than standard FOL + PA, because with ordinals you can prove Goodstein's theorem, while FOL + PA can not (according to reversed mathematics). But I don't want to add ordinals. Instead I want to add binary trees and an axiom scheme, in such way that it is as strong as the system with ordinals. –  Lucas K. Aug 12 '10 at 23:03