subsingleton in nLab

Contents

Definition

A subsingleton generally refers to a subset (of some ambient set AA) having at most one element. That is, it is a subset BB of AA such that any two elements of BB are equal.

Of course, classically any subsingleton is either empty or a singleton, but constructively this need not hold. In a topos, the “object of subsingletons in AA” is the partial map classifier for AA, often denoted A ⊥A_\bot.

 Generating subsingletons from propositions

Given a proposition PP and a singleton {*}\{*\}, one can construct the subsingleton

{p∈{*}|(p=*)∧P}\{p \in \{*\} \vert (p = *) \wedge P\}

This means that one can use the set-theoretic operations to define the BHK interpretation of logic: Given two propositions PP and QQ, purely PP or QQ is given by an element of the binary disjoint union

{p∈{*}|(p=*)∧P}⊎{p∈{*}|(p=*)∧Q}\{p \in \{*\} \vert (p = *) \wedge P\} \uplus \{p \in \{*\} \vert (p = *) \wedge Q\}

and the pure existential quantifier of a predicate P(x)P(x) on a set AA is given by an element of the indexed disjoint union

⨄ x∈A{p∈{*}|(p=*)∧P(x)}\biguplus_{x \in A} \{p \in \{*\} \vert (p = *) \wedge P(x)\}

Relation to the principles of omniscience

Suppose that AA is a subsingleton. Then the existential quantifier ∃x.x∈A\exists x.x \in A which says that AA is an inhabited set is equivalent to the existential quantifier ∃x:A.(λt.1)(x)=1\exists x:A.(\lambda t.1)(x) = 1, where λt.1\lambda t.1 is the constant function from AA to the boolean domain which takes elements of AA to the boolean 1∈bool1 \in \mathrm{bool}. Then, one can show that various principles of omniscience are equivalent to weak versions of the internal excluded middle, via the special case of the constant function λt.1\lambda t.1:

• That the limited principle of omniscience holds for all subsingletons is equivalent to internal excluded middle.

• That the weak limited principle of omniscience holds for all subsingletons is equivalent to internal weak excluded middle.

• That the lesser limited principle of omniscience holds for all subsingletons is equivalent to internal de Morgan's law.

• That Markov's principle holds for all subsingletons is equivalent to the internal double negation law.

See also

• h-proposition
• support
• decidable subsingleton