The Ginsberg–Fitting product bilattice

[Avr96] [Gin88]

The fundamental bilattice construction ([Avr96] Def 2.4): the product L ⊙ R of two lattices carries pairs (a, b) recording evidence for (a ∈ L) and against (b ∈ R) a proposition, ordered two ways:

• the truth order — more for, less against — is the carrier's ≤: as a type, L ⊙ R := L × Rᵒᵈ, so the Prod/OrderDual instances provide the truth lattice, its bounds t = (⊤, ⊥) and f = (⊥, ⊤), and distributivity outright;
• the knowledge order — more evidence both ways — is the plain Prod order, installed on the synonym Know (L ⊙ R) (see Core.Logic.Bilattice.Interlaced).

The Interlaced (L ⊙ R) instance packages the four monotonicity laws ([Avr96] Def 2.1(3)): the product is an interlaced bilattice — the constructive half of the structure theory ([Avr96] Thm 2.5). The converse representation theorem is Bilattice.decompose (ibid. Thm 4.3). On the diagonal L ⊙ L, swapping the coordinates is Ginsberg's negation ([Gin88]; [Avr96] Thm 2.5(2)).

The construction "was essentially introduced by Ginsberg [Gin88], and further generalized by Fitting" ([Avr96]). The algebraic-logic literature sometimes calls the diagonal case with swap-negation a twist structure; that term names an older single-factor lineage, so this file keeps Avron's name. [UPSTREAM] candidate (mathlib has no bilattices).

Main definitions

• Bilattice.Product (L ⊙ R) — the carrier, with truth-order instances from L × Rᵒᵈ and knowledge-order instances on Know (L ⊙ R) from L × R
• Product.mk/pro/con — plain-coordinate constructor and projections
• the Interlaced (L ⊙ R) instance — the four interlacing laws
• Product.neg — Ginsberg negation on the diagonal L ⊙ L

def OrderIso.prodCongr {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [Preorder α] [Preorder β] [Preorder γ] [Preorder δ] (e₁ : α ≃o β) (e₂ : γ ≃o δ) : α × γ ≃o β × δ

Componentwise product of order isomorphisms. [UPSTREAM] candidate: mathlib has Equiv.prodCongr but no order-iso version.

Equations

• e₁.prodCongr e₂ = { toEquiv := e₁.prodCongr e₂.toEquiv, map_rel_iff' := ⋯ }

def Bilattice.Product (L : Type u_1) (R : Type u_2) : Type (max u_2 u_1)

The Ginsberg–Fitting product L ⊙ R ([Avr96] Def 2.4): pairs of evidence for/against. The carrier order is the truth order (L × Rᵒᵈ: more for, less against); the knowledge order lives on Know (L ⊙ R) (L × R: more evidence both ways).

Equations

• Bilattice.Product L R = (L × Rᵒᵈ)

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

The Ginsberg–Fitting product L ⊙ R ([Avr96] Def 2.4): pairs of evidence for/against. The carrier order is the truth order (L × Rᵒᵈ: more for, less against); the knowledge order lives on Know (L ⊙ R) (L × R: more evidence both ways).

Equations

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

def Bilattice.Product.mk {L : Type u_1} {R : Type u_2} (a : L) (b : R) : Product L R

Build L ⊙ R from plain coordinates: evidence a for, b against.

Equations

• Bilattice.Product.mk a b = (a, OrderDual.toDual b)

def Bilattice.Product.pro {L : Type u_1} {R : Type u_2} (x : Product L R) : L

The evidence-for coordinate.

Equations

• x.pro = x.1

def Bilattice.Product.con {L : Type u_1} {R : Type u_2} (x : Product L R) : R

The evidence-against coordinate.

Equations

• x.con = OrderDual.ofDual x.2

@[simp]

theorem Bilattice.Product.pro_mk {L : Type u_1} {R : Type u_2} (a : L) (b : R) : (mk a b).pro = a

@[simp]

theorem Bilattice.Product.con_mk {L : Type u_1} {R : Type u_2} (a : L) (b : R) : (mk a b).con = b

@[simp]

theorem Bilattice.Product.mk_pro_con {L : Type u_1} {R : Type u_2} (x : Product L R) : mk x.pro x.con = x

theorem Bilattice.Product.ext {L : Type u_1} {R : Type u_2} {x y : Product L R} (h₁ : x.pro = y.pro) (h₂ : x.con = y.con) : x = y

theorem Bilattice.Product.ext_iff {L : Type u_1} {R : Type u_2} {x y : Product L R} : x = y ↔ x.pro = y.pro ∧ x.con = y.con

The truth order

The carrier instances, transported from L × Rᵒᵈ: ≤ is the truth order ([Avr96] Def 2.4(ii)), ⊓/⊔ the truth meet/join (ibid. Def 2.4(iv), (iii)), ⊤ = t/⊥ = f the truth bounds (ibid. Def 2.4(vii)), and the product of distributive lattices is distributive (ibid. Thm 2.5).

@[implicit_reducible]

instance Bilattice.Product.instPreorder {L : Type u_1} {R : Type u_2} [Preorder L] [Preorder R] : Preorder (Product L R)

Equations

• Bilattice.Product.instPreorder = { le := Bilattice.Product.instPreorder._aux_1, lt := Bilattice.Product.instPreorder._aux_3, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯ }

@[implicit_reducible]

instance Bilattice.Product.instPartialOrder {L : Type u_1} {R : Type u_2} [PartialOrder L] [PartialOrder R] : PartialOrder (Product L R)

Equations

• Bilattice.Product.instPartialOrder = { toPreorder := Bilattice.Product.instPreorder, le_antisymm := ⋯ }

@[implicit_reducible]

instance Bilattice.Product.instLattice {L : Type u_1} {R : Type u_2} [Lattice L] [Lattice R] : Lattice (Product L R)

Equations

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

@[implicit_reducible]

instance Bilattice.Product.instDistribLattice {L : Type u_1} {R : Type u_2} [DistribLattice L] [DistribLattice R] : DistribLattice (Product L R)

Equations

• Bilattice.Product.instDistribLattice = { toLattice := Bilattice.Product.instLattice, le_sup_inf := ⋯ }

@[implicit_reducible]

instance Bilattice.Product.instBoundedOrder {L : Type u_1} {R : Type u_2} [Preorder L] [Preorder R] [BoundedOrder L] [BoundedOrder R] : BoundedOrder (Product L R)

Equations

• Bilattice.Product.instBoundedOrder = { top := Bilattice.Product.instBoundedOrder._aux_1, le_top := ⋯, bot := Bilattice.Product.instBoundedOrder._aux_4, bot_le := ⋯ }

@[implicit_reducible]

instance Bilattice.Product.instDecidableLE {L : Type u_1} {R : Type u_2} [Preorder L] [Preorder R] [DecidableLE L] [DecidableLE R] : DecidableLE (Product L R)

Equations

• Bilattice.Product.instDecidableLE = Bilattice.Product.instDecidableLE._aux_1

@[implicit_reducible]

instance Bilattice.Product.instDecidableEq {L : Type u_1} {R : Type u_2} [DecidableEq L] [DecidableEq R] : DecidableEq (Product L R)

Equations

• Bilattice.Product.instDecidableEq = Bilattice.Product.instDecidableEq._aux_1

@[implicit_reducible]

instance Bilattice.Product.instFintype {L : Type u_1} {R : Type u_2} [Fintype L] [Fintype R] : Fintype (Product L R)

Equations

• Bilattice.Product.instFintype = { elems := Bilattice.Product.instFintype._aux_1, complete := ⋯ }

@[simp]

theorem Bilattice.Product.mk_le_mk {L : Type u_1} {R : Type u_2} [Preorder L] [Preorder R] {a₁ a₂ : L} {b₁ b₂ : R} : mk a₁ b₁ ≤ mk a₂ b₂ ↔ a₁ ≤ a₂ ∧ b₂ ≤ b₁

The truth order in plain coordinates: more for, less against ([Avr96] Def 2.4(ii)).

@[simp]

theorem Bilattice.Product.mk_inf_mk {L : Type u_1} {R : Type u_2} [Lattice L] [Lattice R] {a₁ a₂ : L} {b₁ b₂ : R} : mk a₁ b₁ ⊓ mk a₂ b₂ = mk (a₁ ⊓ a₂) (b₁ ⊔ b₂)

Truth meet ∧ in plain coordinates ([Avr96] Def 2.4(iv)).

@[simp]

theorem Bilattice.Product.mk_sup_mk {L : Type u_1} {R : Type u_2} [Lattice L] [Lattice R] {a₁ a₂ : L} {b₁ b₂ : R} : mk a₁ b₁ ⊔ mk a₂ b₂ = mk (a₁ ⊔ a₂) (b₁ ⊓ b₂)

Truth join ∨ in plain coordinates ([Avr96] Def 2.4(iii)).

theorem Bilattice.Product.top_eq {L : Type u_1} {R : Type u_2} [Preorder L] [Preorder R] [BoundedOrder L] [BoundedOrder R] : ⊤ = mk ⊤ ⊥

The truth top t = (⊤, ⊥) ([Avr96] Def 2.4(vii)).

theorem Bilattice.Product.bot_eq {L : Type u_1} {R : Type u_2} [Preorder L] [Preorder R] [BoundedOrder L] [BoundedOrder R] : ⊥ = mk ⊥ ⊤

The truth bottom f = (⊥, ⊤) ([Avr96] Def 2.4(vii)).

The knowledge order

The instances on the synonym Know (L ⊙ R), transported from the plain Prod order on L × R; ⊗/⊕/≤ₖ are then the generic knowledge operations of Core.Logic.Bilattice.Interlaced.

@[implicit_reducible]

instance Bilattice.Product.instPreorderKnow {L : Type u_1} {R : Type u_2} [Preorder L] [Preorder R] : Preorder (Know (Product L R))

Equations

• Bilattice.Product.instPreorderKnow = { le := Bilattice.Product.instPreorderKnow._aux_1, lt := Bilattice.Product.instPreorderKnow._aux_3, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯ }

@[implicit_reducible]

instance Bilattice.Product.instPartialOrderKnow {L : Type u_1} {R : Type u_2} [PartialOrder L] [PartialOrder R] : PartialOrder (Know (Product L R))

Equations

• Bilattice.Product.instPartialOrderKnow = { toPreorder := Bilattice.Product.instPreorderKnow, le_antisymm := ⋯ }

@[implicit_reducible]

instance Bilattice.Product.instLatticeKnow {L : Type u_1} {R : Type u_2} [Lattice L] [Lattice R] : Lattice (Know (Product L R))

Equations

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

@[implicit_reducible]

instance Bilattice.Product.instDistribLatticeKnow {L : Type u_1} {R : Type u_2} [DistribLattice L] [DistribLattice R] : DistribLattice (Know (Product L R))

Equations

• Bilattice.Product.instDistribLatticeKnow = { toLattice := Bilattice.Product.instLatticeKnow, le_sup_inf := ⋯ }

@[implicit_reducible]

instance Bilattice.Product.instBoundedOrderKnow {L : Type u_1} {R : Type u_2} [Preorder L] [Preorder R] [BoundedOrder L] [BoundedOrder R] : BoundedOrder (Know (Product L R))

Equations

• Bilattice.Product.instBoundedOrderKnow = { top := Bilattice.Product.instBoundedOrderKnow._aux_1, le_top := ⋯, bot := Bilattice.Product.instBoundedOrderKnow._aux_4, bot_le := ⋯ }

@[implicit_reducible]

instance Bilattice.Product.instDecidableLEKnow {L : Type u_1} {R : Type u_2} [Preorder L] [Preorder R] [DecidableLE L] [DecidableLE R] : DecidableLE (Know (Product L R))

Equations

• Bilattice.Product.instDecidableLEKnow = Bilattice.Product.instDecidableLEKnow._aux_1

@[simp]

theorem Bilattice.Product.mk_kLE_mk {L : Type u_1} {R : Type u_2} [Preorder L] [Preorder R] {a₁ a₂ : L} {b₁ b₂ : R} : kLE (mk a₁ b₁) (mk a₂ b₂) ↔ a₁ ≤ a₂ ∧ b₁ ≤ b₂

The knowledge order in plain coordinates: more evidence both ways ([Avr96] Def 2.4).

@[simp]

theorem Bilattice.Product.mk_kInf_mk {L : Type u_1} {R : Type u_2} [Lattice L] [Lattice R] {a₁ a₂ : L} {b₁ b₂ : R} : kInf (mk a₁ b₁) (mk a₂ b₂) = mk (a₁ ⊓ a₂) (b₁ ⊓ b₂)

Knowledge meet ⊗ (consensus) in plain coordinates ([Avr96] Def 2.4).

@[simp]

theorem Bilattice.Product.mk_kSup_mk {L : Type u_1} {R : Type u_2} [Lattice L] [Lattice R] {a₁ a₂ : L} {b₁ b₂ : R} : kSup (mk a₁ b₁) (mk a₂ b₂) = mk (a₁ ⊔ a₂) (b₁ ⊔ b₂)

Knowledge join ⊕ (gullibility) in plain coordinates ([Avr96] Def 2.4).

theorem Bilattice.Product.know_top_eq {L : Type u_1} {R : Type u_2} [Preorder L] [Preorder R] [BoundedOrder L] [BoundedOrder R] : ⊤ = toKnow (mk ⊤ ⊤)

The knowledge top ⊤ = (⊤, ⊤) ([Avr96] Def 2.4(vii)).

theorem Bilattice.Product.know_bot_eq {L : Type u_1} {R : Type u_2} [Preorder L] [Preorder R] [BoundedOrder L] [BoundedOrder R] : ⊥ = toKnow (mk ⊥ ⊥)

The knowledge bottom ⊥ = (⊥, ⊥) ([Avr96] Def 2.4(vii)).

instance Bilattice.Product.instInterlaced {L : Type u_1} {R : Type u_2} [Lattice L] [Lattice R] : Interlaced (Product L R)

The product is an interlaced bilattice ([Avr96] Thm 2.5): each order's meet and join are monotone for the other order.

Negation

On the diagonal L ⊙ L, Ginsberg's negation swaps the coordinates: an involution reversing the truth order and preserving the knowledge order ([Gin88]; [Avr96] Thm 2.5(2)).

def Bilattice.Product.neg {L : Type u_1} (x : Product L L) : Product L L

Ginsberg negation on L ⊙ L: swap evidence for/against.

Equations

• x.neg = Bilattice.Product.mk x.con x.pro

@[simp]

theorem Bilattice.Product.neg_mk {L : Type u_1} (a b : L) : (mk a b).neg = mk b a

@[simp]

theorem Bilattice.Product.neg_neg {L : Type u_1} (x : Product L L) : x.neg.neg = x

theorem Bilattice.Product.neg_le_neg {L : Type u_1} [Preorder L] {x y : Product L L} (h : x ≤ y) : y.neg ≤ x.neg

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

theorem Bilattice.Product.neg_kLE_neg {L : Type u_1} [Preorder L] {x y : Product L L} (h : kLE x y) : kLE x.neg y.neg

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

@[implicit_reducible]

instance Bilattice.Product.instNegation {L : Type u_1} [Preorder L] : Negation (Product L L)

Ginsberg's swap is a negation on the diagonal ([Avr96] Thm 2.5(2)).

Equations

• Bilattice.Product.instNegation = { neg := Bilattice.Product.neg, neg_neg := ⋯, neg_le_neg := ⋯, neg_kLE_neg := ⋯ }

Recovering the factors

The abstract decomposition applied to a product recovers its factors: the knowledge ideals below the truth bounds are order-isomorphic to L and R (iicKTopIso/iicKBotIso), so Bilattice.decompose closes the representation loop, Know (L ⊙ R) ≃o L × R (decomposeProdIso) — the concrete half of [Avr96] Thm 4.3's uniqueness clause.

def Bilattice.Product.iicKTopIso {L : Type u_1} {R : Type u_2} [PartialOrder L] [PartialOrder R] [BoundedOrder L] [BoundedOrder R] : ↑(Set.Iic (toKnow ⊤)) ≃o L

The knowledge ideal below the truth top is the evidence-for factor, L_{L ⊙ R} ≃o L.

Equations

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

def Bilattice.Product.iicKBotIso {L : Type u_1} {R : Type u_2} [PartialOrder L] [PartialOrder R] [BoundedOrder L] [BoundedOrder R] : ↑(Set.Iic (toKnow ⊥)) ≃o R

The knowledge ideal below the truth bottom is the evidence-against factor, R_{L ⊙ R} ≃o R.

Equations

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

def Bilattice.Product.decomposeProdIso {L : Type u_1} {R : Type u_2} [Lattice L] [Lattice R] [BoundedOrder L] [BoundedOrder R] : Know (Product L R) ≃o L × R

The representation loop closed: Bilattice.decompose applied to a product recovers the factors, Know (L ⊙ R) ≃o L × R — the concrete half of [Avr96] Thm 4.3's uniqueness clause.

Equations

• Bilattice.Product.decomposeProdIso = Bilattice.decompose.trans (Bilattice.Product.iicKTopIso.prodCongr Bilattice.Product.iicKBotIso)