Inhabited set

Property of sets used in constructive mathematics

In mathematics, a set A {\displaystyle A} is inhabited if there exists an element  a ∈ A {\displaystyle a\in A} .

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

[edit]

In the formal language of first-order logic, set  A {\displaystyle A} has the property of being inhabited if

∃ z . ( z ∈ A ) . {\displaystyle \exists z.(z\in A).}

### Related definitions

[edit]

A set  A {\displaystyle A} has the property of being empty if  ∀ z . ( z ∉ A ) {\displaystyle \forall z.(z\notin A)} , or equivalently  ¬ ∃ z . ( z ∈ A ) {\displaystyle \neg \exists z.(z\in A)} . Here  z ∉ A {\displaystyle z\notin A} stands for the negation  ¬ ( z ∈ A ) {\displaystyle \neg (z\in A)} .

A set  A {\displaystyle A} is non-empty if it is not empty, that is, if  ¬ ∀ z . ( z ∉ A ) {\displaystyle \neg \forall z.(z\notin A)} , or equivalently  ¬ ¬ ∃ z . ( z ∈ A ) {\displaystyle \neg \neg \exists z.(z\in A)} .

## Theorems

[edit]

Modus ponens implies  P -> ( ( P -> Q ) -> Q ) {\displaystyle P\to ((P\to Q)\to Q)} , and taking any a false proposition for  Q {\displaystyle Q} establishes that  P -> ¬ ¬ P {\displaystyle P\to \neg \neg P} is always valid. Hence, any inhabited set is provably also non-empty.

## Discussion

[edit]

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  ∃ z . ϕ ( z ) {\displaystyle \exists z.\phi (z)} to hold for some formula ϕ {\displaystyle \phi } , it is necessary for a specific value of  z {\displaystyle z} satisfying  ϕ {\displaystyle \phi } 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

[edit]

Sets such as  { 2 , 3 , 4 , 7 } {\displaystyle \\{2,3,4,7\\}} or  Q {\displaystyle \mathbb {Q} } are inhabited, as e.g. witnessed by  3 ∈ { 2 , 3 , 4 , 7 } {\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 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  S ⊂ { 0 } {\displaystyle S\subset \\{0\\}} defined as  S := { n ∈ { 0 } ∣ P } {\displaystyle S:=\\{n\in \\{0\\}\mid P\\}} , the proposition  P {\displaystyle P} may always equivalently be stated as  0 ∈ S {\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.

#### Example relating to excluded middle

[edit]

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

A := { n ∈ { 0 , 1 } ∣ ( P ∧ n = 0 ) ∨ ( ¬ P ∧ n = 1 ) } {\displaystyle A:=\\{n\in \\{0,1\\}\mid (P\land n=0)\lor (\neg P\land n=1)\\}}

Clearly  P ↔ 0 ∈ A {\displaystyle P\leftrightarrow 0\in A} and  ( ¬ P ) ↔ 1 ∈ A {\displaystyle (\neg P)\leftrightarrow 1\in A} , and from the principle of non-contradiction one concludes  ¬ ( 0 ∈ A ∧ 1 ∈ A ) {\displaystyle \neg (0\in A\land 1\in A)} . Further,  ( P ∨ ¬ P ) ↔ ( 0 ∈ A ∨ 1 ∈ A ) {\displaystyle (P\lor \neg P)\leftrightarrow (0\in A\lor 1\in A)} and in turn

( P ∨ ¬ P ) -> ∃ ! ( n ∈ { 0 , 1 } ) . n ∈ A {\displaystyle (P\lor \neg P)\to \exists !(n\in \\{0,1\\}).n\in A}

Already minimal logic proves  ¬ ¬ ( P ∨ ¬ P ) {\displaystyle \neg \neg (P\lor \neg P)} , the double-negation for any excluded middle statement, which here is equivalent to  ¬ ( 0 ∉ A ∧ 1 ∉ A ) {\displaystyle \neg (0\notin A\land 1\notin A)} . So by performing two contrapositions on the previous implication, one establishes  ¬ ¬ ∃ ! ( n ∈ { 0 , 1 } ) . n ∈ A {\displaystyle \neg \neg \exists !(n\in \\{0,1\\}).n\in A} . In words: It cannot consistently be ruled out that exactly one of the numbers  0 {\displaystyle 0} and  1 {\displaystyle 1} inhabits  A {\displaystyle A} . In particular, the latter can be weakened to  ¬ ¬ ∃ n . n ∈ A {\displaystyle \neg \neg \exists n.n\in A} , saying  A {\displaystyle A} is proven non-empty.

As example statements for  P {\displaystyle P} , 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  0 ∈ A {\displaystyle 0\in A} or  1 ∈ A {\displaystyle 1\in A} is equivalent to knowledge about  P {\displaystyle P} as above, and cannot be obtained. Given neither  P {\displaystyle P} nor  ¬ P {\displaystyle \neg P} can be proven in the theory, it will also not prove  A {\displaystyle A} to be inhabited by some particular number. Further, a constructive framework with the disjunction property then cannot prove  P ∨ ¬ P {\displaystyle P\lor \neg P} either. There is no evidence for  0 ∈ A {\displaystyle 0\in A} , nor for  1 ∈ A {\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  A {\displaystyle A} is not empty. Classical logic adopts  P ∨ ¬ P {\displaystyle P\lor \neg P} axiomatically, spoiling a constructive reading.

#### Example relating to choice

[edit]

There are various easily characterized sets the existence of which is not provable in  Z F {\displaystyle {\mathsf {ZF}}} , but which are implied to exist by the full axiom of choice A C {\displaystyle {\mathrm {AC} }} . As such, that axiom is itself independent of  Z F {\displaystyle {\mathsf {ZF}}} . 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  A C {\displaystyle {\mathrm {AC} }} .

In  Z F {\displaystyle {\mathsf {ZF}}} , the  A C {\displaystyle {\mathrm {AC} }} 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  Z F {\displaystyle {\mathsf {ZF}}} 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

[edit]

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  X {\displaystyle X} but does not satisfy " X {\displaystyle X} is inhabited".

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

## See also

[edit]

* 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

[edit]

* D. Bridges and F. Richman. 1987. Varieties of Constructive Mathematics. Oxford University Press. ISBN 978-0-521-31802-0

* v
* t
* e

Mathematical logic

General|

* Axiom
* list
* Cardinality
* First-order logic
* Formal proof
* Formal semantics
* Foundations of mathematics
* Information theory
* Lemma
* Logical consequence
* Model
* Theorem
* Theory
* Type theory

Theorems (list)
and paradoxes|

* Gödel's completeness and incompleteness theorems
* Tarski's undefinability
* Banach–Tarski paradox
* Cantor's theorem, paradox and diagonal argument
* Compactness
* Halting problem
* Lindström's
* Löwenheim–Skolem
* Russell's paradox

Logics|

| Traditional|

* Classical logic
* Logical truth
* Tautology
* Proposition
* Inference
* Logical equivalence
* Consistency
* Equiconsistency
* Argument
* Soundness
* Validity
* Syllogism
* Square of opposition
* Venn diagram

|

Propositional|

* Boolean algebra
* Boolean functions
* Logical connectives
* Propositional calculus
* Propositional formula
* Truth tables
* Many-valued logic
* 3
* finite
* ∞

Predicate|

* First-order
* list
* Second-order
* Monadic
* Higher-order
* Fixed-point
* Free
* Quantifiers
* Predicate
* Monadic predicate calculus

Set theory|

* Set
* hereditary
* Class
* (Ur-)Element
* Ordinal number
* Extensionality
* Forcing
* Relation
* equivalence
* partition
* Set operations:
* intersection
* union
* complement
* Cartesian product
* power set
* identities

Types of sets|

* Countable
* Uncountable
* Empty
* Inhabited
* Singleton
* Finite
* Infinite
* Transitive
* Ultrafilter
* Recursive
* Fuzzy
* Universal
* Universe
* constructible
* Grothendieck
* Von Neumann

Maps and cardinality|

* Function/Map
* domain
* codomain
* image
* In/Sur/Bi-jection
* Schröder–Bernstein theorem
* Isomorphism
* Gödel numbering
* Enumeration
* Large cardinal
* inaccessible
* Aleph number
* Operation
* binary

Set theories|

* Zermelo–Fraenkel
* axiom of choice
* continuum hypothesis
* General
* Kripke–Platek
* Morse–Kelley
* Naive
* New Foundations
* Tarski–Grothendieck
* Von Neumann–Bernays–Gödel
* Ackermann
* Constructive

Formal systems (list),
language and syntax|

* Alphabet
* Arity
* Automata
* Axiom schema
* Expression
* ground
* Extension
* by definition
* conservative
* Relation
* Formation rule
* Grammar
* Formula
* atomic
* closed
* ground
* open
* Free/bound variable
* Language
* Metalanguage
* Logical connective
* ¬
* ∨
* ∧
* →
* ↔
* =
* Predicate
* functional
* variable
* propositional variable
* Proof
* Quantifier
* ∃
* !
* ∀
* rank
* Sentence
* atomic
* spectrum
* Signature
* String
* Substitution
* Symbol
* function
* logical/constant
* non-logical
* variable
* Term
* Theory
* list

Example axiomatic
systems (list)|

* of arithmetic:
* Peano
* second-order
* elementary function
* primitive recursive
* Robinson
* Skolem
* of the real numbers
* Tarski's axiomatization
* of Boolean algebras
* canonical
* minimal axioms
* of geometry:
* Euclidean:
* Elements
* Hilbert's
* Tarski's
* non-Euclidean

* Principia Mathematica

Proof theory|

* Formal proof
* Natural deduction
* Logical consequence
* Rule of inference
* Sequent calculus
* Theorem
* Systems
* axiomatic
* deductive
* Hilbert
* list
* Complete theory
* Independence (from ZFC)
* Proof of impossibility
* Ordinal analysis
* Reverse mathematics
* Self-verifying theories

Model theory|

* Interpretation
* function
* of models
* Model
* equivalence
* finite
* saturated
* spectrum
* submodel
* Non-standard model
* of arithmetic
* Diagram
* elementary
* Categorical theory
* Model complete theory
* Satisfiability
* Semantics of logic
* Strength
* Theories of truth
* semantic
* Tarski's
* Kripke's
* T-schema
* Transfer principle
* Truth predicate
* Truth value
* Type
* Ultraproduct
* Validity

Computability theory|

* Church encoding
* Church–Turing thesis
* Computably enumerable
* Computable function
* Computable set
* Decision problem
* decidable
* undecidable
* P
* NP
* P versus NP problem
* Kolmogorov complexity
* Lambda calculus
* Primitive recursive function
* Recursion
* Recursive set
* Turing machine
* Type theory

Related|

* Abstract logic
* Algebraic logic
* Automated theorem proving
* Category theory
* Concrete/Abstract category
* Category of sets
* History of logic
* History of mathematical logic
* timeline
* Logicism
* Mathematical object
* Philosophy of mathematics
* Supertask

Mathematics portal

This article incorporates material from Inhabited set on PlanetMath, which is licensed under the Creative Commons Attribution/Share-Alike License.
*[v]: View this template
*[t]: Discuss this template
*[e]: Edit this template