Inhabited Set - Example

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 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 intutionistic 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).