The Ginsberg–Fitting bilattice product (twist structure)

[Avr96] [AA96]

A bilattice carries two lattice orders on one carrier — a truth order ≤_t and a knowledge/information order ≤_k — with the four operations monotone w.r.t. both (an interlaced bilattice, [Avr96] Def 2.1). The fundamental construction is the twist product (Ginsberg–Fitting product) L ⊙ R of two bounded lattices ([Avr96] Def 2.4): the carrier is L × R, where a value (a, b) records evidence for (a ∈ L) and against (b ∈ R).

• the knowledge order ≤_k is the product order on L × R (more evidence both ways) — i.e. mathlib's Prod lattice, with ⊗ = ⊓, ⊕ = ⊔;
• the truth order ≤_t dualizes the second factor (more for, less against); its operations ∧/∨ are tInf/tSup.

Following the project's plain-Prop convention (and avoiding the Prod-instance clash of putting two Lattices on one type), the knowledge structure is mathlib's Prod lattice (≤, ⊓, ⊔), while the truth structure is the named relations/operations tLE, tInf, tSup.

This file proves the constructive half of the structure theory ([Avr96] Thm 2.5): the twist product is an interlaced bilattice — the truth relations form a lattice, and all four operations are interlaced.

Evidential S (Core.Logic.Bilattice) is the diagonal case S ⊙ S; FOUR = Bool ⊙ Bool, PRESUP = Fin 3 ⊙ Fin 3.

Main results

• Bilattice.TwistProduct.tLE/tInf/tSup — the truth order, meet ∧, join ∨
• tInf_isGLB-style lemmas (tInf_tLE_left, le_tInf, …) — the truth lattice
• tInf_kmono/tSup_kmono/kInf_tmono/kSup_tmono — the four interlacing laws (truth ops are ≤_k-monotone; knowledge ops ⊓/⊔ are ≤_t-monotone)
• neg, neg_neg, neg_tLE, neg_kLE — Ginsberg negation on the diagonal L ⊙ L

TODO

The representation theorem ([Avr96] Thm 4.3), the converse of Thm 2.5: every interlaced bilattice B is isomorphic to L_B ⊙ R_B for bounded lattices L_B = {x | ⊥ ≤_t x}, R_B = {x | x ≤_t ⊥}, via g x = (x ∨ ⊥, x ∧ ⊥) with inverse (a, b) ↦ a ⊕ b; L_B, R_B are unique up to isomorphism, and with a negation L_B ≅ R_B. This needs an abstract InterlacedBilattice class and the interlacing-algebra chain (Avron Prop 3.2 → Cor 3.8 → Thm 4.3); it is the theorem that earns the abstract class.

def Bilattice.TwistProduct.tLE {L : Type u} {R : Type v} [Lattice L] [Lattice R] (x y : L × R) : Prop

Truth order ≤_t on L × R: more evidence-for, less evidence-against ([Avr96] Def 2.4(ii)). The knowledge order ≤_k is the Prod order ≤.

Equations

• Bilattice.TwistProduct.tLE x y = (x.fst ≤ y.fst ∧ y.snd ≤ x.snd)

def Bilattice.TwistProduct.tInf {L : Type u} {R : Type v} [Lattice L] [Lattice R] (x y : L × R) : L × R

Truth meet ∧: meet the evidence-for, join the evidence-against ([Avr96] Def 2.4(iv)). The knowledge meet ⊗ is the Prod meet ⊓.

Equations

• Bilattice.TwistProduct.tInf x y = (x.fst ⊓ y.fst, x.snd ⊔ y.snd)

def Bilattice.TwistProduct.tSup {L : Type u} {R : Type v} [Lattice L] [Lattice R] (x y : L × R) : L × R

Truth join ∨: join the evidence-for, meet the evidence-against ([Avr96] Def 2.4(iii)). The knowledge join ⊕ is the Prod join ⊔.

Equations

• Bilattice.TwistProduct.tSup x y = (x.fst ⊔ y.fst, x.snd ⊓ y.snd)

theorem Bilattice.TwistProduct.tLE_refl {L : Type u} {R : Type v} [Lattice L] [Lattice R] (x : L × R) : tLE x x

theorem Bilattice.TwistProduct.tLE_trans {L : Type u} {R : Type v} [Lattice L] [Lattice R] {x y z : L × R} (h₁ : tLE x y) (h₂ : tLE y z) : tLE x z

theorem Bilattice.TwistProduct.tLE_antisymm {L : Type u} {R : Type v} [Lattice L] [Lattice R] {x y : L × R} (h₁ : tLE x y) (h₂ : tLE y x) : x = y

The truth order is a lattice

theorem Bilattice.TwistProduct.tInf_tLE_left {L : Type u} {R : Type v} [Lattice L] [Lattice R] (x y : L × R) : tLE (tInf x y) x

theorem Bilattice.TwistProduct.tInf_tLE_right {L : Type u} {R : Type v} [Lattice L] [Lattice R] (x y : L × R) : tLE (tInf x y) y

theorem Bilattice.TwistProduct.tLE_tInf {L : Type u} {R : Type v} [Lattice L] [Lattice R] {x y z : L × R} (h₁ : tLE z x) (h₂ : tLE z y) : tLE z (tInf x y)

theorem Bilattice.TwistProduct.tLE_tSup_left {L : Type u} {R : Type v} [Lattice L] [Lattice R] (x y : L × R) : tLE x (tSup x y)

theorem Bilattice.TwistProduct.tLE_tSup_right {L : Type u} {R : Type v} [Lattice L] [Lattice R] (x y : L × R) : tLE y (tSup x y)

theorem Bilattice.TwistProduct.tSup_tLE {L : Type u} {R : Type v} [Lattice L] [Lattice R] {x y z : L × R} (h₁ : tLE x z) (h₂ : tLE y z) : tLE (tSup x y) z

Interlacing

The four operations are monotone w.r.t. both orders ([Avr96] Def 2.1(3)). The knowledge structure is mathlib's Prod lattice (≤, ⊓, ⊔); the truth operations are tInf/tSup.

theorem Bilattice.TwistProduct.tInf_kmono {L : Type u} {R : Type v} [Lattice L] [Lattice R] {x y : L × R} (z : L × R) (h : x ≤ y) : tInf x z ≤ tInf y z

Interlacing 1: the truth meet ∧ is ≤_k-monotone.

theorem Bilattice.TwistProduct.tSup_kmono {L : Type u} {R : Type v} [Lattice L] [Lattice R] {x y : L × R} (z : L × R) (h : x ≤ y) : tSup x z ≤ tSup y z

Interlacing 2: the truth join ∨ is ≤_k-monotone.

theorem Bilattice.TwistProduct.kInf_tmono {L : Type u} {R : Type v} [Lattice L] [Lattice R] {x y : L × R} (z : L × R) (h : tLE x y) : tLE (x ⊓ z) (y ⊓ z)

Interlacing 3: the knowledge meet ⊗ = ⊓ is ≤_t-monotone.

theorem Bilattice.TwistProduct.kSup_tmono {L : Type u} {R : Type v} [Lattice L] [Lattice R] {x y : L × R} (z : L × R) (h : tLE x y) : tLE (x ⊔ z) (y ⊔ z)

Interlacing 4: the knowledge join ⊕ = ⊔ is ≤_t-monotone.

Bounds

With bounded factors the twist product has four extremes ([Avr96] Def 2.4(vii)): truth bounds t = (⊤, ⊥), f = (⊥, ⊤), and knowledge bounds ⊤ = (⊤, ⊤), ⊥ = (⊥, ⊥) (the latter are the Prod BoundedOrder).

def Bilattice.TwistProduct.tTop {L : Type u} {R : Type v} [Lattice L] [Lattice R] [BoundedOrder L] [BoundedOrder R] : L × R

Truth top t = (⊤, ⊥) (maximal for, minimal against).

Equations

• Bilattice.TwistProduct.tTop = (⊤, ⊥)

def Bilattice.TwistProduct.tBot {L : Type u} {R : Type v} [Lattice L] [Lattice R] [BoundedOrder L] [BoundedOrder R] : L × R

Truth bottom f = (⊥, ⊤).

Equations

• Bilattice.TwistProduct.tBot = (⊥, ⊤)

theorem Bilattice.TwistProduct.tLE_tTop {L : Type u} {R : Type v} [Lattice L] [Lattice R] [BoundedOrder L] [BoundedOrder R] (x : L × R) : tLE x tTop

theorem Bilattice.TwistProduct.tBot_tLE {L : Type u} {R : Type v} [Lattice L] [Lattice R] [BoundedOrder L] [BoundedOrder R] (x : L × R) : tLE tBot x

Negation

On the diagonal L ⊙ L, Ginsberg's negation swaps the coordinates: it reverses ≤_t, preserves ≤_k, and is an involution ([Avr96] Thm 2.5(2)).

def Bilattice.TwistProduct.neg {L : Type u} (x : L × L) : L × L

Ginsberg negation on L ⊙ L: swap evidence for/against.

Equations

• Bilattice.TwistProduct.neg x = (x.snd, x.fst)

@[simp]

theorem Bilattice.TwistProduct.neg_neg {L : Type u} (x : L × L) : neg (neg x) = x

theorem Bilattice.TwistProduct.neg_tLE {L : Type u} [Lattice L] {x y : L × L} (h : tLE x y) : tLE (neg y) (neg x)

Negation reverses the truth order ([Avr96] Def 2.3(ii)).

theorem Bilattice.TwistProduct.neg_kLE {L : Type u} [Lattice L] {x y : L × L} (h : x ≤ y) : neg x ≤ neg y

Negation preserves the knowledge order ([Avr96] Def 2.3(iii)).