Processing math: 0%
An application of graphical enumeration to PA*
Weiermann, Andreas
J. Symbolic Logic, Tome 68 (2003) no. 1, p. 5-16 / Harvested from Project Euclid
For \al less than \eo let N\al be the number of occurrences of \om in the Cantor normal form of \al. Further let \lh n denote the binary length of a natural number n, let \lhh n denote the h-times iterated binary length of n and let \inv n be the least h such that \lhh n \leq2. We show that for any natural number h first order Peano arithmetic, \PA, does not prove the following sentence: For all K there exists an M which bounds the lengths n of all strictly descending sequences $\langle \al0,... ,\aln\rangle of ordinals less than \eo which satisfy the condition that the Norm N\ali of the i-th term \ali is bounded by K + \lh i\cdot \lhh{i}. ¶ As a supplement to this (refined Friedman style) independence result we further show that e.g., primitive recursive arithmetic, \PRA, proves that for all K there is an M which bounds the length n of any strictly descending sequence \langle \al0,... ,\aln\rangle of ordinals less than \eo which satisfies the condition that the Norm N\ali of the i-th term \ali is bounded by K + \lh i \cdot \inv i$. The proofs are based on results from proof theory and techniques from asymptotic analysis of Polya-style enumerations. ¶ Using results from Otter and from Matou{\v{s}}ek and Loebl we obtain similar characterizations for finite bad sequences of finite trees in terms of Otter's tree constant 2.9557652856... .
Publié le : 2003-03-14
Classification: 
@article{1045861503,
     author = {Weiermann, Andreas},
     title = {An application of graphical enumeration to PA<sup>*</sup>},
     journal = {J. Symbolic Logic},
     volume = {68},
     number = {1},
     year = {2003},
     pages = { 5-16},
     language = {en},
     url = {http://dml.mathdoc.fr/item/1045861503}
}
Weiermann, Andreas. An application of graphical enumeration to PA*. J. Symbolic Logic, Tome 68 (2003) no. 1, pp.  5-16. http://gdmltest.u-ga.fr/item/1045861503/