The Ginsberg–Fitting product bilattice

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

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

The IsInterlaced (L ⊙ R) instance packages the four monotonicity laws, so the product is an interlaced bilattice. On the diagonal L ⊙ L, swapping the coordinates is Ginsberg's negation. Avron credits the construction to Ginsberg, generalized by Fitting. [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.
• Bilattice.Product.mk, Bilattice.Product.pro, Bilattice.Product.con: the plain-coordinate constructor and projections.
• the Compl (L ⊙ L) instance: Ginsberg negation on the diagonal, with the InvolutiveCompl and Negation instances it underlies.
• Bilattice.Product.conflation: the conflation induced by an involution of the factor.

Main results

• Bilattice.Product.isExact_iff, Bilattice.Product.isConsistent_iff, Bilattice.Product.isAnticonsistent_iff: the three classes in coordinates.

References

• [Avr96]
• [Fit94]
• [Fit21]
• [Gin88]

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

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

Equations

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

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

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

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

The pair with evidence a for and 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 are transported from L × Rᵒᵈ. Its ≤ is the truth order ([Avr96] Def 2.4(ii)), ⊓ and ⊔ the truth meet and join (ibid. Def 2.4(iv), (iii)), ⊤ = t and ⊥ = f the truth bounds (ibid. Def 2.4(vii)), and the product of distributive lattices is distributive (ibid. Thm 2.5).

@[instance_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 := ⋯ }

@[instance_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 := ⋯ }

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

@[instance_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 := ⋯ }

@[instance_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 := ⋯ }

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

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

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

In the truth order a pair lies higher with more evidence for and 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₂)

The truth meet meets the evidence for and joins the evidence against ([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₂)

The truth join joins the evidence for and meets the evidence against ([Avr96] Def 2.4(iii)).

theorem Bilattice.Product.le_def {L : Type u_1} {R : Type u_2} [Preorder L] [Preorder R] {x y : Product L R} : x ≤ y ↔ x.pro ≤ y.pro ∧ y.con ≤ x.con

A pair lies below another in the truth order when it has less evidence for and more against.

@[simp]

theorem Bilattice.Product.pro_inf {L : Type u_1} {R : Type u_2} [Lattice L] [Lattice R] (x y : Product L R) : (x ⊓ y).pro = x.pro ⊓ y.pro

@[simp]

theorem Bilattice.Product.con_inf {L : Type u_1} {R : Type u_2} [Lattice L] [Lattice R] (x y : Product L R) : (x ⊓ y).con = x.con ⊔ y.con

@[simp]

theorem Bilattice.Product.pro_sup {L : Type u_1} {R : Type u_2} [Lattice L] [Lattice R] (x y : Product L R) : (x ⊔ y).pro = x.pro ⊔ y.pro

@[simp]

theorem Bilattice.Product.con_sup {L : Type u_1} {R : Type u_2} [Lattice L] [Lattice R] (x y : Product L R) : (x ⊔ y).con = x.con ⊓ y.con

@[simp]

theorem Bilattice.Product.pro_top {L : Type u_1} {R : Type u_2} [Preorder L] [Preorder R] [BoundedOrder L] [BoundedOrder R] : ⊤.pro = ⊤

@[simp]

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

@[simp]

theorem Bilattice.Product.pro_bot {L : Type u_1} {R : Type u_2} [Preorder L] [Preorder R] [BoundedOrder L] [BoundedOrder R] : ⊥.pro = ⊥

@[simp]

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

The knowledge order

The instances on the synonym Know (L ⊙ R) are transported from the plain Prod order on L × R, so ⊓ₖ, ⊔ₖ and ≤ₖ are the generic knowledge operations of Core.Order.Bilattice.Defs.

@[instance_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 := ⋯ }

@[instance_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 := ⋯ }

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

@[instance_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 := ⋯ }

@[instance_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 := ⋯ }

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

In the knowledge order a pair lies higher with 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₂)

The knowledge meet, consensus, meets both 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₂)

The knowledge join, gullibility, joins both coordinates ([Avr96] Def 2.4).

@[simp]

theorem Bilattice.Product.pro_kInf {L : Type u_1} {R : Type u_2} [Lattice L] [Lattice R] (x y : Product L R) : (kInf x y).pro = x.pro ⊓ y.pro

@[simp]

theorem Bilattice.Product.con_kInf {L : Type u_1} {R : Type u_2} [Lattice L] [Lattice R] (x y : Product L R) : (kInf x y).con = x.con ⊓ y.con

@[simp]

theorem Bilattice.Product.pro_kSup {L : Type u_1} {R : Type u_2} [Lattice L] [Lattice R] (x y : Product L R) : (kSup x y).pro = x.pro ⊔ y.pro

@[simp]

theorem Bilattice.Product.con_kSup {L : Type u_1} {R : Type u_2} [Lattice L] [Lattice R] (x y : Product L R) : (kSup x y).con = x.con ⊔ y.con

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

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

Negation

On the diagonal L ⊙ L, Ginsberg's negation swaps the coordinates ([Gin88]; [Avr96] Thm 2.5(2)). It needs no order on L, so it is a bare Compl instance. Over a preorder it is an involution of the truth order (InvolutiveCompl) and a bilattice Negation, so over a bounded distributive lattice the truth lattice is a De Morgan algebra ([Fit21] §8.3).

@[instance_reducible]

instance Bilattice.Product.instCompl {L : Type u_1} : Compl (Product L L)

Ginsberg negation on L ⊙ L swaps the evidence for and the evidence against.

Equations

• Bilattice.Product.instCompl = { compl := fun (x : Bilattice.Product L L) => Bilattice.Product.mk x.con x.pro }

@[simp]

theorem Bilattice.Product.pro_compl {L : Type u_1} (x : Product L L) : xᶜ.pro = x.con

@[simp]

theorem Bilattice.Product.con_compl {L : Type u_1} (x : Product L L) : xᶜ.con = x.pro

@[simp]

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

@[simp]

theorem Bilattice.Product.compl_compl {L : Type u_1} (x : Product L L) : xᶜᶜ = x

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

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

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

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

@[instance_reducible]

instance Bilattice.Product.instInvolutiveCompl {L : Type u_1} [Preorder L] : InvolutiveCompl (Product L L)

Equations

• Bilattice.Product.instInvolutiveCompl = { toCompl := Bilattice.Product.instCompl, compl_compl := ⋯, compl_le_compl := ⋯ }

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)).

Conflation

Swapping the coordinates and applying an order-reversing involution of the factor to each is a conflation of L ⊙ L ([Fit94] §7, [Fit21] §8.8). An involutive complement of the factor gives the conflation instance, which commutes with Ginsberg negation, and the exact, consistent and anticonsistent values read off the coordinates.

@[reducible, inline]

abbrev Bilattice.Product.conflation {L : Type u_1} [Preorder L] (f : L → L) (hf : Function.Involutive f) (ha : Antitone f) : Conflation (Product L L)

The conflation ⟨a, b⟩ ↦ ⟨f b, f a⟩ of L ⊙ L induced by an order-reversing involution f of the factor.

Equations

• Bilattice.Product.conflation f hf ha = { conf := fun (x : Bilattice.Product L L) => Bilattice.Product.mk (f x.con) (f x.pro), conf_conf := ⋯, conf_le_conf := ⋯, conf_kLE_conf := ⋯ }

@[instance_reducible]

instance Bilattice.Product.instConflation {L : Type u_1} [Preorder L] [InvolutiveCompl L] : Conflation (Product L L)

Equations

• Bilattice.Product.instConflation = Bilattice.Product.conflation (fun (x : L) => xᶜ) ⋯ ⋯

instance Bilattice.Product.instNegConfComm {L : Type u_1} [Preorder L] [InvolutiveCompl L] : NegConfComm (Product L L)

@[simp]

theorem Bilattice.Product.pro_conf {L : Type u_1} [Preorder L] [InvolutiveCompl L] (x : Product L L) : (conf x).pro = x.conᶜ

@[simp]

theorem Bilattice.Product.con_conf {L : Type u_1} [Preorder L] [InvolutiveCompl L] (x : Product L L) : (conf x).con = x.proᶜ

theorem Bilattice.Product.isExact_iff {L : Type u_1} [Preorder L] [InvolutiveCompl L] (x : Product L L) : IsExact x ↔ x.con = x.proᶜ

The exact values are the pairs ⟨a, aᶜ⟩.

theorem Bilattice.Product.isConsistent_iff {L : Type u_1} [Preorder L] [InvolutiveCompl L] (x : Product L L) : IsConsistent x ↔ x.con ≤ x.proᶜ

A pair is consistent when its evidence against lies below the complement of its evidence for.

theorem Bilattice.Product.isAnticonsistent_iff {L : Type u_1} [Preorder L] [InvolutiveCompl L] (x : Product L L) : IsAnticonsistent x ↔ x.proᶜ ≤ x.con

A pair is anticonsistent when the complement of its evidence for lies below its evidence against.

Disjoint coordinates

The pairs whose evidence for and against are disjoint are closed under negation by the symmetry of Disjoint and, over a distributive factor, under the truth operations, and negation satisfies the Kleene law on them: they form Kalman's construction Kalman L (Core/Order/DeMorganAlgebra/Kalman.lean). Over a Boolean factor disjointness is Fitting's consistency. Over a De Morgan factor neither implies the other: ⟨0, 0⟩ in SignType ⊙ SignType is consistent but not disjoint, and the pair of the glut and the gap in FOUR ⊙ FOUR is disjoint but not consistent. Over a Heyting factor, whose pseudocomplement is no involution, disjointness is the only notion available.

theorem Bilattice.Product.inf_compl_le_sup_compl_of_disjoint {L : Type u_1} [Lattice L] [OrderBot L] {x y : Product L L} (hx : Disjoint x.pro x.con) (hy : Disjoint y.pro y.con) : x ⊓ xᶜ ≤ y ⊔ yᶜ

On pairs with disjoint coordinates negation satisfies the Kleene law, since a contradiction x ⊓ xᶜ has no evidence for and an excluded middle y ⊔ yᶜ no evidence against.

theorem Bilattice.Product.supClosed_disjoint_pro_con {L : Type u_1} [DistribLattice L] [OrderBot L] : SupClosed {x : Product L L | Disjoint x.pro x.con}

theorem Bilattice.Product.infClosed_disjoint_pro_con {L : Type u_1} [DistribLattice L] [OrderBot L] : InfClosed {x : Product L L | Disjoint x.pro x.con}