nLab true proposition

Idea

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

The truth is commonly denoted $true$, $T$, $\top$, or $1$. These may be pronounced ‘true’ even where it would be ungrammatical for an adjective to appear in ordinary English.

Definitions

In natural deduction the inference rules for true is given by

$$\frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash \top \; \mathrm{prop}} \qquad \frac{\Gamma \; \mathrm{ctx}}{\Xi \vdash \top \; \mathrm{true}}$$

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, $true$ 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 linear logic

In linear logic, there is both additive truth, denoted $\top$, and multiplicative truth, denoted $1$. As the notation suggests, it is $\top$ that is the top element of the lattice of linear truth values. (In particular, $1 \vdash \top$ but $\top \nvdash 1$.)

In a topos

In terms of the internal logic of a topos (or other category), $true$ 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 (even if it is boolean, so there may be other truth values besides $true$ and $false$.

In type theory

In type theory with propositions as types, truth is represented by the unit type.

In homotopy type theory

In homotopy type theory, truth is represented by any contractible type.

Examples

In the topos $Set$

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

• a set as a 0-truncated $\infty$-groupoid: a 0-groupoid;

• a subsingleton set as a $(-1)$-truncated $\infty$-groupoid: a (?1)-groupoid?;

• the singleton set as the $(-2)$-truncated $\infty$-groupoid: the unique (up to equivalence) (?2)-groupoid.

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

Related concepts

• true, unit type

• false, empty type

• contradiction, inconsistency, consistency

• correspondence theory of truth

homotopy level	n-truncation	homotopy theory	higher category theory	higher topos theory	homotopy type theory
h-level 0	(-2)-truncated	contractible space	(-2)-groupoid		true/​unit type/​contractible type
h-level 1	(-1)-truncated	contractible-if-inhabited	(-1)-groupoid/​truth value	(0,1)-sheaf/​ideal	mere proposition/​h-proposition
h-level 2	0-truncated	homotopy 0-type	0-groupoid/​set	sheaf	h-set
h-level 3	1-truncated	homotopy 1-type	1-groupoid/​groupoid	(2,1)-sheaf/​stack	h-groupoid
h-level 4	2-truncated	homotopy 2-type	2-groupoid	(3,1)-sheaf/​2-stack	h-2-groupoid
h-level 5	3-truncated	homotopy 3-type	3-groupoid	(4,1)-sheaf/​3-stack	h-3-groupoid
h-level $n+2$	$n$-truncated	homotopy n-type	n-groupoid	(n+1,1)-sheaf/​n-stack	h-$n$-groupoid
h-level $\infty$	untruncated	homotopy type	∞-groupoid	(∞,1)-sheaf/​∞-stack	h-$\infty$-groupoid