Schöter's evidential bilattices: PRESUP and the defeasible 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. A value is a pair (for, against) of degrees of evidence drawn from a chain S.

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 adds the top of Schöter's progression:

• PRESUP := Evidential (Fin 3) — evidence from the 3-chain 0 < ½ < 1, adding defeasible (presumed) values P⁺/P⁻ above FOUR.
• embed : FOUR → PRESUP — FOUR is a sub-bilattice of PRESUP (order-preserving in both ≤_t and ≤_k): Schöter's "FOUR is a sublattice of all bilattices."
• the presupposition gap U and a defeasible presumption P⁺ are both consistent (non-glut); only the overdefined I is excluded — so the gap-based presupposition logic survives and gains a defeasible layer.

Scope: the value space and the progression. Schöter's inference apparatus (assertion/evaluation/inference, evidential links, the implemented engine, FOEBL/FOMEBL) is out of scope.

@[reducible, inline]

abbrev Schoter1996.PRESUP : Type

Schöter's PRESUP: 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 = (0, 0)

def Schoter1996.PRESUP.T : PRESUP

Definite truth (full evidence for, none against).

Equations

• Schoter1996.PRESUP.T = (2, 0)

def Schoter1996.PRESUP.F : PRESUP

Definite falsity.

Equations

• Schoter1996.PRESUP.F = (0, 2)

def Schoter1996.PRESUP.I : PRESUP

Inconsistent / overdefined (a glut).

Equations

• Schoter1996.PRESUP.I = (2, 2)

def Schoter1996.PRESUP.Pplus : PRESUP

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

Equations

• Schoter1996.PRESUP.Pplus = (1, 0)

def Schoter1996.PRESUP.Pminus : PRESUP

Presumably false.

Equations

• Schoter1996.PRESUP.Pminus = (0, 1)

@[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 : Bilattice.FOUR → PRESUP

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

Equations

• Schoter1996.embed = Prod.map Schoter1996.boolToFin3 Schoter1996.boolToFin3

theorem Schoter1996.embed_tLE (x y : Bilattice.FOUR) : Bilattice.Evidential.tLE x y ↔ Bilattice.Evidential.tLE (embed x) (embed y)

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

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

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

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.