A subsingleton generally refers to a subset (of some ambient set ) having at most one element. That is, it is a subset of such that any two elements of 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 ” is the partial map classifier for , often denoted .
Sometimes a slightly different convention is used: There what we call subsingletons are called subterminals, and a subset of is a subsingleton if and only if there exists an element such that every element of is equal to . With this nomenclature, any subsingleton is a subterminal, but the converse doesn’t hold in general. (See flabby sheaf for a class of examples where the converse does hold.)
Given a proposition and a singleton , one can construct the subsingleton
This means that one can use the set-theoretic operations to define the BHK interpretation of logic: Given two propositions and , purely or is given by an element of the binary disjoint union
and the pure existential quantifier of a predicate on a set is given by an element of the indexed disjoint union
Suppose that is a subsingleton. Then the existential quantifier which says that is an inhabited set is equivalent to the existential quantifier , where is the constant function from to the boolean domain which takes elements of to the boolean . 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 :
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.
computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory
Last revised on September 25, 2024 at 21:38:07. See the history of this page for a list of all contributions to it.