9
$\begingroup$

I'm presenting in final projects for my computability and computational topology courses on the connections between computability, continuity, and logic. As a mathematician/unmentored baby logician this correspondence was my large driver for taking these particular courses. For computability and logic I'll be discussing realizability, and for continuity and logic will be topological models like the topological topos as well as a discussion of Brouwerian continuity and its realizability. Domain theory I'm vaguely aware is one way of completing this triangle by connecting computability and topology, but as we haven't discussed dcpo's in any of the coursework and I have less personal background than with topos theory, I'll leave for future personal understanding.

So, then, I'm interested in filling this horn by looking for geometric morphisms between the topological topos TT and the effective topos Eff (perhaps generalize to realizability over more suitable PCAs but K1 would be desirable for this material). As this is to be a lit review I'd appreciate links to a paper where this is elaborated, if such has been written yet. While ad-hoc connections and nonexistence arguments are accessible (undecidability of nontrivial predicates on RR being to my knowledge the standard example), a systematic translation between these two semantics would be very interesting to present on. I'm aware of synthetic topology and my understanding of this approach is as an enrichment of constructive type theory, assuming a subdominance of the type of propositions to define internal versions of topological notions, an approach I'm interested in and that connects with computation via program termination. Can such be externalized to a morphism from Eff to TT? can one go the other direction as well, and, assuming from my current knowledge of realizability the existence in Eff of nonterminating/"divergent" functions, what would then be the semantics of divergent programs w.r.t. such a topological interpretation?

Improve this question
$\endgroup$
4
  • 3
    $\begingroup$ There can't be a geometric morphism $f:Eff \to TT$ that's for sure. $f^*$ would preserve NNO (because $f^*$ always does) and as TT is a Grothendieck topos every function $N \to N$ is defined on the NNO of TT. But in EFF only computable functions acts on the NNO... $\endgroup$
    – Simon Henry
    Commented Apr 13 at 21:55
  • 3
    $\begingroup$ To clarify slightly: every external function (i.e. in Set) $\mathbb{N}\to \mathbb{N}$ gives an endofunction on the NNO of $TT$. $\endgroup$
    – David Roberts ♦
    Commented Apr 13 at 23:25
  • 1
    $\begingroup$ I have a recollection of listening to a lecture by Peter Johnstone in which he stated that every geometric morphism from a Grothendieck topos to a ealizability topos factors trough Set. Or perhaps I got the directions reversed? Anyhow, you should stop looking for a geometric morphism of this kind and instead prove they're all trivial, or not even there. $\endgroup$
    – Andrej Bauer
    Commented Apr 14 at 9:18
  • 4
    $\begingroup$ Here is a thing you could do, in lieu the geometric morphisms which likely don't exist/are trivial: Internally to the effective topos, you could construct a (suitable version of) the topological topos. That would basically amount to rereading the account of TT, but now not in a metatheory such as ZFC or IZF, but using Russian-style constructivism as the metatheory (with its formal Church–Turing thesis, every function $\mathbb{N} \to \mathbb{N}$ is Turing-computable). You could also do it the other way round. $\endgroup$
    – Ingo Blechschmidt
    Commented Apr 14 at 10:50

1 Answer 1

Reset to default
11
$\begingroup$

There is no geometric morphism $f : E \to F$ if $E$ is a realizaiblity topos and $F$ is a Grothendieck topos. Indeed, if we had such an $f$, then for any indexing set $I$, the topos $E$ would have the $I$-fold coproduct $\coprod_I 1$ of terminal objects: such a coproduct exists in $F$ and $f^*$ will carry it over to $E$, as it preserves the terminal object and coproducts. Taking $I$ to be the underlying pca of $E$ shows that this is impossible by a cadinality argument, see also the notion of width in Lemma 2.11 in Sheaf toposes for realizability, PDF here. Come to think of it, the paper might be of some independent interst to you.

Regarding the opposite direction, I once heard Peter Johnstone state that every geometric morphism from a Grothendieck topos to a realizability topos factors through $(\Gamma \dashv \nabla) : \mathsf{Set} \to \mathsf{RT}(A)$, but I cannot remember why (I was too young to understand much of Peter Johnstone anyway).

A topos that combines computability and topology in a particularly nice way is the Kleene-Vesley topos $\mathsf{RT}(\mathbb{N}^\mathbb{N}, (\mathbb{N}^\mathbb{N})_\mathsf{eff})$, and a slightly less nice one is $\mathsf{RT}(\mathcal{P}(\mathbb{N}), \mathsf{RE})$, see my PhD thesis or these unfinished notes on realizability.

Improve this answer
$\endgroup$
0

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .