Is there a correspondence between principles of omniscience and computability classes?

Question

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}$.

Answer 1

See Rathjen, Constructive Zermelo–Fraenkel set theory and the limited principle of omniscience for a proof that adding $\mathbf{LPO}$ to $\mathbf{CZF}$ does not change the consistency strength. This does indeed use a realizability model over $E$-recursive functions as in Hinman as part of the proof.

I think it should be possible to phrase some of this stuff in terms of subtoposes of the effective topos, although I would have to think some more to be sure. This is still a bit speculative. If you have a family of local operators $j_i : \Omega \to \Omega$ indexed over $i \in I$ you can take define the (internal) meet as $(\bigwedge_{i \in I} j_i)(p) := \forall i\,j_i(p)$. I think $\mathbf{LPO}$ will have the property of being stable under internal meets (in the sense that if it is forced by each local operator $j_i$, then it is forced by $\bigwedge_i j_i$). This would correspond to a largest subtopos of the effective topos that satisfies $\mathbf{LPO}$. If you look at which functions $\mathbb{N} \to \mathbb{N}$ are representable as morphisms from the natural number object to itself in the subtopos, I expect it would be exactly the hyperarithmetic ones. This is the same property that Van Oosten showed for Pitts' local operator, but it's not clear to me whether it is the same local operator, or just shares this property.