This is a talk in the UH Mānoa Mathematical Logic seminar on Monday, September 17 at 2:30pm.

In this talk we will consider computable structure theoretical aspects of forcing. Given an oracle for a countable model of set theory $M$, to what extent can we compute information about forcing extensions $M[G]$? The main theorem I will present gives a robustly affirmative answer in several senses.

  • Given an oracle for the atomic diagram of a countable model of set theory $M$, then for any forcing notion $\mathbb P \in M$ we can compute an $M$-generic filter $G \subseteq \mathbb P$.

  • From the $\Delta_0$ diagram for $M$ we can moreover compute the atomic diagram of the forcing extension $M[G]$, and indeed its $\Delta_0$ diagram.

  • From the elementary for $M$ we can compute the elementary diagram of the forcing extension $M[G]$, and this goes level by level for the $\Sigma_n$ diagrams.

On the other hand, there is no functorial process for computing forcing extensions.

  • If ZFC is consistent then there is no computable procedure (nor even a Borel procedure) which takes as input the elementary diagram for a countable model $M$ of ZFC and a partial order $\mathbb P \in M$ and returns a generic $G$ so that isomorphic copies of the same input model always result in the same corresponding isomorphic copy of $G$.

This talk is a sequel to my previous talk. The work in this talk is joint with Joel David Hamkins and Russell Miller.