Interlaced bilattices (abstract)

[Avr96]

An interlaced bilattice ([Avr96] Def 2.1) is one carrier with two bounded lattice orders — a truth order ≤_t and a knowledge order ≤_k — such that all four lattice operations are monotone with respect to both orders.

To carry two lattice structures on one carrier without an instance clash, we use the OrderDual-style trick: the truth lattice is the carrier's own [Lattice B] [BoundedOrder B], while the knowledge lattice lives on a type synonym Know B (a distinct type head, so [Lattice (Know B)] is a separate instance). The truth meet/join are ⊓/⊔; the knowledge meet/join (consensus ⊗, gullibility ⊕) are written through the synonym.

This file sets up the synonym, the interlacing mixin, and proves the general representation theorem ([Avr96] Thm 4.3): every interlaced bilattice is the twist product of the knowledge-order principal ideals of its truth bounds. Unlike Core.Logic.Bilattice.Representation (which handles the distributive special case via whole-lattice distributivity), this holds for any interlaced bilattice — the key identities (Cor 3.5, Cor 3.8) are derived from interlacing alone, by truth-antisymmetry and a fiber lemma rather than Avron's interval argument.

Main definitions / results

• Bilattice.Know — the knowledge-order synonym; toKnow/ofKnow the casts
• Bilattice.kInf/kSup — knowledge meet ⊗ / join ⊕ (scoped ⊗/⊕)
• Bilattice.kLE — knowledge order ≤_k (scoped ≤ₖ)
• Bilattice.Interlaced — the four interlacing laws (mixin, [Avr96] Def 2.1)
• Bilattice.inf_kT_sup_inf_kF — Cor 3.8: X = (X ⊗ t) ⊕ (X ⊗ f)
• Bilattice.isCompl_truthBounds — Cor 3.5: t, f are knowledge-complementary
• Bilattice.decompose — Thm 4.3: Know B ≃o Iic t × Iic f

def Bilattice.Know (B : Type u) : Type u

The knowledge-order synonym of a bilattice carrier (cf. OrderDual). It is the same underlying type as B, but a distinct type head, so it can carry the knowledge lattice as a separate instance from B's truth lattice.

Equations

• Bilattice.Know B = B

def Bilattice.toKnow {B : Type u} : B ≃ Know B

Cast into the knowledge synonym.

Equations

• Bilattice.toKnow = Equiv.refl B

def Bilattice.ofKnow {B : Type u} : Know B ≃ B

Cast out of the knowledge synonym.

Equations

• Bilattice.ofKnow = Equiv.refl B

@[simp]

theorem Bilattice.toKnow_ofKnow {B : Type u} (x : Know B) : toKnow (ofKnow x) = x

@[simp]

theorem Bilattice.ofKnow_toKnow {B : Type u} (x : B) : ofKnow (toKnow x) = x

def Bilattice.kInf {B : Type u} [Lattice (Know B)] (x y : B) : B

Knowledge meet ⊗ (consensus): the meet in the knowledge lattice.

Equations

• Bilattice.kInf x y = Bilattice.ofKnow (Bilattice.toKnow x ⊓ Bilattice.toKnow y)

def Bilattice.kSup {B : Type u} [Lattice (Know B)] (x y : B) : B

Knowledge join ⊕ (gullibility): the join in the knowledge lattice.

Equations

• Bilattice.kSup x y = Bilattice.ofKnow (Bilattice.toKnow x ⊔ Bilattice.toKnow y)

def Bilattice.«term_⊗_» : Lean.TrailingParserDescr

Knowledge meet ⊗ (consensus): the meet in the knowledge lattice.

Equations

• Bilattice.«term_⊗_» = Lean.ParserDescr.trailingNode `Bilattice.«term_⊗_» 70 70 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊗ ") (Lean.ParserDescr.cat `term 71))

def Bilattice.«term_⊕_» : Lean.TrailingParserDescr

Knowledge join ⊕ (gullibility): the join in the knowledge lattice.

Equations

• Bilattice.«term_⊕_» = Lean.ParserDescr.trailingNode `Bilattice.«term_⊕_» 65 65 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊕ ") (Lean.ParserDescr.cat `term 66))

@[simp]

theorem Bilattice.toKnow_kInf {B : Type u} [Lattice (Know B)] (x y : B) : toKnow (kInf x y) = toKnow x ⊓ toKnow y

@[simp]

theorem Bilattice.toKnow_kSup {B : Type u} [Lattice (Know B)] (x y : B) : toKnow (kSup x y) = toKnow x ⊔ toKnow y

theorem Bilattice.kInf_self {B : Type u} [Lattice (Know B)] (x : B) : kInf x x = x

Knowledge meet is idempotent.

theorem Bilattice.kSup_self {B : Type u} [Lattice (Know B)] (x : B) : kSup x x = x

Knowledge join is idempotent.

theorem Bilattice.kInf_comm {B : Type u} [Lattice (Know B)] (x y : B) : kInf x y = kInf y x

Knowledge meet is commutative.

theorem Bilattice.kSup_comm {B : Type u} [Lattice (Know B)] (x y : B) : kSup x y = kSup y x

Knowledge join is commutative.

theorem Bilattice.kSup_kInf_self {B : Type u} [Lattice (Know B)] (x y : B) : kSup x (kInf x y) = x

Knowledge absorption: x ⊕ (x ⊗ y) = x.

theorem Bilattice.kInf_kSup_self {B : Type u} [Lattice (Know B)] (x y : B) : kInf x (kSup x y) = x

Knowledge absorption: x ⊗ (x ⊕ y) = x.

def Bilattice.kLE {B : Type u} [Preorder (Know B)] (x y : B) : Prop

Knowledge order ≤_k.

Equations

• Bilattice.kLE x y = (Bilattice.toKnow x ≤ Bilattice.toKnow y)

def Bilattice.«term_≤ₖ_» : Lean.TrailingParserDescr

Knowledge order ≤_k.

Equations

• Bilattice.«term_≤ₖ_» = Lean.ParserDescr.trailingNode `Bilattice.«term_≤ₖ_» 50 51 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≤ₖ ") (Lean.ParserDescr.cat `term 51))

theorem Bilattice.kLE_def {B : Type u} [Preorder (Know B)] {x y : B} : kLE x y ↔ toKnow x ≤ toKnow y

theorem Bilattice.kLE_refl {B : Type u} [Preorder (Know B)] (x : B) : kLE x x

theorem Bilattice.kLE_trans {B : Type u} [Preorder (Know B)] {x y z : B} (h₁ : kLE x y) (h₂ : kLE y z) : kLE x z

theorem Bilattice.kLE_antisymm {B : Type u} [PartialOrder (Know B)] {x y : B} (h₁ : kLE x y) (h₂ : kLE y x) : x = y

The interlacing mixin

class Bilattice.Interlaced (B : Type u) [Lattice B] [Lattice (Know B)] : Prop

The four interlacing laws ([Avr96] Def 2.1(3)): each operation is monotone w.r.t. the other order. The same-order monotonicities are automatic (an operation is monotone for its own order).

• inf_kmono {x y : B} : kLE x y → ∀ (z : B), kLE (x ⊓ z) (y ⊓ z)

  truth meet ∧ = ⊓ is ≤_k-monotone

• sup_kmono {x y : B} : kLE x y → ∀ (z : B), kLE (x ⊔ z) (y ⊔ z)

  truth join ∨ = ⊔ is ≤_k-monotone

• kInf_tmono {x y : B} : x ≤ y → ∀ (z : B), kInf x z ≤ kInf y z

  knowledge meet ⊗ is ≤_t-monotone

• kSup_tmono {x y : B} : x ≤ y → ∀ (z : B), kSup x z ≤ kSup y z

  knowledge join ⊕ is ≤_t-monotone

Representation (Avron Thm 4.3, interlaced case)

The converse of the twist product: every interlaced bilattice is isomorphic to the twist product (Iic t) ⊙ (Iic f) of the knowledge-order principal ideals of its truth bounds t = ⊤, f = ⊥. Proved here at the knowledge lattice via the decomposition X ↦ (X ⊓ t, X ⊓ f), inverse (a, b) ↦ a ⊔ b ([Avr96] Thm 4.3). The two helper lemmas are [Avr96]'s Cor 3.5 and Cor 3.8, derived from interlacing (Prop 3.2 → 3.6 → 3.7 → 3.8).

Avron §3 chain (interlacing helpers)

The §3 lemmas below are stated in B-land via the knowledge operations ⊗/⊕/≤ₖ, then ported to Know B for the representation theorem. The two truth-monotonicity facts tle_kInf_top/kInf_bot_tle (Avron's building blocks for Prop 3.2) feed the decomposition identities decomp_kSup/decomp_kInf (Cor 3.8 and its dual), which in turn give Cor 3.5.

theorem Bilattice.isCompl_truthBounds {B : Type u} [Lattice B] [BoundedOrder B] [Lattice (Know B)] [BoundedOrder (Know B)] [Interlaced B] : IsCompl (toKnow ⊤) (toKnow ⊥)

[Avr96] Cor 3.5: the truth bounds are complementary in the knowledge order (t ⊗ f = ⊥, t ⊕ f = ⊤). Derived from interlacing via decomp_kSup (for codisjointness: every Z is ≤ₖ kT ⊕ kF) and decomp_kInf (for disjointness: kT ⊗ kF is ≤ₖ every Z).

theorem Bilattice.inf_kT_sup_inf_kF {B : Type u} [Lattice B] [BoundedOrder B] [Lattice (Know B)] [Interlaced B] (X : Know B) : X ⊓ toKnow ⊤ ⊔ X ⊓ toKnow ⊥ = X

[Avr96] Cor 3.8(1): every element is the knowledge-join of its knowledge-meets with the two truth bounds — X = (X ⊗ t) ⊕ (X ⊗ f). This is decomp_kSup ported to Know B: the knowledge meets/join ⊓/⊔ on Know B are definitionally the B-land ⊗/⊕.

def Bilattice.decompose {B : Type u} [Lattice B] [BoundedOrder B] [Lattice (Know B)] [Interlaced B] : Know B ≃o ↑(Set.Iic (toKnow ⊤)) × ↑(Set.Iic (toKnow ⊥))

[Avr96] Thm 4.3 (interlaced case): the knowledge lattice of an interlaced bilattice decomposes as the twist product of the principal ideals of its truth bounds, X ↦ (X ⊓ t, X ⊓ f).

Equations

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