Forcing as a computational process

We investigate how set-theoretic forcing can be seen as a computational process on the models of set theory. Given an oracle for information about a model of set theory ⟨ M , ∈ M ⟩ , we explain senses in which one may compute M -generic filters G ⊆ P ∈ M and the corresponding forcing extensions M [ G ] . Specifically, from the atomic diagram of M one may compute a generic filter G , from the Δ 0 -diagram of M one may compute a presentation of the corresponding forcing extension M [ G ] and its Δ 0 -diagram, and from the elementary diagram of M one may compute the elementary diagram of M [ G ] . We also examine the information necessary to make the process functorial, and conclude that in the general case, no such computational process will be functorial—for any candidate process, there will be different isomorphic presentations of a model of set theory M that lead to non-isomorphic forcing extensions M [ G ] . Indeed, there is no Borel function providing generic filters that is functorial in this sense.