Analogy of $\omega$-models in constructive mathematics

Question

I apologize that this question is a bit vague, however that is partially the point.

In subsystems of second order arithmetic, one considers $\omega$-models, these are models of $\mathsf{RCA}_0$ whose first order part is $\omega = \mathbb{N}$ and whose second order part is a subset of $2^\omega$ closed under Turing reduction and join.

$\omega$-models have the following properties that I am interested in:

• The $\omega$-models are the submodels of true arithmetic (with respect to $\mathsf{RCA}_0$).
• There is a minimal $\omega$-model $\mathsf{REC}$ consisting of all the computable reals.
• Given a set of binary sequences $\mathcal{A}$, one can form the unique $\omega$-model $\mathsf{REC}[\mathcal{A}]$ of all sequences computable from tuples of $\mathcal{A}$.

My first question is:

Are there any good analogues of $\omega$-models in constructive mathematics?

For example, I think the effective topos behaves sort of like $\mathsf{REC}$, being a minimal(ish?) model of computable mathematics. Is it possible to "append a non-computable object $a$ to the effective topos" to get a new model? Are the elements of $2^\omega$ in this new model roughly the sequences truth-table reducible to $a$? This is the idea I am looking for? Is there a standard way to do this?

My second question is:

Given a universe $U$ of set theory (i.e. "the real world"), is there such thing as a "constructive submodel" of $U$? Can we talk about "the binary sequences in this submodel"?

Edit: I am flexible on the logic used. It could be intuitionistic second order arithmetic or it could be a type of set theory, or something else. I want the ability to talk about sets of naturals, real numbers, etc. in the larger model that relate in some way to objects in the submodel.

Answer 1

It is not clear to me exactly what you are asking, but here are some pointers. Let us stay within the realm of realizability theory.

There is a way to extend any given model by an "oracle" or by a "non-computable" object, see Section 1.7 of Jaap van Ooosten's book "Realizability: An Introduction to its Categorical Side" (Elsevier 2008), in particular Theorem 1.7.5 and the second remark at the end of the section.

The effective topos is an "extreme" in the space of all realizability models, but I would not call it "minimal". There are many realizability models which all have the same morphisms $\mathbb{N} \to \mathbb{N}$, namely the Turing computable maps, but these models are not equivalent. If I had to describe how they differ I would say that in the amount of intensional information that is exposed by realizers. The effective topos maximizes the intensional information available.

The object $2^\mathbb{N}$ represents the decidable subsets of $\mathbb{N}$ in whatever model we are in. If we are in the model "Turing machines + oracle $A$" then these will be the subsets which are decidable with respect to $A$-oracle Turing machines.

There is a systematic theory of comparing realizability models, see Section 1.6 on applicative morphisms and Section 2.5 on geometric morphisms between toposes (still Jaap's book). These are all "macro scale" ways of comparing entire realizability models.