Huntington's axioms for Boolean Algebras

In this file we derive an instance of Mathlib's BooleanAlgebra on an inhabited type, starting from operations of binary supremum · ⊔ · and complementation ·ᶜ, obeying the three axioms laid out in [Hun33b] and [Hun33a]:

• Supremum is associative: a ⊔ b ⊔ c = a ⊔ (b ⊔ c),
• Supremum is commutative: a ⊔ b = b ⊔ a, and
• Huntington's axiom: (aᶜ ⊔ b)ᶜ ⊔ (aᶜ ⊔ bᶜ)ᶜ = a.

These axioms are packaged in the class HuntingtonAlgebra, which should only be used for its instance HuntingtonAlgebra.instBooleanAlgebra.

References

• E. V. Huntington, "New Sets of Independent Postulates for the Algebra of Logic, With Special Reference to Whitehead and Russell's Principia Mathematica"
• E. V. Huntington, "Boolean Algebra. A Correction"

class HuntingtonAlgebra (α : Type u_1) extends Max α, Compl α, Inhabited α, Std.Associative fun (x1 x2 : α) => x1 ⊔ x2, Std.Commutative fun (x1 x2 : α) => x1 ⊔ x2 : Type u_1

A class for types obeying Huntington's axioms for Boolean algebras.

• max : α → α → α
• compl : α → α
• default : α
• assoc (a b c : α) : a ⊔ b ⊔ c = a ⊔ (b ⊔ c)
• comm (a b : α) : a ⊔ b = b ⊔ a
• huntington (a b : α) : (aᶜ ⊔ b)ᶜ ⊔ (aᶜ ⊔ bᶜ)ᶜ = a

  Huntington's axiom.

@[instance_reducible]

instance HuntingtonAlgebra.instTop {α : Type u_1} [HuntingtonAlgebra α] : Top α

Equations

• HuntingtonAlgebra.instTop = { top := default ⊔ defaultᶜ }

@[instance_reducible]

instance HuntingtonAlgebra.instBot {α : Type u_1} [HuntingtonAlgebra α] : Bot α

Equations

• HuntingtonAlgebra.instBot = { bot := ⊤ᶜ }

@[instance_reducible]

instance HuntingtonAlgebra.instMin {α : Type u_1} [HuntingtonAlgebra α] : Min α

Equations

• HuntingtonAlgebra.instMin = { min := fun (a b : α) => (aᶜ ⊔ bᶜ)ᶜ }

@[instance_reducible]

instance HuntingtonAlgebra.instBooleanAlgebra {α : Type u_1} [HuntingtonAlgebra α] : BooleanAlgebra α

Huntington algebras are Boolean algebras.

Equations

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