First order consequence of a combinatorial principle

Question

(Base theory $RCA_0$)The principle says there exists a function g such that g dominates any X-recursive function for any X in the model. i.e. For any $f\le_T X$, $\exists b\in M$ such that $g(a)>f(a) \forall a>b$. Here the second order structure (countable) is $\langle M,S_M,+_M,\cdot_M,0_M,1_M \rangle$.

In the context of $\omega$ models, models satisfying such principle could be characterized by closure of high sets with respect to the existing sets in the model by Martin's characterization of high sets. I am curious about the first-order consequence of this principle?

EDIT: (some update) I was trying to separate the domination principle from $B\Sigma_2^0$. Starting from a countable first order model of arithmetic $M$ such that $\neg B\Sigma_2^0 + I\Sigma_1^0$ holds, I was trying to add into the second order part the dominating functions. Dominating functions exist by $B\Sigma_1^0$. However, I need to prove that after augmenting the model with a dominating function $f$, $M[f]$ preserves $I\Sigma_1^0$. I found some similar forcing arguments on trees (Lemma IX.2.4) in Simpson's book and the augmented set is one generic set. However, I am not sure how to impose the special requirement (i.e. dominating property) on the choice of the generic set.

Answer 1

The simplest forcing to add a dominating function is Hechler forcing $\newcommand{\D}{\mathbb{D}}\D$. In set-theoretic circles, conditions in $\D$ are pairs $(s,f)$ where $s$ is a finite sequence of natural numbers and $\newcommand{\N}{\mathbb{N}}f:\N\to\N$, extension is defined by $(s,f) \leq_{\D} (t,g)$ if $t \supseteq s$, $g \geq f$, and $t(n) \geq f(n)$ for $|s| \leq n \lt |t|$. A $\D$-generic filter $G$ defines a function $g = \bigcup \lbrace s : (s,f) \in G\rbrace$ which eventually dominates every ground model function.

Since the statement you're trying to force is localized in the sense that you only want $g$ to dominate all total $X$-computable functions, you can get away with an index-based variant of Hechler forcing. In that case, conditions of $\D_X$ are pairs $(s,i)$ where $s$ is a (coded) finite sequence of natural numbers and $i$ is an index for a total $X$-computable function $\varphi_i^X$, extension is defined by $(s,i) \leq_{\D_X} (t,j)$ if $(s,\varphi_i^X) \leq_{\D} (t,\varphi_j^X)$ in the sense described above. A $\D_X$-generic filter defines a function $g$ as above which eventually dominates every total $X$-computable function.

Note that we cannot expect $\D_X$ conditions to form a set since "$\varphi_i^X$ is total" is a $\Pi^0_2(X)$-complete statement. This is not a major problem since generics are constructed externally and we understand what "$\varphi_i^X$ is total" means from outside the ground model. Note that if the set of conditions exists in the ground model, then $\D_X$ is just a variation on Cohen forcing. However, in general, the ground model will have a very different perception of $\D_X$ and the generic will be quite different from a plain Cohen generic set.

To see that $\D_X$ preserves $\Sigma^0_1$-induction, first show that if some extension $(t,j) \leq_{\D_X} (s,i)$ forces a $\Sigma^0_1$-statement (which may use a fixed ground model set parameter in addition to the generic function $g$) then there is another extension $(u,i) \geq (s,i)$ that also forces the same $\Sigma^0_1$-statement. It follows from this that if $A(x)$ is a $\Sigma^0_1$ statement in the forcing language, then the set $$\lbrace x \in \N : (s,i) \nVdash \lnot A(x)\rbrace$$ is actually $\Sigma^0_1$-definable over the ground model. By $\Sigma^0_1$-induction in the ground model, this set has a minimal element $x_0$ and there is an extension $(t,j) \geq (s,i)$ (even with $j = i$) such that $$(t,j) \Vdash A(x_0) \land (\forall x \lt x_0)\lnot A(x).$$ This shows that it is dense to either force $\forall x \lnot A(x)$ or to force that there is a minimal $x$ that satisfies $A(x)$. Therefore, forcing with $\D_X$ preserves $\Sigma_1$-induction.

The use of the indexed variant $\D_X$ instead of the full second-order forcing $\D$ is very useful here since $\D$ can be quite devastating to weak subsystems of second-order arithmetic. Indeed, if the ground model satisfies arithmetic comprehension, then every $\Pi^1_1$ statement becomes $\Sigma^0_2$ in the generic extension. So forcing with $\D$ will not preserve systems weaker than $\Pi^1_1$-CA₀ containing ACA₀. The index-based variant $\D_X$ is not so devastating since it is equivalent to Cohen forcing over any model of ACA₀.