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. The interlacing condition is due to [Fit90]; [Avr96], cited throughout for statement locations, develops its structure theory.

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 representation theorem ([Avr96] Thm 4.3) for any interlaced bilattice: the knowledge lattice decomposes as the Ginsberg–Fitting product of the knowledge-order principal ideals of the truth bounds (decompose), and the truth order is recovered from the decomposition (le_iff_kInf_top_kInf_bot). Unlike Core.Logic.Bilattice.Representation (which handles the distributive special case via whole-lattice distributivity), 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. The constructive converse — the product of two lattices is interlaced — is Core.Logic.Bilattice.Product. [UPSTREAM] candidate (mathlib has no bilattices).

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
• Bilattice.le_iff_kInf_top_kInf_bot — Thm 4.3, truth side: x ≤ y iff the t-components grow and the f-components shrink in the knowledge order
• Bilattice.Negation — negation mixin ([Avr96] Def 2.3), with the derived bounds/De Morgan/knowledge-homomorphism equations
• Bilattice.negIicIso, neg_kInf_top — Prop 4.7: with a negation the two ideals are isomorphic (λ x, ∼x : L_B ≃o R_B) and the decomposition is a diagonal product
• Bilattice.Conflation — the knowledge-order inversion ([Fit21] §8.4), with IsConsistent/IsAnticonsistent/IsExact ([Fit21] Def 8.5.1) and their closure, interpolation, and antichain laws (ibid. Props 8.5.2–8.5.4)

TODO

Package [Avr96] Prop 4.7's full equivalence ⟨B, ∼⟩ ≅ L_B ⊙ L_B (its two proof steps are negIicIso and neg_kInf_top); abstract uniqueness of the factors up to isomorphism (ibid. Thm 4.3; the concrete half for products is Bilattice.Product.decomposeProdIso).

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

@[implicit_reducible]

instance Bilattice.instDecidableEqKnow {B : Type u} [DecidableEq B] : DecidableEq (Know B)

Equations

• Bilattice.instDecidableEqKnow = Bilattice.instDecidableEqKnow._aux_1

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

@[implicit_reducible]

instance Bilattice.instTransKLE {B : Type u} [Preorder (Know B)] : Trans kLE kLE kLE

Equations

• Bilattice.instTransKLE = { trans := ⋯ }

@[implicit_reducible]

instance Bilattice.instDecidableRelKLEOfDecidableLEKnow {B : Type u} [Preorder (Know B)] [DecidableLE (Know B)] : DecidableRel kLE

Equations

• Bilattice.instDecidableRelKLEOfDecidableLEKnow x y = Bilattice.instDecidableRelKLEOfDecidableLEKnow._aux_1 x y

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

Negation

A negation on a bilattice ([Avr96] Def 2.3) is an involution reversing the truth order and preserving the knowledge order. The note following Def 2.3 derives the equations used below: negation exchanges the truth bounds (∼t = f), anti-commutes with the truth lattice operations (De Morgan), and is an automorphism of the knowledge lattice.

class Bilattice.Negation (B : Type u) [Preorder B] [Preorder (Know B)] : Type u

A negation ([Avr96] Def 2.3): an involution (i) that reverses the truth order (ii) and preserves the knowledge order (iii).

• neg : B → B

  The negation operation ∼.

• neg_neg (a : B) : neg (neg a) = a

  Negation is an involution ([Avr96] Def 2.3(i)).

• neg_le_neg {a b : B} : a ≤ b → neg b ≤ neg a

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

• neg_kLE_neg {a b : B} : kLE a b → kLE (neg a) (neg b)

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

theorem Bilattice.neg_le_neg_iff {B : Type u} [Preorder B] [Preorder (Know B)] [Negation B] {a b : B} : neg b ≤ neg a ↔ a ≤ b

theorem Bilattice.neg_kLE_neg_iff {B : Type u} [Preorder B] [Preorder (Know B)] [Negation B] {a b : B} : kLE (neg a) (neg b) ↔ kLE a b

def Bilattice.Negation.dualIso {B : Type u} [Preorder B] [Preorder (Know B)] [Negation B] : B ≃o Bᵒᵈ

Negation as an antitone automorphism of the truth order, B ≃o Bᵒᵈ.

Equations

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

def Bilattice.Negation.knowIso {B : Type u} [Preorder B] [Preorder (Know B)] [Negation B] : Know B ≃o Know B

Negation as an automorphism of the knowledge order.

Equations

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

@[simp]

theorem Bilattice.neg_top {B : Type u} [PartialOrder B] [Preorder (Know B)] [BoundedOrder B] [Negation B] : neg ⊤ = ⊥

Negation exchanges the truth bounds, ∼t = f (note following [Avr96] Def 2.3).

@[simp]

theorem Bilattice.neg_bot {B : Type u} [PartialOrder B] [Preorder (Know B)] [BoundedOrder B] [Negation B] : neg ⊥ = ⊤

Negation exchanges the truth bounds, ∼f = t (note following [Avr96] Def 2.3).

theorem Bilattice.neg_inf {B : Type u} [Lattice B] [Preorder (Know B)] [Negation B] (a b : B) : neg (a ⊓ b) = neg a ⊔ neg b

De Morgan: ∼(a ∧ b) = ∼a ∨ ∼b (note following [Avr96] Def 2.3).

theorem Bilattice.neg_sup {B : Type u} [Lattice B] [Preorder (Know B)] [Negation B] (a b : B) : neg (a ⊔ b) = neg a ⊓ neg b

De Morgan: ∼(a ∨ b) = ∼a ∧ ∼b (note following [Avr96] Def 2.3).

theorem Bilattice.neg_kInf {B : Type u} [Preorder B] [Lattice (Know B)] [Negation B] (a b : B) : neg (kInf a b) = kInf (neg a) (neg b)

Negation is a homomorphism of the knowledge meet, ∼(a ⊗ b) = ∼a ⊗ ∼b (note following [Avr96] Def 2.3).

theorem Bilattice.neg_kSup {B : Type u} [Preorder B] [Lattice (Know B)] [Negation B] (a b : B) : neg (kSup a b) = kSup (neg a) (neg b)

Negation is a homomorphism of the knowledge join, ∼(a ⊕ b) = ∼a ⊕ ∼b (note following [Avr96] Def 2.3).

Conflation

The knowledge-order counterpart of negation ([Fit94]'s coinage; axioms as in [Fit21]): an involution preserving the truth order and reversing the knowledge order. With both inversions present, the carrier splits into consistent (a ≤ₖ −a), anticonsistent (−a ≤ₖ a), and exact (−a = a) values — the abstract forms of Kleene's, Priest's, and the classical value spaces inside a bilattice ([Fit21] Def 8.5.1) — and the three classes are closed under the truth operations and (when negation and conflation commute) negation.

class Bilattice.Conflation (B : Type u) [Preorder B] [Preorder (Know B)] : Type u

A conflation ([Fit21] §8.4): an involution (Con-3) that preserves the truth order (Con-2) and reverses the knowledge order (Con-1).

• conf : B → B

  The conflation operation −.

• conf_conf (a : B) : conf (conf a) = a

  Conflation is an involution (Con-3).

• conf_le_conf {a b : B} : a ≤ b → conf a ≤ conf b

  Conflation preserves the truth order (Con-2).

• conf_kLE_conf {a b : B} : kLE a b → kLE (conf b) (conf a)

  Conflation reverses the knowledge order (Con-1).

class Bilattice.NegConfComm (B : Type u) [Preorder B] [Preorder (Know B)] [Negation B] [Conflation B] : Prop

Negation and conflation commute (Con-4).

• neg_conf (a : B) : neg (conf a) = conf (neg a)

theorem Bilattice.conf_le_conf_iff {B : Type u} [Preorder B] [Preorder (Know B)] [Conflation B] {a b : B} : conf a ≤ conf b ↔ a ≤ b

theorem Bilattice.conf_kLE_conf_iff {B : Type u} [Preorder B] [Preorder (Know B)] [Conflation B] {a b : B} : kLE (conf b) (conf a) ↔ kLE a b

def Bilattice.Conflation.orderIso {B : Type u} [Preorder B] [Preorder (Know B)] [Conflation B] : B ≃o B

Conflation as an automorphism of the truth order.

Equations

• Bilattice.Conflation.orderIso = { toFun := Bilattice.conf, invFun := Bilattice.conf, left_inv := ⋯, right_inv := ⋯, map_rel_iff' := ⋯ }

def Bilattice.Conflation.knowDualIso {B : Type u} [Preorder B] [Preorder (Know B)] [Conflation B] : Know B ≃o (Know B)ᵒᵈ

Conflation as an antitone automorphism of the knowledge order, Know B ≃o (Know B)ᵒᵈ.

Equations

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

@[simp]

theorem Bilattice.conf_top {B : Type u} [PartialOrder B] [Preorder (Know B)] [BoundedOrder B] [Conflation B] : conf ⊤ = ⊤

Conflation fixes the truth top, −t = t (note following [Fit21] Def 8.5.1).

@[simp]

theorem Bilattice.conf_bot {B : Type u} [PartialOrder B] [Preorder (Know B)] [BoundedOrder B] [Conflation B] : conf ⊥ = ⊥

Conflation fixes the truth bottom, −f = f.

theorem Bilattice.conf_inf {B : Type u} [Lattice B] [Preorder (Know B)] [Conflation B] (a b : B) : conf (a ⊓ b) = conf a ⊓ conf b

Conflation commutes with truth meet (CDeM-1).

theorem Bilattice.conf_sup {B : Type u} [Lattice B] [Preorder (Know B)] [Conflation B] (a b : B) : conf (a ⊔ b) = conf a ⊔ conf b

Conflation commutes with truth join (CDeM-2).

The consistent / anticonsistent / exact classes

def Bilattice.IsConsistent {B : Type u} [Preorder B] [Preorder (Know B)] [Conflation B] (a : B) : Prop

Consistent values, a ≤ₖ −a ([Fit21] Def 8.5.1): the abstract form of the Kleene value space.

Equations

• Bilattice.IsConsistent a = Bilattice.kLE a (Bilattice.conf a)

def Bilattice.IsAnticonsistent {B : Type u} [Preorder B] [Preorder (Know B)] [Conflation B] (a : B) : Prop

Anticonsistent values, −a ≤ₖ a ([Fit21] Def 8.5.1): the abstract form of Priest's LP value space.

Equations

• Bilattice.IsAnticonsistent a = Bilattice.kLE (Bilattice.conf a) a

def Bilattice.IsExact {B : Type u} [Preorder B] [Preorder (Know B)] [Conflation B] (a : B) : Prop

Exact values, −a = a ([Fit21] Def 8.5.1): the abstract classical value space.

Equations

• Bilattice.IsExact a = (Bilattice.conf a = a)

theorem Bilattice.IsExact.isConsistent {B : Type u} [Preorder B] [Preorder (Know B)] [Conflation B] {a : B} (h : IsExact a) : IsConsistent a

theorem Bilattice.IsExact.isAnticonsistent {B : Type u} [Preorder B] [Preorder (Know B)] [Conflation B] {a : B} (h : IsExact a) : IsAnticonsistent a

@[implicit_reducible]

instance Bilattice.instDecidablePredIsConsistentOfDecidableLEKnow {B : Type u} [Preorder B] [Preorder (Know B)] [Conflation B] [DecidableLE (Know B)] : DecidablePred IsConsistent

Equations

• Bilattice.instDecidablePredIsConsistentOfDecidableLEKnow a = Bilattice.instDecidablePredIsConsistentOfDecidableLEKnow._aux_1 a

@[implicit_reducible]

instance Bilattice.instDecidablePredIsAnticonsistentOfDecidableLEKnow {B : Type u} [Preorder B] [Preorder (Know B)] [Conflation B] [DecidableLE (Know B)] : DecidablePred IsAnticonsistent

Equations

• Bilattice.instDecidablePredIsAnticonsistentOfDecidableLEKnow a = Bilattice.instDecidablePredIsAnticonsistentOfDecidableLEKnow._aux_1 a

@[implicit_reducible]

instance Bilattice.instDecidablePredIsExactOfDecidableEq {B : Type u} [Preorder B] [Preorder (Know B)] [Conflation B] [DecidableEq B] : DecidablePred IsExact

Equations

• Bilattice.instDecidablePredIsExactOfDecidableEq a = Bilattice.instDecidablePredIsExactOfDecidableEq._aux_1 a

theorem Bilattice.isExact_top {B : Type u} [PartialOrder B] [Preorder (Know B)] [BoundedOrder B] [Conflation B] : IsExact ⊤

The truth bounds are exact ([Fit21] Prop 8.5.2).

theorem Bilattice.isExact_bot {B : Type u} [PartialOrder B] [Preorder (Know B)] [BoundedOrder B] [Conflation B] : IsExact ⊥

theorem Bilattice.IsConsistent.inf {B : Type u} [Lattice B] [Lattice (Know B)] [Interlaced B] [Conflation B] {a b : B} (ha : IsConsistent a) (hb : IsConsistent b) : IsConsistent (a ⊓ b)

The consistent values are closed under truth meet ([Fit21] Prop 8.5.2).

theorem Bilattice.IsConsistent.sup {B : Type u} [Lattice B] [Lattice (Know B)] [Interlaced B] [Conflation B] {a b : B} (ha : IsConsistent a) (hb : IsConsistent b) : IsConsistent (a ⊔ b)

The consistent values are closed under truth join.

theorem Bilattice.IsAnticonsistent.inf {B : Type u} [Lattice B] [Lattice (Know B)] [Interlaced B] [Conflation B] {a b : B} (ha : IsAnticonsistent a) (hb : IsAnticonsistent b) : IsAnticonsistent (a ⊓ b)

The anticonsistent values are closed under truth meet.

theorem Bilattice.IsAnticonsistent.sup {B : Type u} [Lattice B] [Lattice (Know B)] [Interlaced B] [Conflation B] {a b : B} (ha : IsAnticonsistent a) (hb : IsAnticonsistent b) : IsAnticonsistent (a ⊔ b)

The anticonsistent values are closed under truth join.

theorem Bilattice.IsExact.inf {B : Type u} [Lattice B] [Lattice (Know B)] [Conflation B] {a b : B} (ha : IsExact a) (hb : IsExact b) : IsExact (a ⊓ b)

The exact values are closed under truth meet.

theorem Bilattice.IsExact.sup {B : Type u} [Lattice B] [Lattice (Know B)] [Conflation B] {a b : B} (ha : IsExact a) (hb : IsExact b) : IsExact (a ⊔ b)

The exact values are closed under truth join.

theorem Bilattice.IsConsistent.neg {B : Type u} [Lattice B] [Lattice (Know B)] [Conflation B] [Negation B] [NegConfComm B] {a : B} (ha : IsConsistent a) : IsConsistent (Bilattice.neg a)

The consistent values are closed under negation ([Fit21] Prop 8.5.2; needs Con-4).

theorem Bilattice.IsAnticonsistent.neg {B : Type u} [Lattice B] [Lattice (Know B)] [Conflation B] [Negation B] [NegConfComm B] {a : B} (ha : IsAnticonsistent a) : IsAnticonsistent (Bilattice.neg a)

The anticonsistent values are closed under negation.

theorem Bilattice.IsExact.neg {B : Type u} [Lattice B] [Lattice (Know B)] [Conflation B] [Negation B] [NegConfComm B] {a : B} (ha : IsExact a) : IsExact (Bilattice.neg a)

The exact values are closed under negation.

theorem Bilattice.IsConsistent.exists_exact_kLE {B : Type u} [Lattice B] [Lattice (Know B)] [Interlaced B] [Conflation B] {a : B} (ha : IsConsistent a) : ∃ (b : B), IsExact b ∧ kLE a b

Every consistent value is knowledge-below an exact value ([Fit21] Prop 8.5.3): a ⊔ −a is exact.

theorem Bilattice.IsAnticonsistent.exists_exact_kLE {B : Type u} [Lattice B] [Lattice (Know B)] [Interlaced B] [Conflation B] {a : B} (ha : IsAnticonsistent a) : ∃ (b : B), IsExact b ∧ kLE b a

Every anticonsistent value is knowledge-above an exact value ([Fit21] Prop 8.5.3): a ⊓ −a is exact.

theorem Bilattice.IsExact.eq_of_kLE {B : Type u} [Preorder B] [PartialOrder (Know B)] [Conflation B] {a b : B} (ha : IsExact a) (hb : IsExact b) (h : kLE a b) : a = b

The exact values form a knowledge-order antichain ([Fit21] Prop 8.5.4).

Representation (Avron Thm 4.3, interlaced case)

The converse of Core.Logic.Bilattice.Product: every interlaced bilattice is isomorphic to the 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.

The truth side of Thm 4.3

decompose is a knowledge-order isomorphism; the theorem below recovers the truth order from the same components: x ≤ y iff the t-components grow and the f-components shrink in the knowledge order — the product's twisted truth order on the factors (cf. Bilattice.Product.mk_le_mk).

theorem Bilattice.le_iff_kInf_top_kInf_bot {B : Type u} [Lattice B] [BoundedOrder B] [Lattice (Know B)] [Interlaced B] {x y : B} : x ≤ y ↔ kLE (kInf x ⊤) (kInf y ⊤) ∧ kLE (kInf y ⊥) (kInf x ⊥)

[Avr96] Thm 4.3, truth side: the truth order is recovered from the knowledge-order decomposition — x ≤ y iff the t-components grow and the f-components shrink in the knowledge order.

Negation and the decomposition (Avron Prop 4.7)

With a negation, the two decomposition factors are isomorphic and the decomposition is a diagonal product: [Avr96] Prop 4.7 exhibits ⟨B, ∼⟩ ≅ L_B ⊙ L_B with Ginsberg's swap negation, via x ↦ (x ⊗ t, x ⊗ f) followed by (x, y) ↦ (x, ∼y). Formalized here: the ideal isomorphism λ x, ∼x : L_B ≃o R_B (negIicIso) and the transport equation ∼x ⊗ t = ∼(x ⊗ f) (neg_kInf_top) — the two steps of Avron's proof.

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

[Avr96] Prop 4.7, key step: negation is an isomorphism between the knowledge ideals L_B = Iic t and R_B = Iic f.

Equations

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

theorem Bilattice.neg_kInf_top {B : Type u} [Lattice B] [BoundedOrder B] [Lattice (Know B)] [Negation B] (x : B) : kInf (neg x) ⊤ = neg (kInf x ⊥)

[Avr96] Prop 4.7, transport step (the map (x, y) ↦ (x, ∼y)): negation exchanges the two decomposition components, ∼x ⊗ t = ∼(x ⊗ f).