Representation of distributive bilattices

[Avr96]

Constructive direction (Core.Logic.Bilattice.Product): the Ginsberg–Fitting product L ⊙ R is an interlaced bilattice. This file proves the converse / representation theorem for the distributive case ([Avr96] Thm 4.3 generalizes its knowledge-order conclusion to all interlaced bilattices — see Core.Logic.Bilattice.Interlaced).

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 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.decomposeOfIsCompl — the knowledge-order isomorphism B ≃o Iic t × Iic f (the general interlaced version is Bilattice.decompose)
• Bilattice.tLE / tLE_iff_decomposeOfIsCompl — the recovered truth order is the twisted order on the factors (first factor up, second factor down): the bilattice representation (cf. Bilattice.Product.mk_le_mk)

def Bilattice.decomposeOfIsCompl {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

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

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

theorem Bilattice.decomposeOfIsCompl_symm_apply {B : Type u_1} [DistribLattice B] [BoundedOrder B] {t f : B} (h : IsCompl t f) (p : ↑(Set.Iic t) × ↑(Set.Iic f)) : (decomposeOfIsCompl 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_decomposeOfIsCompl {B : Type u_1} [DistribLattice B] [BoundedOrder B] {t f : B} (h : IsCompl t f) (x y : B) : tLE t f x y ↔ ((decomposeOfIsCompl h) x).1 ≤ ((decomposeOfIsCompl h) y).1 ∧ ((decomposeOfIsCompl h) y).2 ≤ ((decomposeOfIsCompl h) x).2

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