This is a talk for the MidWest Computability Seminar conference held May 2, 2023 at the University of Chicago. The talk will be available via Zoom at https://notredame.zoom.us/j/99754332165?pwd=RytjK1RFZU5KWnZxZ3VFK0g4YTMyQT09.
Abstract: I shall explore several 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 (M,∈M) of set theory, for example, there are senses in which one may compute M-generic filters G⊂ℙ∈M over that model and compute the diagrams of the corresponding forcing extensions M[G]. 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 myself, Russell Miller and Kameryn Williams.
The paper is available on the arxiv at https://arxiv.org/abs/2007.00418.
The talk took place in “The Barn” in the upper space between the Reyerson Laboratory and Eckhart Hall, where the University of Chicago Department of Mathematics is located:
This is *very* interesting. Is there a paper for this? Does it affect what we’ve talked about regarding “potentialism” and forcing?
The paper is on the arXiv:
https://arxiv.org/abs/2007.00418
I think there is a connection with some kinds of potentialism. In particular, part of the work involves the extent to which one can treat the set-theoretic generic multiverse also as a computational process. Given an oracle for a model of set theory, we define the computable set-theoretic generic multiverse, consisting of a computable presentation of a countable portion of the generic multiverse of that model.
Thanks both! I guess my point was more (and I know that you don’t have *so* much time for this position), that this work might help to respond to the worry that forcing potentialism is not a “real” kind of potentialism (in contrast to, say, rank potentialism, where we have a clear notion of “operation” to take us from one world to another, and it’s determinate what you get). The issue with forcing is that the notion of “operation” is only determinate insofar as we’ve already got access to the parameter G. (Maybe this is what’s meant by your point about it being non-functorial—haven’t had chance to read the paper yet.) So is there a way of thinking of forcing using this work as an “operation” on the ground model.
(I should probably just read the paper—snatching some time in between meetings, but I’d love to hear if there’s a simple response.)
The point about nonfunctoriality is, the generic you build depends on your enumeration of the model. So running the process on isomorphic copies of the same model of set theory may not produce the same generic. Or phrased in another way: forcing isn’t determinate in just the model, but it is determinate in the model equipped with an enumeration of its elements.
I’m not sure whether this undercuts your proposed rebuttal to forcing potentialism not being real potentialism. Presumably the forcing (and only forcing) potentialist wouldn’t think their models are countable, so they wouldn’t think it makes sense for them to come along with an omega-enumeration.