nLab truth value




Classically, a truth value is either \top (true) or \bot (false), hence an element of the boolean domain.

(In constructive mathematics, this is not so simple, although it still holds that any truth value that is not true is false.)

More generally, a truth value in a topos TT is a morphism 1Ω1 \to \Omega (where 11 is the terminal object and Ω\Omega is the subobject classifier) in TT. By definition of Ω\Omega, this is equivalent to an (equivalence class of) monomorphisms U1U\hookrightarrow 1. In a two-valued topos, it is again true that every truth value is either \top or \bottom, while in a Boolean topos this is true in the internal logic.

Truth values form a poset (the poset of truth values) by declaring that pp precedes qq iff the conditional pqp \to q is true. In a topos TT, pp precedes qq if the corresponding subobject P1P\hookrightarrow 1 is contained in Q1Q\hookrightarrow 1. Classically (or in a two-valued topos), one can write this poset as {}\{\bot \to \top\}.

The poset of truth values is a Heyting algebra. Classically (or internal to a Boolean topos), this poset is even a Boolean algebra. It is also a complete lattice; in fact, it can be characterised as the initial complete lattice. As a complete Heyting algebra, it is a frame, corresponding to the one-point locale.

When the set of truth values is equipped with the specialization topology, the result is Sierpinski space.

A truth value may be interpreted as a 00-poset or as a (1)(-1)-groupoid. It is also the best interpretation of the term ‘(1)(-1)-category’, although this doesn't fit all the patterns of the periodic table.

homotopy leveln-truncationhomotopy theoryhigher category theoryhigher topos theoryhomotopy type theory
h-level 0(-2)-truncatedcontractible space(-2)-groupoidtrue/​unit type/​contractible type
h-level 1(-1)-truncatedcontractible-if-inhabited(-1)-groupoid/​truth value(0,1)-sheaf/​idealmere proposition/​h-proposition
h-level 20-truncatedhomotopy 0-type0-groupoid/​setsheafh-set
h-level 31-truncatedhomotopy 1-type1-groupoid/​groupoid(2,1)-sheaf/​stackh-groupoid
h-level 42-truncatedhomotopy 2-type2-groupoid(3,1)-sheaf/​2-stackh-2-groupoid
h-level 53-truncatedhomotopy 3-type3-groupoid(4,1)-sheaf/​3-stackh-3-groupoid
h-level n+2n+2nn-truncatedhomotopy n-typen-groupoid(n+1,1)-sheaf/​n-stackh-nn-groupoid
h-level \inftyuntruncatedhomotopy type∞-groupoid(∞,1)-sheaf/​∞-stackh-\infty-groupoid

Last revised on January 26, 2024 at 20:08:47. See the history of this page for a list of all contributions to it.