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... (shrink)

We define a class of functions, the descent recursive functions, relative to an arbitrary elementary recursive system of ordinal notations. By means of these functions, we provide a general technique for measuring the proof-theoretic strength of a variety of systems of first-order arithmetic. We characterize the provable well-orderings and provably recursive functions of these systems, and derive various conservation and equiconsistency results.

For α < ε0, Nα denotes the number of occurrences of ω in the Cantor normal form of α with the base ω. For a binary number-theoretic function f let B denote the length n of the longest descending chain of ordinals <ε0 such that for all i < n, Nαi ≤ f . Simpson [2] called ε0 as slowly well ordered when B is totally defined for f = K · . Let |n| denote the binary length of the (...) natural number n, and |n|k the k-times iterate of the logarithmic function |n|. For a unary function h let L denote the function B ) with h0 = K + |i| · |i|h. In this note we show, inspired from Weiermann [4], that, under a reasonable condition on h, the functionL is primitive recursive in the inverse h–1 and vice versa. (shrink)

It is well known that the Ackermann function can be defined via diagonalization from an iteration hierarchy which is built on a start function like the successor function. In this paper we study for a given start function g iteration hierarchies with a sub-linear modulus h of iteration. In terms of g and h we classify the phase transition for the resulting diagonal function from being primitive recursive to being Ackermannian.

We give a self-contained and streamlined version of the classification of the provably computable functions of PA. The emphasis is put on illuminating as well as seems possible the intrinsic computational character of the standard cut elimination process. The article is intended to be suitable for teaching purposes and just requires basic familiarity with PA and the ordinals below ε0. (Familiarity with a cut elimination theorem for a Gentzen or Tait calculus is helpful but not presupposed).

Dynamic ordinal analysis is ordinal analysis for weak arithmetics like fragments of bounded arithmetic. In this paper we will define dynamic ordinals – they will be sets of number theoretic functions measuring the amount of sΠ b 1(X) order induction available in a theory. We will compare order induction to successor induction over weak theories. We will compute dynamic ordinals of the bounded arithmetic theories sΣ b n (X)−L m IND for m=n and m=n+1, n≥0. Different dynamic ordinals lead to (...) separation. In this way we will obtain several separation results between these relativized theories. We will generalize our results to further languages extending the language of bounded arithmetic. (shrink)

This paper is intended to give for a general mathematical audience a survey of intriguing connections between analytic combinatorics and logic. We define the ordinals below ε0 in non-logical terms and we survey a selection of recent results about the analytic combinatorics of these ordinals. Using a versatile and flexible compression technique we give applications to phase transitions for independence results, Hilbert’s basis theorem, local number theory, Ramsey theory, Hydra games, and Goodstein sequences. We discuss briefly universality and renormalization issues (...) in this context. Finally, we indicate how regularity properties of ordinal count functions can be used to prove logical limit laws. (shrink)

We classify the phase transition thresholds from provability to unprovability for certain Friedman-style miniaturizations of Kruskal's Theorem and Higman's Lemma. In addition we prove a new and unexpected phase transition result for ε0. Motivated by renormalization and universality issues from statistical physics we finally state a universality hypothesis.

We survey a selection of results about majorization hierarchies. The main focus is on classical and recent results about the comparison between the slow and fast growing hierarchies.

Continuing the earlier research from [T. Bigorajska, H. Kotlarski, Partitioning α-large sets: some lower bounds, Trans. Amer. Math. Soc. 358 4981–5001] we show that for the price of multiplying the number of parts by 3 we may construct partitions all of whose homogeneous sets are much smaller than in [T. Bigorajska, H. Kotlarski, Partitioning α-large sets: some lower bounds, Trans. Amer. Math. Soc. 358 4981–5001]. We also show that the Paris–Harrington independent statement remains unprovable if the number of colors is (...) restricted to 2, in fact, the statement is unprovable in IΣb. Other results concern some lower bounds for partitions of pairs. (shrink)