nLab exhaustible set

Definition

In constructive mathematics, a set $A$ is exhaustible or omniscient if it satisfies a version of the limited principle of omniscience for the set $A$ rather than the natural numbers $\mathbb{N}$: For all functions $f$ from $A$ to the booleans $\{0, 1\}$, either there exists an element $x \in A$ such that $f(x) = 1$, or for all elements $x \in A$, $f(x) = 0$.

One can equivalently use decidable subsets instead of functions into the booleans. A set $A$ is exhaustible or omniscient if the existential quantification of any decidable proposition on $A$ is again decidable. That is,

$$(\forall x \in A, P(x) \vee \neg{P(x)}) \Rightarrow (\exists x \in A, P(x)) \vee \neg(\exists x \in A, P(x)) ,$$

or equivalently

$$(\forall x \in A, P(x) \vee \neg{P(x)}) \Rightarrow (\exists x \in A, P(x)) \vee (\forall x \in A, \neg{P(x)}) .$$

If you take the set $A$ to be the subsingleton corresponding to a given truth value and apply this principle to the constantly true proposition, then the subsingleton is decidable follows, since $\forall x \in A, P(x)$ holds, then either the subsingleton is inhabited, in which $\exists x \in A, P(x)$ holds, or the subsingleton is empty, in which $\forall x \in A, \neg P(x)$ holds. Thus, that every subsingleton is exhaustible implies $EM$; conversely, $EM$ implies that every set is exhaustible (over any domain). Note that propositions of the form $\exists x, P(x)$ when $P$ is decidable are the open truth values in the Rosolini dominance.

We can also state the principle set-theoretically: a set $A$ is exhaustible or omniscient if for all subsets $P \in \mathcal{P}(A)$, if $P$ is a decidable subset of $A$ ($P \cup \bar{P} = A$), then either $P$ is inhabited or $\bar{P} = A$, where $\bar{P}$ is the complement of $P$.

Examples

• the set $\mathbb{N}$ of natural numbers being exhaustible is the limited principle of omniscience,

• the set $\overline{\mathbb{N}}$ of extended natural numbers is provably exhaustible in constructive mathematics; see theorems 3.5 and 3.6 of Escardó 2013 for this. This is related to the fact that $\overline{\mathbb{N}}$ may constructively be given a compact topology.

• searchable sets are exhaustible by lemma 2.2 of Escardó 2013

Properties

This section appears to be original research, as there doesn’t seem to be any existing literature on these properties. Note that the material in this section originally appeared on the article limited principle of omniscience before being moved here, so please check that article for the history of this material.

Theorem

A set $A$ is exhaustible if and only if the function set $\mathbb{2}^A$ has decidable tight apartness, where the tight apartness relation on the function set $\mathbb{2}^A$ be defined as

$$f \# g \coloneqq \exists x \in A.f(x) \neq g(x)$$

Proof

Since the boolean domain is a boolean ring, the function set $\mathbb{2}^A$ is also a boolean ring via pointwise addition, subtraction and multiplication of boolean-valued functions. Thus, for functions $f$ and $g$ from $A$ to $\mathbb{2}$, the tight apartness relation on the function set $\mathbb{2}^A$, defined by

$$f \# g \coloneqq \exists x \in A.f(x) \neq g(x)$$

is logically equivalent to $\exists x \in A.f(x) - g(x) = 1$, since $f(x) \neq g(x)$ is logically equivalent to $f(x) = g(x) + 1$.

Suppose that $A$ is exhaustible holds. Then for functions $f$ and $g$ from $A$ to $\mathbb{2}$, define the function $h$ by $h(x) = f(x) - g(x)$ for all $x \in \mathbb{N}$. Then since $A$ being exhaustible says that $\exists x \in A.h(x) = 1$ is decidable, and $\exists x \in A.h(x) = 1$ is logically equivalent to $f \# g$, then $f \# g$ is decidable.

Conversely, assume that $f \# g$ is decidable. Then take $g$ to be the constant function at the boolean $0$, and $f \# \lambda x \in A.0$ is logically equivalently to $\exists x \in A.f(x) - 0 = 1$ and thus $\exists x \in A.f(x) = 1$. Since $f \# g$ is decidable, then $\exists x \in A.f(x) = 1$ is decidable, which is precisely that $A$ is exhaustible.

The next two statements relate a set $A$ being exhaustible with axioms that the tight apartness relation on certain other function sets are a decidable tight apartness.

Theorem

More generally, given a finite set $S$ of cardinality $n \gt 1$, a set $A$ is exhaustible if and only if that the function set $S^A$ has decidable tight apartness, where the tight apartness relation on the function set $S^A$ be defined as

$$f \# g \coloneqq \exists x \in A.f(x) \neq g(x)$$

Theorem

A set $A$ is exhaustible if and only if the function set $\mathbb{N}^A$ has decidable tight apartness, where the tight apartness relation on the function set $\mathbb{N}^\mathbb{N}$ be defined as

$$f \# g \coloneqq \exists x \in A.f(x) \neq g(x)$$

Exhaustible subsingletons and excluded middle

There is a constant function $x \mapsto 1$ from every subsingleton $A$ to the boolean domain $\mathbb{2}$ taking every element $x \in A$ to the boolean $1 \in \mathbb{2}$.

Theorem

Given a subsingleton $A$, suppose that $A$ is exhaustible: either there exists $x \in A$ such that $(x \mapsto 1)(x) = 1$, or for all $x \in A$, $(x \mapsto 1)(x) = 0$. Then $A$ is a decidable subsingleton.

Proof

We prove by case analysis.

Suppose that there exists $x:A$ such that $(x \mapsto 1)(x) = 1$. Then $A$ is a inhabited subsingleton and thus a decidable subsingleton.

Then suppose that for all $x:A$, $(x \mapsto 1)(x) = 0$. Then $A$ is empty and thus a decidable subsingleton.

This exhausts all options for decidable subsingletons, and exhausts all possible conditions in the hypothesis.

Theorem

Suppose that for sets $A$ and $B$ with decidable tight apartness relations, the tight apartness relation on the function set $B^A$, defined by $f \# g \coloneqq \exists x:A.f(x) \neq g(x)$, is decidable. Then excluded middle holds.

Proof

Every subsingleton $A$ has a decidable tight apartness relation where $x \# y$ is always false. The boolean domain $\mathbb{2}$ also has a decidable tight apartness relation where $x \# y$ is given by the denial inequality $x \neq y$. We proved earlier in the article that a set $A$ being exhaustible is equivalent to the tight apartness relation on the function set $\mathbb{2}^A$ being decidable, and every subsingleton $A$ being exhaustible implies that every subsingleton $A$ is a decidable subsingleton, which is precisely the condition of excluded middle.

There is also a constant function $x \mapsto 0$ from every subsingleton $A$ to the boolean domain $\mathbb{2}$ taking every element $x \in A$ to the boolean $0 \in \mathbb{2}$.

Theorem

Given a subsingleton $A$, suppose that either there exists $x \in A$ such that $(x \mapsto 1)(x) \neq (x \mapsto 0)(x)$, or for all $x \in A$, $(x \mapsto 1)(x) = (x \mapsto 0)(x)$. Then $A$ is a decidable subsingleton.

Proof

We prove by case analysis.

Suppose that there exists $x \in A$ such that $(x \mapsto 1)(x) \neq (x \mapsto 0)(x)$. Then $A$ is a inhabited subsingleton and thus a decidable subsingleton.

Then suppose that for all $x \in A$, $(x \mapsto 1)(x) = (x \mapsto 0)(x)$. Then $A$ is empty and thus a decidable subsingleton, since $(x \mapsto 1) = (x \mapsto 0)$ by function extensionality.

This exhausts all options for decidable subsingletons, and exhausts all possible conditions in the hypothesis.

In dependent type theory

In the context of dependent type theory, a type $A$ being exhaustible or omniscient is expressed as

$$\prod_{f:A \to \mathbb{2}} (\exists x:A.f(x) = 1) \vee \left(\prod_{x:A} f(x) = 0\right)$$

Note that $\prod_{x:A} f(x) = 0$ is always a proposition by weak function extensionality.

However, there are in general two ways of interpreting predicate logic, the traditional interpretation using propositional truncations, and the BHK interpretation which do not use propositional truncations. This results in four different interpretations of an exhaustible or omniscient type, depending on whether the existential quantifier is truncated or untruncated, and whether the disjunction is truncated or untruncated.

• When the disjunction is truncated and the existential quantifier is truncated, this results in the usual concept of an exhaustible or omniscient type $A$

• When the disjunction is untruncated and the existential quantifier is truncated, by using the sum type, this results in the concept of a $\exists$-compact type $A$ (Escardó 18)

$$\prod_{f:A \to \mathbb{2}} \left(\exists x:A.f(x) = 1\right) + \left(\prod_{x:A} f(x) = 0\right)$$

• When both the disjunction and the existential quantifier are untruncated, by using the sum type and dependent sum type, this results in the concept of a compact type $A$ (Escardó 11)

$$\prod_{f:A \to \mathbb{2}} \left(\left(\sum_{x:A} f(x) = 1\right) + \prod_{x:A} f(x) = 0\right)$$

• The case where the disjunction is truncated and the existential quantifier is untruncated remains undefined in the literature.

$$\prod_{f:\mathbb{N} \to \mathbb{2}} \left(\sum_{x:A} f(x) = 1\right) \vee \left(\prod_{x:A} f(x) = 0\right)$$

Note that Escardó 11 and Escardó 18 uses $\neg \sum_{x:A} f(x) = 1$ instead of $\prod_{x:A} f(x) = 0$. But one can show that $\neg \sum_{x:A} f(x) = 1$ is logically equivalent to $\prod_{x:A} \neg f(x) = 1$ in Martin-Lof type theory, see here for example, and $\neg f(x) = 1$ is $f(x) = 0$. In addition, the two sources define a decidable type using a sum type $A + \neg A$ rather than disjunction $A \vee \neg A$.

Related concepts

• limited principle of omniscience

References

• Martín Escardó: Exhaustible sets in higher-type computation, Logical Methods in Computer Science, Volume 4, Issue 3 (August 27, 2008) [doi:10.2168/LMCS-4(3-3)2008, arXiv:0808.0441v2]

• Martin Escardo: TypeTopology.CompactTypes, TypeTopology Agda library, web.

• Martín Escardó: Infinite sets that satisfy the principle of omniscience in any variety of constructive mathematics. The Journal of Symbolic Logic, Vol 78, September 2013, pp. 764-784. [doi:10.2178/jsl.7803040, pdf]

• Martin Escardo: TypeTopology.WeaklyCompactTypes, TypeTopology Agda library, web.