Finding limit-nondecreasing sets for certain functions This is a question that arose a while ago in work with Damir Dzhafarov on some pieces of reverse mathematics. As far as I know, it has no deep significance; however, it feels like the sort of thing we ought to know. The solution is probably very simple, but I don't see it.
Fix a computable total function $f$ of two variables such that $$f(x, s)\ge f(x, s+1),$$ and let $$F(x)=\lim_{s\rightarrow\infty}f(x, s).$$ Then there is an infinite set $X\subseteq\omega$ satisfying $$i, j\in X, i<j\implies F(i)\le F(j).$$ Call such an $X$ $f$-good. My question is:

How complicated must such an $X$ be?

Specifically,

Is there an $f$ as above such that any $f$-good $X$ computes $0'$?

Note that trivially, $0'$ will always compute such an $X$, so this is the upper bound. 
It's easy to show that there are not always computable such $X$ - indeed, there are $f$ such that any $f$-good $X$ computes a DNR function. However, coding $0'$ seems very difficult, because the "current guess" to whether $F(i)\le F(j)$ can only change a (bounded) finite number of times. (Note that by contrast, if we look at $f$ satisfying $f(x, s)\le f(x, s+1)$, then it is very easy to code $0'$.)

EDIT: We can ask an even weaker question:

Suppose $d$ computes an $f$-good $X$ for every computable $f$. Must $d\ge_T0'$?

This ought to be easier to show, but I am at a loss. I can't even show that if $Y$ is such that for every computable $f$ there is some $n$ such that $Y\setminus n$ is $f$-good, then $Y$ computes $0'$!
 A: You're right. This is the kind of things we ought to know.
Let $\mathsf{LNS}$ be the statement that every such function f has an f-good set.
Results
I claim that $\mathsf{LNS}$ admits 


*

*cone avoidance (if A is non-computable, then any computable instance of $\mathsf{LNS}$ has a solution X such that A is not X-computable)

*preservation of hyperimmunity (if $A_0, A_1, \dots$ are countably many hyperimmune sets, then every computable instance of $\mathsf{LNS}$ has a solution X such that the $A$'s are hyperimmune relative to $X$).


Therefore, $\mathsf{LNS}$ implies neither $\mathsf{ACA}_0$, nor $\mathsf{ADS}$.
Combinatorics
Fix a computable instance $f : \mathbb{N} \times \mathbb{N} \to \mathbb{N}$,
let $f_0 : \mathbb{N} \to \mathbb{N}$ and $\tilde{f} : \mathbb{N} \to \mathbb{N}$
be the functions defined by $f_0(x) = f(x, 0)$ and $\tilde{f}(x) = \lim_s f(x, s)$, respectively.
Note that $f_0$ is computable, while $\tilde{f}$ is not.
If there is some $i$ such that $\tilde{f}(x) = i$ for infinitely many $x$,
then pick the least such $i$, and notice that the set $\{ x : \tilde{f}(x) = i \}$
is c.e. and every infinite computable subset of it is $f$-good.
So from now on, we will assume that for every $i$ and almost every $x$, $\tilde{f}(x) > i$.
We will build an $f$-good set by forcing, using a variant of Mathias forcing $(F, X)$, where


*

*$F$ is a finite set over which $\tilde{f}$ is non-decreasing.

*$X$ is an infinite set such that $\max F < \min X$.

*for every $x \in F$ and $y \in X$, $\tilde{f}(x) \leq \tilde{f}(y)$.


In particular, $(\emptyset, \omega)$ is a valid condition,
and given a condition $(F, X)$ and a finite set $H \subseteq X$ which is non-decreasing for $\tilde{f}$,
$(F \cup H, X \setminus [0, n])$ is a valid extension for some $n \in \mathbb{N}$.
We now want to decide a $\Sigma^0_1$ formula $\varphi(G)$ given a condition $(F, X)$.
Let $\mathcal{C}$ be the $\Pi^{0,X}_1$ class of all functions $h : \mathbb{N} \to \mathbb{N}$ dominated by $f_0$,
such that $\varphi(F \cup H)$ does not hold for every finite set $H \subset X$ over which $h$ is non-decreasing.
There are two cases.


*

*Case 1: $\mathcal{C}$ is empty. In this case, since $\tilde{f} \not \in \mathcal{C}$,
there is a finite set $H \subseteq X$ such that $\varphi(F \cup H)$ holds and over which $\tilde{f}$ is non-decreasing.
The condition $(F \cup H, X \setminus [0, n])$ for some sufficiently large $n$ is a valid extension forcing $\varphi(G)$ to hold.

*Case 2: $\mathcal{C}$ is non-empty. By weak K\"onig's lemma, pick an $h \in \mathcal{C}$
and $h \oplus X$-computably thin-out the set $X$ to obtain an infinite set $Y$ over which $h$ is non-decreasing.
The condition $(F, Y)$ forces $\varphi(G)$ not to hold.
An example
Suppose for example that we want to prove that $\mathsf{LNS}$ admits cone avoidance.
Let $A$ be a non-computable set and $f$ be a computable instance of $\mathsf{LNS}$.
We work with conditions $(F, X)$ as above, with the extra property that $A \not \leq_T X$.
Given a condition $(F, X)$ and a $\{0,1\}$-valued Turing functional $\Gamma$,
I claim there is an extension forcing $\Gamma^G \neq A$. 
To see this, for each $n \in \mathsf{N}$ and $i \in \{0,1\}$, let $\mathcal{C}_{n, i}$  be the $\Pi^{0,X}_1$ class 
of all functions $h : \mathbb{N} \to \mathbb{N}$ dominated by $f_0$,
such that $\Gamma^{F \cup H}(n) \uparrow$ or $\Gamma^{F \cup H}(n) \downarrow \neq i$
for every finite set $H \subset X$ over which $h$ is non-decreasing.
Consider the $X$-c.e. set $S = \{ (n, i) : \mathcal{C}_{n,i} = \emptyset \}$.
We have three cases.


*

*Case 1: $(n, 1-A(n)) \in S$ for some $n$. In this case, since $\mathcal{C}_{n,1-A(n)} = \emptyset$,
there is a finite set $H \subseteq X$ such that $\Gamma^{F \cup H}(n) \downarrow = 1-A(n)$ and over which $\tilde{f}$
is non-decreasing. The condition $(F \cup H, X \setminus [0, n])$ for some sufficiently large $n$
forces $\Gamma^G(n) \neq A(n)$.

*Case 2: $(n, 0)$ and $(n, 1) \not \in S$ for some $n$. In this case, by the cone avoidance basis theorem,
there are two functions $h_0 \in \mathcal{C}_{n,0}$, $h_1 \in \mathcal{C}_{n,1}$ such that
$A \not \leq_T h_0 \oplus h_1 \oplus X$. By $h_0 \oplus h_1 \oplus X$-computably thinning-out
the set $X$, we obtain a set $Y$ over which both $h_0$ and $h_1$ are non-decreasing.
The condition $(F, Y)$ forces $\Gamma^G(n) \neq 0$ and $\Gamma^G(n) \neq 1$, so forces $\Gamma^G(n) \uparrow$.

*Case 3: $S = \{ (n, A(n)) : n \in \mathbb{N} \}$. In this case, we can $X$-compute $A$, contradiction.
This completes the proof of cone avoidance.

EDIT: Note that one can easily use cone avoidance of $\mathsf{LNS}$ as a blackbox to build for any non-computable set $A$ a set $X$ such that $A \not \leq_T X$ and for every computable $f$, there is some $n$ such that $X \setminus [0, n]$ is $f$-good.
Indeed, fix the set $A$, and consider Mathias conditions $(F, X)$ such that $A \not \leq_T X$. For every such condition $(F, X)$ and every computable function $f$, one can apply cone avoidance of $\mathsf{LNS}$ to obtain an $f$-good set~$Y \subseteq X$ such that $A \not \leq_T Y$. The condition $(F, Y)$ forces $G$ to be $f$-good up to finite changes. Moreover, for every condition $(F, X)$ and every $e$, there is an extension $(H, Y)$ forcing $\Phi_e^G \neq A$. Every sufficiently generic for this notion of forcing yields the desired set.
