Is forcing computable? By results similar to Tennenbaum's theorem we know that there exist no computable models of $ZF$. But suppose we are given, as a sort of oracle, access to some model of $ZF$ (e.g. we can make oracle answer queries of form $a\in b?$ for $\in$ being relation on $\Bbb N$ modelling $ZF$). My question then is: is it possible to, given this oracle representation of a model, compute a relation which would create model of $ZF$ with some property we desire, e.g. $AC$ and $\neg CH$?
I hope I have explained my question well enough.
Thanks in advance.
 A: 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.
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?
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]$.
