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.

We show that each of Δ13-CA0 + Σ13-IND and Π12-CA0 + Π13-TI proves Δ03-Det and that neither Σ31-IND nor Π13-TI can be dropped. We also show that neither Δ13-CA0 + Σ1∞-IND nor Π12-CA0 + Π1∞-TI proves Σ03-Det. Moreover, we prove that none of Δ21-CA0, Σ31-IND and Π21-TI is provable in Δ11-Det0 = ACA0 + Δ11-Det.

We say that a linear ordering is extendible if every partial ordering that does not embed can be extended to a linear ordering which does not embed either. Jullien’s theorem is a complete classification of the countable extendible linear orderings. Fraïssé’s conjecture, which is actually a theorem, is the statement that says that the class of countable linear ordering, quasiordered by the relation of embeddability, contains no infinite descending chain and no infinite antichain. In this paper we study the strength (...) of these two theorems from the viewpoint of Reverse Mathematics and Effective Mathematics. As a result of our analysis we get that they are equivalent over the basic system of .We also prove that Fraïssé’s conjecture is equivalent, over , to two other interesting statements. One that says that the class of well founded labeled trees, with labels from {+,−}, and with a very natural order relation, is well quasiordered. The other statement says that every linear ordering which does not contain a copy of the rationals is equimorphic to a finite sum of indecomposable linear orderings.While studying the proof theoretic strength of Jullien’s theorem, we prove the extendibility of many linear orderings, including ω2 and η, using just . Moreover, for all these linear orderings, , we prove that any partial ordering, , which does not embed has a linearization, hyperarithmetic in , which does not embed. (shrink)

§1. Introduction. A linear ordering embedsinto another linear ordering if it is isomorphic to a subset of it. Two linear orderings are said to beequimorphicif they can be embedded in each other. This is an equivalence relation, and we call the equivalence classesequimorphism types. We analyze the structure of equimorphism types of linear orderings, which is partially ordered by the embeddability relation. Our analysis is mainly fromthe viewpoints of Computability Theory and Reverse Mathematics. But we also obtain results, as the (...) definition of equimorphism invariants for linear orderings, which provide a better understanding of the shape of this structure in general.This study of linear orderings started by analyzing the proof-theoretic strength of a theorem due to Jullien [Jul69]. As is often the case in Reverse Mathematics, to solve this problem it was necessary to develop a deeper understanding of the objects involved. This led to a variety of results on the structure of linear orderings and the embeddability relation on them. These results can be divided into three groups. (shrink)

Attempts to extend the classical Hausdorff difference hierarchy to the case of partitions of a space to k > 2 subsets lead to non‐equivalent notions. In a hope to identify the “right” extension we consider the extensions appeared in the literature so far: the limit‐, level‐, Boolean and Wadge hierarchies of k ‐partitions. The advantages and disadvantages of the four hierarchies are discussed. The main technical contribution of this paper is a complete characterization of the Wadge degrees of Δ02‐measurable k (...) ‐partitions of the Baire space. (© 2007 WILEY‐VCH Verlag GmbH & Co. KGaA, Weinheim). (shrink)

We show that each of $\Delta _{3}^{1}-{\rm CA}_{0}+\Sigma _{3}^{1}-{\rm IND}$ and $\Pi _{2}^{1}-{\rm CA}_{0}+\Pi _{3}^{1}-{\rm TI}$ proves $\Delta _{3}^{0}-{\rm Det}$ and that neither $\Sigma _{3}^{1}-{\rm IND}$ nor $\Pi _{3}^{1}-{\rm TI}$ can be dropped. We also show that neither $\Delta _{3}^{1}-{\rm CA}_{0}+\Sigma _{\infty}^{1}-{\rm IND}$ nor $\Pi _{2}^{1}-{\rm CA}_{0}+\Pi _{\infty}^{1}-{\rm TI}$ proves $\Sigma _{3}^{0}-{\rm Det}$. Moreover, we prove that none of $\Delta _{2}^{1}-{\rm CA}_{0}$, $\Sigma _{3}^{1}-{\rm IND}$ and $\Pi _{2}^{1}-{\rm TI}$ is provable in $\Delta _{1}^{1}-{\rm Det}_{0}={\rm ACA}_{0}+\Delta _{1}^{1}-{\rm Det}$.

We prove that the maximal order type of the wqo of linear orders of finite Hausdorff rank under embeddability is φ2, the first fixed point of the ε-function. We then show that Fraïssé’s conjecture restricted to linear orders of finite Hausdorff rank is provable in +“φ2 is well-ordered” and, over , implies +“φ2 is well-ordered”.