2
$\begingroup$

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.

Improve this question
$\endgroup$
2
  • 1
    $\begingroup$ 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. $\endgroup$
    – Henry Towsner
    Commented Oct 22, 2010 at 1:36
  • $\begingroup$ 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. $\endgroup$
    – Lucas K.
    Commented Oct 28, 2010 at 19:22

4 Answers 4

Reset to default
2
$\begingroup$

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

Improve this answer
$\endgroup$
0
$\begingroup$

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.

Improve this answer
$\endgroup$
1
  • $\begingroup$ 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. $\endgroup$
    – Lucas K.
    Commented Aug 12, 2010 at 23:03
0
$\begingroup$

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.

Improve this answer
$\endgroup$
2
  • $\begingroup$ Thanks for the answer. The problem is that Koning's lemma can not expressed as axiom scheme in FOL (at least I don't know how). Currently I am investigating how FOL + PA + addition and multiplication is build up. It is quite complicated to construct a pair operator. I have some doubt with this construction. It looks like that some simple proofs with pairs are not possible, but that is I have further to investigate. Reverse Mathematics looks at second order logic. Good sources about FOL + PA, are rather rare (most theorems are about FOL without PA). $\endgroup$
    – Lucas K.
    Commented Oct 11, 2010 at 20:44
  • $\begingroup$ The difference between König's lemma and its weak form is not whether nodes can have any finite number of children or only two. Weak König's lemma requires the nodes, regarded as finite sequences of integers, to have explicit, a priori bounds on the integers involved. I believe that one can design an infinite recursive subtree T of the tree of finite sequences of integers such that each node has at most two children in T, yet any path through T encodes the solution of the halting problem. The difference from WKL is that there is no recursive bound on the integers occurring in nodes of T. $\endgroup$
    – Andreas Blass
    Commented Dec 31, 2010 at 15:59
0
$\begingroup$

Does the wiki article http://en.wikipedia.org/wiki/Structural_induction help?

Improve this answer
$\endgroup$
1
  • $\begingroup$ Then the question is, whether Goodstein's theorem can be proven with structural induction. I doubt that. It would mean that FOL + PA + SI (structural induction) can proof Goodstein, while current theorems say that you need second order logic. $\endgroup$
    – Lucas K.
    Commented Dec 18, 2010 at 22:46

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .