Inhabited set

A set ${\displaystyle A}$ has the property of being empty if ${\displaystyle \forall z.(z\notin A)}$, or equivalently ${\displaystyle \neg \exists z.(z\in A)}$. Here ${\displaystyle z\notin A}$ stands for the negation ${\displaystyle \neg (z\in A)}$.

A set ${\displaystyle A}$ is non-empty if it is not empty, that is, if ${\displaystyle \neg \forall z.(z\notin A)}$, or equivalently ${\displaystyle \neg \neg \exists z.(z\in A)}$.

Sets such as ${\displaystyle \{2,3,4,7\}}$ or ${\displaystyle \mathbb {Q} }$ are inhabited, as e.g. witnessed by ${\displaystyle 3\in \{2,3,4,7\}}$. The set ${\displaystyle \{\}}$ is empty and thus not inhabited. Naturally, the example section thus focuses on non-empty sets that are not provably inhabited.

It is easy to give examples for any simple set theoretical property, because logical statements can always be expressed as set theoretical ones, using an axiom of separation. For example, with a subset ${\displaystyle S\subset \{0\}}$ defined as ${\displaystyle S:=\{n\in \{0\}\mid P\}}$, the proposition ${\displaystyle P}$ may always equivalently be stated as ${\displaystyle 0\in S}$. The double-negated existence claim of an entity with a certain property can be expressed by stating that the set of entities with that property is non-empty.

Define a subset ${\displaystyle A\subset \{0,1\}}$ via

${\displaystyle A:=\{n\in \{0,1\}\mid (P\land n=0)\lor (\neg P\land n=1)\}}$

Clearly ${\displaystyle P\leftrightarrow 0\in A}$ and ${\displaystyle (\neg P)\leftrightarrow 1\in A}$, and from the principle of non-contradiction one concludes ${\displaystyle \neg (0\in A\land 1\in A)}$. Further, ${\displaystyle (P\lor \neg P)\leftrightarrow (0\in A\lor 1\in A)}$ and in turn

${\displaystyle (P\lor \neg P)\to \exists$ !(n\in \{0,1\}).n\in A}

Already minimal logic proves ${\displaystyle \neg \neg (P\lor \neg P)}$, the double-negation for any excluded middle statement, which here is equivalent to ${\displaystyle \neg (0\notin A\land 1\notin A)}$. So by performing two contrapositions on the previous implication, one establishes ${\displaystyle \neg \neg \exists$ !(n\in \{0,1\}).n\in A} . In words: It cannot consistently be ruled out that exactly one of the numbers ${\displaystyle 0}$ and ${\displaystyle 1}$ inhabits ${\displaystyle A}$. In particular, the latter can be weakened to ${\displaystyle \neg \neg \exists n.n\in A}$, saying ${\displaystyle A}$ is proven non-empty.

As example statements for ${\displaystyle P}$, consider the consistency of the theory at hand, an infamous provenly theory-independent statement such as the continuum hypothesis, or, informally, an unknowable claim about the past or future. By design, these are chosen to be unprovable. A variant of this is to consider mathematiacal propositions that are merely not yet established - see also Brouwerian counterexamples. Knowledge of the validity of either ${\displaystyle 0\in A}$ or ${\displaystyle 1\in A}$ is equivalent to knowledge about ${\displaystyle P}$ as above, and cannot be obtained. As neither ${\displaystyle P}$ nor ${\displaystyle \neg P}$ can be proven in the theory, it will also not prove ${\displaystyle A}$ to be inhabited by some particular number. Further, a constructive framework with the disjunction property then cannot prove ${\displaystyle P\lor \neg P}$ either. There is no evidence for ${\displaystyle 0\in A}$, nor for ${\displaystyle 1\in A}$, and constructive unprovability of their disjunction reflects this. Nonetheless, since ruling out excluded middle is provenly always inconsistent, it is also established that ${\displaystyle A}$ is not empty. Classical logic adopts ${\displaystyle P\lor \neg P}$ axiomatically, spoiling a constructive reading.

The full axiom of choice is independent of ${\displaystyle {\mathsf {ZF}}}$ and provenly not constructively compatible with other common set theory axioms. So a theory including these axioms that does not permit excluded middle does also not validate that function existence principle.

In ${\displaystyle {\mathsf {ZF}}}$, the choice axiom is equivalent to the statement that for every vector space there exists basis. So more concretely, consider the question of existence of a Hamel bases of the real numbers over the rational numbers. Such an object is elusive in the sense that are different ${\displaystyle {\mathsf {ZF}}}$ models that either negate and validate its existence. So it is also consistent to just postulate that existence cannot be ruled out here, in the sense that it cannot be negated. Again, that postulate may be expressed as saying that the set of such Hamel bases is non-empty.

Because inhabited sets are the same as nonempty sets in classical logic, it is not possible to produce a model in the classical sense that contains a nonempty set ${\displaystyle X}$ but does not satisfy "${\displaystyle X}$ is inhabited".

However, it is possible to construct a Kripke model ${\displaystyle M}$ that differentiates between the two notions. Since an implication is true in every Kripke model if and only if it is provable in intuitionistic logic, this indeed establishes that one cannot intuitionistically prove that "${\displaystyle X}$ is nonempty" implies "${\displaystyle X}$ is inhabited".