nLab boolean domain

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.

Definition

In type theory

Assuming that identification types and dependent product types exist in the type theory, the boolean domain is the inductive type generated by two elements, and is defined by the following inference rules:

type formation rules for the boolean domain

ΓctxΓBittype\frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash \mathrm{Bit} \; \mathrm{type}}


term introduction rules for the boolean domain:

Γctx0:BitΓctxΓ1:Bit\frac{\Gamma \; \mathrm{ctx}}{\vdash 0:\mathrm{Bit}} \qquad \frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash 1:\mathrm{Bit}}


term elimination rules for the boolean domain:

Γ,x:BitC(x)typeΓ,c 0:C(0),c 1:C(1),p:Bitind Bit C(c 0,c 1,p):C(p)\frac{\Gamma, x:\mathrm{Bit} \vdash C(x) \; \mathrm{type}}{\Gamma, c_0:C(0), c_1:C(1), p:\mathrm{Bit} \vdash \mathrm{ind}_\mathrm{Bit}^C(c_0, c_1, p):C(p)}


computation rules for the boolean domain:

  • judgmental computation rules

    Γ,x:BitC(x)typeΓ,c 0:C(0),c 1:C(1)ind Bit C(c 0,c 1,0)c 0:C(0)\frac{\Gamma, x:\mathrm{Bit} \vdash C(x) \; \mathrm{type}}{\Gamma, c_0:C(0), c_1:C(1) \vdash \mathrm{ind}_\mathrm{Bit}^C(c_0, c_1, 0) \equiv c_0:C(0)}
    Γ,x:BitC(x)typeΓ,c 0:C(0),c 1:C(1)ind Bit C(c 0,c 1,1)c 1:C(1)\frac{\Gamma, x:\mathrm{Bit} \vdash C(x) \; \mathrm{type}}{\Gamma, c_0:C(0), c_1:C(1) \vdash \mathrm{ind}_\mathrm{Bit}^C(c_0, c_1, 1) \equiv c_1:C(1)}
  • propositional computation rules

    Γ,x:BitC(x)typeΓ,c 0:C(0),c 1:C(1)ind Bit C(c 0,c 1,0)= C(0)c 0true\frac{\Gamma, x:\mathrm{Bit} \vdash C(x) \; \mathrm{type}}{\Gamma, c_0:C(0), c_1:C(1) \vdash \mathrm{ind}_\mathrm{Bit}^C(c_0, c_1, 0) =_{C(0)} c_0 \; \mathrm{true}}
    Γ,x:BitC(x)typeΓ,c 0:C(0),c 1:C(1)ind Bit C(c 0,c 1,1)= C(1)c 1true\frac{\Gamma, x:\mathrm{Bit} \vdash C(x) \; \mathrm{type}}{\Gamma, c_0:C(0), c_1:C(1) \vdash \mathrm{ind}_\mathrm{Bit}^C(c_0, c_1, 1) =_{C(1)} c_1 \; \mathrm{true}}
  • typal computation rules

    Γ,x:BitC(x)typeΓ,c 0:C(0),c 1:C(1)β Bit 0(c 0,c 1):Id C(0)(ind Bit C(c 0,c 1,0),c 0)\frac{\Gamma, x:\mathrm{Bit} \vdash C(x) \; \mathrm{type}}{\Gamma, c_0:C(0), c_1:C(1) \vdash \beta_\mathrm{Bit}^0(c_0, c_1):\mathrm{Id}_{C(0)}(\mathrm{ind}_\mathrm{Bit}^C(c_0, c_1, 0), c_0)}
    Γ,x:BitC(x)typeΓ,c 0:C(0),c 1:C(1)β Bit 1(c 0,c 1,1):Id C(1)(ind Bit C(c 0,c 1,1),c 1)\frac{\Gamma, x:\mathrm{Bit} \vdash C(x) \; \mathrm{type}}{\Gamma, c_0:C(0), c_1:C(1) \vdash \beta_\mathrm{Bit}^1(c_0, c_1, 1):\mathrm{Id}_{C(1)}(\mathrm{ind}_\mathrm{Bit}^C(c_0, c_1, 1), c_1)}


uniqueness rules for the boolean domain:

  • judgmental uniqueness rules

    Γ,x:BitC(x)typeΓ,c: x:BitC(x),p:Bitind Bit C(c(0),c(1),p)c(p):C(p)\frac{\Gamma, x:\mathrm{Bit} \vdash C(x) \; \mathrm{type}}{\Gamma, c:\prod_{x:\mathrm{Bit}} C(x), p:\mathrm{Bit} \vdash \mathrm{ind}_\mathrm{Bit}^C(c(0), c(1), p) \equiv c(p):C(p)}
  • propositional uniqueness rules

    Γ,x:BitC(x)typeΓ,c: x:BitC(x),p:Bitind Bit C(c(0),c(1),p)= C(p)c(p)true\frac{\Gamma, x:\mathrm{Bit} \vdash C(x) \; \mathrm{type}}{\Gamma, c:\prod_{x:\mathrm{Bit}} C(x), p:\mathrm{Bit} \vdash \mathrm{ind}_\mathrm{Bit}^C(c(0), c(1), p) =_{C(p)} c(p) \; \mathrm{true}}
  • typal uniqueness rules

    Γ,x:BitC(x)typeΓ,c: x:BitC(x),p:Bitη Bit(c,p):Id C(p)(ind Bit C(c(0),c(1),p),c(p))\frac{\Gamma, x:\mathrm{Bit} \vdash C(x) \; \mathrm{type}}{\Gamma, c:\prod_{x:\mathrm{Bit}} C(x), p:\mathrm{Bit} \vdash \eta_\mathrm{Bit}(c, p):\mathrm{Id}_{C(p)}(\mathrm{ind}_\mathrm{Bit}^C(c(0), c(1), p), c(p))}


The elimination, typal computation, and typal uniqueness rules for the boolean domain state that the boolean domain satisfies the dependent universal property of the boolean domain. If the dependent type theory also has dependent sum types and product types, allowing one to define the uniqueness quantifier, the dependent universal property of the boolean domain could be simplified to the following rule:

Γ,x:BitC(x)typeΓ,c 0:C(0),c 1:C(1)up Bit C(c 0,c 1):!c: x:BitC(x).Id C(0)(c(0),c 0)×Id C(1)(c(1),c 1)\frac{\Gamma, x:\mathrm{Bit} \vdash C(x) \; \mathrm{type}}{\Gamma, c_0:C(0), c_1:C(1)\vdash \mathrm{up}_\mathrm{Bit}^C(c_0, c_1):\exists!c:\prod_{x:\mathrm{Bit}} C(x).\mathrm{Id}_{C(0)}(c(0), c_0) \times \mathrm{Id}_{C(1)}(c(1), c_1)}

The judgmental computation and uniqueness rules imply the typal computation and uniqueness rules and thus imply the dependent universal property of the boolean domain.

Extensionality principle of the boolean domain

The elements of the boolean domain represent certain truth values or propositions, namely, true and false. By the principle of propositions as some types, truth values or propositions are represented as certain types: specifically, true or 11 is represented by the unit type 𝟙\mathbb{1}, and false or 00 is represented by the empty type 𝟘\mathbb{0}. We represent the above by making the boolean domain into a Tarski universe, by including rules

ΓctxΓ,x:BitEl Bit(x)typeΓctxΓEl Bit(1)𝟙typeΓctxΓEl Bit(0)𝟘type\frac{\Gamma \; \mathrm{ctx}}{\Gamma, x:\mathrm{Bit} \vdash \mathrm{El}_\mathrm{Bit}(x) \; \mathrm{type}} \qquad\frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash \mathrm{El}_\mathrm{Bit}(1) \equiv \mathbb{1} \; \mathrm{type}} \qquad \frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash \mathrm{El}_\mathrm{Bit}(0) \equiv \mathbb{0} \; \mathrm{type}}

The extensionality principle of the boolean domain is then given by the univalence axiom:

ΓctxΓ,x:Bit,y:Bitua(x,y):Id Bit(x,y)(El Bit(x)El Bit(y))\frac{\Gamma \; \mathrm{ctx}}{\Gamma, x:\mathrm{Bit}, y:\mathrm{Bit} \vdash \mathrm{ua}(x, y):\mathrm{Id}_\mathrm{Bit}(x, y) \simeq (\mathrm{El}_\mathrm{Bit}(x) \simeq \mathrm{El}_\mathrm{Bit}(y))}

Since the empty type is not equivalent to the unit type, this automatically implies that 00 is not equal to 11.

In homotopy type theory

In homotopy type theory the type of booleans / bits looks as above (using judgemental equality, propositional equality, or typal equality for the computation rule and uniqueness rule) but now it may equivalently be thought of as the sphere type of the 0-sphere and as such as the beginning of the suspension type-tower of types of “higher homotopy bits” — the n n -sphere types:


References

See also:

Discussion in type theory as a simple example of an inductive type:

Discussion in homotopy type theory:

Last revised on June 6, 2023 at 12:46:38. See the history of this page for a list of all contributions to it.