In this paper we calibrate the exact proof-theoretic strength of Kruskal's theorem, thereby giving, in some sense, the most elementary proof of Kruskal's theorem. Furthermore, these investigations give rise to ordinal analyses of restricted bar induction.

Simpson has claimed that “ATR0 is the weakest set of axioms which permits the development of a decent theory of countable ordinals” [8]. This paper provides empirical support for Simpson's claim. In particular, Cantor's Normal Form Theorem and Sherman's Inequality for countable well-orderings are both equivalent to ATR0. The proofs of these results require a substantial development of ordinal exponentiation and a strengthening of the comparability result in [3].

We show that the principle of ω model reflection for Π1n − 1 formulas is equivalent over ACA0 to the scheme of Π1n bar induction. This extends and refines previous results of Friedman and Simpson.

In this article we characterize a countable ordinal known as the big Veblen number in terms of natural well-partially ordered tree-like structures. To this end, we consider generalized trees where the immediate subtrees are grouped in pairs with address-like objects. Motivated by natural ordering properties, extracted from the standard notations for the big Veblen number, we investigate different choices for embeddability relations on the generalized trees. We observe that for addresses using one finite sequence only, the embeddability coincides with the (...) classical tree-embeddability, but in this article we are interested in more general situations. We prove that the maximal order type of some of these new embeddability relations hit precisely the big Veblen ordinal ϑΩΩ\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$${\vartheta \Omega^{\Omega}}$$\end{document}. Somewhat surprisingly, changing a little bit the well-partially ordered addresses, the maximal order type hits an ordinal which exceeds the big Veblen number by far, namely ϑΩΩΩ\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$${\vartheta \Omega^{\Omega^\Omega}}$$\end{document}. Our results contribute to the research program on classifying properties of natural well-orderings in terms of order-theoretic properties of the functions generating the orderings. (shrink)

A rank function for a directed graph G assigns elements of a well ordering to the vertices of G in a fashion that preserves the order induced by the edges. While topological sortings require a one-to-one matching of vertices and elements of the ordering, rank functions frequently must assign several vertices the same value. Theorems stating basic properties of rank functions vary significantly in logical strength. Using the techniques of reverse mathematics, we present results that require the subsystems ${\ensuremath{\vec{RCA}_0}}$ , (...) ${{\vec{ACA}_0}}$ , ${{\vec{ATR}_0}}$ , and ${{\vec{\Pi^1_1 - CA}_0}}$. (shrink)

For f: On → On let supp: = ξ: 0, and let S := {f : On → On : supp finite}. For f,g ϵ S definef ≤ g : ↔ [h one-to-one ⁁ f ≤ g)].A function ψ : S → On is called monotonic increasing, if f≤ψ and if f ≤ g implies ψ ≤ ψ. For a mapping ψ : S → On let Clψ be the least set T of ordinals which contains 0 as an element (...) and which is closed under the following rule: If f ϵ S, range ⊆ T and supp ⊆ T, then ψ ϵ T. Let φ be the enumeration function of the class {ξ: [ξ = ωn]}. Let φ be the induced Schütte-Klammerterm-function which generates the Schütte-Veblen-hierarchy of ordinals. Then φ is monotonic increasing. We show: If ψ: S → On is monotonic increasing, then otyp) ≤ min {ξ : ξ = Φ, where 1ξ = 1 if α = ξ and 1ξ = 0 if α ↔ = 0 if α ≠ ξ. For τ an ordinal let Sτ := {f ϵ S : supp ⊆ τ}. A function ψ : Sτ → On is called τ-monotonic increasing if fξ and if f ≤ g implies ψ ≤ . For a function ψ Sτ → On let Clψ ↔ τ be the least set T of ordinals, which contains 0 as an element, such that if f ϵ Sτ and range ϵ T, then ψ ϵ T. We show: if ≥2 and if ψ Sτ → On is τ-monotonic increasing, then otyp ↔ τ) ≤. We also prove a generalization of this theorem in terms of well-partial orderings. MSC: 03F15, 03E10, 06A06. (shrink)

Let $\Omega:= \aleph_1$ . For any $\alpha \Omega:\xi = \omega^\xi\}$ let EΩ (α) be the finite set of ε-numbers below Ω which are needed for the unique representation of α in Cantor-normal form using 0, Ω, +, and ω. Let $\alpha^\ast:= \max (E_\Omega(\alpha) \cup \{0\})$ . A function f: εΩ + 1 → Ω is called essentially increasing, if for any $\alpha < \varepsilon_{\Omega + 1}; f(\alpha) \geq \alpha^\ast: f$ is called essentially monotonic, if for any $\alpha,\beta < \varepsilon_{\Omega + (...) 1}$; $\alpha \leq \beta \wedge \alpha^\ast \leq \beta^\ast \Rightarrow f(\alpha) \leq f(\beta).$ Let Clf(0) be the least set of ordinals which contains 0 as an element and which satisfies the following two conditions: (a) $\alpha,\beta \epsilon \mathrm{Cl}_f(0) \Rightarrow \omega^\alpha + \beta \epsilon \mathrm{Cl}_f(0)$ , (b) $E_\Omega\alpha \subseteq \mathrm{Cl}_f(0) \Rightarrow f(\alpha) \epsilon \mathrm{Cl}_f(0)$ . Let ϑεΩ + 1 be the Howard-Bachmann ordinal, which is, for example, defined in [3]. The following theorem is shown: If f:εΩ + 1 → Ω is essentially monotonic and essentially increasing, then the order type of Clf(0) is less than or equal to ϑεΩ + 1. (shrink)