Return to Answer

Dan's comment below answers the question that was actually asked. Let me explain one way to look at it. If $M$ is any model of ZF and $T$ is any consistent computably axiomatizable theory, then we may look at the version of $T$ inside $M$. There will be some longest initial segment of the axiomatization of $T$ that $M$ thinks is consistent, and this will include the actual $T$. By the completeness theorem applied in $M$, there is a complete consistent Henkin extension of this theory in $M$, and it is represented by a particular number in the presentation of $M$. Using the $\in^M$ relation as an oracle, we can now compute this theory outside $M$, and thereby construct a model of $T$ outside. So we can not only present the $\in$ relation of the model of $T$, but we can decide the entire satisfaction relation fort he model.

Dan's comment below answers the question that was actually asked. Let me explain one way to look at it. If $M$ is any model of ZF and $T$ is any consistent computably axiomatizable theory, then we may look at the version of $T$ inside $M$. There will be some longest initial segment of the axiomatization of $T$ that $M$ thinks is consistent, and this will include the actual $T$. By the completeness theorem applied in $M$, there is a complete consistent Henkin extension of this theory in $M$, and it is represented by a particular number in the presentation of $M$. Using the $\in^M$ relation as an oracle, we can now compute this theory outside $M$, and thereby construct a model of $T$ outside. So we can not only present the $\in$ relation of the model of $T$, but we can decide the entire satisfaction relation for the model.

Todd's comment below answers the question that was actually asked.

Let me focus on the related question that I find to be implicitly suggested here, namely, given a model of set theory $M$, presented to us as an oracle, under what circumstances can we compute a structure for a forcing extension $M[G]$ of a particular kind?

Dan's comment below answers the question that was actually asked. Let me explain one way to look at it. If $M$ is any model of ZF and $T$ is any consistent computably axiomatizable theory, then we may look at the version of $T$ inside $M$. There will be some longest initial segment of the axiomatization of $T$ that $M$ thinks is consistent, and this will include the actual $T$. By the completeness theorem applied in $M$, there is a complete consistent Henkin extension of this theory in $M$, and it is represented by a particular number in the presentation of $M$. Using the $\in^M$ relation as an oracle, we can now compute this theory outside $M$, and thereby construct a model of $T$ outside. So we can not only present the $\in$ relation of the model of $T$, but we can decide the entire satisfaction relation fort he model.

Let me now focus on the related question that I find to be implicitly suggested here, namely, given a model of set theory $M$, presented to us as an oracle, under what circumstances can we compute a structure for a forcing extension $M[G]$ of a particular kind?

If you have an oracle coding not only the atomic truth of the model but also the $\Delta_0$ diagram, then yes, given any poset $P$ in that model, we can compute a representation of a forcing extension $M[G]$, with $M$-generic $G\subset P$. The main reason is that the oracle for $M$ includes a way for us computably to enumerate all the dense subsets of $P$ in $M$, and from that, we may computably construct an $M$-generic filter $G\subset P$. Specifically, $P$ is represented in the oracle by some number $P$; the relation $\leq_P$ is also represented by some number, and the collection $D$ of all dense subsets of $P$ in $M$ is represented by some number. Now, we computably construct a sequence $p_n$ which will be descending in $P$ and meet every dense set in $M$, simply by searching for the next element of the oracle that is in $P$ and in the next thing we find that is in $D$, and such that it is $\leq_P$ related to $p_n$ (this requires us to find the object in $M$ coding the pair, etc.). We don't need the $\Delta_0$ diagram to compute $G$. But now, having computed an $M$-generic filter $G$, we can compute an oracle for $M[G]$ as follows: we can use the $\Delta_0$ oracle to tell when an element of $M$ is a  $P$-name and when two names are forced to be equal by a condition in $G$ (the particular conditions we put into $G$ will either force them to be equal or force them to be unequal). So we can build a computable representation of  $M[G]$ by using the names as indices, and using our decision procedure for equality modulo $G$ to avoid double representation, and then using the fact that $p\Vdash \tau\in\sigma$ is $\Delta_0$ to compute the relation $\in^{M[G]}$ for our representation.

Similarly, if we have an oracle for the full elementary diagram of  $M$, then we can compute an oracle for the full elementary diagram of  $M[G]$.

In the end, the Turing degree of the original representation of $M$ and the representation of $M[G]$ will be the same; they are computable from each other.

In particular, the result follows for models of Gödel-Bernays set theory, where we are given the sets and classes and the $\in$ relation, since in this case, there is a particular number representing the class of $\Delta_0$ truth, from which we can then build the forcing extension in the manner I described.

In the case that the oracle only gives you access to $\in^M$, however, and not the $\Delta_0$ diagram of $M$, then although you can still compute a particular generic filter $G$, it isn't clear to me that we should expect to be able to compute equality of names modulo $G$, and so I suspect that one might not be able to compute a representation of $M[G]$ in this general case. Perhaps there might be some way to build a counterexample model $M$ by means of diagonalizing against the putative algorithms meant to compute $M[G]$. But I'm not sure how to do this.

Todd's comment below answers the question that was actually asked.

Let me focus on the related question that I find to be implicitly suggested here, namely, given a model of set theory $M$, presented to us as an oracle, under what circumstances can we compute a structure for a forcing extension $M[G]$ of a particular kind?

So let us suppose that $M=\langle\mathbb{N},\in^M\rangle$ has underlying set the natural numbers, in the style of computable model theory, and suppose that $P$ is a partial order in $M$ with which we want to force. We'd like to compute a presentation of $\langle M[G],\in^{M[G]}\rangle$ for some $M$-generic filter $G\subset P$.

There are a number of interesting things to say.

Theorem. If we are given the $\Delta_0$-elementary diagram of $M$ as an oracle, then we can compute a presentation for a forcing extension $M[G]$ via $P$, along with its $\Delta_0$-elementary diagram.

Proof. The main idea is that the presentation of $M$ gives us a canonical enumeration of the dense sets of $P$ in $M$, and using that we can compute an $M$-generic filter $G$ an provide a presentation of $M[G]$. Specifically, let $\cal{D}$ be the object in $M$ that $M$ thinks is all the open dense subsets of $P$, and fix the objects coding the order $\leq_P$ and so on. We compute $G$ as follows. At any given stage, we will have committed ourselves to a certain finite number of compatible elements being in $G$. At stage $k$, we extend this set by searching for the first element of $P$ we can find that is below all of those elements and also in $D_k$, and then we put that element into $G$, and also all elements previously found in $P$ that are above it, and we put out of $G$ any elements of $P$ that we have found so far that are incompatible with that new element. All these questions are $\Delta_0$ in the data we have available, and so in this way, we'll compute an $M$-generic filter $G$.

Next, we build a presentation of $M[G]$ using the $P$-names of $M$. We can computably decide whether a given object in $M$ is a  $P$-name, because given $\tau$ we can find an object $A$ that $M$ thinks is a transitive set containing $\tau$ and $P$, and then it becomes a $\Delta_0$ property about $(A,\tau,P)$ whether $\tau$ is a $P$-name. Similarly, using the oracle we can computably decide the relations $p\Vdash\tau=\sigma$ and $p\Vdash\tau\in\sigma$, by searching for a large transitive set containing all that data, which thinks that it is true. We now build a presentation of  $M[G]$ by enumerating all the $P$-names in $M$, and including the next name on the list just in case there is a condition in $G$ forcing that it is different from all the previous names on our list; otherwise, we find a condition in $G$ forcing that it is the same as one of our previous names. Similarly, we can decide any $\Delta_0$ statement for our presentation, since $p\Vdash\varphi(\tau)$ will be $\Delta_0$ in $M$ with respect to a large transitive set containing all the relevant data, and so we can go search for such a set and then consult our oracle. QED

Theorem. From an oracle for the full elementary diagram of  $M$, we can compute an oracle for the full elementary diagram of  $M[G]$.

Proof. This makes things even easier, since we don't have to worry about reducing things to $\Delta_0$. QED

Observation. Using only $\in^M$ as an oracle, we can compute a set $G$ that is an $M$-generic filter. Further, for any large ordinal $\theta$ in $M$, we can compute a presentation of $V_\theta^M[G]$.

Proof. The main point is that to construct $G$, we don't need a full oracle for the $\Delta_0$-elementary diagram of $M$. Rather, it would suffice to have an oracle for $\Delta_0$-truth in some large $V_\theta^M$, well above the rank of $P$. We can fix the number representing such a $V_\theta^M$, and another number representing the full satisfaction relation on $V_\theta^M$, since $M$ of course can compute a satisfaction relation for any of its sets. Now, using only $\in^M$ as an oracle, for any given $\Delta_0$ assertion $\varphi$ about $V_\theta^M$, we can search in $M$ for the thing that $M$ thinks is $\varphi$ and then look and see if it is in the corresponding thing that $M$ thinks is $\Delta_0$ truth in $V_\theta^M$, and thereby compute $\Delta_0$ truth relative to $V_\theta^M$. The point now is that this is all we needed in order to construct the filter $G$, since for that part of the construction, we needed only to know whether particular conditions were compatible, and so on. Similarly, using the $\Delta_0$ truth of $V_\theta^M$ (or perhaps we would want $\Delta_0$ truth for some much larger $V_\lambda^M$, we can compute a presentation of $V_\theta^M[G]$ as previously. QED

Corollary. If $M$ is computably saturated, then using only an oracle for $\in^M$, we can computably provide a presentation of a forcing extension $M[G]$, where $G\subset p$ is $M$-generic for any desired $P$.

Proof. If $M$ is computably saturated, then it follows, using a result of Harvey Friedman (see Ali Enayat's slides), that $M$ is isomorphic to some rank-initial segment $V_\theta^M$. Let $Q$ be the image of $P$ in that model. The previous theorem shows how to compute a presentation of a forcing extension $V_\theta^M[H]$, where $H\subset Q$ is $V_\theta^M$-generic. This will be isomorphic to a forcing extension $M[G]$, where $G\subset P$ is $M$-generic. QED

In the corollary, we do not necessarily expect that the inclusion $M\subset M[G]$ is computable from the oracle, since I do not see that we can expect the isomorphism of $M$ with $V_\theta^M$ to be computable relative to $\in^M$. I am curious to know whether or not there could be a presentation of a model $M$ for which the oracle $\in^M$ does not compute any presentation of a particular kind of forcing extension $M[G]$.

Question. Is there a presentation of a model $M=\langle\mathbb{N},\in^M\rangle\models\text{ZFC}$ such that no presentation of a forcing extension $M[G]$, for a particular forcing notion $P\in M$, is computable relative to oracle $\in^M$?

I have a feeling one might be able to construct such a model $M$ by diagonalizing somehow against the possible computations of $M[G]$.