Orthocomplemented Lattices

@cite{holliday-mandelkern-2024}

An orthocomplemented lattice (ortholattice) is a bounded lattice equipped with an involutive, order-reversing complement satisfying non-contradiction and excluded middle. Ortholattices generalize Boolean algebras by dropping distributivity — the algebraic foundation of possibility semantics.

Main definitions

• OrthocomplementedLattice — typeclass for ortholattices

Main results

• De Morgan laws: compl_sup, compl_inf
• ComplementedLattice instance
• Every BooleanAlgebra is an OrthocomplementedLattice

What fails

Not every ortholattice satisfies distributivity (a ⊓ (b ⊔ c) = (a ⊓ b) ⊔ (a ⊓ c)), pseudocomplementation (a ⊓ b = ⊥ → b ≤ aᶜ), or orthomodularity (a ≤ b → b = a ⊔ (aᶜ ⊓ b)). Concrete counterexamples live in PossibilitySemantics/Epistemic.lean.

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

An orthocomplemented lattice (ortholattice) is a bounded lattice with a complement ᶜ that is involutive and order-reversing, satisfying non-contradiction and excluded middle.

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 Semantics.PossibilitySemantics.OrthocomplementedLattice.inf_compl_eq_bot {α : Type u_1} [OrthocomplementedLattice α] (a : α) : a ⊓ aᶜ = ⊥

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

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

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

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

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

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

@[instance 100]

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

Every Boolean algebra is an orthocomplemented lattice. The converse fails: ortholattices need not be distributive.

Equations

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