Bilattices

A bilattice ([Avr96] Def 2.1) is one carrier with two lattice orders, a truth order ≤ and a knowledge order ≤ₖ. It is interlaced when the meet and join of each order are monotone for the other order, a condition due to [Fit90].

The truth lattice is the carrier's own [Lattice B]. The knowledge lattice lives on the type synonym Know B, a distinct type head (cf. OrderDual), so both can be instances at once. On B itself the knowledge meet and join, Fitting's consensus ⊗ and gullibility ⊕, are written ⊓ₖ and ⊔ₖ.

Main definitions

• Bilattice.Know, Bilattice.toKnow, Bilattice.ofKnow: the knowledge-order synonym and its casts.
• Bilattice.kInf, Bilattice.kSup, Bilattice.kLE: the knowledge meet ⊓ₖ, join ⊔ₖ and order ≤ₖ.
• Bilattice.IsInterlaced: the four interlacing laws.

References

• [Avr96]
• [Fit90]

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

@[instance_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

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

@[instance_reducible]

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

Equations

• Bilattice.instTransKLE = { trans := ⋯ }

@[instance_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.IsInterlaced (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