Forcing as a computational process

TL;DR

This paper explores the interpretation of set-theoretic forcing as a computational process, detailing how models and extensions can be computed from various diagrams and discussing the limitations of functoriality in this context.

Contribution

It formalizes the computational aspects of forcing in set theory and analyzes the functoriality limitations of such processes.

Findings

Computing generic filters from the atomic diagram of a model.

Computing forcing extensions from the $ riangle_0$-diagram.

No Borel functorial process exists for generic filters.

Abstract

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 $\langle M,\in^M\rangle$, we explain senses in which one may compute $M$-generic filters $G\subseteq\mathbb{P}\in M$ and the corresponding forcing extensions $M[G]$. Specifically, from the atomic diagram one may compute $G$, from the $\Delta_0$-diagram one may compute $M[G]$ and its $\Delta_0$-diagram, and from the elementary diagram 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 such process, it will always be possible to have different isomorphic presentations of a model of set theory $M$ that lead to different non-isomorphic forcing extensions $M[G]$. Indeed, there is no Borel function providing generic filters that is functorial in this sense.