Representation of distributive bilattices

[Avr96] [AA96]

Constructive direction (Core.Logic.TwistProduct): the twist product L ⊙ R is an interlaced bilattice. This file proves the converse / representation theorem for the distributive case (Ginsberg–Fitting; [Avr96] Thm 4.3 generalizes it to all interlaced bilattices).

Presented knowledge-first: a distributive bilattice is a bounded distributive lattice B — the knowledge lattice (≤_k, ⊗ = ⊓, ⊕ = ⊔, ⊥, ⊤) — together with the two truth bounds t, f, which are complementary (IsCompl t f: t ⊗ f = ⊥, t ⊕ f = ⊤). The truth order is recovered from the decomposition.

The representation: B decomposes as the twist product (Iic t) ⊙ (Iic f) of the two principal ideals, via x ↦ (x ⊗ t, x ⊗ f) with inverse (a, b) ↦ a ⊕ b ([Avr96] Cor 3.8(1), Thm 4.3). The factors Iic t = {x | ⊥ ≤_t x} and Iic f = {x | x ≤_t ⊥} are [Avr96]'s L_B, R_B.

Main results

• Bilattice.decompose — the knowledge-order isomorphism B ≃o Iic t × Iic f
• Bilattice.tLE / tLE_iff_decompose — the recovered truth order is the twist order on the factors (first factor up, second factor down): the bilattice representation (cf. Core.Logic.TwistProduct.tLE)

def Bilattice.decompose {B : Type u_1} [DistribLattice B] [BoundedOrder B] {t f : B} (h : IsCompl t f) : B ≃o ↑(Set.Iic t) × ↑(Set.Iic f)

The knowledge-order decomposition of a distributive bilattice: x ↦ (x ⊓ t, x ⊓ f) is an order isomorphism B ≃o Iic t × Iic f ([Avr96] Thm 4.3, distributive case), with inverse (a, b) ↦ a ⊔ b.

Equations

• Bilattice.decompose h = { toFun := fun (x : B) => (⟨x ⊓ t, ⋯⟩, ⟨x ⊓ f, ⋯⟩), invFun := fun (p : ↑(Set.Iic t) × ↑(Set.Iic f)) => ↑p.1 ⊔ ↑p.2, left_inv := ⋯, right_inv := ⋯, map_rel_iff' := ⋯ }

theorem Bilattice.decompose_apply {B : Type u_1} [DistribLattice B] [BoundedOrder B] {t f : B} (h : IsCompl t f) (x : B) : (decompose h) x = (⟨x ⊓ t, ⋯⟩, ⟨x ⊓ f, ⋯⟩)

theorem Bilattice.decompose_symm_apply {B : Type u_1} [DistribLattice B] [BoundedOrder B] {t f : B} (h : IsCompl t f) (p : ↑(Set.Iic t) × ↑(Set.Iic f)) : (decompose h).symm p = ↑p.1 ⊔ ↑p.2

def Bilattice.tLE {B : Type u_1} [DistribLattice B] (t f x y : B) : Prop

The recovered truth order on a distributive bilattice: x ≤_t y iff x has less evidence-for-truth (⊓ t) and more evidence-for-falsity (⊓ f) ([Avr96] Def 2.4(ii)).

Equations

• Bilattice.tLE t f x y = (x ⊓ t ≤ y ⊓ t ∧ y ⊓ f ≤ x ⊓ f)

theorem Bilattice.tLE_iff_decompose {B : Type u_1} [DistribLattice B] [BoundedOrder B] {t f : B} (h : IsCompl t f) (x y : B) : tLE t f x y ↔ ((decompose h) x).1 ≤ ((decompose h) y).1 ∧ ((decompose h) y).2 ≤ ((decompose h) x).2

The recovered truth order is the twist order on the decomposition factors (Iic t up, Iic f down): this exhibits B as the twist product (Iic t) ⊙ (Iic f), i.e. the bilattice representation.