Title: Forcing as a computational process
Abstract: 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 P∈M we can compute an M-generic filter G⊆P.
* From the Δ0 diagram for M we can moreover compute the atomic diagram of the forcing extension M[G], and indeed its Δ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 Σ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 P∈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.