Orthocomplemented Lattices

An orthocomplemented lattice (or ortholattice) is a bounded lattice equipped with an involutive, order-reversing complement satisfying non-contradiction and excluded middle. It is the structural dual of a HeytingAlgebra: where Heyting drops the law of excluded middle but retains distributivity, ortholattices keep excluded middle but drop distributivity. BooleanAlgebra = OrthocomplementedLattice + DistribLattice.

The canonical examples are:

• closed subspaces of an inner-product space (orthocomplement = orthogonal complement) — see Birkhoff & von Neumann (1936) "The Logic of Quantum Mechanics", Annals of Mathematics 37(4):823-843, originally formulating ortholattices for quantum-mechanical propositions;
• Set-of-◇-regular subsets of a compatibility frame (Holliday & Mandelkern 2024 "The Orthologic of Epistemic Modals", Journal of Philosophical Logic).

Main definitions

• OrthocomplementedLattice α — typeclass extending Lattice α, BoundedOrder α, Compl α with the four ortholattice axioms.

Main results

• De Morgan laws (compl_sup, compl_inf).
• compl_injective, compl_surjective, compl_le_compl_iff_le.
• instBooleanOrtho: every BooleanAlgebra is an OrthocomplementedLattice (low priority so Boolean instances aren't obscured).
• instComplementedLattice: every ortholattice is ComplementedLattice (the existential mathlib typeclass; we strengthen it to a chosen complement function).

What fails (relative to BooleanAlgebra)

Ortholattices need not satisfy:

• distributivity: a ⊓ (b ⊔ c) = (a ⊓ b) ⊔ (a ⊓ c);
• pseudocomplementation: a ⊓ b = ⊥ → b ≤ aᶜ;
• orthomodularity: a ≤ b → b = a ⊔ (aᶜ ⊓ b).

Imposing distributivity collapses the typeclass to BooleanAlgebra; imposing orthomodularity yields orthomodular lattices (the algebra of quantum-mechanical propositions). Concrete counterexamples to all three appear in Linglib.Phenomena.Modality.Studies.HollidayMandelkern2024.

TODO

Upstream candidate for Mathlib/Order/Ortholattice.lean. The natural mathlib consumer is the lattice of closed subspaces of a Hilbert space (via Mathlib.Analysis.InnerProductSpace.Orthogonal), which currently provides every ingredient (Submodule.orthogonal, inf_orthogonal_eq_bot, le_orthogonal_orthogonal) but stops short of packaging an OrthocomplementedLattice instance because the typeclass is missing.

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

An orthocomplemented lattice (ortholattice) is a bounded lattice α equipped with an involutive, order-reversing complement ᶜ satisfying non-contradiction (a ⊓ aᶜ ≤ ⊥) and excluded middle (⊤ ≤ a ⊔ aᶜ).

Every BooleanAlgebra is an ortholattice. The converse fails: ortholattices need not be distributive.

• 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_antitone {a b : α} : a ≤ b → bᶜ ≤ aᶜ

  Complement is order-reversing.

• inf_compl_le_bot (a : α) : a ⊓ aᶜ ≤ ⊥

  Non-contradiction: a ⊓ aᶜ ≤ ⊥.

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

  Excluded middle: ⊤ ≤ a ⊔ aᶜ.

@[simp]

theorem OrthocomplementedLattice.inf_compl_eq_bot {α : Type u_1} [OrthocomplementedLattice α] (a : α) : a ⊓ aᶜ = ⊥

@[simp]

theorem OrthocomplementedLattice.sup_compl_eq_top {α : Type u_1} [OrthocomplementedLattice α] (a : α) : a ⊔ aᶜ = ⊤

@[simp]

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

@[simp]

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

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

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

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

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

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

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

theorem OrthocomplementedLattice.isCompl_compl {α : Type u_1} [OrthocomplementedLattice α] (a : α) : IsCompl a aᶜ

instance OrthocomplementedLattice.instComplementedLattice {α : Type u_1} [OrthocomplementedLattice α] : ComplementedLattice α

@[implicit_reducible, instance 100]

instance instBooleanOrtho {α : Type u_1} [BooleanAlgebra α] : OrthocomplementedLattice α

Every Boolean algebra is an orthocomplemented lattice. The converse fails: ortholattices need not be distributive. Low priority so existing BooleanAlgebra API is preferred where applicable.

Equations

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