14
$\begingroup$

Koepke's paper Turing Computations on Ordinals defines a notion of "ordinal computability" using Turing machines with a tape the length of Ord and that can run for Ord-many steps, and shows that a set of ordinals is ordinal computable from a finite set of ordinal parameters if and only if it is an element of Gödel's constructible universe $L$.

Usually, whenever we have a notion of "computation", we can assemble the computations into a partial combinatory algebra (PCA), which can then be used to define a realizability topos. For example, the infinite time Turing machines of Hamkins and Lewis (which apparently predated and inspired Koepke's ordinal computations, having only a countably infinite tape but being allowed to run transfinitely long) were used by Bauer to construct a topos in which Baire space injects into the natural numbers.

I assume that Koepke's notion of ordinal computation gives rise to some kind of proper-class-sized PCA. (If it doesn't, please correct me!) If so, then it should also give rise to some kind of realizability category, although size issues might prevent this category from being a topos. My question is:

What is the relationship between this "ordinal realizability category" and Gödel's constructible universe $L$?

The ordinal realizability category is almost certainly not equivalent to the category $\mathrm{Set}_L$ of sets and functions in $L$. Among other reasons, realizability categories are usually non-Boolean and contain $\mathrm{Set} = \mathrm{Set}_V$ as the reflective subcategory of double-negation sheaves, but $L$ is already Boolean and not provably equivalent to the entire cumulative hierarchy $V$. However, it seems possible to me that $\mathrm{Set}_L$ might be some category of "discrete objects" in the ordinal realizability category.

In an ordinary realizability topos, the discrete objects are the subquotients of the natural numbers object, where the latter is the usual set of natural numbers embedded "discretely" with each natural number realized by a different computation (in contrast to the natural numbers sitting inside $\mathrm{Set}_V \subsetneq \mathcal{E}$ which are "indiscrete" with every number realized by the same computations). I would expect that for ordinal realizability there is a similar "discrete embedding" of all the ordinals into the realizability category, and a natural generalization of "discrete object" would be the subquotients of these ordinals, or maybe of finite products of them. Since these are in a different sense the objects "obtained by ordinal computation from a finite number of ordinals", it doesn't seem impossible that they might coincide with $\mathrm{Set}_L$, given Koepke's result about $L$.

However, even if this optimistic guess is wrong, it seems likely to me that there is some relationship between $L$ and the ordinal realizability category.

(Thanks to James E Hanson, who made me aware of Koepke's result and helped me refine this question on the category theory Zulip.)

$\endgroup$
14
  • 3
    $\begingroup$ Nice question, hope to learn something. $\endgroup$ Commented May 15 at 21:25
  • 1
    $\begingroup$ Is there some standard notion of 'topos but the subobject classifier might be large'? I remember people talking about this in the context of the category of (non-light) condensed sets. $\endgroup$ Commented May 15 at 21:27
  • 3
    $\begingroup$ @JoelDavidHamkins Aw darn, you were one of the people I was hoping might know the answer! (-: $\endgroup$ Commented May 15 at 21:36
  • 2
    $\begingroup$ @MikeShulman Oh, I know all about the Koeopke model, and indeed I was there at the very start, since Koepke was visiting me in New York, staying in my apartment, when it was invented. And there have been many dissertations, etc. since then. But I don't know much about the PCA or realizability toposes. One observation is that the construction must not be very absolute, since if you jump inside $L$ and construct it there, then you shouldn't expect to find all pieces from $\text{Set}_V$ inside it. Perhaps it isn't a construction that can be formulated internally to models of set theory at all? $\endgroup$ Commented May 15 at 22:37
  • 2
    $\begingroup$ One observation that I have is that while the connection between OTM and $L$ is true for computations starting with finitely many ordinal inputs, the connection is lost when one allows more arbitrary input to the computations, and in the general case of allowing all patterns of input, then one is getting $V$ instead of $L$. $\endgroup$ Commented May 16 at 2:36

1 Answer 1

5
$\begingroup$

As pointed out by Noah and Hanul in the comments, there are known models of set theory making use of class sized pcas. The earliest relevant to this question is probably Tharp, A quasi-intuitionistic set theory. Most of these don't use ordinal computability but other similar notions. I don't think it matters which one you choose. I'm most familiar with E-recursion, so that's the one I have in mind for the answer. For set theory, these models are related to, but distinct from, Gödel's $L$. This is particularly clear in Rathjen, Indefiniteness in semi-intuitionistic set theories: on a conjecture of Feferman, where he first defines a relativised version of $L$, uses that to define a notion of computation, and then uses that in a realizability model, which is distinct from just working in $L[X]$ as a model.

The realizability models have different logical properties to $L$: in particular they only satisfy the law of excluded middle for bounded formulas, but not in general. We can understand this by looking at how universal quantifiers and disjunction are interpreted in the model. $$ \begin{align} e \Vdash \forall x.\varphi(x) &\text{ iff }\forall a.ea \Vdash \varphi(a) \\ e \Vdash \varphi \vee \psi &\text{ iff }((e)_0 = 0 \wedge (e)_1 \Vdash\varphi) \vee ((e)_0 = 1 \wedge (e)_1 \Vdash \psi) \end{align} $$ A realizer for the law of excluded middle would entail that we have an effective way to decide whether or not the E-recursive function coded by a set $e$ is defined or not on input $e$, which by the usual diagonal argument is not possible. On the other hand since $L$ is just a first order model, we do have $L \vDash e.e {\downarrow} \vee \neg e.e {\downarrow}$, because we just need one clause or the other to hold without requiring an effective way to decide which one.

Also note that the realizability model works fine if the underlying domain of the model and/or the pca contain all sets - the logic will still be different to working over $V$, because propositions need to be realized in order to hold. It is also possible to restrict either the pca or both the pca and the domain of the model to $L$ by just defining them that way, or by assuming $V = L$ in the background. This ensures that the domain of the realizability model is exactly $L$, but as noted above the logic will not be the same as truth in $L$.

It's a little messy to relate this kind of realizability to the categorical kind. You can define a category of modest assemblies $\mathbf{Mod}(\mathcal{A})$ for any pca $\mathcal{A}$, including when $\mathcal{A}$ is a proper class. These are the the ones that can be viewed as subquotients of $\mathcal{A}$, and you do get a locally cartesian closed category (assuming $\mathcal{A}$ is either small or satisfies some other conditions). The problem is that the pca structure is not just used for bounded quantifiers, but also for quantifiers over the class of all sets/objects. One way to deal with this is to define a "large modest assembly," where the carrier set is the class $L$, and the set of realizers for $x \in L$ is just the singleton $\{x\}$ (i.e. every set is its own realizer). Using this as a universe to define the cumulative hierarchy should give something similar to the models in set theory above. I couldn't figure out how to do this via stack semantics.

$\endgroup$
8
  • $\begingroup$ Thanks for this! What I'm interested in is building a realizability model without using anything about $L$ to start with, and then comparing the resulting model to $L$. You seem to be saying that this will be different from $L$ because it will only satisfy excluded middle for bounded formulas whereas $L$ satisfies it for all formulas. Can you say anything positive about how they are related? $\endgroup$ Commented May 21 at 18:47
  • $\begingroup$ @MikeShulman I am not sure it answers your question, but Passman's realizability model also satisfies $V=L$. (Formulating $V=L$ over $\mathsf{CZF}$ appears in joint paper by Matthews and Rathjen) and the realizability model and $L$ satisfy the same $\Sigma$-statements. It might be possible that if we can appropriately formulate set theory over the ordinal realizability topos, then it satisfies $V=L$. $\endgroup$
    – Hanul Jeon
    Commented May 23 at 17:57
  • $\begingroup$ @HanulJeon Thanks, that's interesting and certainly relevant. But I think it doesn't quite answer the question as I asked it, since a model that satisfies $V=L$ internally isn't necessarily itself equivalent to, or even related to, the $L$ of the ambient model, is it? $\endgroup$ Commented May 23 at 19:44
  • $\begingroup$ @MikeShulman Right, Even if Passman's realizability model satisfies $V=L$ it does not mean it is equal to $L$. (I am not even sure what the "equal to $L$" should mean since both $L$ and the realizability model have the same "sets." They are still different since they have different ways to check the validity of formulas.) $\endgroup$
    – Hanul Jeon
    Commented May 23 at 23:24
  • 1
    $\begingroup$ @HanulJeon There's a few variants of the realizability in Passman's paper and I think that V = L would only hold in the ones that explicitly restrict to L (marked with a subscript L). Ideally there would be a way to get these models without requiring a definition of L a priori. I think the same would be the case for $\Sigma_1$ conservativity. $\endgroup$
    – aws
    Commented May 24 at 11:01

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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