(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.



First order consequence of a combinatorial principle
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$-CA0 containing ACA0. The index-based variant $\D\_X$ is not so devastating since it is equivalent to Cohen forcing over any model of ACA0.


