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."


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.

  • 1
    $\begingroup$ That would make an interesting multiverse, the computable multiverse. $\endgroup$ – Asaf Karagila Jun 28 '18 at 5:19
  • 11
    $\begingroup$ It's not the computable multiverse. It's the multiverse with computable wormholes connecting the universes, but the universes themselves need not be computable. $\endgroup$ – Andrej Bauer Jun 28 '18 at 10:39
  • 1
    $\begingroup$ Is any of this sensitive to the fact that we're talking about set theory, or could much of it be applied to models of first-order theories in general? $\endgroup$ – Andrej Bauer Jun 28 '18 at 10:40
  • 3
    $\begingroup$ Atomic diagrams are uninformative due to the minimalistic language of set theory, but what about $\Delta_0$-diagrams? $\endgroup$ – Emil Jeřábek Jun 28 '18 at 11:37
  • 2
    $\begingroup$ Class forcing is fine, provided that the forcing relations are definable, but this is true for all pre-tame class forcing notions. And yes, the diagram of any set-forcing ground model is computable from that of any extension, since the ground is a definable class. $\endgroup$ – Joel David Hamkins Jun 28 '18 at 18:48

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.

  • $\begingroup$ The degree theory of sets relative to ordinal Turing machines, is just the old fashioned realtive constructibility degree theory. This was much analysed in the 70's and there is an extensive body of literature on it. Unfortunately the OTM model does not bring anything new to it. $\endgroup$ – Philip Welch Jul 2 '18 at 17:29
  • $\begingroup$ @PhilipWelch: Except that the non-r.e. sets are the nonconstructible sets. Where to get those, I wonder (since $ZFC$ + $V$ = $L$ is an acceptable point of view)....? $\endgroup$ – Thomas Benjamin Jul 2 '18 at 20:38
  • $\begingroup$ One must assume $V\neq L$ for otherwise there is no degree theory to investigate - there is just the bottommost degree $0$! But we have $$x \mbox{ is OTM computable from } y \leftrightarrow x \leq_L y$$ where $x \leq _L y$ means $x\in L[y]$, and it was the latter that was much investigated under "degrees of constructibility". For example the `jump' of a set $x$ could be assigned to its sharp, $x^\sharp$; a Spector ordinal assignment for, say reals, was then $(\omega_1)^{+{L[x]}}$ etc. $\endgroup$ – Philip Welch Jul 3 '18 at 8:06
  • 1
    $\begingroup$ (I think we are getting somewhat away from the original q.) An OTM without any parameters supplied to it basically just computes up to $L_\sigma$ where $\sigma$ is least so that $L_\sigma \prec _{\Sigma_1} L$. So there is a sense of a (parameter free) universal OTM, and diagonalising past it gives a set not in $L_\sigma$. Similarly for any other given fixed finite sequence $\vec p$ of ordinal parameters on its input tape, there'd be a $\vec p$-universal OTM machine, defined uniformly in the param. seq. $\vec p$. But there is no one universal OTM-machine that could diagonalise outside of $L$. $\endgroup$ – Philip Welch Jul 3 '18 at 20:21
  • 1
    $\begingroup$ If you had OTM's that mimicked the p.r. set functions then they'd be producing all of $L$ and so not a proper sub-hierachy (if I understand you correctly.) If by $Z$ you mean Zermelo set theory, then I disagree: $Z$ cannot prove the existence of $HF$ (unless you change the axioms in order to let it do so, $Z$'s Axiom of Infinity is formally '$\omega \in V$', but that is not enough to get '$HF\in V$'). Also the statement that sets of reals in the Borel class $\Sigma^0_{\omega+1}$ are determined, cannot be proven in $Z$. But that statement is a statement in analysis. $\endgroup$ – Philip Welch Jul 3 '18 at 20:31

Your Answer

By clicking "Post Your Answer", you acknowledge that you have read our updated terms of service, privacy policy and cookie policy, and that your continued use of the website is subject to these policies.

Not the answer you're looking for? Browse other questions tagged or ask your own question.