In constructive mathematics, a set *A* is **inhabited** if there exists an element . 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 *nonempty* if it is not empty, that is, if

It is *inhabited* if

In intuitionistic logic, the negation of a universal quantifier is weaker than an existential quantifier, not equivalent to it as in classical logic.

## 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 to hold, for some formula , it is necessary for a specific value of *z* satisfying to be known.

For example, consider a subset *X* of {0,1} 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).

## References

- D. Bridges and F. Richman. 1987.
*Varieties of Constructive Mathematics*. Oxford University Press. ISBN 978-0-521-31802-0

*This article incorporates material from Inhabited set on PlanetMath, which is licensed under the Creative Commons Attribution/Share-Alike License.*