$\neg\neg$-Stability

Question

I see that some authors say that there are sets, for example, $\mathbb{N}$ and $\mathsf{Bool}$, that are $\neg\neg$-stable (i.e., satisfying $\neg\neg X\rightarrow X$). I understand what it means when $X$ is a proposition, but what does it mean for a set (e.g., $\mathbb{N}$, $\mathsf{Bool}$) to be $\neg\neg$-stable? Thanks in advance!

Answer 1

Welcome to math.SE! Given the tags, (and the recent related question where the examples $\mathbb{N}$ and $\mathbf{Bool}$ came up), I will answer in the context of intuitionistic type theory. There are other, related notions of stability, e.g. in topological semantics, where certain sets can be stable; I will not touch upon these scenarios.

Under the propositions-as-types interpretation (see The HoTT Book, section 1.11), we identify each proposition $P$ with the type ($\approx$ collection) of all its proofs, and each type $S$ with the proposition that $S$ has an inhabitant ($\approx$ element). So each inhabitant of $S$ gives rise to a proof of the corresponding proposition. For example, the empty type $\bot$ can be seen as a false proposition: it is not provable, and viewed as a collection it has no inhabitants.

Under propositions-as-types, conjunctions $\wedge$ usually correspond to the formation of Cartesian product types $\times$, and implications to the formation function types $\rightarrow$. Negation is defined in terms of the empty type $\bot$ and function types: the expression $\neg S$ simply abbreviates the function type $S \rightarrow \bot$. This type has all functions with domain $S$ and codomain $\bot$ as inhabitants. For example, $\bot \rightarrow \bot$ has an inhabitant: the function $x \mapsto x$.

The type $\mathbb{N}$ of natural numbers corresponds to the proposition "$\mathbb{N}$ has inhabitants", and its inhabitants $0,1,2,\dots$ of the type $\mathbb{N}$ correspond to proofs of this proposition.

Putting everything together, the type $\neg\neg \mathbb{N}$ abbreviates the collection of functions $(\mathbb{N} \rightarrow \bot) \rightarrow \bot$. This type is inhabited, for example the function $f \mapsto f(12)$ inhabits it.

So what does it mean for $\mathbb{N}$ to be $\neg\neg$-stable? It means that the function type $\neg\neg \mathbb{N} \rightarrow \mathbb{N}$ has an inhabitant. This is easy to show: for example, the function $f \mapsto 51$ associates to every inhabitant $f$ of the type $\neg\neg \mathbb{N}$ an inhabitant of the type $\mathbb{N}$ (namely $51$) , so $f \mapsto 51$ inhabits the type $\neg\neg \mathbb{N} \rightarrow \mathbb{N}$.

In more sophisticated type theories, such as Homotopy Type Theory, people prefer to use subtler variants of the propositions-as-types interpretation, but the underlying idea remains the same: $\neg\neg$-stability of the type $S$ means that we can find an inhabitant of the type $((S \rightarrow \bot) \rightarrow \bot) \rightarrow S$.