This article includes alist of references,related reading, orexternal links,but its sources remain unclear because it lacksinline citations. Please helpimprove this article byintroducing more precise citations.(September 2025) (Learn how and when to remove this message)

In mathematics, aset${\displaystyle A}$ isinhabited if there exists an element${\displaystyle a\in A}$.

Inclassical mathematics, the property of being inhabited is equivalent to being non-empty. However, this equivalence is not valid in constructive orintuitionistic logic, and so this separate terminology is mostly used in theset theory ofconstructive mathematics.

In the formal language offirst-order logic, set${\displaystyle A}$ has the property of beinginhabited if

${\displaystyle \mathrm{\exists }z(z\in A).}$

A set${\displaystyle A}$ has the property of beingempty if${\displaystyle \mathrm{\forall }z(z\notin A)}$, or equivalently${\displaystyle \mathrm{\neg }\mathrm{\exists }z(z\in A)}$. Here${\displaystyle z\notin A}$ stands for the negation${\displaystyle \mathrm{\neg }(z\in A)}$.

A set${\displaystyle A}$ isnon-empty if it is not empty, that is, if${\displaystyle \mathrm{\neg }\mathrm{\forall }z(z\notin A)}$, or equivalently${\displaystyle \mathrm{\neg }\mathrm{\neg }\mathrm{\exists }z(z\in A)}$.

Theinference rules for${\displaystyle \to }$ imply${\displaystyle P\to ((P\to Q)\to Q)}$, and taking any a false proposition for${\displaystyle Q}$ establishes that${\displaystyle P\to \mathrm{\neg }\mathrm{\neg }P}$ 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, anexistence 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${\displaystyle \mathrm{\exists }z\varphi (z)}$ to hold for someformula${\displaystyle \varphi }$, it is necessary for a specific value of${\displaystyle z}$ satisfying${\displaystyle \varphi }$ 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${\displaystyle \{2,3,4,7\}}$ or${\displaystyle \mathbb{Q}}$ are inhabited, as e.g. witnessed by${\displaystyle 3\in \{2,3,4,7\}}$. The set${\displaystyle \{\}}$ 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 theaxiom of separation, as with it logical statements can always be translated to set-theoretical ones. For example, with a subset${\displaystyle S\subseteq \{0\}}$ defined as${\displaystyle S:=\{n\in \{0\}\mid P\}}$, the proposition${\displaystyle P}$ may always equivalently be stated as${\displaystyle 0\in S}$. 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.

Define a subset${\displaystyle A\subseteq \{0,1\}}$ via

${\displaystyle A:=\{n\in \{0,1\}\mid (P\wedge n=0)\vee (\mathrm{\neg }P\wedge n=1)\}}$

Clearly${\displaystyle P\leftrightarrow 0\in A}$ and${\displaystyle (\mathrm{\neg }P)\leftrightarrow 1\in A}$, and from theprinciple of non-contradiction one concludes${\displaystyle \mathrm{\neg }(0\in A\wedge 1\in A)}$. Further,${\displaystyle (P\vee \mathrm{\neg }P)\leftrightarrow (0\in A\vee 1\in A)}$ and in turn

${\displaystyle (P\vee \mathrm{\neg }P)\to \mathrm{\exists }!(n\in \{0,1\})n\in A}$

Alreadyminimal logic proves${\displaystyle \mathrm{\neg }\mathrm{\neg }(P\vee \mathrm{\neg }P)}$, the double-negation for any excluded middle statement, which here is equivalent to${\displaystyle \mathrm{\neg }(0\notin A\wedge 1\notin A)}$. So by performing two contrapositions on the previous implication, one establishes${\displaystyle \mathrm{\neg }\mathrm{\neg }\mathrm{\exists }!(n\in \{0,1\})n\in A}$. In words: Itcannot consistently be ruled out that exactly one of the numbers${\displaystyle 0}$ and${\displaystyle 1}$ inhabits${\displaystyle A}$. In particular, the latter can be weakened to${\displaystyle \mathrm{\neg }\mathrm{\neg }\mathrm{\exists }nn\in A}$, saying${\displaystyle A}$ is proven non-empty.

As example statements for${\displaystyle P}$, consider the infamous provenly theory-independent statements such as thecontinuum 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 alsoBrouwerian counterexamples. Knowledge of the validity of either${\displaystyle 0\in A}$ or${\displaystyle 1\in A}$ is equivalent to knowledge about${\displaystyle P}$ as above, and cannot be obtained. Given neither${\displaystyle P}$ nor${\displaystyle \mathrm{\neg }P}$ can be proven in the theory, it will also not prove${\displaystyle A}$ to be inhabited by some particular number. Further, a constructive framework with thedisjunction property then cannot prove${\displaystyle P\vee \mathrm{\neg }P}$ either. There is neither evidence${\displaystyle 0\in A}$ nor for${\displaystyle 1\in A}$, and constructive unprovability of their disjunction reflects this. Nonetheless, since ruling out excluded middle is provenly always inconsistent, it is also established that${\displaystyle A}$ is not empty. Classical logic adopts${\displaystyle P\vee \mathrm{\neg }P}$ axiomatically, spoiling a constructive reading.

There are various easily characterized sets the existence of which are not provable in${\displaystyle \mathsf{Z}\mathsf{F}}$, but which are implied to exist by the fullaxiom of choice${\displaystyle \mathrm{A}\mathrm{C}}$. As such, that axiom is itselfindependent of${\displaystyle \mathsf{Z}\mathsf{F}}$. It in fact contradicts other potential axioms for a set theory. Further, it indeed alsocontradicts constructive principles, in a set-theory context. A theory that does not permit excluded middle does also not validate the function existence principle${\displaystyle \mathrm{A}\mathrm{C}}$.

In${\displaystyle \mathsf{Z}\mathsf{F}}$, the${\displaystyle \mathrm{A}\mathrm{C}}$is equivalent to the statement that everyvector space has abasis. So more concretely, consider the question of existence of aHamel basis of thereal numbers over therational numbers. This object is elusive in the sense that there are different${\displaystyle \mathsf{Z}\mathsf{F}}$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 amodel in the classical sense that contains a nonempty set${\displaystyle X}$ but does not satisfy "${\displaystyle X}$ is inhabited".

However, it is possible to construct a first-orderKripke model${\displaystyle M}$ 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 "${\displaystyle X}$ is nonempty" implies "${\displaystyle X}$ is inhabited".

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

• 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 onPlanetMath, which is licensed under theCreative Commons Attribution/Share-Alike License.

• Basic concepts in set theory
• Concepts in logic
• Constructivism (philosophy of mathematics)
• Mathematical objects
• Set theory

• Articles with short description
• Short description is different from Wikidata
• Articles lacking in-text citations from September 2025
• All articles lacking in-text citations
• Wikipedia articles incorporating text from PlanetMath
• Pages that use a deprecated format of the math tags