Pursuing the proof-theoretic program of Friedman and Simpson, we begin the study of the metamathematics of countable linear orderings by proving two main results. Over the weak base system consisting of arithmetic comprehension, II 1 1 -CA0 is equivalent to Hausdorff's theorem concerning the canonical decomposition of countable linear orderings into a sum over a dense or singleton set of scattered linear orderings. Over the same base system, ATR0 is equivalent to a version of the Continuum Hypothesis for linear orderings, (...) which states that every countable linear ordering either has countably many or continuum many Dedekind cuts. (shrink)

For several subsystems of second order arithmetic T we show that the proof-theoretic strength of T + (bar rule) can be characterized in terms of T + (bar induction) □ , where the latter scheme arises from the scheme of bar induction by restricting it to well-orderings with no parameters. In addition, we demonstrate that ACA + 0 , ACA 0 + (bar rule) and ACA 0 + (bar induction) □ prove the same Π 1 1 -sentences.

§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)

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)