Evidential bilattices over a chain

[Fit94] [Sch96a]

The evidential bilattices ([Sch96a]) are the diagonal Ginsberg–Fitting products S ⊙ S over a chain S (Core.Logic.Bilattice.Product): a value is a pair (for, against) of degrees of evidence, with

• ≤ truer = more evidence-for, less evidence-against (the truth order);
• ≤ₖ more informative = more evidence both ways (the knowledge order);
• Product.neg (truth inversion) swaps the two coordinates;
• conf (knowledge inversion, the conflation) complements each coordinate.

With S = Bool this is [Bel77]'s FOUR, whose logic is developed as a bilattice by [AA96]; with S = Fin 3 (the chain 0 < ½ < 1) it is [Sch96a]'s 9-valued PRESUP (see Studies.Schoter1996).

Main definitions

• Bilattice.Evidential S := S ⊙ S — the evidential bilattice over a chain S
• Evidential.conf/Consistent — conflation and the consistent (x ≤ₖ −x, non-glut) fragment
• Bilattice.FOUR := Evidential Bool — Belnap's four-valued bilattice

@[reducible, inline]

abbrev Bilattice.Evidential (S : Type u_1) : Type u_1

The evidential bilattice over a chain S: the diagonal product S ⊙ S, values are (for, against) pairs ([Sch96a]).

Equations

• Bilattice.Evidential S = Bilattice.Product S S

def Bilattice.Evidential.conf {S : Type u_1} (compl : S → S) (x : Evidential S) : Evidential S

Conflation −: knowledge inversion, complements each coordinate by compl, which is intended to be the order-reversing involution on the chain S ((! ·) for Bool, Fin.rev for Fin n).

Equations

• Bilattice.Evidential.conf compl x = Bilattice.Product.mk (compl (Bilattice.Product.con x)) (compl (Bilattice.Product.pro x))

@[reducible]

def Bilattice.Evidential.Consistent {S : Type u_1} [Preorder S] (compl : S → S) (x : Evidential S) : Prop

The consistent (non-glut) fragment: x ≤ₖ −x ([Fit94]).

Equations

• Bilattice.Evidential.Consistent compl x = Bilattice.kLE x (Bilattice.Evidential.conf compl x)

@[reducible]

def Bilattice.Evidential.IsClassical {S : Type u_1} (compl : S → S) (x : Evidential S) : Prop

The classical fragment: x = −x, the fixed points of conflation ([Fit94]; [Sch96a]'s CLAS).

Equations

• Bilattice.Evidential.IsClassical compl x = (x = Bilattice.Evidential.conf compl x)

theorem Bilattice.Evidential.consistent_iff_con_le {S : Type u_1} [Preorder S] {compl : S → S} (hanti : Antitone compl) (hinv : Function.Involutive compl) {x : Evidential S} : Consistent compl x ↔ Product.con x ≤ compl (Product.pro x)

Over an order-reversing involution compl, consistency reduces to a single inequality: the evidence-against is below the complement of the evidence-for ([Sch96a]'s CONS = {⟨a, b⟩ | a ≤ b′}).

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

Fitting's guard connective φ : ψ ([Sch96a] Def 4): the value of the second coordinate, attenuated by the positive evidence for the first.

Equations

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

theorem Bilattice.Evidential.guard_kLE_guard {S : Type u_1} [SemilatticeInf S] {x x' y y' : Evidential S} (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), as [Sch96a] Def 4 notes — though it is not a lattice-theoretic connective.

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

If the guard's first coordinate is at least true on ≤ₖ, the guard is its second coordinate ([Sch96a] Def 4).

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

With no positive evidence for the first coordinate, the guard is U ([Sch96a] Def 4).

@[reducible, inline]

abbrev Bilattice.FOUR : Type

[Bel77]'s four-valued bilattice FOUR = Bool ⊙ Bool, (for, against) over Bool.

Equations

• Bilattice.FOUR = Bilattice.Evidential Bool

def Bilattice.FOUR.U : FOUR

⊥: neither — no information (a truth-value gap).

Equations

• Bilattice.FOUR.U = Bilattice.Product.mk false false

def Bilattice.FOUR.T : FOUR

true.

Equations

• Bilattice.FOUR.T = Bilattice.Product.mk true false

def Bilattice.FOUR.F : FOUR

false.

Equations

• Bilattice.FOUR.F = Bilattice.Product.mk false true

def Bilattice.FOUR.I : FOUR

⊤: both — inconsistent (a truth-value glut).

Equations

• Bilattice.FOUR.I = Bilattice.Product.mk true true

@[reducible]

def Bilattice.FOUR.conf (x : FOUR) : FOUR

Conflation on FOUR (Boolean complement).

Equations

• x.conf = Bilattice.Evidential.conf (fun (x : Bool) => !x) x

@[reducible]

def Bilattice.FOUR.Consistent (x : FOUR) : Prop

The consistent (non-glut) fragment of FOUR — equivalently x ≠ I.

Equations

• x.Consistent = Bilattice.Evidential.Consistent (fun (x : Bool) => !x) x

@[reducible]

def Bilattice.FOUR.IsClassical (x : FOUR) : Prop

The classical fragment of FOUR — equivalently {F, T}.

Equations

• x.IsClassical = Bilattice.Evidential.IsClassical (fun (x : Bool) => !x) x

@[simp]

theorem Bilattice.FOUR.consistent_iff (x : FOUR) : x.Consistent ↔ x ≠ I

@[simp]

theorem Bilattice.FOUR.isClassical_iff (x : FOUR) : x.IsClassical ↔ x = F ∨ x = T

The classical fragment of FOUR is {F, T} ([Fit94]; [Sch96a]).