There is a class of forcing notions I've been playing around with recently. They have a couple nice properties, and all have the same theme, but I've found them difficult to analyze beyond the basics. Before I spend too much time with them, I'd like to ask whether they (or things like them) have been studied before.
My interest in them is that they can be used to build interesting (hopefully) models in which the reverse-mathematical principle ADS (and related principles) fails; I've sketched this construction below the main question.
The basic forcing I'm considering is the following:
A nonempty tree $T\subseteq[0, 1]^{<\omega}$ with no dead ends is $\epsilon$-robust ($\epsilon>0$) if the following hold: $(i)$ if $\sigma\in T$ and $m<n<\vert\sigma\vert$ then $\sigma(m)\not=\sigma(n)$ (this isn't essential, but it cleans things up) and $(ii)$ for every $\sigma\in T$ above the stem of $T$ and every open set $U\subseteq [0, 1]$ with $m(U)<\epsilon$, there is a path $f$ through $T$ extending $\sigma$ such that $f(k)\not\in U$ for all $k\ge\vert\sigma\vert$. $T$ is robust if it is $\epsilon$-robust for some $\epsilon>0$.
Let $\mathbb{T}$ denote the poset of robust trees, ordered by inclusion. My question is:
Question. Is there already literature on $\mathbb{T}$, or related forcing notions?
Let me say a bit about what variations one might consider:
As an obvious first step, we can alter $\mathbb{T}$ by demanding that a condition $T$ be "nice" - e.g. for each $\sigma\in T$, the set of $r$ such that $\sigma^\smallfrown \langle r\rangle\in T$ is Borel, or (assuming large cardinals) that $T$ live in $L(\mathbb{R})$, or so on.
Another change would be to control the robustness, too: e.g. force with pairs $(T,\epsilon)$ where $T$ is $\epsilon$-robust and $(T,\epsilon)\le(S,\delta)$ iff $T\subseteq S$ and $\epsilon>\delta$
Finally, a more elaborate change we can make is to broaden the forcing notion by being more flexible about what "robust" means. Consider the following game $R(T, \epsilon)$ associated to a tree $T\subseteq[0, 1]^{<\omega}$ and an $\epsilon>0$:
Players $1$ and $2$ alternate moves, with player $1$ playing a strictly increasing sequence $\sigma_0\prec \sigma_1\prec\sigma_2\prec …$ of nodes of $T$ and player $2$ playing a strictly increasing sequence of open sets $U_0\subset U_1\subset U_2\subset …$.
On move $i+1$, player $1$ must not use any reals in the open set built by player $2$ so far: if $k\ge\vert \sigma_i\vert$ and $k<\vert\sigma_{i+1}\vert$, then $\sigma_{i+1}(k)\not\in U_i$.
For each $i$, the measure of $U_i$ is $<\epsilon$.
Player $1$ wins iff they always make a legal move.
Call a tree $T$ playfully $\epsilon$-robust if player $1$ has a winning strategy in $R(T,\epsilon)$; we can force with such trees instead of genuinely robust trees.
Alright, why do I care about these forcings? It turns out that we can use them to produce $\omega$-models of RCA$_0$ in which the reverse-mathematical principle ADS ("every infinite linear order has an infinite ascending or descending sequence") fails, and I'm interested in figuring out other properties of these models. So let me say a bit about how this works.
Forcing with $\mathbb{T}$ produces a generic sequence $G$ of elements of $[0, 1]$. We isolate a nice class of names for reals:
Let $\nu$ be a $\mathbb{T}$-name for a subset of $\omega$. We say $\nu$ is stable if for all $T_0,T_1\in\mathbb{T}$ with the same stem and every $k\in\omega$, we have $T_0\Vdash k\in\nu\iff T_1\Vdash k\in \nu$ and $T_0\Vdash k\not\in\nu\iff T_1\Vdash k\not\in \nu$.
This then lets us build an $\omega$-model of RCA$_0$ as follows:
Fix $G$ $\mathbb{T}$-generic over $V$. We set $\mathcal{M}_G=\{\nu[G]:\nu$ is stable$\}$, and conflate this with the corresponding $\omega$-model of RCA$_0$.
(That this is indeed an $\omega$-model is easy to check.)
It turns out that the models we get in this way never satisfy the ADS. The relation "$G(x)\le G(y)$" has a stable name and defines a linear order on $\omega$ in $\mathcal{M}_G$. However, $\mathcal{M}_G$ can have no infinite ascending or descending sequence for this ordering (call it "$\trianglelefteq$"). To see this, suppose $\nu$ were a stable name for a (WLOG) infinite descending sequence through $\trianglelefteq$, and that this is forced by some condition $T$. Let $$r=\inf\{s\in[0,1]: \exists T'\le T, n\in\omega(stem(T')(n)=s\mbox{ and }T'\Vdash n\in\nu) \}.$$ Pick $s\in [0, 1]$, $T'\le T$, and $n\in\omega$ such that the following hold: $\vert s-r\vert<\epsilon$, $stem(T')(n)=s$, and $T'\Vdash n\in\nu$. Letting $T'$ be $\epsilon$-robust, pick some open set $U$ of measure $\delta<\epsilon$ containing the interval $[r, s]$, and let $$\hat{T}=\{\sigma\in T: \forall k\ge\vert stem(T')\vert \mbox{ we have }\sigma(k)\not\in U\}.$$ $\hat{T}$ is $(\epsilon-\delta$)-robust, hence $\hat{T}\le T'$, and $T'$ forces that $\nu$ is not a name for an infinite descending sequence in $\trianglelefteq$.
(The variations on $\mathbb{T}$ described above also allow this same argument to go through. There are also simpler versions of $\mathbb{T}$ with the same basic property, but they seem less interesting.)
I'm trying to figure out whether these models may actually be interesting from a reverse-mathematical point of view. For this to be the case, we would need some nontrivial principle to hold in $\mathcal{M}_G$, e.g. WKL$_0$; however, I haven't been able to prove that such a phenomenon occurs. (To me these models are interesting on their own, but I'm particularly interested in their reverse-mathematical potential.) Hence this question.
