# Inhabited set

In mathematics, a set is **inhabited** if there exists an element .

In classical mathematics, the property of being inhabited is equivalent to being non-

## Definition

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

### Related definitions

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 .

## Theorems

Modus ponens implies , and taking any a false proposition for establishes that 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

### Examples

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

#### Example relating to excluded middle

Define a subset via

Clearly and , and from the

Already minimal logic proves , the double-negation for any excluded middle statement, which here is equivalent to . So by performing two contrapositions on the previous implication, one establishes . In words: It *cannot consistently be ruled out* that exactly one of the numbers and inhabits . In particular, the latter can be weakened to , saying is proven non-empty.

As example statements for , consider the infamous provenly theory-independent statement 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. Knowledge of the validity of either or is equivalent to knowledge about as above, and cannot be obtained. Given neither nor can be proven in the theory, it will also not prove to be inhabited by some particular number. Further, a constructive framework with the

#### Example relating to choice

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

### Model theory

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

## See also

- Intersection (set theory) – Set of elements common to all of some sets
- Nothing – Complete absence of anything; the opposite of everything
- Type inhabitation in type theory.

## References

- 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 *

*Creative Commons Attribution/Share-Alike License*

*.*