Forcing Computable Functions

Question

I was wondering about the following issue and could not see how to address it. Let $Comp_V(\omega)$ be the set of all computable funtions over $\omega$ in some universe $V$ of ZFC. Is it possible to find a forcing extension $V[G]$ such that $ Comp_{V[G]}\nsubseteq Comp_V(\omega)$? Or is it the case that recursive functions are absolute?

Answer 1

Computable(/recursive) functions, and indeed much more, are unaffected by forcing. This is immediate from the fact that $\omega^V=\omega^{V[G]}$: anything definable purely in terms of natural numbers can't vary between models of set theory which don't disagree about the natural numbers.

(To phrase this as a precise result: Kleene's $T$-predicate is absolute.)

In fact absoluteness extends well beyond the arithmetical. The standard highlight here is Shoenfield absoluteness, which rules out anything interesting happening at or below the level of $\Pi^1_2$ properties. But this is massive overkill here.

Answer 2

No, it’s not possible. Or rather, the set $\{n \in \omega \mid $ according to $V[G]$, $n$ is a total computable function$\}$ is identical to the actual set of total computable functions. I’m not familiar enough with the notation to know whether I’m saying the same thing.

I have only seen the topos-theoretic version of forcing, but it’s straightforward to prove the following (assuming classical logic in the meta theory):

Thm. Let $S$ be a sentence in 1st-order arithmetic, and let $G$ be a cocomplete topos. If $\mathbb{N} \models S$, then $G \Vdash \mathbb{N} \models S$, and if $\mathbb{N} \nvDash S$, then $G \Vdash \mathbb{N} \models \neg S$.

Proof: we proceed by structural induction on $S$. The only atomic proposition we have to worry about is equality, which is trivial. The $\neg$, $\land$, $\lor$, and $\implies$ cases are also trivial when we take advantage of the law of excluded middle in the metatheory.

The trick here is the inductive step with $\exists$. If $\mathbb{N} \models \exists x . P(x)$, then there is some term $t$ such that $\mathbb{N} \models P(t)$. By the inductive hypothesis, $\mathbb{N} \models P(t)$ holds in $G$, and therefore $\mathbb{N} \models \exists x . P(x)$ also holds in $G$.

Conversely, suppose $\mathbb{N} \nvDash \exists x . P(x)$. [This is the one part of the proof which will be different in set-theoretic forcing]. Then for all terms $t$, we have $\mathbb{N} \nvDash P(t)$.

Consider in the Grothendieck topos the subobject $K = \{x \in \mathbb{N} \mid P(x)\}$. Note that for all global natural numbers $n$, we have $K \cap \{n\} = 0$ by the inductive hypothesis. Now $\bigcup\limits_{n \in \mathbb{N}} \{n\}$ is the natural numbers object in $G$ (the union being taken over the external $\mathbb{N}$). Since intersections commute with arbitrary unions, we have $K \cap \bigcup\limits_{n \in \mathbb{N}} \{n\} = \bigcup\limits_{n \in \mathbb{N}} K \cap \{n\} = \bigcup\limits_{n \in \mathbb{N}} 0 = 0$. Therefore, $\mathbb{N} \models \neg \exists x . P(x)$ holds in the internal logic of $G$.

Finally, for the universal case ($S = \forall x . P(x)$). The trick here is that for all $x$, we have either $\mathbb{N} \models P(x)$ or $\mathbb{N} \nvDash P(x)$. Thus, we can show in the topos's internal logic that $\mathbb{N} \models \forall x . P(x) \lor \neg P(x)$. Thus, in the topos's internal logic, we have $\mathbb{N} \models (\forall x . P(x)) \iff (\neg \exists x . \neg P(x))$. So we can rely on our existential quantifier and negation cases which we've already proved.

$\square$

Grothendieck toposes are a special case of co-complete toposes which encompass not only forcing models but also encompass symmetric submodels and permutation models. So these also can’t say anything new about the arithmetic of the natural numbers.

Interestingly, the models obtained from cocomplete toposes are always models of IZF but can fail to be models of the Law of Excluded Middle. To make a model of ZF(C), we typically need to use the double-negation topology, which is where the dense set part of forcing comes in. But even though they don't necessarily model excluded middle, they still model all instances of excluded middle in 1st-order arithmetic, which they inherit from the metatheory. This is a rather fascinating fact, and it indicates that we can never hope to find models of, say, Church's Thesis by looking at Grothendieck toposes.

This result can be extended somewhat up the arithmetic hierarchy. It's analogous to Schoenfield Absoluteness.