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.
In the formal language of first-order logic, set
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.
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.
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, as with it logical statements can always be translated to set theoretical ones.
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.
, the double-negation for any excluded middle statement, which here is equivalent to
So by performing two contrapositions on the previous implication, one establishes
, 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.
A variant of this is to consider mathematical propositions that are merely not yet established - see also Brouwerian counterexamples.
Further, a constructive framework with the disjunction property then cannot prove
, and constructive unprovability of their disjunction reflects this.
Nonetheless, since ruling out excluded middle is provenly always inconsistent, it is also established that
axiomatically, spoiling a constructive reading.
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
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
is equivalent to the statement that for every vector space there exists basis.
models that either negate and validate its existence.
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.
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 "
This article incorporates material from Inhabited set on PlanetMath, which is licensed under the Creative Commons Attribution/Share-Alike License.