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.



Is forcing computable?
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](http://www.math.uni-bonn.de/ag/logik/events/young-set-theory-2011/Slides/Ali_Enayat_slides_2.pdf)),
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]$.


