nLab boolean domain

Redirected from "Boolean field".
Contents

Contents

Idea

The boolean domain or boolean field (often just: BoolBool) is a 22-element set, say 𝔹={0,1}\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 xx is a variable that takes its value in a boolean domain, as xβˆˆπ”Ή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 22 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.

Boolβ‰…{P∈Ω|P∨¬P}\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)P(n) true for every bit, it suffices to prove it for falsehood P(0)P(0) and truth P(1)P(1).

Similarly, the boolean domain also has a recursion principle, which states that to define a function f:Bool→Af:\mathrm{Bool} \to A from the boolean domain to a set AA, it suffices to define the function when evaluated at falsehood f(0)f(0) and truth f(1)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=yx = y, inductively defined by

0=0istrue0=1isfalse1=0isfalse1=1istrue0 = 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≠yx \neq y, inductively defined by

0β‰ 0isfalse0β‰ 1istrue1β‰ 0istrue1β‰ 1isfalse0 \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∨xβ‰ yx = 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=yx = y if and only if x= Boolyx =_\mathrm{Bool} y for the predefined equality relation x= Boolyx =_\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≀yx \leq y is inductively defined by

0≀0istrue0≀1istrue1≀0isfalse1≀1istrue0 \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β‰₯yx \geq y is inductively defined by

0β‰₯0istrue0β‰₯1isfalse1β‰₯0istrue1β‰₯1istrue0 \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<yx \lt y is inductively defined by

0<0isfalse0<1istrue1<0isfalse1<1isfalse0 \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>yx \gt y is inductively defined by

0>0isfalse0>1isfalse1>0istrue1>1isfalse0 \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≀y∨x>yx \leq y \vee x \gt y.

  • the relation <\lt and β‰₯\geq are mutually decidable x<y∨xβ‰₯yx \lt y \vee x \geq y.

Boolean algebra structure

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

Definition

The negation of a boolean x↦¬xx \mapsto \neg x is recursively defined by

Β¬0≔1Β¬1≔0\neg 0 \coloneqq 1 \qquad \neg 1 \coloneqq 0

Definition

The conjunction of two booleans x,y↦x∧yx, y \mapsto x \wedge y is recursively defined by

0∧0≔00∧1≔01∧0≔01∧1≔10 \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↦x∨yx, y \mapsto x \vee y is recursively defined by

0∨0≔00∨1≔11∨0≔11∨1≔10 \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↦x∨̲yx, y \mapsto x \underline{\vee} y is recursively defined by

0∨̲0≔00∨̲1≔11∨̲0≔11∨̲1≔00 \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↦xβ†’yx, y \mapsto x \rightarrow y is recursively defined by

0β†’0≔10β†’1≔11β†’0≔01β†’1≔10 \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↦x↛yx, y \mapsto x \nrightarrow y is recursively defined by

0↛0≔00↛1≔01↛0≔11↛1≔00 \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↦x←yx, y \mapsto x \leftarrow y is recursively defined by

0←0≔10←1≔01←0≔11←1≔10 \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↦xβ†šyx, y \mapsto x \nleftarrow y is recursively defined by

0β†š0≔00β†š1≔11β†š0≔10β†š1≔00 \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↦x⇔yx, y \mapsto x \iff y is recursively defined by

0⇔0≔10⇔1≔01⇔0≔01⇔1≔10 \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

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

  • (Bool,0,1,∧,∨,β†’,←,≀)(\mathrm{Bool}, 0, 1, \wedge, \vee, \rightarrow, \leftarrow, \leq) forms a bi-Heyting algebra with respect to the inductively defined total order above,

  • (Bool,0,1,Β¬,∧,∨̲)(\mathrm{Bool}, 0, 1, \neg, \wedge, \underline{\vee}) and (Bool,1,0,Β¬,∨,∨̲)(\mathrm{Bool}, 1, 0, \neg, \vee, \underline{\vee}) both form a Boolean ring

  • For all booleans xx and yy,

    x⇔y=1iffx=yx∨̲y=1iffxβ‰ yx \iff y = 1 \;\mathrm{iff}\; x = y \qquad x \underline{\vee} y = 1 \;\mathrm{iff}\; x \neq y
    xβ†’y=1iffx≀yx↛y=1iffx>yx←y=1iffxβ‰₯yxβ†šy=1iffx<yx \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

References

See also:

Last revised on May 15, 2025 at 11:25:04. See the history of this page for a list of all contributions to it.