Timeline for Can transfinite induction be defined as axiom scheme in FOL on bin-tree structures?
Current License: CC BY-SA 2.5
3 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Dec 31, 2010 at 15:59 | comment | added | Andreas Blass | 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. | |
| Oct 11, 2010 at 20:44 | comment | added | Lucas K. | 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). | |
| Oct 8, 2010 at 0:48 | history | answered | Steven Stadnicki | CC BY-SA 2.5 |