(Generalized) Boolean algebras

This file sets up the theory of (generalized) Boolean algebras.

A Boolean algebra is a bounded distributive lattice with a complement operator. Boolean algebras generalize the (classical) logic of propositions and the lattice of subsets of a set.

Generalized Boolean algebras may be less familiar, but they are essentially Boolean algebras which do not necessarily have a top element (⊤) (and hence not all elements may have complements). One example in mathlib is Finset α, the type of all finite subsets of an arbitrary (not-necessarily-finite) type α.

GeneralizedBooleanAlgebra α is defined to be a distributive lattice with bottom (⊥) admitting a relative complement operator, written using "set difference" notation as x \ y (sdiff x y). For convenience, the BooleanAlgebra type class is defined to extend GeneralizedBooleanAlgebra so that it is also bundled with a \ operator.

(A terminological point: x \ y is the complement of y relative to the interval [⊥, x]. We do not yet have relative complements for arbitrary intervals, as we do not even have lattice intervals.)

Main declarations

• GeneralizedBooleanAlgebra: a type class for generalized Boolean algebras
• BooleanAlgebra: a type class for Boolean algebras.
• Prop.booleanAlgebra: the Boolean algebra instance on Prop

Implementation notes

The sup_inf_sdiff and inf_inf_sdiff axioms for the relative complement operator in GeneralizedBooleanAlgebra are taken from Wikipedia.

[Stone's paper introducing generalized Boolean algebras][Stone1935] does not define a relative complement operator a \ b for all a, b. Instead, the postulates there amount to an assumption that for all a, b : α where a ≤ b, the equations x ⊔ a = b and x ⊓ a = ⊥ have a solution x. Disjoint.sdiff_unique proves that this x is in fact b \ a.

References

• https://en.wikipedia.org/wiki/Boolean_algebra_(structure)#Generalizations
• [Postulates for Boolean Algebras and Generalized Boolean Algebras, M.H. Stone][Stone1935]
• [Lattice Theory: Foundation, George Grätzer][Gratzer2011]

Tags

generalized Boolean algebras, Boolean algebras, lattices, sdiff, compl

Generalized Boolean algebras

class GeneralizedBooleanAlgebra (α : Type u) extends DistribLattice α, SDiff α, Bot α : Type u

A generalized Boolean algebra is a distributive lattice with ⊥ and a relative complement operation \ (called sdiff, after "set difference") satisfying (a ⊓ b) ⊔ (a \ b) = a and (a ⊓ b) ⊓ (a \ b) = ⊥, i.e. a \ b is the complement of b in a.

This is a generalization of Boolean algebras which applies to Finset α for arbitrary (not-necessarily-Fintype) α.

• le : α → α → Prop
• lt : α → α → Prop
• le_refl (a : α) : a ≤ a
• le_trans (a b c : α) : a ≤ b → b ≤ c → a ≤ c
• lt_iff_le_not_ge (a b : α) : a < b ↔ a ≤ b ∧ ¬b ≤ a
• le_antisymm (a b : α) : a ≤ b → b ≤ a → a = b
• sup : α → α → α
• le_sup_left (a b : α) : a ≤ sup a b
• le_sup_right (a b : α) : b ≤ sup a b
• sup_le (a b c : α) : a ≤ c → b ≤ c → sup a b ≤ c
• inf : α → α → α
• inf_le_left (a b : α) : Lattice.inf a b ≤ a
• inf_le_right (a b : α) : Lattice.inf a b ≤ b
• le_inf (a b c : α) : a ≤ b → a ≤ c → a ≤ Lattice.inf b c
• le_sup_inf (x y z : α) : (x ⊔ y) ⊓ (x ⊔ z) ≤ x ⊔ y ⊓ z
• sdiff : α → α → α
• bot : α
• sup_inf_sdiff (a b : α) : a ⊓ b ⊔ a \ b = a

  For any a, b, (a ⊓ b) ⊔ (a / b) = a

• inf_inf_sdiff (a b : α) : a ⊓ b ⊓ a \ b = ⊥

  For any a, b, (a ⊓ b) ⊓ (a / b) = ⊥

Boolean algebras

class BooleanAlgebra (α : Type u) extends DistribLattice α, HasCompl α, SDiff α, HImp α, Top α, Bot α : Type u

A Boolean algebra is a bounded distributive lattice with a complement operator ᶜ such that x ⊓ xᶜ = ⊥ and x ⊔ xᶜ = ⊤. For convenience, it must also provide a set difference operation \ and a Heyting implication ⇨ satisfying x \ y = x ⊓ yᶜ and x ⇨ y = y ⊔ xᶜ.

This is a generalization of (classical) logic of propositions, or the powerset lattice.

Since BoundedOrder, OrderBot, and OrderTop are mixins that require LE to be present at define-time, the extends mechanism does not work with them. Instead, we extend using the underlying Bot and Top data typeclasses, and replicate the order axioms of those classes here. A "forgetful" instance back to BoundedOrder is provided.

• le : α → α → Prop
• lt : α → α → Prop
• le_refl (a : α) : a ≤ a
• le_trans (a b c : α) : a ≤ b → b ≤ c → a ≤ c
• lt_iff_le_not_ge (a b : α) : a < b ↔ a ≤ b ∧ ¬b ≤ a
• le_antisymm (a b : α) : a ≤ b → b ≤ a → a = b
• sup : α → α → α
• le_sup_left (a b : α) : a ≤ sup a b
• le_sup_right (a b : α) : b ≤ sup a b
• sup_le (a b c : α) : a ≤ c → b ≤ c → sup a b ≤ c
• inf : α → α → α
• inf_le_left (a b : α) : Lattice.inf a b ≤ a
• inf_le_right (a b : α) : Lattice.inf a b ≤ b
• le_inf (a b c : α) : a ≤ b → a ≤ c → a ≤ Lattice.inf b c
• le_sup_inf (x y z : α) : (x ⊔ y) ⊓ (x ⊔ z) ≤ x ⊔ y ⊓ z
• compl : α → α
• sdiff : α → α → α
• himp : α → α → α
• top : α
• bot : α
• inf_compl_le_bot (x : α) : x ⊓ xᶜ ≤ ⊥

  The infimum of x and xᶜ is at most ⊥

• top_le_sup_compl (x : α) : ⊤ ≤ x ⊔ xᶜ

  The supremum of x and xᶜ is at least ⊤

• le_top (a : α) : a ≤ ⊤

  ⊤ is the greatest element

• bot_le (a : α) : ⊥ ≤ a

  ⊥ is the least element

• sdiff_eq (x y : α) : x \ y = x ⊓ yᶜ

  x \ y is equal to x ⊓ yᶜ

• himp_eq (x y : α) : x ⇨ y = y ⊔ xᶜ

  x ⇨ y is equal to y ⊔ xᶜ

@[instance 100]

instance BooleanAlgebra.toBoundedOrder {α : Type u} [h : BooleanAlgebra α] : BoundedOrder α

Equations

• BooleanAlgebra.toBoundedOrder = { toTop := h.toTop, le_top := ⋯, toBot := h.toBot, bot_le := ⋯ }

instance Prop.instBooleanAlgebra : BooleanAlgebra Prop

Equations

• One or more equations did not get rendered due to their size.

instance Bool.instBooleanAlgebra : BooleanAlgebra Bool

Equations

• One or more equations did not get rendered due to their size.

theorem Bool.sup_eq_bor : (fun (x1 x2 : Bool) => max x1 x2) = or

theorem Bool.inf_eq_band : (fun (x1 x2 : Bool) => min x1 x2) = and

@[simp]

theorem Bool.compl_eq_bnot : compl = not

instance PUnit.instBooleanAlgebra : BooleanAlgebra PUnit.{u_2 + 1}

Equations

• One or more equations did not get rendered due to their size.

noncomputable def DistribLattice.booleanAlgebraOfComplemented (α : Type u) [DistribLattice α] [BoundedOrder α] [ComplementedLattice α] : BooleanAlgebra α

An alternative constructor for Boolean algebras: a distributive lattice that is complemented is a Boolean algebra.

This is not an instance, because it creates data using choice.

Equations

• One or more equations did not get rendered due to their size.