Kalman's construction

Over a distributive lattice L with a least element, the pairs (a, b) with a ⊓ b = ⊥ form a distributive lattice Kalman L with meet (a, b) ⊓ (c, d) = (a ⊓ c, b ⊔ d), and the swap (a, b)ᶜ = (b, a) is an involution satisfying Kleene's law; when L is bounded, Kalman L is a Kleene algebra. Reading a as evidence for and b as evidence against a proposition, these are the pairs of the product bilattice L ⊙ L whose evidence never overlaps, and Kalman L is that subtype, with the truth order, truth operations and Ginsberg negation of L ⊙ L. A bounded lattice homomorphism acts on both coordinates (Kalman.map), which is the action on morphisms of Cignoli's functor from bounded distributive lattices to Kleene algebras.

Main definitions

• Kalman L: the pairs of L ⊙ L with disjoint coordinates, with its DistribLattice, BoundedOrder, InvolutiveCompl and IsKleene instances.
• Kalman.map: the construction on bounded lattice homomorphisms.

Implementation notes

Kalman L is a subtype of L ⊙ L in the manner of mathlib's Complementeds, rather than a Sublattice, so that its order and involution need only a partial order with a least element. The closure of the disjoint pairs under the operations and the Kleene law are lemmas about the product (Bilattice.Product.supClosed_disjoint_pro_con, Bilattice.Product.infClosed_disjoint_pro_con, Bilattice.Product.inf_compl_le_sup_compl_of_disjoint).

TODO

• Kalman's general P(a): for any element a of a distributive lattice, the pairs with x ⊓ y ≤ a ≤ x ⊔ y form a normal i-lattice with center (a, a); this file is the case a = ⊥.
• Kalman's Theorem 6: the normal extensions of L are the i-sublattices of Kalman L containing the pairs (⊥, y) and (x, ⊥).

References

• [Cig86]
• [JSM17]
• [Kal58]

@[reducible, inline]

abbrev Kalman (L : Type u_1) [PartialOrder L] [OrderBot L] : Type u_1

Kalman's construction is the type of pairs of the product bilattice L ⊙ L with disjoint coordinates, written P(O) in [Kal58] §3.

Equations

• Kalman L = { x : Bilattice.Product L L // Disjoint x.pro x.con }

The order and the involution

def Kalman.mk {L : Type u_1} [PartialOrder L] [OrderBot L] (a b : L) (h : Disjoint a b) : Kalman L

The Kalman pair (a, b).

Equations

• Kalman.mk a b h = ⟨Bilattice.Product.mk a b, h⟩

def Kalman.pro {L : Type u_1} [PartialOrder L] [OrderBot L] (x : Kalman L) : L

The first coordinate, the evidence for.

Equations

• x.pro = (↑x).pro

def Kalman.con {L : Type u_1} [PartialOrder L] [OrderBot L] (x : Kalman L) : L

The second coordinate, the evidence against.

Equations

• x.con = (↑x).con

theorem Kalman.disjoint_pro_con {L : Type u_1} [PartialOrder L] [OrderBot L] (x : Kalman L) : Disjoint x.pro x.con

@[simp]

theorem Kalman.pro_coe {L : Type u_1} [PartialOrder L] [OrderBot L] (x : Kalman L) : (↑x).pro = x.pro

@[simp]

theorem Kalman.con_coe {L : Type u_1} [PartialOrder L] [OrderBot L] (x : Kalman L) : (↑x).con = x.con

@[simp]

theorem Kalman.pro_mk {L : Type u_1} [PartialOrder L] [OrderBot L] (a b : L) (h : Disjoint a b) : (mk a b h).pro = a

@[simp]

theorem Kalman.con_mk {L : Type u_1} [PartialOrder L] [OrderBot L] (a b : L) (h : Disjoint a b) : (mk a b h).con = b

@[simp]

theorem Kalman.coe_mk {L : Type u_1} [PartialOrder L] [OrderBot L] (a b : L) (h : Disjoint a b) : ↑(mk a b h) = Bilattice.Product.mk a b

@[simp]

theorem Kalman.mk_pro_con {L : Type u_1} [PartialOrder L] [OrderBot L] (x : Kalman L) : mk x.pro x.con ⋯ = x

theorem Kalman.ext {L : Type u_1} [PartialOrder L] [OrderBot L] {x y : Kalman L} (h₁ : x.pro = y.pro) (h₂ : x.con = y.con) : x = y

theorem Kalman.ext_iff {L : Type u_1} [PartialOrder L] [OrderBot L] {x y : Kalman L} : x = y ↔ x.pro = y.pro ∧ x.con = y.con

theorem Kalman.le_def {L : Type u_1} [PartialOrder L] [OrderBot L] {x y : Kalman L} : x ≤ y ↔ x.pro ≤ y.pro ∧ y.con ≤ x.con

A pair lies higher with more evidence for and less against.

@[simp]

theorem Kalman.mk_le_mk {L : Type u_1} [PartialOrder L] [OrderBot L] {a₁ b₁ a₂ b₂ : L} {h₁ : Disjoint a₁ b₁} {h₂ : Disjoint a₂ b₂} : mk a₁ b₁ h₁ ≤ mk a₂ b₂ h₂ ↔ a₁ ≤ a₂ ∧ b₂ ≤ b₁

@[instance_reducible]

instance Kalman.instInhabited {L : Type u_1} [PartialOrder L] [OrderBot L] : Inhabited (Kalman L)

The pair with no evidence either way, the fixed point of the involution.

Equations

• Kalman.instInhabited = { default := Kalman.mk ⊥ ⊥ ⋯ }

@[instance_reducible]

instance Kalman.instInvolutiveCompl {L : Type u_1} [PartialOrder L] [OrderBot L] : InvolutiveCompl (Kalman L)

Ginsberg's negation, swapping the coordinates, restricts to the disjoint pairs.

Equations

• Kalman.instInvolutiveCompl = { compl := fun (x : Kalman L) => ⟨(↑x)ᶜ, ⋯⟩, compl_compl := ⋯, compl_le_compl := ⋯ }

@[simp]

theorem Kalman.coe_compl {L : Type u_1} [PartialOrder L] [OrderBot L] (x : Kalman L) : ↑xᶜ = (↑x)ᶜ

@[simp]

theorem Kalman.compl_compl {L : Type u_1} [PartialOrder L] [OrderBot L] (x : Kalman L) : xᶜᶜ = x

@[simp]

theorem Kalman.pro_compl {L : Type u_1} [PartialOrder L] [OrderBot L] (x : Kalman L) : xᶜ.pro = x.con

@[simp]

theorem Kalman.con_compl {L : Type u_1} [PartialOrder L] [OrderBot L] (x : Kalman L) : xᶜ.con = x.pro

@[simp]

theorem Kalman.mk_compl {L : Type u_1} [PartialOrder L] [OrderBot L] (a b : L) (h : Disjoint a b) : (mk a b h)ᶜ = mk b a ⋯

@[instance_reducible]

instance Kalman.instBoundedOrder {L : Type u_1} [PartialOrder L] [BoundedOrder L] : BoundedOrder (Kalman L)

Equations

• Kalman.instBoundedOrder = Subtype.boundedOrder ⋯ ⋯

@[simp]

theorem Kalman.coe_top {L : Type u_1} [PartialOrder L] [BoundedOrder L] : ↑⊤ = ⊤

@[simp]

theorem Kalman.coe_bot {L : Type u_1} [PartialOrder L] [BoundedOrder L] : ↑⊥ = ⊥

@[simp]

theorem Kalman.pro_top {L : Type u_1} [PartialOrder L] [BoundedOrder L] : ⊤.pro = ⊤

@[simp]

theorem Kalman.con_top {L : Type u_1} [PartialOrder L] [BoundedOrder L] : ⊤.con = ⊥

@[simp]

theorem Kalman.pro_bot {L : Type u_1} [PartialOrder L] [BoundedOrder L] : ⊥.pro = ⊥

@[simp]

theorem Kalman.con_bot {L : Type u_1} [PartialOrder L] [BoundedOrder L] : ⊥.con = ⊤

The Kleene lattice

@[instance_reducible]

instance Kalman.instDistribLattice {L : Type u_1} [DistribLattice L] [OrderBot L] : DistribLattice (Kalman L)

Equations

• Kalman.instDistribLattice = Subtype.distribLattice ⋯ ⋯

@[simp]

theorem Kalman.coe_sup {L : Type u_1} [DistribLattice L] [OrderBot L] (x y : Kalman L) : ↑(x ⊔ y) = ↑x ⊔ ↑y

@[simp]

theorem Kalman.coe_inf {L : Type u_1} [DistribLattice L] [OrderBot L] (x y : Kalman L) : ↑(x ⊓ y) = ↑x ⊓ ↑y

@[simp]

theorem Kalman.pro_sup {L : Type u_1} [DistribLattice L] [OrderBot L] (x y : Kalman L) : (x ⊔ y).pro = x.pro ⊔ y.pro

@[simp]

theorem Kalman.con_sup {L : Type u_1} [DistribLattice L] [OrderBot L] (x y : Kalman L) : (x ⊔ y).con = x.con ⊓ y.con

@[simp]

theorem Kalman.pro_inf {L : Type u_1} [DistribLattice L] [OrderBot L] (x y : Kalman L) : (x ⊓ y).pro = x.pro ⊓ y.pro

@[simp]

theorem Kalman.con_inf {L : Type u_1} [DistribLattice L] [OrderBot L] (x y : Kalman L) : (x ⊓ y).con = x.con ⊔ y.con

@[simp]

theorem Kalman.mk_sup_mk {L : Type u_1} [DistribLattice L] [OrderBot L] {a₁ b₁ a₂ b₂ : L} (h₁ : Disjoint a₁ b₁) (h₂ : Disjoint a₂ b₂) : mk a₁ b₁ h₁ ⊔ mk a₂ b₂ h₂ = mk (a₁ ⊔ a₂) (b₁ ⊓ b₂) ⋯

@[simp]

theorem Kalman.mk_inf_mk {L : Type u_1} [DistribLattice L] [OrderBot L] {a₁ b₁ a₂ b₂ : L} (h₁ : Disjoint a₁ b₁) (h₂ : Disjoint a₂ b₂) : mk a₁ b₁ h₁ ⊓ mk a₂ b₂ h₂ = mk (a₁ ⊓ a₂) (b₁ ⊔ b₂) ⋯

instance Kalman.instIsKleene {L : Type u_1} [DistribLattice L] [OrderBot L] : IsKleene (Kalman L)

The disjoint pairs satisfy the Kleene law, so they form a normal i-lattice in the sense of [Kal58] §3.

Functoriality

def Kalman.map {L : Type u_1} {M : Type u_2} [DistribLattice L] [BoundedOrder L] [DistribLattice M] [BoundedOrder M] (f : BoundedLatticeHom L M) : BoundedLatticeHom (Kalman L) (Kalman M)

Kalman's construction on morphisms applies a bounded lattice homomorphism to both coordinates ([Cig86], as presented by [JSM17]).

Equations

• Kalman.map f = { toFun := fun (x : Kalman L) => Kalman.mk (f x.pro) (f x.con) ⋯, map_sup' := ⋯, map_inf' := ⋯, map_top' := ⋯, map_bot' := ⋯ }

@[simp]

theorem Kalman.pro_map {L : Type u_1} {M : Type u_2} [DistribLattice L] [BoundedOrder L] [DistribLattice M] [BoundedOrder M] (f : BoundedLatticeHom L M) (x : Kalman L) : ((map f) x).pro = f x.pro

@[simp]

theorem Kalman.con_map {L : Type u_1} {M : Type u_2} [DistribLattice L] [BoundedOrder L] [DistribLattice M] [BoundedOrder M] (f : BoundedLatticeHom L M) (x : Kalman L) : ((map f) x).con = f x.con

@[simp]

theorem Kalman.map_mk {L : Type u_1} {M : Type u_2} [DistribLattice L] [BoundedOrder L] [DistribLattice M] [BoundedOrder M] (f : BoundedLatticeHom L M) (a b : L) (h : Disjoint a b) : (map f) (mk a b h) = mk (f a) (f b) ⋯

@[simp]

theorem Kalman.map_compl {L : Type u_1} {M : Type u_2} [DistribLattice L] [BoundedOrder L] [DistribLattice M] [BoundedOrder M] (f : BoundedLatticeHom L M) (x : Kalman L) : (map f) xᶜ = ((map f) x)ᶜ

map f commutes with the involution.

@[simp]

theorem Kalman.map_id {L : Type u_1} [DistribLattice L] [BoundedOrder L] : map (BoundedLatticeHom.id L) = BoundedLatticeHom.id (Kalman L)

@[simp]

theorem Kalman.map_comp {L : Type u_1} {M : Type u_2} {N : Type u_3} [DistribLattice L] [BoundedOrder L] [DistribLattice M] [BoundedOrder M] [DistribLattice N] [BoundedOrder N] (f : BoundedLatticeHom L M) (g : BoundedLatticeHom M N) : map (g.comp f) = (map g).comp (map f)