10
$\begingroup$

Reflective oracles are a kind of Turing oracle that give stochastic answers about the outputs of Turing machines. This works in a self-referential way, where they can answer queries about Turing machines that have access to the same reflective oracle. I recently wrote up some results involving reflective-oracle-computable functions. Now, I basically don't know any topos theory, but I get the sense from things like Andrej Bauer's work on synthetic computability theory that these theorems could probably be better expressed within the internal language of some topos.

Instead of describing my results directly, I'll now guess at what they would say when translated into the internal language of a suitable topos, since this will be nicer. My Theorem 1 should correspond to the existence of an internal surjection $\mathbb{N} \to [0,1]^\mathbb{N}$, and my Theorem 2 (Brouwer's fixed point theorem), should internalize to the existence of a map $\rm{fix} \colon ([0,1]^n)^{[0,1]^n} \to [0,1]^n$ such that for all $h \colon [0,1]^n \to [0,1]^n$, we have $h(\rm{fix}(h)) = \rm{fix}(h)$. This is all made possible by my Lemma 1, which has a less clear translation. I think it should correspond to something like a surjection $[0,1]_\bot \to [0,1]$, for some notion of the set of partial values $A_\bot$ of a set $A$ that would be more general than then one in Andrej's paper. (Andrej's is really only suitable for $A$ that feel more "discrete" than $[0,1]$.) All this seems to have a lot in common with Andrej's discussion of focal sets.

(That Theorem 2 follows from Theorem 1 is very related to a previous MO question on the relationship between the Lawvere and Brouwer fixed point theorems.)

Anyway, I am interested in knowing the following:

  1. Is there actually some topos, presumably something like a relativized effective topos, in which these results have a nice statement in the internal language?
  2. If such a topos were to exist, does topos theory have something new to say about reflective-oracle-computable functions? Do reflective-oracle-computable functions have something new to say about topos theory?
Improve this question
$\endgroup$
5
  • 2
    $\begingroup$ If you can find a topos in which there is an internal surjection $\mathbb{N} \to [0,1]$ then you will solve the open problem "can there be a topos with an internal surjection $\mathbb{N} \to \mathbb{R}$", and in fact such a topos will be rather amazing. It cannot satisfy countable choice (because countable choice implies there is no surjection $\mathbb{N} \to [0,1]$), so realizability toposes are not going to work. It cannot be a Boolean topos for the same reason. I looked but couldn't find it, nor do I have a proof that it doesn't exist. $\endgroup$
    – Andrej Bauer
    Commented Dec 1, 2017 at 13:20
  • $\begingroup$ @AndrejBauer Is this still open? $\endgroup$
    – James E Hanson
    Commented Feb 20, 2022 at 17:23
  • $\begingroup$ @JamesHanson: If you are referring to my comment, then yes, see this thread for a summary of what is known. $\endgroup$
    – Andrej Bauer
    Commented Feb 20, 2022 at 19:09
  • $\begingroup$ @AndrejBauer Ingo mentions that there is an intuitionistic proof that the MacNeille reals are uncountable. Is this written down somewhere? $\endgroup$
    – James E Hanson
    Commented Feb 20, 2022 at 19:50
  • $\begingroup$ @JamesHanson: arxiv.org/abs/1902.07366 $\endgroup$
    – Andrej Bauer
    Commented Feb 20, 2022 at 20:09

0

Reset to default

You must log in to answer this question.