Inhabited set

Property of sets used in constructive mathematics
In mathematics, a set is inhabited if there exists an element
In classical mathematics, the property of being inhabited is equivalent to being non empty. However, this equivalence is not valid in constructive or intuitionistic logic, and so this separate terminology is mostly used in the set theory of constructive mathematics.

A set has the property of being empty if , or equivalently Here stands for the negation

A set is non empty if it is not empty, that is, if , or equivalently .

Modus ponens implies , and taking any a false proposition for establishes that is always valid. Hence, any inhabited set is provably also non empty.

In constructive mathematics, the double negation elimination principle is not automatically valid. In particular, an existence statement is generally stronger than its double negated form. The latter merely expresses that the existence cannot be ruled out, in the strong sense that it cannot consistently be negated. In a constructive reading, in order for to hold for some formula , it is necessary for a specific value of satisfying to be constructed or known. Likewise, the negation of a universal quantified statement is in general weaker than an existential quantification of a negated statement. In turn, a set may be proven to be non empty without one being able to prove it is inhabited.

Sets such as or are inhabited, as e. g. witnessed by The set is empty and thus not inhabited. Naturally, the example section thus focuses on non empty sets that are not provably inhabited. It is easy to give examples for any simple set theoretical property, because logical statements can always be expressed as set theoretical ones, using an axiom of separation. For example, with a subset defined as , the proposition may always equivalently be stated as The double negated existence claim of an entity with a certain property can be expressed by stating that the set of entities with that property is non empty.

There are various easily characterized sets the existence of which is not provable in , but which are implied to exist by the full axiom of choice As such, that axiom is itself independent of It in fact contradicts other potential axioms for a set theory. Further, it indeed also contradicts constructive principles, in a set theory context. A theory that does not permit excluded middle does also not validate the function existence principle
In , the is equivalent to the statement that for every vector space there exists basis. So more concretely, consider the question of existence of a Hamel bases of the real numbers over the rational numbers. This object is elusive in the sense that are different models that either negate and validate its existence. So it is also consistent to just postulate that existence cannot be ruled out here, in the sense that it cannot consistently be negated. Again, that postulate may be expressed as saying that the set of such Hamel bases is non empty. Over a constructive theory, such a postulate is weaker than the plain existence postulate, but (by design) is still strong enough to then negate all propositions that would imply the non existence of a Hamel basis.

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". However, it is possible to construct a Kripke model that differentiates between the two notions. Since an implication is true in every Kripke model if and only if it is provable in intuitionistic logic, this indeed establishes that one cannot intuitionistically prove that " is nonempty" implies " is inhabited".