nLab boolean domain

Idea

The boolean domain or boolean field (often just: $Bool$) is a $2$-element set, say $\mathbb{B} = \{ 0, 1 \}$ (“bits”) or $\mathbb{B} = \{ \bot, \top \}$ (“bottom”, “top”), whose elements may be interpreted as truth values.

Note that $\mathbb{B}$ is the set of all truth values in classical logic, but this cannot be assumed in non-classical logic such as intuitionistic logic.

The Boolean domain plays the role of the subobject classifier in the Boolean topos of Sets.

If we think of the classical $\mathbb{B}$ as a pointed set equipped with the true element, then there is an effectively unique boolean domain.

A boolean variable $x$ is a variable that takes its value in a boolean domain, as $x \in \mathbb{B}$. If this variable depends on parameters, then it is (or defines) a Boolean-valued function, that is a function whose target is $\mathbb{B}$.

An element of $\mathbb{B}$ is a binary digit, or bit.

The boolean domain is the initial set with two elements. It is also the initial set with an element and an involution. It is also the tensor unit for the smash product in the monoidal category of pointed sets.

Remark

(relation to boolean algebra)
The term ‘boolean field’ (or just ‘field’, depending on the context) is sometimes used more generally for any boolean algebra. In fact, the boolean domain is the initial boolean algebra. If we interpret a boolean algebra as a boolean ring, then the boolean domain is the finite field with $2$ elements.

In dependent type theory the boolean domain is called the type of booleans.

Properties

The boolean domain is in bijection with the set of decidable truth values.

$$\mathrm{Bool} \cong \{P \in \Omega \vert P \vee \neg P\}$$

As a result, sometimes the boolean domain is called a decidable subset classifier.

Induction and recursion on the boolean domain

Like the natural numbers, the boolean domain has an induction principle, which states that to prove a statement $P(n)$ true for every bit, it suffices to prove it for falsehood $P(0)$ and truth $P(1)$.

Similarly, the boolean domain also has a recursion principle, which states that to define a function $f:\mathrm{Bool} \to A$ from the boolean domain to a set $A$, it suffices to define the function when evaluated at falsehood $f(0)$ and truth $f(1)$.

Equality and inequality

Definition

By the induction principle of the boolean domain, we can define an equality relation on the boolean domain $x = y$, inductively defined by

$$0 = 0 \; \mathrm{is} \; \mathrm{true} \qquad 0 = 1 \; \mathrm{is} \; \mathrm{false} \qquad 1 = 0 \; \mathrm{is} \; \mathrm{false} \qquad 1 = 1 \; \mathrm{is} \; \mathrm{true}$$

Definition

Similarly, we can define an inequality relation on the boolean domain $x \neq y$, inductively defined by

$$0 \neq 0 \; \mathrm{is} \; \mathrm{false} \qquad 0 \neq 1 \; \mathrm{is} \; \mathrm{true} \qquad 1 \neq 0 \; \mathrm{is} \; \mathrm{true} \qquad 1 \neq 1 \; \mathrm{is} \; \mathrm{false}$$

We can show that equality is an equivalence relation and the inequality relation is a apartness relation, and that equality and inequality are mutually decidable $x = y \vee x \neq y$.

If the ambient foundations already has an equality relation for all sets that satisfy the principle of substitution, then one can show that $x = y$ if and only if $x =_\mathrm{Bool} y$ for the predefined equality relation $x =_\mathrm{Bool} y$ on the boolean domain.

Order structure

In addition, we can define various order structures on the boolean domain.

Definition

The order relation $x \leq y$ is inductively defined by

$$0 \leq 0 \; \mathrm{is} \; \mathrm{true} \qquad 0 \leq 1 \; \mathrm{is} \; \mathrm{true} \qquad 1 \leq 0 \; \mathrm{is} \; \mathrm{false} \qquad 1 \leq 1 \; \mathrm{is} \; \mathrm{true}$$

Definition

The order relation $x \geq y$ is inductively defined by

$$0 \geq 0 \; \mathrm{is} \; \mathrm{true} \qquad 0 \geq 1 \; \mathrm{is} \; \mathrm{false} \qquad 1 \geq 0 \; \mathrm{is} \; \mathrm{true} \qquad 1 \geq 1 \; \mathrm{is} \; \mathrm{true}$$

Definition

The order relation $x \lt y$ is inductively defined by

$$0 \lt 0 \; \mathrm{is} \; \mathrm{false} \qquad 0 \lt 1 \; \mathrm{is} \; \mathrm{true} \qquad 1 \lt 0 \; \mathrm{is} \; \mathrm{false} \qquad 1 \lt 1 \; \mathrm{is} \; \mathrm{false}$$

Definition

The order relation $x \gt y$ is inductively defined by

$$0 \gt 0 \; \mathrm{is} \; \mathrm{false} \qquad 0 \gt 1 \; \mathrm{is} \; \mathrm{false} \qquad 1 \gt 0 \; \mathrm{is} \; \mathrm{true} \qquad 1 \gt 1 \; \mathrm{is} \; \mathrm{false}$$

We can show that

• the relations $\leq$ and $\geq$ are total orders with respect to the equality relation defined above and opposite of each other

• the relations $\lt$ and $\lt$ are pseudo-orders with respect to the equality relation defined above and opposite of each other

• the relations $\leq$ and $\gt$ are mutually decidable $x \leq y \vee x \gt y$.

• the relation $\lt$ and $\geq$ are mutually decidable $x \lt y \vee x \geq y$.

Boolean algebra structure

We can also define the logical functions on $\mathrm{Bool}$ using the recursion principle of the boolean domain.

Definition

The negation of a boolean $x \mapsto \neg x$ is recursively defined by

$$\neg 0 \coloneqq 1 \qquad \neg 1 \coloneqq 0$$

Definition

The conjunction of two booleans $x, y \mapsto x \wedge y$ is recursively defined by

$$0 \wedge 0 \coloneqq 0 \qquad 0 \wedge 1 \coloneqq 0 \qquad 1 \wedge 0 \coloneqq 0 \qquad 1 \wedge 1 \coloneqq 1$$

Definition

The disjunction of two booleans $x, y \mapsto x \vee y$ is recursively defined by

$$0 \vee 0 \coloneqq 0 \qquad 0 \vee 1 \coloneqq 1 \qquad 1 \vee 0 \coloneqq 1 \qquad 1 \vee 1 \coloneqq 1$$

Definition

The exclusive disjunction of two booleans $x, y \mapsto x \underline{\vee} y$ is recursively defined by

$$0 \underline{\vee} 0 \coloneqq 0 \qquad 0 \underline{\vee} 1 \coloneqq 1 \qquad 1 \underline{\vee} 0 \coloneqq 1 \qquad 1 \underline{\vee} 1 \coloneqq 0$$

Definition

The implication of two booleans $x, y \mapsto x \rightarrow y$ is recursively defined by

$$0 \rightarrow 0 \coloneqq 1 \qquad 0 \rightarrow 1 \coloneqq 1 \qquad 1 \rightarrow 0 \coloneqq 0 \qquad 1 \rightarrow 1 \coloneqq 1$$

Definition

The abjunction of two booleans $x, y \mapsto x \nrightarrow y$ is recursively defined by

$$0 \nrightarrow 0 \coloneqq 0 \qquad 0 \nrightarrow 1 \coloneqq 0 \qquad 1 \nrightarrow 0 \coloneqq 1 \qquad 1 \nrightarrow 1 \coloneqq 0$$

Definition

The converse implication of two booleans $x, y \mapsto x \leftarrow y$ is recursively defined by

$$0 \leftarrow 0 \coloneqq 1 \qquad 0 \leftarrow 1 \coloneqq 0 \qquad 1 \leftarrow 0 \coloneqq 1 \qquad 1 \leftarrow 1 \coloneqq 1$$

Definition

The converse abjunction of two booleans $x, y \mapsto x \nleftarrow y$ is recursively defined by

$$0 \nleftarrow 0 \coloneqq 0 \qquad 0 \nleftarrow 1 \coloneqq 1 \qquad 1 \nleftarrow 0 \coloneqq 1 \qquad 0 \nleftarrow 1 \coloneqq 0$$

Definition

The biconditional of two booleans $x, y \mapsto x \iff y$ is recursively defined by

$$0 \iff 0 \coloneqq 1 \qquad 0 \iff 1 \coloneqq 0 \qquad 1 \iff 0 \coloneqq 0 \qquad 1 \iff 1 \coloneqq 1$$

We can prove that

• $(\mathrm{Bool}, 0, 1, \neg, \wedge, \vee, \leq)$ forms a Boolean algebra with respect to the inductively defined total order above,

• $(\mathrm{Bool}, 0, 1, \wedge, \vee, \rightarrow, \leftarrow, \leq)$ forms a bi-Heyting algebra with respect to the inductively defined total order above,

• $(\mathrm{Bool}, 0, 1, \neg, \wedge, \underline{\vee})$ and $(\mathrm{Bool}, 1, 0, \neg, \vee, \underline{\vee})$ both form a Boolean ring

• For all booleans $x$ and $y$,

  $$x \iff y = 1 \;\mathrm{iff}\; x = y \qquad x \underline{\vee} y = 1 \;\mathrm{iff}\; x \neq y$$
  $$x \rightarrow y = 1 \;\mathrm{iff}\; x \leq y \qquad x \nrightarrow y = 1 \;\mathrm{iff}\; x \gt y \qquad x \leftarrow y = 1 \;\mathrm{iff}\; x \geq y \qquad x \nleftarrow y = 1 \;\mathrm{iff}\; x \lt y$$

In category theory

In category theory, the boolean domain is the discrete category $\mathbb{2}$ with two objects $0, 1 \in \mathbb{2}$. Pairs of objects in a category $C$ are equivalently functors $F:\mathbb{2} \to C$ from the boolean domain to $C$ by the recursion principle of the boolean domain. As a result, the boolean domain can be called the walking pair of objects or free-standing pair of objects or free-living pair of objects.

In addition, the boolean domain is the groupoid core of a number of categories, including the interval category and the walking parallel pair.

Related concepts

• decidable equality

• set of truth values

• boolean domain object

• type of booleans

• classical logic, two-valued logic

• walking structure

  • the boolean domain $2 \coloneqq \partial \Delta^1$; i.e. the walking pair of objects

  • the directed interval category $I \coloneqq \Delta^1$; i.e. the walking morphism

  • the (2,0)-horn category $\Lambda_0^2$; i.e. the walking cospan

  • the (2,1)-horn category $\Lambda_1^2$; i.e. the walking composable pair

  • the (2,2)-horn category $\Lambda_2^2$; i.e. the walking span

  • the 2-simplex category $\Delta^2$; i.e. the walking commutative triangle

  • the walking parallel pair

  • the walking isomorphism

  • Adj; i.e. the walking adjunction

  • the walking equivalence

  • the walking adjoint equivalence

  • the walking 2-isomorphism with trivial boundary

  • the syntactic category of a theory $T$; i.e. the walking $T$-model

• In dependent type theory, many higher inductive types can be considered to be walking structures:

  • the unit type is the walking element

  • the boolean type is the walking pair of elements

  • the interval type is the walking identification

  • one definition of the circle type is the walking self-identification

  • another definition of the circle type is the walking parallel pair of identifications.

  • the suspension type of a type $I$ is the walking parallel $I$-indexed family of identifications.

  • the natural numbers type is the walking sequence

  • the integers type is the walking bi-infinite sequence

  • the walking bridge

  • the directed interval type is the walking morphism in the sense of element of a hom type

References

See also:

• Wikipedia, Boolean domain