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$.

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))