My question will be speculative and therefore a little vague.

I wonder if attempts have been made to define a correspondence between, on the one hand, *limited principles of omniscience* that can be added to some form of constructive mathematics (perhaps second-order Heyting arithmetic) and, on the other hand, *computability classes* (in classical logic) defined by means of computability relative to some higher-type functional.

In order to be somewhat less vague, let me give an example of what I expect such a program would place in correspondence:

The “Limited Principle of Omniscience” (LPO) is the statement (which is a triviality in classical logic) that if $f \colon \mathbb{N} \to \{0,1\}$ then

*either*$\exists n.f(n)=0$*or*$\forall n.f(n)=1$.In the context of classical computability theory, the type-2 functional $\mathsf{E}$ is the function $\{0,1\}^{\mathbb{N}} \to \{0,1\}$ defined by $\mathsf{E}(f) = 0$ if $\exists n.f(n)=0$ and $\mathsf{E}(f) = 1$ if $\forall n.f(n)=1$ (precisely because the LPO holds in classical logic, $\mathsf{E}$ is

*total*): see Hinman,*Recursive-Theoretic Hierarchies*(1978), p. 262. We can then develop a theory of computability relative to this functional, with the classical result that the functions $\mathbb{N}\to\mathbb{N}$ computable in $\mathsf{E}$ are precisely the ones which are hyperarithmetical ($\Delta^1_1$): Hinman,*op. cit.*, theorem 1.8 (p. 267). (Also, there is an ordinal associated to the situation, namely the Church-Kleene ordinal.)

Now it's not just that the LPO and the $\mathsf{E}$ described above look a lot the same: in one direction, the LPO asserts that $\mathsf{E}$ is total, and in the other direction, if we form the topos analogous to the effective topos but starting from functions computable in $\mathsf{E}$ (as partial combinatorial algebra), we should obtain a topos which validates the LPO. (I say “should” because I didn't check this too carefully: it seems intuitively clear, but maybe there's a hidden gotcha that I missed. There is certainly some relation with the situation described in this paper by van Oosten, but sadly no mention is made there of LPO.)

So I would expect this hypothetical correspondence to pair LPO with functions computable in $\mathsf{E}$. Similarly, I would expect it to pair $\mathsf{E}_1$ (defined in Hinman, *op. cit.*, p. 263, and associated with the first computably inaccessible ordinal) with the statement that “every binary tree is either finite or has an infinite branch”. And perhaps it might go below Church-Turing computability and associate the latter with Markov's principle (which holds in the effective topos and appears to be related to Kleene's unbounded search operator).

Does this make sense? Have there been attempts to establish such a correspondence? Are there obvious stumbling blocks which would make it unrealistic? Or is this, perhaps, a banal idea which many have thought of before (I can hardly claim that pointing the analogy between LPO and $\mathsf{E}$ is a deep insight!), but which nobody knows how to formalize?

**PS:** While writing this question, I noticed this preprint by Takyuki Kihara which seems very much related to what I'm asking for, except that the author seems to consider *oracles* (computability in functions $\mathbb{N}\to\mathbb{N}$), not higher-type functionals such as $\mathsf{E}$.