Computability and Forcing

Question

In view of the paper "Forcing As A Computational Process" by J. Hamkins, R. Miller and K. Williams, I have revised my original question, part (a) about the computability of the Forcing Truth Definition, Looking into the Future within Forcing as follows (instead of Cohen's book, using Shoenfield paper :
https://mathweb.ucsd.edu/~sbuss/CourseWeb/Math260_2012F2013W/Shoenfield_UnramifiedForcing.pdf)

In demonstrating the definability of forcing in the base model M, the definition of $\Vdash$* includes (page 362 definition (c)):

p $\Vdash$* $\neg$ $\Phi$ $\;$ iff $\;$ For all q $\leqq$ p $\neg$ (q $\Vdash$* $\Phi$ ) …………………(1)

Although the complexity of the construction of a formula $\Phi$ is finite, there is an infinite number of finite q $\leqq$ p to test for q $\Vdash$* $\Phi$. If none of the q lead to q $\Vdash$* $\Phi$, this would mean that a completed infinity of tests may be required to establish (1) making the overall calculation not computable.

However "Forcing As A Computational Process" in Main Theorem 1 on page 1 says that : G is computable from the Atomic Diagram of M.

So I was wondering whether anyone could help to identify the error in thinking that "determination of expressions like (1) could require a completed infinity of calculations."

Answer 1

Note that in the Forcing as a computational process paper, the theorem merely states that some generic is computable from (the atomic diagram of) $M$, not that every generic is.

Proof:

The proof of the theorem is roughly this: from $M$, we can decide whether any given $p\in M$ is in $\mathbb{P}\in M$, and similarly whether or not $p\leqslant^{\mathbb{P}}q$ for $p,q\in \mathbb{P}$. Since $M$ has the set of all its dense subsets of $\mathbb{P}$ (and the set of all non-dense subsets), it's also decidable from $M$ whether or not any given subset of $\mathbb{P}$ is dense or not. So $\mathbb{P}$, $\leqslant^{\mathbb{P}}$, being dense, and so on are all decidable relative to $M$. How do we therefore compute a new generic? Well the same way we would for generating a generic from any countable transitive model: just continually extend $q_n$ into the next dense set $D_{n+1}$ to get $q_{n+1}$. The upward closure of this $\{q_n:n\in \omega\}$ is the resulting generic $G$. Note that $\{q_n:n\in\omega\}$ is decidable from $M$.

So to compute membership $p\in G$, we just need $p$ to be above the "least" element $q_n\in D_n$ such that $q_n$ extends $q_m$ for all $m<n$, and where $D_n$ in the $n$th dense set. This gives an algorithm that outputs "yes" if $p\in G$, basically meaning $G$ is $\Sigma^0_1$ relative to $M$. To determine if $p\not\in G$, we use antichains: if we consider two incompatible elements $p,q\in \mathbb{P}$, if $p\not\in G$ then $p$ must be incompatible with some element of $G$ (otherwise just take the dense set of things below $p$ in union with things incompatible with $p$ and see which $G$ can intersect). As a result, to check whether $p\not\in G$, we just need to check if the pair $\langle p,q_n\rangle$ is in the set of incompatible pairs of elements of $\mathbb{P}$ for some $n\in\omega$ where $q_n$ is as above. This gives an algorithm that spits out "no" to the question "is $p\in G$?" whenever $p\not\in G$. In other words, $G$ is $\Pi^0_1$ relative to $M$ and hence is $\Delta^0_1$ (i.e. decidable) relative to $M$.$\blacksquare$

Now what does this tell us about the computability of the forcing relation? Not much. The paper goes into this a bit, talking about how with only access to the membership relation in $M$, we can't compute much about the theory of $M[G]$ (where $G$ is computable from $M$ as above). With access to the entire theory of $M$, we can compute more of $M[G]$, as expected, with negation increasing the complexity needed to compute more about $M[G]$.