Schöter (1996b): Evidential Bilattice Logic and Lexical Inference

This file formalizes the value space of the paper's Evidential Bilattice Logic. Natural reasoning is partial, paraconsistent, relevant and defeasible, and the paper captures the four properties by climbing a progression of lattices (Fig. 1): the classical two values, Kleene's three, Belnap's FOUR, and the evidential bilattice PRESUP over the chain 0 < ½ < 1, whose values are pairs of degrees of evidence for and against a proposition (PRESUP, the diagonal product Fin 3 ⊙ Fin 3), so that presumptions, confusion and defeated defaults join the gap and the glut. FOUR embeds in it preserving both orders (embed_le, embed_kLE). The evidential space is partitioned into Fitting's classical and consistent values and the paper's designated and semi-designated ones, with the paper's order-theoretic characterizations of the latter two (designated_iff_top_kLE, semiDesignated_iff). The semi-designation function, the presumably operator of the evaluation clauses and the evidential weighting that keeps only the dominant evidence are value-level connectives (semiDesignation, presumably, weight), the last mapping PRESUP onto the constants of [Gin88]'s default bilattice without being a homomorphism.

Implementation notes

• The paper writes a value as ⟨against, for⟩, reversing Fitting's coordinate order to fit its diagrams; this file keeps the substrate's (for, against) order, so the paper's ⟨a, b⟩ is .mk b a here.
• Fitting's conflation on PRESUP complements each coordinate on the chain by Fin.rev; it is the study's Conflation instance, built by Bilattice.Product.conflation.
• The paper's epistemic states, evidential links, its assertion, evaluation and closure semantics, and the §4 analyses of entailment, implicature and presupposition that run on them are not formalized; only the value level is.

References

• [Sch96a]
• [Fit94]
• [Gin88]
• [Bel77]

@[reducible, inline]

abbrev Schoter1996b.PRESUP : Type

The paper's PRESUP (§2.1): the evidential bilattice over the 3-chain Fin 3 ~ {0, ½, 1}, FOUR with defeasible and presumed values added.

Equations

• Schoter1996b.PRESUP = Bilattice.Product (Fin 3) (Fin 3)

@[instance_reducible]

instance Schoter1996b.instConflationPRESUP : Bilattice.Conflation PRESUP

Fitting's conflation on PRESUP, complementing each coordinate on the chain by Fin.rev.

Equations

• Schoter1996b.instConflationPRESUP = Bilattice.Product.conflation Fin.rev Schoter1996b.instConflationPRESUP._proof_1 Schoter1996b.instConflationPRESUP._proof_2

def Schoter1996b.PRESUP.U : PRESUP

⊥: no information, a presupposition gap.

Equations

• Schoter1996b.PRESUP.U = Bilattice.Product.mk 0 0

def Schoter1996b.PRESUP.T : PRESUP

Definite truth: full evidence for, none against.

Equations

• Schoter1996b.PRESUP.T = Bilattice.Product.mk 2 0

def Schoter1996b.PRESUP.F : PRESUP

Definite falsity.

Equations

• Schoter1996b.PRESUP.F = Bilattice.Product.mk 0 2

def Schoter1996b.PRESUP.I : PRESUP

Inconsistent or overdefined, a glut.

Equations

• Schoter1996b.PRESUP.I = Bilattice.Product.mk 2 2

def Schoter1996b.PRESUP.Pplus : PRESUP

Presumably true: defeasible (½) evidence for, none against.

Equations

• Schoter1996b.PRESUP.Pplus = Bilattice.Product.mk 1 0

def Schoter1996b.PRESUP.Pminus : PRESUP

Presumably false.

Equations

• Schoter1996b.PRESUP.Pminus = Bilattice.Product.mk 0 1

def Schoter1996b.PRESUP.C : PRESUP

Confused: conflicting defeasible evidence, not as strong a contradiction as I (§2.1).

Equations

• Schoter1996b.PRESUP.C = Bilattice.Product.mk 1 1

def Schoter1996b.PRESUP.Dplus : PRESUP

The defeated default D⁺: default evidence for falsity overridden by definite evidence for truth (§2.1).

Equations

• Schoter1996b.PRESUP.Dplus = Bilattice.Product.mk 2 1

def Schoter1996b.PRESUP.Dminus : PRESUP

The defeated default D⁻: default evidence for truth overridden by definite evidence for falsity (§2.1).

Equations

• Schoter1996b.PRESUP.Dminus = Bilattice.Product.mk 1 2

def Schoter1996b.boolToFin3 : Bool → Fin 3

Bool ↪ Fin 3: false ↦ 0 (no evidence), true ↦ 2 (full evidence).

Equations

• Schoter1996b.boolToFin3 b = if b = true then 2 else 0

def Schoter1996b.embed (x : Bilattice.FOUR) : PRESUP

The embedding of FOUR into PRESUP, onto the definite values.

Equations

• Schoter1996b.embed x = Bilattice.Product.mk (Schoter1996b.boolToFin3 (Bilattice.Product.pro x)) (Schoter1996b.boolToFin3 (Bilattice.Product.con x))

theorem Schoter1996b.embed_le (x y : Bilattice.FOUR) : x ≤ y ↔ embed x ≤ embed y

FOUR is a sub-bilattice of PRESUP in the truth order: the embedding preserves and reflects ≤.

theorem Schoter1996b.embed_kLE (x y : Bilattice.FOUR) : Bilattice.kLE x y ↔ Bilattice.kLE (embed x) (embed y)

FOUR is a sub-bilattice of PRESUP in the knowledge order: the embedding preserves and reflects ≤ₖ.

theorem Schoter1996b.gap_and_presumption_consistent : Bilattice.IsConsistent PRESUP.U ∧ Bilattice.IsConsistent PRESUP.Pplus ∧ ¬Bilattice.IsConsistent PRESUP.I

A presupposition gap and a defeasible presumption are both consistent; only the overdefined glut is excluded, so PRESUP keeps the gap-based logic and layers defeasible values on it.

Partitions of the evidential space (§2.2)

The classical and consistent subspaces are Fitting's (IsExact, IsConsistent); the designated and semi-designated subspaces are the paper's, with its footnote characterizations DES = {x | t ≤ₖ x} and SEMI = {x | ¬x ≤ x, U <ₖ x} proved as order-theoretic facts.

@[reducible]

def Schoter1996b.Designated {S : Type u_1} [LinearOrder S] [BoundedOrder S] (x : Bilattice.Product S S) : Prop

A designated value (§2.2) has maximal positive evidence: DES = {⟨a, b⟩ | b = 1}.

Equations

• Schoter1996b.Designated x = (x.pro = ⊤)

@[reducible]

def Schoter1996b.SemiDesignated {S : Type u_1} [LinearOrder S] [BoundedOrder S] (x : Bilattice.Product S S) : Prop

A semi-designated value (§2.2) has some positive evidence, at least as strong as its negative evidence: SEMI = {⟨a, b⟩ | a ≤ b, 0 < b}.

Equations

• Schoter1996b.SemiDesignated x = (x.con ≤ x.pro ∧ ⊥ < x.pro)

theorem Schoter1996b.designated_iff_top_kLE {S : Type u_1} [LinearOrder S] [BoundedOrder S] {x : Bilattice.Product S S} : Designated x ↔ Bilattice.kLE ⊤ x

The footnote characterization of designation: a value is designated iff it is knowledge-above the truth top, DES = {x | t ≤ₖ x} (§2.2).

theorem Schoter1996b.semiDesignated_iff {S : Type u_1} [LinearOrder S] [BoundedOrder S] {x : Bilattice.Product S S} : SemiDesignated x ↔ xᶜ ≤ x ∧ ⊥ < Bilattice.toKnow x

The footnote characterization of semi-designation: a value is semi-designated iff it is truer than its negation and contains some information, SEMI = {x | ¬x ≤ x, U <ₖ x} (§2.2).

theorem Schoter1996b.designated_cases (x : PRESUP) : Designated x ↔ x = PRESUP.T ∨ x = PRESUP.Dplus ∨ x = PRESUP.I

The designated subspace of PRESUP is {T, D⁺, I} (§2.2).

theorem Schoter1996b.semiDesignated_cases (x : PRESUP) : SemiDesignated x ↔ x = PRESUP.Pplus ∨ x = PRESUP.C ∨ x = PRESUP.T ∨ x = PRESUP.Dplus ∨ x = PRESUP.I

The semi-designated subspace of PRESUP is {P⁺, C, T, D⁺, I} (§2.2).

theorem Schoter1996b.four_semiDesignated_iff_designated (x : Bilattice.FOUR) : SemiDesignated x ↔ Designated x

On FOUR, with no defeasible evidence, semi-designation collapses to designation, SEMI = DES (§2.2).

theorem Schoter1996b.four_consistent_closed (x y : Bilattice.FOUR) : Bilattice.IsConsistent x → Bilattice.IsConsistent y → Bilattice.IsConsistent xᶜ ∧ Bilattice.IsConsistent (x ⊓ y) ∧ Bilattice.IsConsistent (x ⊔ y) ∧ Bilattice.IsConsistent (Bilattice.kInf x y)

The consistent fragment of FOUR is closed under negation, the truth operations and consensus ⊓ₖ (§2.2).

theorem Schoter1996b.four_consistent_not_closed_kSup : ¬∀ (x y : Bilattice.FOUR), Bilattice.IsConsistent x → Bilattice.IsConsistent y → Bilattice.IsConsistent (Bilattice.kSup x y)

The consistent fragment is not closed under gullibility ⊔ₖ: credulously combining consistent evidence can produce the glut, so paraconsistency is localized rather than absent.

theorem Schoter1996b.four_isClassical_closed (x y : Bilattice.FOUR) : Bilattice.IsExact x → Bilattice.IsExact y → Bilattice.IsExact xᶜ ∧ Bilattice.IsExact (x ⊓ y) ∧ Bilattice.IsExact (x ⊔ y)

The classical fragment of FOUR is closed under negation and the truth operations (§2.2), and so supports classical logic.

Value-level connectives (Definitions 4, 5, 14 and 16)

The recursive evaluation clauses of Definition 14 are value-functional except for the inference-link connective: clause 1 is Ginsberg negation ᶜ, clauses 3 and 4 are ⊓ and ⊔, clause 5 is Fitting's guard, and clause 2, the presumably operator, is built from the guard and the semi-designation function.

def Schoter1996b.semiDesignation {S : Type u_1} [LinearOrder S] [BoundedOrder S] (x : Bilattice.Product S S) : Bilattice.Product S S

The semi-designation function σ (Definition 5): T on the semi-designated values, F elsewhere.

Equations

• Schoter1996b.semiDesignation x = if Schoter1996b.SemiDesignated x then Bilattice.Product.mk ⊤ ⊥ else Bilattice.Product.mk ⊥ ⊤

def Schoter1996b.presumably {S : Type u_1} [LinearOrder S] [BoundedOrder S] (v : Bilattice.Product S S) : Bilattice.Product S S

The value-level presumably operator π (Definition 14, clause 2): σ(v) : T ⊕ σ(¬v) : F, presumably true if the value is semi-designated, presumably false if its negation is, the two unified informationally.

Equations

• Schoter1996b.presumably v = Bilattice.kSup ((Schoter1996b.semiDesignation v).guard (Bilattice.Product.mk ⊤ ⊥)) ((Schoter1996b.semiDesignation vᶜ).guard (Bilattice.Product.mk ⊥ ⊤))

theorem Schoter1996b.presumably_table : presumably PRESUP.Pplus = PRESUP.T ∧ presumably PRESUP.T = PRESUP.T ∧ presumably PRESUP.F = PRESUP.F ∧ presumably PRESUP.U = PRESUP.U ∧ presumably PRESUP.I = PRESUP.I

presumably fixes the definite values and the gap, and raises a presumption to definite truth.

def Schoter1996b.weight {S : Type u_1} [LinearOrder S] [BoundedOrder S] (x : Bilattice.Product S S) : Bilattice.Product S S

The evidential-weighting function f⋆ (Definition 16) suppresses the dominated evidence, so that only the dominant evidence figures in evaluation.

Equations

• Schoter1996b.weight x = if x.con < x.pro then Bilattice.Product.mk x.pro ⊥ else if x.pro < x.con then Bilattice.Product.mk ⊥ x.con else x

theorem Schoter1996b.weight_dplus : weight PRESUP.Dplus = PRESUP.T

Weighting evaluates a defeated default as the definite value that defeated it: f⋆(D⁺) = T.

theorem Schoter1996b.weight_dminus : weight PRESUP.Dminus = PRESUP.F

f⋆(D⁻) = F.

theorem Schoter1996b.weight_mem_default (x : PRESUP) : weight x ∈ [PRESUP.U, PRESUP.Pminus, PRESUP.Pplus, PRESUP.C, PRESUP.F, PRESUP.T, PRESUP.I]

f⋆ maps PRESUP onto the seven constants of [Gin88]'s default bilattice (Definition 16).

theorem Schoter1996b.weight_not_kSup_hom : ¬∀ (x y : PRESUP), weight (Bilattice.kSup x y) = Bilattice.kSup (weight x) (weight y)

The weighting is not a bilattice homomorphism onto the default bilattice (Definition 16): it fails to commute with gullibility ⊔ₖ.