Evidential bilattices over a chain

[Fit94] [Sch96a]

A bilattice carries two orders on one carrier — a truth order ≤_t and an information/knowledge order ≤_k ([Fit94]). The evidential bilattices ([Sch96a]) are the ones of the form S ⊙ S for a chain S: a value is a pair (for, against) of degrees of evidence, with

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

With S = Bool this is Belnap's FOUR; with S = Fin 3 (the chain 0 < ½ < 1) it is [Sch96a]'s 9-valued PRESUP (see Studies.Schoter1996). This file is the shared substrate; concrete bilattices and their linguistic uses live in the consuming Studies files.

Main definitions

• Bilattice.Evidential S := S × S — the evidential bilattice over a chain S
• Evidential.tLE/kLE/neg/conf/Consistent — the two orders, negation, conflation, and the consistent (x ≤_k −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: values are (for, against) pairs ([Sch96a]'s S ⊙ S).

Equations

• Bilattice.Evidential S = (S × S)

@[reducible]

def Bilattice.Evidential.tLE {S : Type u_1} [Preorder S] (x y : Evidential S) : Prop

Truth order: more evidence-for and less evidence-against.

Equations

• x.tLE y = (x.fst ≤ y.fst ∧ y.snd ≤ x.snd)

@[reducible]

def Bilattice.Evidential.kLE {S : Type u_1} [Preorder S] (x y : Evidential S) : Prop

Knowledge order: more evidence both ways.

Equations

• x.kLE y = (x.fst ≤ y.fst ∧ x.snd ≤ y.snd)

def Bilattice.Evidential.neg {S : Type u_1} : Evidential S → Evidential S

Negation: truth inversion, swaps the coordinates.

Equations

• Bilattice.Evidential.neg = Prod.swap

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 = (compl x.snd, compl x.fst)

@[reducible]

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

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

Equations

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

@[reducible, inline]

abbrev Bilattice.FOUR : Type

Belnap'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 = (false, false)

def Bilattice.FOUR.T : FOUR

true.

Equations

• Bilattice.FOUR.T = (true, false)

def Bilattice.FOUR.F : FOUR

false.

Equations

• Bilattice.FOUR.F = (false, true)

def Bilattice.FOUR.I : FOUR

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

Equations

• Bilattice.FOUR.I = (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

@[simp]

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