The maximal linear extension theorem in second order arithmetic

TL;DR

This paper establishes the logical equivalence of the maximal linear extension theorem for well partial orders and the maximal chain theorem to ATR_0 within second order arithmetic, clarifying their foundational strength.

Contribution

It proves the equivalence of these theorems to ATR_0 over RCA_0, providing new insights into their logical and foundational status.

Findings

Maximal linear extension theorem is equivalent to ATR_0 over RCA_0.

Maximal chain theorem is equivalent to ATR_0 over RCA_0.

Clarifies the logical strength of these theorems in second order arithmetic.

Abstract

We show that the maximal linear extension theorem for well partial orders is equivalent over RCA_0 to ATR_0. Analogously, the maximal chain theorem for well partial orders is equivalent to ATR_0 over RCA_0.