Skip to main content
8 of 8
edited body
Joel David Hamkins
  • 236.3k
  • 44
  • 777
  • 1.4k

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]$.

Joel David Hamkins
  • 236.3k
  • 44
  • 777
  • 1.4k