Shirt a Phobia

In mathematics, the effective topos ${\mathsf {Eff}}$ introduced by Martin Hyland (1982) captures the mathematical idea of effectivity within the category theoretical framework.

Preliminaries

Kleene realizability

The topos is based on the partial combinatory algebra given by Kleene’s first algebra ${\mathcal {K}}_{1}$ . In Kleene’s notion of recursive realizability, any predicate is assigned realizing numbers, i.e. a subset of ${\mathbb {N} }$ . The extremal propositions are $\top$ and $\bot$ , realized by ${\mathbb {N} }$ and $\{\}$ . However in general, this process assigns more data to a proposition than just a binary truth value.

A formula with $k$ free variables will give rise to a map in $({\mathcal {P}}{\mathbb {N} })^{{\mathbb {N} }^{k}}$ the values of which are the subsets of corresponding realizing numbers.

Realizability topoi

${\mathsf {Eff}}$ is a prime example of a realizability topos. These are a class of elementary topoi with an intuitionistic internal logic and fulfilling a form of dependent choice. They are generally not Grothendieck topoi.

In particular, the effective topos is ${\mathsf {RT}}({\mathcal {K}}_{1})$ . Other realizability topos constructions can be said to abstract away some aspects played by ${\mathbb {N} }$ here.

Definition

There are several ways to construct the effective topos, for example, via the notion of tripos, or as the ex/reg completion of the category of assemblies. The following is a fully unfolded explicit definition.^[1]^: 115

An object of the effective topos is a set $X$ equipped with a function $E:X^{2}\to {\mathcal {P}}(\mathbb {N} )$ satisfying certain conditions. We denote $n\in E(x,y)$ by $n\Vdash x=y$ . (The notation is not standardized; the usage of the $=$ symbol overloads its normal meaning, similarly to the notation $P(X=Y)$ in probability theory.) Informally, this means that $n$ is a computational witness, or realizer of the equality $x=y$ . The conditions to be satisfied are the following:

There must exist a program $e$ such that for all $n\in \mathbb {N}$ and $x,y\in X$ , if $n\Vdash x=y$ then the output of $e$ on $n$ , i.e., $\phi _{e}(n)$ (where $\phi _{e}$ is the $e$ -th partial computable function), is defined, and $\phi _{e}(n)\Vdash y=x$ . In short, $e$ takes a realizer of $x=y$ and outputs a realizer of $y=x$ (for all $x,y$ ). (Note that $e$ cannot depend on $x,y$ , and it only receives the realizer of $x=y$ as input, without further information on $x$ and $y$ .)
Similarly, there must exist a program which takes a realizer of $x=y$ and a realizer of $y=z$ , and outputs a realizer of $x=z$ (for all $x,y,z$ ).

A realizer of $x=x$ will be called more simply a realizer of $x$ .

A functional relation from an object $X$ to an object $Y$ is a function $f:X\times Y\to {\mathcal {P}}(\mathbb {N} )$ , again satisfying certain conditions. We suggestively denote $n\in f(x,y)$ by $n\Vdash f(x)=y$ (again, this is a special notation; $f(x)$ has no meaning by itself). This informally means that $n$ realizes the fact that $f$ sends $x$ to $y$ , or “realizes $f(x)=y$ ”. The conditions are the following:

There exists a program which takes a realizer of $f(x)=y$ and outputs a realizer of $x$ and a realizer of $y$ (for all $x\in X,y\in Y$ ).
There exists a program which takes a realizer of $f(x)=y$ and realizers of $x=x'$ and $y=y'$ , and outputs a realizer of $f(x')=y'$ (for all $x,x',y,y'$ ).
There exists a program which takes realizers of $f(x)=y$ and $f(x)=y'$ , and outputs a realizer of $y=y'$ (for all $x,y,y'$ ).
There exists a program $e$ such that for all $x\in X$ and for all realizer $n$ of $x$ , there exists some $y\in Y$ such that the output $\phi _{e}(n)$ realizes $f(x)=y$ .

Suppose $f$ is a functional relation from $X$ to $Y$ and $g$ is a functional relation from $Y$ to $Z$ . The composition $g\circ f$ is the functional relation from $X$ to $Z$ defined by letting the realizers of $(g\circ f)(x)=z$ be the codes of pairs $(r,s)$ such that, for some $y\in Y$ , we have $r\Vdash f(x)=y$ and $s\Vdash g(y)=z$ . The identity functional relation $\operatorname {id}$ on an object $X$ is defined by letting the realizers of $\operatorname {id} (x)=y$ be just the realizers of $x=y$ .

The morphisms from $X$ to $Y$ in the effective topos are the functional relations from $X$ to $Y$ , quotiented to identify $f$ and $g$ when there exists a program which maps realizers of $f(x)=y$ to realizers of $g(x)=y$ (for all $x,y$ ), and another program which maps realizers of $g(x)=y$ to realizers of $f(x)=y$ . Composition of morphisms is induced on the quotients by composition on the level of functional relations, and likewise for identity morphisms.

Relationship to assemblies

The effective topos arises as a completion of the simpler category of assemblies.

An assembly is a set $X$ equipped with a function $R:X\to {\mathcal {P}}(\mathbb {N} )$ . We denote $n\in R(x)$ by $n\Vdash x$ , read “ $n$ realizes $x$ ”. Every assembly $X$ can be construed as an object of the effective topos, by declaring that $n$ realizes $x=y$ when $x$ and $y$ are actually equal and $n$ realizes them in the assembly $X$ . (Thus, the realizers of $x$ in $X$ as an object of the effective topos, i.e., the realizers of $x=x$ , are exactly the realizers of $x$ in $X$ as an assembly.)

A morphism of assemblies $f:X\to Y$ is a function $f:X\to Y$ between the underlying sets such that there exists a program, independent of $x\in X$ , which maps realizers of $x$ to realizers of $f(x)$ . Such a morphism gives rise to a morphism in the effective topos, represented by the functional relation (still denoted $f$ ) where $f(x)=y$ is realized if and only if $f(x)$ is actually equal to $y$ , and then the realizers of $f(x)=y$ are the pairs of a realizer of $x$ and a realizer of $y$ .

This correspondence makes the category of assemblies a full subcategory of the effective topos.

The category of sets is a full subcategory of the category of assemblies, via the functor $\nabla$ that maps a set $X$ to the assembly with underlying set $X$ where every element is realized by every natural number. In particular, the category of sets is also a full subcategory of the effective topos.^[1]^: 117

Categorical operations in the effective topos

The effective topos is an elementary topos with natural numbers object. This means that it supports a number of standard categorical constructions, which are explicitly performed as follows.

The initial object is the empty assembly.
The terminal object is the unit assembly, a singleton where the unique element is realized by every natural number.
The natural numbers object is $\mathbb {N}$ where each natural number is realized only by itself.
The product of two objects $X$ and $Y$ is the Cartesian product of sets $X\times Y$ where a realizer of $(x,y)$ in $X\times Y$ is the code of a pair of a realizer of $x$ and a realizer of $y$ .
The coproduct of $X$ and $Y$ is the coproduct of sets $X+Y$ where a realizer of $x\in X$ in $X+Y$ is the code of a pair of 0 and a realizer of $x$ in $X$ , and a realizer of $y\in Y$ in $X+Y$ is the code of a pair of 1 and a realizer of $y$ in $Y$ .
The subobject classifier $\Omega$ is ${\mathcal {P}}(\mathbb {N} )$ where a realizer of $P=Q$ is a pair of a program which returns an element of $Q$ given an element of $P$ , and a program which returns an element of $P$ given an element of $Q$ . It is not (isomorphic to) an assembly.

Properties

Relation to Sets

Some objects exhibit a rather trivial existence predicate depending only on the validity of the equality relation “ $=$ ” of sets, so that valid equality maps to the top set $\mathbb {N}$ and rejected equality maps to $\{\}$ . This gives rise to a full and faithful functor $\nabla \colon {\mathsf {Sets}}\to {\mathsf {Eff}}$ out of the category of sets, which has the finite-limit preserving global sections functor $\Gamma$ as its left-adjoint. This factors through a finite-limit preserving, full and faithful embedding $\omega$ – ${\mathsf {Sets}}\to {\mathsf {Eff}}$ .

NNO

The topos has a natural numbers object $N=\langle {\mathbb {N} },E_{\mathbb {N} }\rangle$ with simply $E_{\mathbb {N} }(n)=\{n\}$ . Sentences true about $N$ are exactly the recursively realized sentences of Heyting arithmetic ${\mathsf {HA}}$ .

Now arrows $N\to N$ may be understood as the total recursive functions and this also holds internally for $N^{N}$ . The latter is the pair given by total recursive functions $\mathrm {TR}$ and a relation such that $E_{\mathrm {TR} }(f)$ is the set of codes $e\in {\mathbb {N} }$ for $f$ . The latter is a subset of the naturals but not just a singleton, since there are several indices computing the same recursive function. So here the second entry of the objects represent the realizing data.

With $N$ and functions from and to it, as well as with simple rules for the equality relations when forming finite products $\times$ , one may now more broadly define the hereditarily effective operations. Again one may think of functions in $N^{N}$ as given by indices and their equality is determined by the objects that compute the same function. This equality clearly puts a constraint on $N^{(N^{N})}$ , as these functions come out to be only those computable functions that also properly respect the mentioned equality in their domain. Et cetera. The situation for general $\langle X,E_{X}\rangle \to \langle Y,E_{Y}\rangle$ , equality (in the sense of the $E$ ‘s) in domain and image must be respected.

Properties and principles

With this, one may validate Markov’s principle ${\mathrm {MP} }$ and the extended Church’s principle ${\mathrm {ECT} }_{0}$ (and a second-order variant thereof), which come down to simple statement about object such as $N^{N}$ or $(1+1)^{N}$ . These imply ${\mathrm {CT} }_{0}$ and independence of premise ${\mathrm {IP} }_{0}$ .

A choice principle $N^{N}$ related to Brouwerian weak continuity fails. From any object, there are only countably many arrows to $N$ . $\Omega ^{N}$ fulfills a uniformity principle. $N$ is not the countable coproduct of copies of $1$ . This topos is not a category of sheaves.

Analysis

The object $\langle {\mathbb {Q} }^{\mathbb {N} },E_{{\mathbb {Q} }^{\mathbb {N} }}\rangle$ is effective in a formal sense and from it one may define computable Cauchy sequences. Through a quotient, the topos has a real numbers object which has no non-trivial decidable subobject. With choice, the notion of Dedekind reals coincides with the Cauchy one.

Properties and principles

Analysis here corresponds to the recursive school of constructivism. It rejects the claim that $x\leq 0\lor 0\leq x$ would hold for all reals $x$ . Formulations of the intermediate value theorem fail and all functions from the reals to the reals are provenly continuous. A Specker sequence exists and then Bolzano–Weierstrass fails.

References

^ ^a ^b Jaap van Oosten (2008). Realizability: an introduction to its categorical side. Elsevier Science. ISBN 9780444515841.

Hyland, J. M. E. (1982), “The effective topos” (PDF), in Troelstra, A. S.; Dalen, D. van (eds.), The L.E.J. Brouwer Centenary Symposium (Noordwijkerhout, 1981), Studies in Logic and the Foundations of Mathematics, vol. 110, Amsterdam: North-Holland, pp. 165–216, doi:10.1016/S0049-237X(09)70129-6, ISBN 978-0-444-86494-9, MR 0717245
Kleene, S. C. (1945). “On the interpretation of intuitionistic number theory”. Journal of Symbolic Logic. 10 (4): 109–124. doi:10.2307/2269016. JSTOR 2269016. S2CID 40471120.
Phoa, Wesley (1992). An introduction to fibrations, topos theory, the effective topos and modest sets (Technical report). Laboratory for Foundations of Computer Science, University of Edinburgh. CiteSeerX 10.1.1.112.4533. ECS-LFCS-92-208.
Bernadet, Alexis; Graham-Lengrand, Stéphane (2013). “A simple presentation of the effective topos”. arXiv:1307.3832 [cs.LO].
Corfield, David; Ramesh, Sridhar; Schreiber, Urs; Bartels, Toby; Škoda, Zoran; Shulman, Mike; Trimble, Todd; Roberts, David; Holder, Thomas (January 22, 2023) [July 10, 2009], effective topos (19 ed.), nLab

[rdp-we-cite_note-van-oosten-1] Jaap van Oosten (2008). Realizability: an introduction to its categorical side. Elsevier Science. ISBN 9780444515841.

[1]

Sample Page

Preliminaries

Kleene realizability

Realizability topoi

Definition

Relationship to assemblies

Categorical operations in the effective topos

Properties

Relation to Sets

NNO

Properties and principles

Analysis

Properties and principles

See also

References