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

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.

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 reals $\mathcal{A}$, one can form the unique $\omega$-model $\mathsf{REC}[\mathcal{A}]$ of all reals 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 reals 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 reals in this submodel"?

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