The ortholattice of a symmetric, irreflexive relation #

[UPSTREAM] candidate.

For a symmetric, irreflexive relation r : S → S → Prop — an orthogonality relation, written x ⊥ y — the formal Concepts of r form an OrthocomplementedLattice. The lattice structure is mathlib's concept lattice (Mathlib.Order.Concept); the new content is the orthocomplement Aᶜ = upperPolar r A = {x | ∀ y ∈ A, x ⊥ y}, which for symmetric r restricts to an order-reversing involution on extents.

This is the framework-agnostic core of possibility semantics for orthologic ([HM24] Proposition 4.8): the Semantics.Modality.Orthologic stack is the special case r = ¬compat, where orthoNeg = upperPolar r, regularClosure = extentClosure r, and the load-bearing involutivity (Proposition 4.8) is mathlib's upperPolar_lowerPolar_upperPolar. The bridge to that stack lives downstream (Core cannot import the semantics layer).

Main definitions #

Concept.instCompl — the orthocomplement Aᶜ = upperPolar r A.
Concept.instOrthocomplementedLattice — the concept lattice of a symmetric, irreflexive relation is an ortholattice.
Orthoframe — a bundled symmetric, irreflexive orthogonality relation; Orthoframe.Regular F is its ortholattice of regular propositions.

TODO #

Goldblatt representation ([HM24] Theorem 4.13): every complete ortholattice is isomorphic to Orthoframe.Regular of its canonical orthoframe on a join-dense set, with a ⊥ b ↔ a ≤ bᶜ.

source

theorem Order.upperPolar_eq_lowerPolar {S : Type u_1} (r : S → S → Prop) [Std.Symm r] (s : Set S) :

upperPolar r s = lowerPolar r s

For a symmetric relation the upper and lower polars coincide.

source

theorem Order.isExtent_upperPolar {S : Type u_1} (r : S → S → Prop) [Std.Symm r] (s : Set S) :

IsExtent r (upperPolar r s)

For a symmetric relation the upper polar of any set is an extent.

source

@[implicit_reducible]

instance Concept.instCompl {S : Type u_1} (r : S → S → Prop) [Std.Symm r] :

Compl (Concept S S r)

Orthocomplement of a concept: the concept whose extent is the intent (= upperPolar r) of c. Well-defined because r is symmetric.

Equations

Concept.instCompl r = { compl := fun (c : Concept S S r) => Concept.ofIsExtent r c.intent ⋯ }

source

@[simp]

theorem Concept.extent_compl {S : Type u_1} (r : S → S → Prop) [Std.Symm r] (c : Concept S S r) :

cᶜ.extent = c.intent

source

@[simp]

theorem Concept.intent_compl {S : Type u_1} (r : S → S → Prop) [Std.Symm r] (c : Concept S S r) :

cᶜ.intent = upperPolar r c.intent

source

@[implicit_reducible]

instance Concept.instSetLike {S : Type u_1} {r : S → S → Prop} :

SetLike (Concept S S r) S

A concept of a single-sorted relation is determined by its extent, so concepts form a SetLike family with ↑c = c.extent. (No PartialOrder diamond: SetLike supplies only Membership/coercions, and Concept's order is already extent-lifted.)

Equations

Concept.instSetLike = { coe := fun (c : Concept S S r) => c.extent, coe_injective := ⋯ }

source

theorem Concept.extent_bot_eq_empty {S : Type u_1} (r : S → S → Prop) [Std.Irrefl r] :

⊥.extent = ∅

For an irreflexive relation the bottom concept has empty extent (no point is orthogonal to everything, including itself).

source

@[implicit_reducible]

instance Concept.instOrthocomplementedLattice {S : Type u_1} (r : S → S → Prop) [Std.Symm r] [Std.Irrefl r] :

OrthocomplementedLattice (Concept S S r)

The concepts of a symmetric, irreflexive relation form an orthocomplemented lattice ([HM24] Proposition 4.8). The lattice structure is mathlib's concept lattice; only the orthocomplement and its four axioms are new.

Equations

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

Bundled orthoframes #

source

structure Orthoframe (S : Type u_1) :

Type u_1

An orthoframe: a set with a symmetric, irreflexive orthogonality relation ortho (written x ⊥ y). Its regular propositions form an ortholattice (Orthoframe.Regular). The Semantics.Modality.Orthologic compatibility frames are the special case ortho = ¬compat.

ortho : S → S → Prop
The orthogonality relation, written x ⊥ y.
ortho_symm : Std.Symm self.ortho
ortho_irrefl : Std.Irrefl self.ortho