Inhabited set

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

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.

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 ${\displaystyle \exists z\phi (z)}$ to hold, for some formula ${\displaystyle \phi }$, it is necessary for a specific value of z satisfying ${\displaystyle \phi }$ to be known.

...
Wikipedia