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?

  • 1
    $\begingroup$ 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. $\endgroup$ – user21820 Mar 21 '16 at 2:35
  • $\begingroup$ 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. $\endgroup$ – user21820 Mar 21 '16 at 2:53
  • $\begingroup$ 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. $\endgroup$ – Asaf Karagila Mar 21 '16 at 8:21
  • 1
    $\begingroup$ @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. $\endgroup$ – user21820 Mar 21 '16 at 9:30
  • $\begingroup$ 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. $\endgroup$ – 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:

  • Krivine's realizability. In particular, a lot of work has been done to provide a realizability interpretation for the axiom of choice. You can get an overview of this work in Thomas Streicher's "Krivine’s Classical Realizability from a Categorical Perspective".

  • Damiano Mazza's work in implicit complexity. He precisely studied functional characterization of computational complexity classes that are typically defined through bounded Turing machines, and how the presentations as machines with Oracle tape can influence the design of a corresponding computational calculus. See for example "Parsimonious Types and Non-uniform Computation".

The first one is probably what you are looking for.

  • $\begingroup$ After looking into the matter, I think that reliability is really what I'm looking for here. In addition to your citation, I recently stumbled upon this paper by Andrej Bauer, which even touches on a few of my specific questions. Though, I would certainly like to see some more detail, this is a good start. $\endgroup$ – Nathan BeDell Mar 31 '16 at 23:18

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.