inhabited set

**natural deduction** metalanguage, practical foundations

**type theory** (dependent, intensional, observational type theory, homotopy type theory)

**computational trinitarianism** = **propositions as types** +**programs as proofs** +**relation type theory/category theory**

In set theory, an **inhabited set** or **occupied set** is a set that contains an element.

More generally, in type theory an **inhabited type** is a type that has a term.

At least assuming classical logic, this is the same thing as a set that is not empty. Usually inhabited sets are simply called ‘non-empty’, but the positive word ‘inhabited’ reminds us that this is the simpler notion, which emptiness is defined as the negation of.

The terms ‘inhabited’ and ‘occupied’ come from constructive mathematics. In constructive mathematics (such as the internal logic of some topos or generally in type theory), a set/type that is not empty is not already necessarily inhabited. This is because double negation is nontrivial in intuitionistic logic. All the same, many constructive mathematicians use the old word ‘non-empty’ with the understanding that it *really* means inhabited.

There is a distinction between ‘inhabited’ and ‘occupied’ spaces in Abstract Stone Duality (which probably corresponds to something about locales, should explain that here).

An inhabited set is the special case of an inhabited object in the topos Set.

Revised on September 26, 2012 10:09:14
by Urs Schreiber
(82.169.65.155)