How (non-)computable is set theory?

Question

Here is a naive outsiders perspective on set theory: A typical set-theoretical result involves constructing new models of set theory from given ones (typically with different theories for the original model and the resulting model). Typically, from a meta-perspective we are allowed (encouraged, or even required) to assume that the models are countable.

To the extent that this view is correct, set-theoretic constructions correspond to partial, multivalued operations $T : \subseteq \{0,1\}^\mathbb{N} \rightrightarrows \{0,1\}^\mathbb{N}$ which are defined on sequences coding a model of the original theory, and are outputting a sequence coding a model of the desired theory. These are multivalued, because the constructions may involve something like "pick a generic filter for this forcing notion".

Question: Are these operations typically computable, and if not, how non-computable are they?

The Weihrauch degrees (https://arxiv.org/abs/1707.03202) provide a framework for classifying non-computability of operations of these types. An answer, however, could also take forms like "For arguments like this, a resulting model is typically computable in the join of the original model and a 1-generic."

Answer 1

The question is extremely interesting, and I have looked into this kind of thing with various colleagues (including Russell Miller and Kameryn Williams), although our investigation has not yet resulted in any paper.

One important realization to which we had come was that the question is highly sensitive to whether the input data includes just the set-membership information, or instead the diagram (the truths) of the original model.

With an oracle for the elementary diagram of a countable model $\langle M,\in^M\rangle$ of a model of set theory, that is, an oracle listing all the true statements of the model, with names for every element, then for any forcing notion $\mathbb{P}$ in $M$, one can compute an $M$-generic filter $G$ and the elementary diagram of the corresponding forcing extension $M[G]$. This can be seen as a strong positive answer to your question. The reason you can find such a $G$ is that the oracle for the diagram of $M$ allows you to find a canonical enumeration of the dense sets of $M$, and so by the usual diagonalization, one can compute a filter getting into all those dense sets, and this filter will therefore be generic. (In this sense, your remarks about multi-valued seem to be unnecessary — one can compute a specific generic filter.) Using this filter $G$, one can evaluate the diagram of the extension $V[G]$ in terms of names, using the forcing relation, which is expressed in the diagram of the original model. Thus, from the diagram of a model $M$, you can compute the diagram of the forcing extension $M[G]$.

In particular, this shows that from the diagram of any model of ZFC, you can compute the diagram of a model of ZFC+CH or of ZFC+$\neg$CH or ZFC+MA and so on, for all the various results obtained by forcing.

One can also compute the elementary diagram of many other kinds of set-theoretic constructions, such as inner models $L$ and $\text{HOD}$, and ultrapowers $\text{Ult}(M,\mu)$ by an ultrafilter $\mu$ in $M$, or an extender ultrapower.

You don't need the whole diagram to compute the generic filter $G$, and in fact, even just the atomic diagram, which contains information only about the membership relation $n\in m$ for specific objects, is sufficient to compute a generic filter $G$. One simply fixes the object whose elements are the dense subsets of $\mathbb{P}$ and an object for the order relation, and then you can carry out the diagonalization.

Nevertheless, and this is an important point, if all you have is the atomic diagram of the original model $M$, then it turns out that you cannot compute much about the model or its forcing extensions at all. For example, you cannot even reliably identify from the atomic diagram which is the empty set of $M$, since for any computable algorithm, there is a model $M$ that will fool it. And there are many further such examples. I take these examples to illustrate that one shouldn't think of a model of set theory merely as its atomic diagram, but as a bit more.

Answer 2

For what it's worth, you might also consider the sets computable by Ordinal Turing Machines (see Koepke's paper, Turing Computations on Ordinals, arXiv:math/0502264v1 [math.LO] 13 Feb 2005). A central theorem regarding Ordinal Turing Machines is the following:

A set $x$ of ordinals is ordinal computable from a finite set of ordinal parameters if and only it is an element of the constructible universe $L$.

Relative to this type of Turing machine, the non-computable sets are just the non-constructible sets.

It would be interesting to study the degree theory of the non-constructible sets relative to Ordinal Turing Machines.