The maximal linear extension theorem in second order arithmetic (Q634769)

A linear extension of a partial order \(\mathcal P = ( P , \leq_P )\) is a linear ordering \(\mathcal L = ( P , \leq_L )\) on \(P\) such that \(x\leq_P y\) implies \(x \leq _L y\). A wpo (well-partial-order) is a well-founded partial order with no infinite antichains. Let MLE assert the existence of maximal linear extensions for wpos, formally, ``every wpo \(\mathcal P\) has a linear extension \(\mathcal Q\) such that \(\mathcal R \preceq \mathcal Q\) for all linear extensions \(\mathcal R\) of \(\mathcal P\).'' The statement MLE formalizes a result of \textit{D. H. J. de Jongh} and \textit{R. Parikh} [Nederl. Akad. Wet., Proc., Ser. A 80, 195--207 (1977; Zbl 0435.06004)]. The bulk of this paper consists of a proof that, working over the reverse mathematics base system RCA\(_0\), MLE is equivalent to ATR\(_0\). Capitalizing on this work, the authors also show that ATR\(_0\) is equivalent to a statement formalizing the existence of maximal chains. This statement, denoted by MC, asserts that ``every wpo \(\mathcal P\) has a chain \(\mathcal C\) such that \(\mathcal C^\prime \preceq \mathcal C\) for every chain \(\mathcal C^\prime\) of \(\mathcal P\).'' MC formalizes a consequence of a theorem of \textit{E. S. Wolk} [Fundam. Math. 60, 175--186 (1967; Zbl 0153.02601)].