An application of graphical enumeration to PA

Journal of Symbolic Logic 68 (1):5-16 (2003)
  Copy   BIBTEX

Abstract

For α less than ε0 let $N\alpha$ be the number of occurrences of ω in the Cantor normal form of α. Further let $\mid n \mid$ denote the binary length of a natural number n, let $\mid n\mid_h$ denote the h-times iterated binary length of n and let inv(n) be the least h such that $\mid n\mid_h \leq 2$ . 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 \alpha_0, ..., \alpha_n\rangle$ of ordinals less than ε0 which satisfy the condition that the Norm $N\alpha_i$ of the i-th term αi is bounded by $K + \mid i \mid \cdot \mid i\mid_h$ . 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 \alpha_0,..., \alpha_n\rangle$ of ordinals less than ε0 which satisfies the condition that the Norm $N\alpha_i$ of the i-th term αi is bounded by $K + \mid i \mid\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 $\breve$ ek and Loebl we obtain similar characterizations for finite bad sequences of finite trees in terms of Otter's tree constant 2.9557652856...

Other Versions

No versions found

Similar books and articles

Analytics

Added to PP
2009-01-28

Downloads
160 (#260,841)

6 months
29 (#310,619)

Historical graph of downloads
How can I increase my downloads?

Citations of this work

Current Research on Gödel’s Incompleteness Theorems.Yong Cheng - 2021 - Bulletin of Symbolic Logic 27 (2):113-167.
Phase transitions for Gödel incompleteness.Andreas Weiermann - 2009 - Annals of Pure and Applied Logic 157 (2-3):281-296.
Pure Σ2-elementarity beyond the core.Gunnar Wilken - 2021 - Annals of Pure and Applied Logic 172 (9):103001.

View all 14 citations / Add more citations

References found in this work

Proof-theoretic investigations on Kruskal's theorem.Michael Rathjen & Andreas Weiermann - 1993 - Annals of Pure and Applied Logic 60 (1):49-88.
Elementary descent recursion and proof theory.Harvey Friedman & Michael Sheard - 1995 - Annals of Pure and Applied Logic 71 (1):1-45.
On the Slowly Well Orderedness of ɛo.Toshiyasu Arai - 2002 - Mathematical Logic Quarterly 48 (1):125-130.

Add more references