topos of recursive sets



Topos Theory

topos theory



Internal Logic

Topos morphisms

Extra stuff, structure, properties

Cohomology and homotopy

In higher category theory




The topos of recursive sets, or, for short, the recursive topos , is a Grothendieck topos \mathcal{R} that provides a cartesian closed context to do higher order recursion theory in. It can be viewed as a discrete analogue to the topological topos.


Let R\mathbf{R} be the monoid of all total recursive functions \mathbb{N}\to\mathbb{N} under concatenation viewed as a category with one object \mathbb{N}. Consider the coverage J()J(\mathbb{N}) whose covers consist of finite families of maps (f i:|1in)(f_i:\mathbb{N}\to\mathbb{N} {}|{} 1\leq i \leq n) such that iIm(f i)=\cup_i Im(f_i)=\mathbb{N}.

The recursive topos is defined as =Sh(R,J)\mathcal{R}=Sh(\mathbf{R}, J).



\mathcal{R} is a local topos i.e. the global section functor Γ:Set\Gamma:\mathcal{R}\to Set has a right adjoint: ΓB:Set\Gamma\dashv B: Set\to \mathcal{R}.

This appears as prop.1.5 in Mulry (1982). BB maps a set XX to the sheaf X X^{\mathbb{N}} of sequences of elements in XX.


The object D\mathbb{R}_D of Dedekind real numbers corresponds to the sheaf of sequences of real numbers r n\langle r_n\rangle satisfying:

For all n +n\in \mathbb{N}^+ there exists a finite recursive cover A 1,A kA_1,\dots A_k such that for all m 1,m 2m_1, m_2 in A iA_i (i=1,,k)(i=1,\dots,k), |r m 2r m 1|<1/n|r_{m_2}-r_{m_1}|\lt 1/n.

This is prop.4.1 in Mulry (1982).


The recursive topos was introduced in

  • P. S. Mulry?, Generalized Banach-Mazur functionals in the topos of recursive sets , JPAA 26 (1982) pp.71-83.

A comparison with the effective topos is in chapter 6 of

  • Giuseppe Rosolini, Continuity and Effectiveness in Topoi , PhD thesis University of Oxford 1986. (ps)

See also

  • Peter Johnstone, Sketches of an Elephant vol. I, Oxford UP 2002. (example A2.1.11(k), p.81)

  • F. William Lawvere, Diagonal arguments and cartesian closed categories , pp.134-145 in LNM 92 Springer Heidelberg 1969. (Reprinted with author’s commentary as TAC Reprint 15 (2006))

  • P. S. Mulry?, Adjointness in recursion ,

    APAL 32 (1986), pp.281–289.

  • P. S. Mulry?, A categorical approach to the theory of computation ,

    APAL 43 (1989), pp.293–305.

  • P. S. Mulry?, Partial map classifiers and partial cartesian closed categories , Theor. Comp. Sci. 136 (1994) pp.109–123.

Last revised on November 2, 2016 at 14:22:54. See the history of this page for a list of all contributions to it.