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

From MaRDI portal
scientific article
Language Label Description Also known as
English
The maximal linear extension theorem in second order arithmetic
scientific article

    Statements

    The maximal linear extension theorem in second order arithmetic (English)
    0 references
    0 references
    0 references
    16 August 2011
    0 references
    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)].
    0 references
    reverse mathematics
    0 references
    well-quasi-order
    0 references
    wqo
    0 references
    maximal linear extension
    0 references
    MLE
    0 references
    maximal chain
    0 references
    MC
    0 references
    ATR
    0 references

    Identifiers

    0 references
    0 references
    0 references
    0 references
    0 references
    0 references