In constructive mathematics, a set ${\displaystyle A}$ is inhabited if there exists an element ${\displaystyle a\in A.}$ In classical mathematics, this is the same as the set being nonempty; however, this equivalence is not valid in intuitionistic logic (or constructive logic).

Comparison with nonempty sets

In classical mathematics, a set is inhabited if and only if it is not the empty set. These definitions diverge in constructive mathematics, however. A set ${\displaystyle A}$ is empty if ${\displaystyle \forall z(z\not \in A)}$ while ${\displaystyle A}$ is nonempty if it is not empty, that is, if

${\displaystyle \lnot [\forall z(z\not \in A)].}$
It is inhabited if
${\displaystyle \exists z(z\in A).}$

Every inhabited set is a nonempty set (because if ${\displaystyle a\in A}$ is an inhabitant of ${\displaystyle A}$ then ${\displaystyle a\not \in A}$ is false and consequently so is ${\displaystyle \forall z(z\not \in A)}$). In intuitionistic logic, the negation of a universal quantifier is weaker than an existential quantifier, not equivalent to it as in classical logic so a nonempty set is not automatically guaranteed to be inhabited.

Example

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". But it is possible to construct a Kripke model ${\displaystyle M}$ that satisfies "${\displaystyle X}$ is nonempty" without satisfying "${\displaystyle X}$ is inhabited". Because an implication is provable in intuitionistic logic if and only if it is true in every Kripke model, this means that one cannot prove in this logic that "${\displaystyle X}$ is nonempty" implies "${\displaystyle X}$ is inhabited".

The possibility of this construction relies on the intuitionistic interpretation of the existential quantifier. In an intuitionistic setting, in order for ${\displaystyle \exists z\phi (z)}$ to hold, for some formula ${\displaystyle \phi }$, it is necessary for a specific value of ${\displaystyle z}$ satisfying ${\displaystyle \phi }$ to be known.

For example, consider a subset ${\displaystyle X}$ of ${\displaystyle \{0,1\))$ specified by the following rule: ${\displaystyle 0}$ belongs to ${\displaystyle X}$ if and only if the Riemann hypothesis is true, and ${\displaystyle 1}$ belongs to ${\displaystyle X}$ if and only if the Riemann hypothesis is false. If we assume that Riemann hypothesis is either true or false, then ${\displaystyle X}$ is not empty, but any constructive proof that ${\displaystyle X}$ is inhabited would either prove that ${\displaystyle 0}$ is in ${\displaystyle X}$ or that ${\displaystyle 1}$ is in ${\displaystyle X.}$ Thus a constructive proof that ${\displaystyle X}$ is inhabited would determine the truth value of the Riemann hypothesis, which is not known, By replacing the Riemann hypothesis in this example by a generic proposition, one can construct a Kripke model with a set that is neither empty nor inhabited (even if the Riemann hypothesis itself is ever proved or refuted).