Contents

topos theory

# Contents

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

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

• 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 18:22:54. See the history of this page for a list of all contributions to it.