# Analogy of $\omega$-models in constructive mathematics

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.

• When you intend to speak to constructive mathematicians you should never ever call a subset of $\mathbb{N}$ a "real" because you will create confusion. Sep 19 '15 at 22:07
• Yes, bad habit. I'll fix that. Sep 19 '15 at 22:08
• While you're at it please also add an explanation of what sort of language and logic you're trying to model. Are you going for intuitionistic (subsystems of) second-order arithmetic? Sep 19 '15 at 22:09

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.