The guard connective

The guard P : Q of [Fit94] is Q when P is at least true and undefined otherwise; it makes Kleene's weak logic and the asymmetric Lisp logic definable over Belnap's FOUR. On a diagonal product L ⊙ L it is ⟨a, b⟩ : ⟨c, d⟩ = ⟨a ⊓ c, a ⊓ d⟩ ([Fit94] Definition 9.4), the second argument attenuated by the evidence for the first. It is knowledge-monotone in both arguments but not a lattice-theoretic connective ([Sch96a] Def 4).

Main definitions

• Bilattice.Product.guard: the guard on L ⊙ L.

Main results

• Bilattice.Product.guard_kLE_guard: the guard is knowledge-monotone.
• Bilattice.Product.guard_of_top_kLE, Bilattice.Product.guard_of_pro_bot: a first argument that is at least true passes the second through, and one with no evidence for it gives ⊥ₖ.
• Bilattice.Product.guard_eq_kSup_compl: the guard is definable from the bilattice operations, P : Q = [(P ⊓ₖ t) ⊔ₖ (P ⊓ₖ t)ᶜ] ⊓ₖ Q ([Fit94] §9).

References

• [Fit94]
• [Sch96a]

def Bilattice.Product.guard {L : Type u_1} [SemilatticeInf L] (x y : Product L L) : Product L L

The guard x : y ([Fit94] Definition 9.4): the value of y, attenuated by the evidence for x.

Equations

• x.guard y = Bilattice.Product.mk (x.pro ⊓ y.pro) (x.pro ⊓ y.con)

@[simp]

theorem Bilattice.Product.pro_guard {L : Type u_1} [SemilatticeInf L] (x y : Product L L) : (x.guard y).pro = x.pro ⊓ y.pro

@[simp]

theorem Bilattice.Product.con_guard {L : Type u_1} [SemilatticeInf L] (x y : Product L L) : (x.guard y).con = x.pro ⊓ y.con

theorem Bilattice.Product.guard_kLE_guard {L : Type u_1} [SemilatticeInf L] {x x' y y' : Product L L} (hx : kLE x x') (hy : kLE y y') : kLE (x.guard y) (x'.guard y')

The guard is monotone in the knowledge order in both arguments ([Sch96a] Def 4).

theorem Bilattice.Product.guard_of_top_kLE {L : Type u_1} [SemilatticeInf L] [BoundedOrder L] {x : Product L L} (h : kLE ⊤ x) (y : Product L L) : x.guard y = y

A first argument that is at least true passes the second through ([Sch96a] Def 4).

theorem Bilattice.Product.guard_of_pro_bot {L : Type u_1} [SemilatticeInf L] [BoundedOrder L] {x : Product L L} (h : x.pro = ⊥) (y : Product L L) : x.guard y = mk ⊥ ⊥

A first argument with no evidence for it gives ⊥ₖ = ⟨⊥, ⊥⟩ ([Sch96a] Def 4).

theorem Bilattice.Product.guard_eq_kSup_compl {L : Type u_1} [Lattice L] [BoundedOrder L] (x y : Product L L) : x.guard y = kInf (kSup (kInf x ⊤) (kInf x ⊤)ᶜ) y

The guard is definable from the bilattice operations, x : y = [(x ⊓ₖ t) ⊔ₖ (x ⊓ₖ t)ᶜ] ⊓ₖ y ([Fit94] §9).