Setup: Let $\alpha$ be an admissible ordinal (viꝫ., one such that $L_\alpha$ is a model of Kripke-Platek set theory), identified as usual with the set of ordinals $<\alpha$. Then there is a standard theory of computability on $\alpha$, known as “alpha-recursion theory” or “admissible recursion theory”, with many analogies to ordinary (Church-Turing) computability on $\mathbb{N}$. Possible references for basic facts on the topic include Sacks's book Higher Recursion Theory (1990), esp. chapter VII, or the (imho more readable) “Short Course on Admissible Recursion Theory” by Simpson, p. 355–290 in Generalized Recursion Theory II (Oslo 1977) edited by Fenstad, Gandy & Sacks (1978). But just so make sure there's no doubt about the definition, a partial function $f \colon \alpha^{\times r} \dashrightarrow \alpha$ is said to be $\alpha$-partial-recursive (i.e., $\alpha$-partial-recursive with parameters) when its graph $\Gamma_f$ is $\Sigma_1(L_\alpha)$ in parameters or, equivalently, when there is a primitive recursive relation $R$ and a parameter $p\in\alpha$ such that $\Gamma_f = \{(x_1,\ldots,x_r,y) \in \alpha^{\times(r+1)} : \exists z\in\alpha.R(x_1,\ldots,x_r,y,z,p)\}$ (the main difference with ordinary computability is that we can't dispense with parameters in general).
Just as for ordinary computability, the $\alpha$-partial-recursive can be given a standard numbering $(\varphi_\varepsilon)_{\varepsilon<\alpha}$ by ordinals $\varepsilon<\alpha$ so that the partial function $(\varepsilon,\gamma) \mapsto \varphi_\varepsilon(\gamma)$ is itself $\alpha$-partial-recursive (“universality”) and such that partial substitution can be performed by primitive recursive functions (“s-m-n”). So by definining $\varepsilon \bullet \gamma$ as $\varphi_\varepsilon(\gamma)$ (if the latter is defined), we make $\alpha$ into a partial combinatory algebra (p.c.a.) exactly analogous to Kleene's first algebra for the case of ordinary computability on $\mathbb{N}$.
Now one can then apply the general framework of realizability over p.c.a.'s to this situation. In particular, there is a realizability topos $\mathsf{RT}(\alpha)$ associated to $\alpha$ just like the effective topos is constructed for ordinary recursion on $\mathbb{N}$ (details of the construction are in van Oosten, Realizability: An Introduction to its Categorical Side (2008), §2.6). This topos comes equipped with a distinguished object (maybe call it $\mathring\alpha$) given by $\alpha$ itself, seen as an assembly with $E(\gamma) = \{\gamma\}$ for all $\gamma<\alpha$. (The natural numbers object $\mathbf{N}$ is a subset of this $\mathring\alpha$.)
Similarly, there is a model of $\mathsf{IZF}$ (intuitionistic Zermelo-Fraenkel) associated to the situation, just like the one constructed by McCarty (“Realizability and recursive set theory”, Ann. Pure Applied Logic 32 (1986) 153–183) for ordinary computability: this model can be seen on its own, or within the aforementioned realizability topos $\mathsf{RT}(\alpha)$ (as explained in van Oosten, op. cit. §3.5.1). Maybe call $V(\alpha)$ this model (not an ideal notation as it might be confused with $V_\alpha$, but I can't think of better).
General question: Has there been any study of realizability on $\alpha$, or specifically of these topoi $\mathsf{RT}(\alpha)$ or $\mathsf{IZF}$ models $V(\alpha)$ in the mathematical literature? (I mean, something about $\mathsf{RT}(\alpha)$ that's more specific than the study of all realizability topoi.) Specifically, I wonder if any work has been done in connecting properties of the (intuitionistic!) internal logic of $\mathsf{RT}(\alpha)$ and $V(\alpha)$ to (classical!) recursion-theoretic properties of $\alpha$.
Here's an example of something that can be said along these lines: recall that an admissible ordinal $\alpha$ is said to be nonprojectible when $L_\alpha$ is a model of $\Sigma_1$-separation. Recursion-theoretically, this means that the image of a total $\alpha$-recursive function $\alpha\to\alpha$ is $\alpha$-recursive, or that the projection of an $\alpha$-recursive subset of $\alpha^{\times 2}$ is recursive. Internally in $\mathsf{RT}(\alpha)$, this means that the object $\mathring\alpha$ is omniscient in the sense that for every function $p\colon\mathring\alpha\to\{0,1\}$ either there is $x$ such that $p(x)=0$ or $p$ is constantly $1$ (see Escardó, “Infinite sets that satisfy the principle of omniscience in any variety of constructive mathematics”, J. Symbolic Logic 78 (2013) 764–784 for a discussion of this notion). I'm not sure whether the analogous result about $\mathring\alpha$ in $V(\alpha)$ holds.
My intuition is that $\mathsf{RT}(\alpha)$ and $V(\alpha)$ should become “more and more classical” in some sense as $\alpha$ becomes more and more recursively large, but of course this can only be true in a limited sense as $\mathsf{RT}(\alpha)$ will never satisfy Excluded Middle (the uniform object $\nabla 2$ will never equal $2$), and in a more restricted sense this is trivial (e.g., the first-order theory of the natural numbers object $\mathbf{N}$ in $\mathsf{RT}(\alpha)$ or $V(\alpha)$ is simply true first-oder arithmetic as soon as $\alpha>\omega$, meaning $\alpha\geq\omega_1^{CK}$). But maybe I can ask about propositional logic or set theory:
Specific question 1: Is there a propositional formula (ideally a plain propositional formula, i.e., with only prenex universal quantification over $\Omega$, or perhaps a second-order propositional formula) which, interpreted in the internal language of $\mathsf{RT}(\alpha)$, hold for certain values of $\alpha$ but not all?
Specific question 2: Can we characterize the formulae of the language of $\mathsf{IZF}$ which are true on $V(\alpha)$ for closed-unboundedly many $\alpha$?
