Computability-theoretic and proof-theoretic aspects of partial and linear orderings (Q1425651)

The authors examine the reverse mathematics and effective content of several variations of Szpilrajn's Theorem [\textit{E. Szpilrajn}, Fundam. Math. 16, 386--389 (1930; JFM 56.0843.02)]. A linear order type \(\tau\) is called {extendible} if every partial order containing no subchains of type \(\tau\) can be extended to a linear ordering containing no subchains of type \(\tau\). The main results of the paper are: (1) ``\(\omega ^*\) is extendible'' is provable in ACA\(_0\) and strictly stronger than WKL\(_0\); (2) ``\(\eta\) is extendible'' is provable in \(\Pi^1_1\)-CA\(_0\), but not in WKL\(_0\); and (3) ``\(\zeta\) is extendible'' is equivalent to ATR\(_0\). Here \(\omega^*\) is \(\omega\) with the reverse order, \(\eta\) is the order type of the rationals, and \(\zeta\) is the order type of the integers. For a survey of linear extensions of partial orderings, see \textit{R. Bonnet} and \textit{M. Pouzet}'s paper ``Linear extensions of ordered sets'' [in: I. Rival (ed.), Ordered sets, Proc. NATO Adv. Study Inst., Banff/Can. 1981, 125--170 (1982; Zbl 0499.06002)]. For background on computability-theoretic aspects of linear orderings, see \textit{R. G. Downey}'s paper ``Computability theory and linear orderings'' [in: Yu. L. Ershov et al. (eds.), Handbook of recursive mathematics. Vol. 2. Recursive algebra, analysis and combinatorics. Amsterdam: Elsevier. Stud. Logic Found. Math. 139, 823--976 (1998; Zbl 0941.03045)].