In logic, the true proposition, or truth, is the proposition which is always true.

The truth is commonly denoted truetrue, TT, \top, or 11.


In classical logic

In classical logic, there are two truth values: true and false. Classical logic is perfectly symmetric between truth and falsehood; see de Morgan duality.

In constructive logic

In constructive logic, truetrue is the top element in the poset of truth values.

Constructive logic is still two-valued in the sense that any truth value which is not true is false.

In a topos

In terms of the internal logic of a topos (or other category), truetrue is the top element in the poset of subobjects of any given object (where each object corresponds to a context in the internal language).

However, not every topos is two-valued, so there may be other truth values besides truetrue and falsefalse.

In homotopy type theory

In homotopy type theory the true is represented by any contractible type.


In the topos SetSet

In the archetypical topos Set, the terminal object is the singleton set {*}\{*\} (the point) and the poset of subobjects of that is classically {*}\{\emptyset \hookrightarrow *\}. Then truth is the singleton set {*}\{*\}, seen as the improper subset of itself. (See Internal logic of Set for more details).

The same is true in the archetypical (∞,1)-topos ∞Grpd. From that perspective it makes good sense to think of

In this sense, the object truetrue in Set or ∞Grpd may canonically be thought of as being the unique (−2)-groupoid.

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

Revised on February 2, 2015 11:35:58 by Urs Schreiber (