How are halting oracles related to set theory?

By the Curry Howard isomorphism, constructive type theory and computation are intimately related to mathematical logic and proofs. Moreover, type theory gives us a nice framework for describing mathematical constructions in an explicit manner, which is difficult to do with standard foundations. This deficiency in standard foundations leads to issues in ZFC such as the Banach Taski paradox, where we can use a non-constructive existence proof to prove an object "exists" that is impossible to construct. That is, Banach Taski is an "intangible" construction.

This got me thinking -- Is there some sense in which a result such as the Banach Taski paradox could be interpreted under the Curry Howard isomorphism as a construction that would be possible with access to a halting oracle? This would in some sense make formal the concept that the axiom of choice allows us to make certain "infinitary constructions" that otherwise would not be possible, by the nature of making uncountably many choices.

Terry Tao offers similar thoughts in one of his blog posts where he uses oracles in an informal construction to relate set theory to computation, and makes the statement:

"Finally one can allow constructions indexed by arbitrary ordinals (i.e. transfinite induction) and arrays of arbitrary infinite size, at which point the theory becomes more or less indistinguishable from standard set theory."

My question is, is there anywhere where this observation has been made precise -- formally relating set theories with an infinitary choice principle such as ZFC to the use of oracles in constructions? Specifically, I'd also be interested to know how different oracles for undecidable problems like halting oracles relate to different axioms such as $LEM$, $AC$, and $AC_\omega$. For example, what axioms would use of a halting oracle in a construction be equivalent to under this equivalence that Tao mentions between use of oracles and set theory?

• I don't understand the close votes. This is a clear question, necessarily vague because it's asking for whether there is something known about the relation between oracle TMs and set-theoretic axioms. – user21820 Mar 21 '16 at 2:35
• I don't know much but one can consider the axiom of choice as using memoization in a functional programming language. This works even when instantiating an existential quantifier results in an object drawn from a random distribution. However, any question about a memoized function's global behaviour then requires knowing the precise way in which the inbuilt memoization works. Alternatively, if the underlying logic is sufficiently constructive and maps existential quantifiers to functions or at least oracles it would automatically give AC. Note that Skolemization is essentially AC. – user21820 Mar 21 '16 at 2:53
• Sure, the axiom of choice can be seen as an oracle. You input a set, and it gives you an element. Just like an oracle might be able to take a Turing machine and an input and tell you what the output (if any) might be. But formally relating them? I'm not sure what you mean by "formally" here, because "formally" implies "precisely" and the question, as noted by @user21820, is inherently vague. – Asaf Karagila Mar 21 '16 at 8:21
• @AsafKaragila: Yea I was thinking the asker might be looking for 1-to-1 correspondences, like the connection between the arithmetical hierarchy and Turing degrees, or the polynomial hierarchy (defined by oracles) and polynomial-bounded quantifier depth. – user21820 Mar 21 '16 at 9:30
• Well now that I read the question again, it seems at least part of it is answered by my comment (and the wikipedia articles) since the halting problem is the first Turing jump. – user21820 Mar 21 '16 at 9:32

When talking about the Curry-Howard correspondence, there's an intuitive aspect (proofs are programs) but also a formal one (terms of some calculus corresponds to proofs in a a specific logical system, e.g. there's an isomorphism between simply typed $\lambda$-calculus and natural deduction). So there are ways to make formal connections between very high-level mathematical concepts, but they can become very complex (see the difference between the first parenthesis and the second parenthesis), so to guide intuitions the discussion is generally kept informal. Here are two examples of formal connections between the two: