In mathematics, a set is inhabited.

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.

Definition

In the formal language of first-order logic has the property of being inhabited if

Related definitions

has the property of being .

is .

Theorems

The inference rules is always valid. Hence, any inhabited set is provably also non-empty.

Discussion

In constructive mathematics, the double-negation elimination principle is not automatically valid. In particular, an existence statement to hold for some formula 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.

Examples

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 such examples by using the axiom of separation. 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.

Example relating to excluded middle

via

, and from the principle of non-contradiction and in turn

Already minimal logic. In words: It cannot consistently be ruled out is proven non-empty.

, consider the infamous provenly theory-independent statements such as the continuum hypothesis, consistency of the sound theory at hand, or, informally, an unknowable claim about the past or future. By design, these are chosen to be unprovable. A variant of this is to consider mathematical propositions that are merely not yet established—see also Brouwerian counterexamples to be inhabited by some particular number. Further, a constructive framework with the disjunction property axiomatically, spoiling a constructive reading.

Example relating to choice

There are various easily characterized sets the existence of which are not provable in {\mathsf {ZF}}, but which are implied to exist by the full axiom of choice. As such, that axiom is itself independent. It in fact contradicts other potential axioms for a set theory. Further, it indeed also contradicts constructive principles.

is equivalent to the statement that every vector space has a basis. So more concretely, consider the question of existence of a Hamel basis of the real numbers over the rational numbers 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.

Model theory

Because inhabited sets are the same as nonempty sets in classical logic, it is not possible to produce a model is inhabited".

However, it is possible to construct a first-order Kripke model is inhabited".

See also

• Type inhabitation in type theory.

References

• D. Bridges and F. Richman. 1987. Varieties of Constructive Mathematics. Oxford University Press.