Weak comparability of well orderings and reverse mathematics (Q918549)

Two countable well orderings are called weakly comparable, if there is an order preserving injective mapping from one into the other. They are called strongly comparable, if the injection is an isomorphism between one of them and an initial segment of the other. CWO denotes the statement that any two countable well orderings are strongly comparable, WCWO is to be the weak comparability analogue. As Friedman announced and Simpson elaborated, CWO is equivalent to \(ATR_ 0\), a subsystem of second order arithmetic frequently used in reverse mathematics. Friedman also proved WCWO to be equivalent to \(ATR_ 0\). The aim of the paper under review is to provide a detailed exposition of this \(result.\) ATR\({}_ 0\) implying WCWO is a consequence of the equivalence of \(ATR_ 0\) and CWO, since CWO entails WCWO. To prove the converse, the equivalence of \(ATR_ 0\) and the \(\Sigma^ 1_ l\) separation principle \[ \neg \exists n(\phi (n)\wedge \psi (n))\Rightarrow \exists Z\forall n(\phi (n)\Rightarrow n\in Z)\wedge (\psi (n)\Rightarrow n\not\in Z) \] is used, \(\phi\) and \(\psi\) being \(\Sigma^ 1_ l\) formulas not containing Z free. To show this with WCWO, sequences of trees are associated to the formulas \(\phi\) and \(\psi\), the Kleene-Brouwer orderings of these trees are well orderings under the present conditions. Thus WCWO can be applied. The existence of Z follows from \(\Sigma^ 1_ l-AC_ 0\), which can be inferred from WCWO. In the next section the foregoing proof is analyzed in the spirit of Reverse Mathematics. It is stressed where WCWO is really applied and that for the other parts of the proof simpler means ae sufficient. Finally, differences between strong and weak comparability are elaborated which on the first glance seem to be suspended by the main result.