De Morgan algebras and Kleene algebras

LatticeWithInvolution is a bounded lattice with an involutive antitone complement ᶜ — the common reduct of OrthocomplementedLattice (which adds the complementation laws) and DeMorganAlgebra (which adds distributivity instead). The De Morgan laws are proved once here, from involution and antitonicity alone. An Order.KleeneAlgebra is a De Morgan algebra satisfying the Kleene law a ⊓ aᶜ ≤ b ⊔ bᶜ: every BooleanAlgebra qualifies (the law degenerates through ⊥), and the three-element chain Trivalent is the canonical non-Boolean example. These are the involution branch between mathlib's DistribLattice and BooleanAlgebra, beside the existing pseudocomplement branch (HeytingAlgebra).

Naming follows the literature exactly ("De Morgan algebra", "Kleene algebra" — the lattice notion, not the regular-expression star-semiring that holds mathlib's root KleeneAlgebra), disambiguated by namespace on the Order.Frame precedent. De Morgan algebras are here bounded, as in Balbes-Dwinger (the nLab entry defines the unbounded variant). [UPSTREAM] candidate for Mathlib/Order/DeMorganAlgebra/; the OrderDual/Prod/Pi instances and the OrderIso α αᵒᵈ bundling live in DeMorganAlgebra/Basic.lean.

Main definitions

• LatticeWithInvolution — bounded lattice + involutive antitone ᶜ; De Morgan (compl_sup/compl_inf), compl_bot/compl_top, and the injectivity/order lemmas are derived here.
• DeMorganAlgebra — a distributive LatticeWithInvolution.
• Order.KleeneAlgebra — a DeMorganAlgebra with the Kleene law (inf_compl_le_sup_compl); every BooleanAlgebra is an instance.

class LatticeWithInvolution (α : Type u_1) extends Lattice α, BoundedOrder α, Compl α : Type u_1

A bounded lattice with an involutive, order-reversing complement — the common reduct of OrthocomplementedLattice and DeMorganAlgebra. Compl is pure notation, so ᶜ carries no complementation laws here: a ⊓ aᶜ = ⊥ may fail.

• 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
• top : α
• le_top (a : α) : a ≤ ⊤
• bot : α
• bot_le (a : α) : ⊥ ≤ a
• compl : α → α
• compl_compl (a : α) : aᶜᶜ = a

  Complement is involutive: aᶜᶜ = a.

• compl_le_compl {a b : α} : a ≤ b → bᶜ ≤ aᶜ

  Complement is order-reversing.

theorem LatticeWithInvolution.compl_anti {α : Type u_1} [LatticeWithInvolution α] : Antitone compl

The complement is antitone (bundled form of the compl_le_compl field).

@[simp]

theorem LatticeWithInvolution.compl_le_compl_iff_le {α : Type u_1} [LatticeWithInvolution α] {a b : α} : aᶜ ≤ bᶜ ↔ b ≤ a

theorem LatticeWithInvolution.compl_injective {α : Type u_1} [LatticeWithInvolution α] : Function.Injective compl

@[simp]

theorem LatticeWithInvolution.compl_inj_iff {α : Type u_1} [LatticeWithInvolution α] {a b : α} : aᶜ = bᶜ ↔ a = b

theorem LatticeWithInvolution.compl_surjective {α : Type u_1} [LatticeWithInvolution α] : Function.Surjective compl

theorem LatticeWithInvolution.compl_eq_iff_eq_compl {α : Type u_1} [LatticeWithInvolution α] {a b : α} : aᶜ = b ↔ a = bᶜ

theorem LatticeWithInvolution.le_compl_comm {α : Type u_1} [LatticeWithInvolution α] {a b : α} : a ≤ bᶜ ↔ b ≤ aᶜ

Orthogonality is symmetric: a ≤ bᶜ ↔ b ≤ aᶜ.

@[simp]

theorem LatticeWithInvolution.compl_sup {α : Type u_1} [LatticeWithInvolution α] (a b : α) : (a ⊔ b)ᶜ = aᶜ ⊓ bᶜ

De Morgan: complement of a join is the meet of complements — from involution and antitonicity alone; no distributivity or complementation is used.

@[simp]

theorem LatticeWithInvolution.compl_inf {α : Type u_1} [LatticeWithInvolution α] (a b : α) : (a ⊓ b)ᶜ = aᶜ ⊔ bᶜ

De Morgan: complement of a meet is the join of complements.

@[simp]

theorem LatticeWithInvolution.compl_bot {α : Type u_1} [LatticeWithInvolution α] : ⊥ᶜ = ⊤

@[simp]

theorem LatticeWithInvolution.compl_top {α : Type u_1} [LatticeWithInvolution α] : ⊤ᶜ = ⊥

class DeMorganAlgebra (α : Type u_1) extends DistribLattice α, LatticeWithInvolution α : Type u_1

A De Morgan algebra: a distributive bounded lattice with an involutive antitone complement. Unlike BooleanAlgebra, complementation may fail (a ⊓ aᶜ ≠ ⊥).

• 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
• top : α
• le_top (a : α) : a ≤ ⊤
• bot : α
• bot_le (a : α) : ⊥ ≤ a
• compl : α → α
• compl_compl (a : α) : aᶜᶜ = a
• compl_le_compl {a b : α} : a ≤ b → bᶜ ≤ aᶜ

class Order.KleeneAlgebra (α : Type u_1) extends DeMorganAlgebra α : Type u_1

A Kleene algebra (the lattice notion, Kalman's variety of strong Kleene logic — not the regular-expression star-semiring at root KleeneAlgebra): a De Morgan algebra satisfying the Kleene law.

• 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
• top : α
• le_top (a : α) : a ≤ ⊤
• bot : α
• bot_le (a : α) : ⊥ ≤ a
• compl : α → α
• compl_compl (a : α) : aᶜᶜ = a
• compl_le_compl {a b : α} : a ≤ b → bᶜ ≤ aᶜ
• inf_compl_le_sup_compl (a b : α) : a ⊓ aᶜ ≤ b ⊔ bᶜ

  The Kleene law: contradictions lie below excluded middles.

@[implicit_reducible, instance 100]

instance BooleanAlgebra.toOrderKleeneAlgebra {α : Type u_1} [BooleanAlgebra α] : Order.KleeneAlgebra α

Every Boolean algebra is a Kleene algebra: the Kleene law degenerates through ⊥. Low priority so Boolean API is preferred where applicable.

Equations

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