nLab topos of recursive sets

Idea

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.

Definition

Let $\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(\mathbb{N})$ whose covers consist of finite families of maps $(f_i:\mathbb{N}\to\mathbb{N} {}|{} 1\leq i \leq n)$ such that $\cup_i Im(f_i)=\mathbb{N}$.

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

Properties

Proposition

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

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

Proposition

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

For all $n\in \mathbb{N}^+$ there exists a finite recursive cover $A_1,\dots A_k$ such that for all $m_1, m_2$ in $A_i$ $(i=1,\dots,k)$, $|r_{m_2}-r_{m_1}|\lt 1/n$.

This is prop.4.1 in Mulry (1982).

Related entries

• Johnstone's topological topos

• bornological topos

• effective topos

• recursive function

References

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.