This will be a talk for Set Theory in the United Kingdom (STUK 1), to be held in the other place, February 16, 2019.

Abstract. We investigate the senses in which set-theoretic forcing can be seen as a computational process on the models of set theory. Given an oracle for the atomic or elementary diagram of a model of set theory ⟨𝑀, ∈𝑀⟩, for example, we explain senses in which one may compute 𝑀-generic filters 𝐺 ⊂𝑃 ∈𝑀 and the corresponding forcing extensions 𝑀⁡[𝐺]. Meanwhile, no such computational process is functorial, for there must always be isomorphic alternative presentations of the same model of set theory 𝑀 that lead by the computational process to non-isomorphic forcing extensions 𝑀⁡[𝐺] ≇𝑀⁡[𝐺′]. Indeed, there is no Borel function providing generic filters that is functorial in this sense.

This is joint work with Russell Miller and Kameryn Williams.