The reverse mathematics of non-decreasing subsequences (Q2402955)

This article analyzes the logical strength of two principles called \(\mathsf{LNS}\) (for \textit{limit non-decreasing subsequence}) and \(\mathsf{CNS}\) (for \textit{computably bounded non-decreasing subsequence}) in the context of reverse mathematics. These principles are both variations of the statement ``every function \(f : \mathbb{N} \rightarrow \mathbb{N}\) admits an infinite non-decreasing subsequence.'' The principle \(\mathsf{LNS}\) states that if a function \(f : \mathbb{N} \times \mathbb{N} \rightarrow \mathbb{N}\) satisfies \(f(n,s+1) \leq f(n,s)\) for every \(n,s \in \mathbb{N}\), then the limiting function \(\tilde{f}(n) = \lim_s f(n,s)\) admits an infinite non-decreasing sequence. The principle \(\mathsf{CNS}\) states that if \(f : \mathbb{N} \times \mathbb{N} \rightarrow \mathbb{N}\) and \(g : \mathbb{N} \rightarrow \mathbb{N}\) are functions where \(\lim_s f(n,s)\) exists and is \(\leq g(n)\) for every \(n \in \mathbb{N}\), then the limiting function \(\tilde{f}(n) = \lim_s f(n,s)\) admits an infinite non-decreasing sequence. The principles \(\mathsf{LNS}\) and \(\mathsf{CNS}\) are compared to well-known combinatorial principles related to König's lemma and Ramsey's theorem over the base system \(\mathsf{RCA}_0\). Together, the following main results show that \(\mathsf{LNS}\) and \(\mathsf{CNS}\) have interesting positions in the zoo of combinatorial principles below \(\mathsf{ACA}_0\). \(\mathsf{CNS}\) is strictly stronger than \(\mathsf{LNS}\). Indeed, the conjunction of \(\mathsf{LNS}\), the Erdős-Moser principle (stating that every countably infinite tournament has an infinite transitive subtournament), and weak König's lemma (which is König's lemma restricted to infinite \(\{0,1\}\)-branching trees) does not suffice to prove \(\mathsf{CNS}\). \(\mathsf{CNS}\) (and therefore \(\mathsf{LNS}\)) does not imply weak weak König's lemma (which is König's lemma restricted to \(\{0,1\}\)-branching trees of positive measure). The conjunction of Ramsey's theorem for pairs and weak König's lemma does not prove \(\mathsf{CNS}\). As with Ramsey's theorem for pairs, every computable instance of \(\mathsf{CNS}\) admits a low\(_2\) solution. The following questions are raised. Does \(\mathsf{CNS}\) imply Ramsey's theorem for pairs? It is shown that \(\mathsf{CNS}\) at least implies stable Ramsey's theorem for pairs. Does Ramsey's theorem for pairs imply \(\mathsf{LNS}\)?