A scattered topos is the topos-theoretic analogue of a scattered topological space and therefore provides a natural environment for an internal interpretation of provability logic.

Definition

A topos $\mathcal{E}$ is called $\bot\negthinspace$-scattered if the subtopos $Sh_{\neg\neg}(\mathcal{E})$ of double negation sheaves is an open subtopos.

A topos $\mathcal{E}$ is called scattered if every closed subtopos of $\mathcal{E}$ is $\bot$-scattered.

Examples

Every Boolean topos$\mathcal{E}$ is $\bot$-scattered since it obviously coincides with $Sh_{\neg\neg}(\mathcal{E})$ and is open in itself (and closed as well). Accordingly, $\mathcal{E}$ is scattered since subtoposes of Boolean toposes are Boolean.

A simple example of a non-Boolean scattered topos is the Sierpinski topos$Set^\rightarrow$ that consists of two copies of $Set$glued together such that one copy corresponding to $Sh_{\neg\neg}(Set^\rightarrow)$ is open and the other one is closed. Since $Set^\rightarrow$ and the closed copy of $Set$ are both $\bot$-scattered the claim follows.

Properties

That the Sierpinski-topos is $\bot$-scattered is an instance of the more general fact that the topos $Sh(X)$ of sheaves on a $T_0$-space $X$ is $\bot$-scattered iff open points are dense in $X$ .^{1}