The computable structure theory of forcing
This is a talk on Wednesday, 29 May 2019 at the Institute of Mathematics at University of Barcelona.
Introduced by Paul Cohen, forcing is a powerful and flexible technique for proving independence results. We can think of forcing as an operation on models of set theory; given a model $M$ of set theory and a partially ordered set $\mathbb P \in M$, we can produce a forcing extension of $M$ by using a generic filter $G$ for $\mathbb P$. This forcing extension is the smallest model of set theory containing both $M$ and $G$.
In this talk we will consider forcing from the perspective of computable structure theory. Given information about a model of set theory, to what extent can we compute information about its forcing extensions? The main theorem I will present answers this question for multiple levels of information. From an oracle for the atomic diagram of a countable model $M$ of set theory, we can compute a $M$-generic filter for any $\mathbb P \in M$. If we moreover have the $\Delta_0$ diagram for $M$ we can compute the atomic and $\Delta_0$-diagrams of the forcing extension, and from the elementary diagram for $M$ we can compute the elementary diagram of the extension. However, these computations are necessarily specific to the presentation of the model. There is no computable, nor even Borel, process to functorially compute forcing extensions.
This is joint work with Joel David Hamkins and Russell Miller.