Schöter's evidential bilattices: PRESUP and the evidential progression

[Sch96a]

[Sch96a]'s Evidential Bilattice Logic analyzes natural-language entailment, implicature, and presupposition by climbing a progression of evidential bilattices S ⊙ S (Bilattice.Evidential): classical ⊂ Kleene-3 ⊂ FOUR ⊂ PRESUP (Fig. 1). A value is a pair (for, against) of degrees of evidence drawn from a chain S — the paper writes ⟨a, b⟩ for (against, for) (reversing Fitting's coordinate order, as its fn. to §2.1 notes); this file keeps the library's (for, against) = Fitting order throughout.

This file is the second consumer of the Bilattice substrate (the first is Studies.Fitting1994, which shows Kleene-3 = the consistent fragment of FOUR). It formalizes the paper's value level:

• PRESUP := Evidential (Fin 3) — evidence from the 3-chain 0 < ½ < 1 (§2.1): the nine values U, T, F, I, P⁺, P⁻, C, D⁺, D⁻. The orderings and inversions of Defs 1–2 are the substrate's ≤/≤ₖ, Product.neg, and Evidential.conf; the meets and joins of Def 3 are ⊓/⊔/⊗/⊕.
• embed : FOUR → PRESUP — FOUR is a sub-bilattice of PRESUP (order-preserving in both ≤ and ≤ₖ): Schöter's "FOUR is a sublattice of all bilattices."
• partitions of the evidential space (§2.2) — Bilattice.Evidential's consistent/classical fragments plus the paper's designated (Designated) and semi-designated (SemiDesignated) subspaces, with their order-theoretic characterizations and the closure facts of §2.2.
• value-level connectives — Fitting's guard φ : ψ (Def 4), the semi-designation function σ (Def 5), the value-level presumably operator π (Def 14, clause 2), and the evidential-weighting function f⋆ (Def 16) onto the constants of [Gin88]'s DEFAULT bilattice.

Scope: the value space, the progression, and the value-level operators. Schöter's epistemic-state apparatus (setups, evidential links, assertion / evaluation / closure, FOEBL/FOMEBL, and the §4 data analyses that run on the implemented engine) is out of scope.

@[reducible, inline]

abbrev Schoter1996.PRESUP : Type

Schöter's PRESUP (§2.1): the evidential bilattice over the 3-chain Fin 3 ~ {0, ½, 1} — FOUR with defeasible/presumed values added.

Equations

• Schoter1996.PRESUP = Bilattice.Evidential (Fin 3)

def Schoter1996.PRESUP.U : PRESUP

⊥: no information (a presupposition gap).

Equations

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

def Schoter1996.PRESUP.T : PRESUP

Definite truth (full evidence for, none against).

Equations

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

def Schoter1996.PRESUP.F : PRESUP

Definite falsity.

Equations

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

def Schoter1996.PRESUP.I : PRESUP

Inconsistent / overdefined (a glut).

Equations

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

def Schoter1996.PRESUP.Pplus : PRESUP

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

Equations

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

def Schoter1996.PRESUP.Pminus : PRESUP

Presumably false.

Equations

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

def Schoter1996.PRESUP.C : PRESUP

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

Equations

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

def Schoter1996.PRESUP.Dplus : PRESUP

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

Equations

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

def Schoter1996.PRESUP.Dminus : PRESUP

Defeated default D⁻: default evidence for truth overridden by definite negative evidence (§2.1).

Equations

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

@[reducible]

def Schoter1996.PRESUP.conf (x : PRESUP) : PRESUP

Conflation on PRESUP, complementing on the chain by Fin.rev.

Equations

• x.conf = Bilattice.Evidential.conf Fin.rev x

@[reducible]

def Schoter1996.PRESUP.Consistent (x : PRESUP) : Prop

The consistent (non-glut) fragment of PRESUP.

Equations

• x.Consistent = Bilattice.Evidential.Consistent Fin.rev x

def Schoter1996.boolToFin3 : Bool → Fin 3

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

Equations

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

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

The embedding of FOUR into PRESUP (definite values only).

Equations

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

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

FOUR ⊂ PRESUP, truth order: the embedding preserves and reflects ≤.

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

FOUR ⊂ PRESUP, knowledge order: the embedding preserves and reflects ≤ₖ.

theorem Schoter1996.gap_and_presumption_consistent : PRESUP.U.Consistent ∧ PRESUP.Pplus.Consistent ∧ ¬PRESUP.I.Consistent

A presupposition gap (U) and a defeasible presumption (P⁺) are both consistent; only the overdefined glut I is excluded. So PRESUP keeps the gap-based presupposition logic and layers defeasible values on top.

Partitions of the evidential space (§2.2)

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

@[reducible]

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

Designated values (§2.2): maximal positive evidence, DES = {⟨a, b⟩ | b = 1}.

Equations

• Schoter1996.Designated x = (Bilattice.Product.pro x = ⊤)

@[reducible]

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

Semi-designated values (§2.2): some positive evidence, at least as strong as the negative evidence — SEMI = {⟨a, b⟩ | a ≤ b, 0 < b}.

Equations

• Schoter1996.SemiDesignated x = (Bilattice.Product.con x ≤ Bilattice.Product.pro x ∧ ⊥ < Bilattice.Product.pro x)

theorem Schoter1996.designated_iff_top_kLE {S : Type u_1} [LinearOrder S] [BoundedOrder S] {x : Bilattice.Evidential 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 Schoter1996.semiDesignated_iff {S : Type u_1} [LinearOrder S] [BoundedOrder S] {x : Bilattice.Evidential S} : SemiDesignated x ↔ Bilattice.Product.neg 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 Schoter1996.designated_cases (x : PRESUP) : Designated x ↔ x = PRESUP.T ∨ x = PRESUP.Dplus ∨ x = PRESUP.I

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

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

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

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

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

theorem Schoter1996.four_consistent_closed (x y : Bilattice.FOUR) : x.Consistent → y.Consistent → Bilattice.FOUR.Consistent (Bilattice.Product.neg x) ∧ (x ⊓ y).Consistent ∧ (x ⊔ y).Consistent ∧ (Bilattice.kInf x y).Consistent

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

theorem Schoter1996.four_consistent_not_closed_kSup : ¬∀ (x y : Bilattice.FOUR), x.Consistent → y.Consistent → (Bilattice.kSup x y).Consistent

...but not under gullibility ⊕: credulously combining consistent evidence can produce the glut — paraconsistency is localized rather than absent.

theorem Schoter1996.four_isClassical_closed (x y : Bilattice.FOUR) : x.IsClassical → y.IsClassical → Bilattice.FOUR.IsClassical (Bilattice.Product.neg x) ∧ (x ⊓ y).IsClassical ∧ (x ⊔ y).IsClassical

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

Value-level connectives (Defs 4, 5, 14, 16)

The recursive evaluation clauses of Def 14 are value-functional except for the inference-link connective: clause 1 is Product.neg, clauses 3–4 are ⊓/⊔, clause 5 is Fitting's guard, and clause 2 (the presumably operator π) is built from the guard and the semi-designation function σ.

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

The semi-designation function σ ([Sch96a] Def 5): T on the semi-designated values, F elsewhere.

Equations

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

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

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

Equations

• One or more equations did not get rendered due to their size.

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

The evidential-weighting function f⋆ ([Sch96a] Def 16): suppresses the dominated evidence, so only the dominant evidence figures in evaluation.

Equations

• One or more equations did not get rendered due to their size.

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

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

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

f⋆(D⁻) = F.

theorem Schoter1996.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 (Def 16).

theorem Schoter1996.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 DEFAULT (Def 16): it fails to commute with gullibility ⊕.