Inhabited set

In constructive mathematics, a set $A$ is inhabited if there exists an element $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 $A$ is if $\forall z (z \not \in A)$ while $A$ is if it is not empty, that is, if
\lnot forall z (z \not \in A)
It is if
$\exists z (z \in A).$

Every inhabited set is a nonempty set (because if $a \in A$ is an inhabitant of $A$ then $a \not\in A$ is false and consequently so is $\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 $X$ but does not satisfy "$X$ is inhabited". But it is possible to construct a Kripke model $M$ that satisfies "$X$ is nonempty" without satisfying "$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 "$X$ is nonempty" implies "$X$ is inhabited".

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

For example, consider a subset $X$ of $\$ specified by the following rule: $0$ belongs to $X$ if and only if the Riemann hypothesis is true, and $1$ belongs to $X$ if and only if the Riemann hypothesis is false. If we assume that Riemann hypothesis is either true or false, then $X$ is not empty, but any constructive proof that $X$ is inhabited would either prove that $0$ is in $X$ or that $1$ is in $X.$ Thus a constructive proof that $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).

See also

*
*

References

* D. Bridges and F. Richman. 1987. ''Varieties of Constructive Mathematics''. Oxford University Press.

{{PlanetMath attribution, id=5931, title=Inhabited set

Basic concepts in set theory
Concepts in logic
Constructivism (mathematics)
Mathematical objects
Set theory