# First order consequence of a combinatorial principle

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

-
To clarify, what is the question? Are you looking for a characterization of models in which the domination principle holds? Or examples of non-standard models where the domination principle holds? Or an answer to your hypothesis about the ordinal that the first-order theory is isomorphic to (is this meant to be a characterization?)? (I don't know the answer to any of these, but I want to make sure your question is clear to others who may know.) – Jason Rute May 16 '13 at 17:03
@Jason: Sorry for its being poorly phrased. I am actually looking for some non-standard model in which RCA_0 and Domination principle hold. My guess of the universe being a regular cardinal is not a characterization for sure because one could easily produce a counter-example. To be exact, I would love some examples of non-standard models in which the principle holds. – Jing Zhang May 16 '13 at 17:12
Any nonstandard universe will be ill-founded, so not any kind of ordinal at all. "Regularity" can sort of be made sense of, through Bounding schemes; is that in fact what you mean? – Noah Schweber May 16 '13 at 17:29
Indeed. That was poorly phrased. I was thinking about the confinality in the ordinal (in order to define a dominating function if any). In this case, it is indeed bounding schemes that may be helpful. – Jing Zhang May 16 '13 at 17:36
Should the property be as follows: $\forall X \exists g \forall f \leq_T X(g \text{ dominates } f)$? $\exists g \forall X \forall f \leq_T X(g \text{ dominates } f)$ is impossible, as $g$ can not dominate $g+1$. – Wei Wang May 17 '13 at 0:39

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.

-
@François: Thanks! Can I just have it clarified what it means to say $g\geq f$ in the definition of poset? Since I am interested in the non-standard universe, do you think the same argument goes through (it occurs to me so). – Jing Zhang May 18 '13 at 10:21
By $g \geq f$, I mean $g(x) \geq f(x)$ for all $x$. I never assumed that the universe was standard, so this works as is in non-standard universes. In particular, this shows that the domination principle does not imply $\Sigma^0_2$-bounding. – François G. Dorais May 18 '13 at 11:37
What is the forcing language here (sorry for getting into messy details)? For example, what is $(s,j)\Vdash \bar{n}\in X$? In the normal context of strings, $\sigma\Vdash \bar{n}\in X \leftrightarrow \sigma(n)=1$ (I got from Odifreddi's book). In addition, my intention was to preserve the first-order universe so that $B\Sigma_2^0$ is still false. But I am not sure whether the forcing mentioned here would alter the first order universe. Thanks! – Jing Zhang May 19 '13 at 8:20
I don't think different approaches to forcing disagree in this case and none of them add new natural numbers. You can use the computability theoretic approach if you want to. In that case the only actual name in the forcing language is the name for the generic function $g$. Then $(s,j) \Vdash g(x) = y$ holds iff $x < |s|$ and $s(x) = y$ and the rest follows the usual inductive definition of forcing. Note that some things are different from Cohen forcing, for example $(s,j) \Vdash g(x) \geq y$ iff $\varphi_j(x) \geq y$ since there is no extension of $(s,j)$ that forces $g(x) = z$ where $z < y$. – François G. Dorais May 19 '13 at 14:24