Inhabited set


In constructive mathematics, a set 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 setsEdit

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   is empty if   while   is nonempty if it is not empty, that is, if

It is inhabited if

Every inhabited set is a nonempty set (because if   is an inhabitant of   then   is false and consequently so is  ). 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.


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   but does not satisfy "  is inhabited". But it is possible to construct a Kripke model   that satisfies "  is nonempty" without satisfying "  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 "  is nonempty" implies "  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   satisfying   to be known.

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


  • 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.