Trivalent Exhaustification

@cite{spector-sudo-2017}

Benjamin Spector and Yasutada Sudo, "Presupposed Ignorance and Exhaustification: How Scalar Implicatures and Presuppositions Interact." Linguistics and Philosophy 40, pp. 473–517.

Core Operators

Two trivalent exhaustification operators extend bivalent EXH (@cite{fox-2007}) to handle presupposition-bearing sentences:

• EXH¹ (weak negation): ~ψ = true when ψ is undefined → does NOT import presuppositions from alternatives
• EXH² (strong negation): ~ψ = # when ψ is undefined → DOES import presuppositions from alternatives

Both reuse the same innocently excludable (IE) alternatives computed by Fox's algorithm on the classical truth conditions.

Connection to Presupposition Projection

@cite{wang-davidson-2026} show that this distinction is empirically consequential for presupposition filtering across disjunction:

• EXH² + any projection theory predicts that exclusive disjunction increases projection (Type A)
• EXH¹ + any projection theory predicts no effect of exclusivity on projection (Type B)

Their Mandarin experiment finds no effect of exclusivity on filtering, consistent with Type B (EXH¹).

Design

This file is generic infrastructure, not a paper replication. The IE computation reuses InnocentExclusion.ieIndices (computable, Bool-based). The trivalent layer wraps the bivalent IE result with Truth3 semantics.

def Exhaustification.Trivalent.classicalPart {W : Type} (p : W → Core.Duality.Truth3) : W → Bool

Extract the classical (bivalent) truth conditions from a trivalent proposition: true maps to true; false and indet both map to false.

The IE computation operates on these classical truth conditions — entailment, consistency, and maximality are all defined bivalently. The trivalent layer applies only after IE is computed.

Equations

• Exhaustification.Trivalent.classicalPart p w = (p w == Core.Duality.Truth3.true)

def Exhaustification.Trivalent.exh1 {W : Type} [BEq W] (domain : List W) (alts : List (W → Core.Duality.Truth3)) (p : W → Core.Duality.Truth3) : W → Core.Duality.Truth3

Trivalent EXH¹ (weak negation).

@cite{spector-sudo-2017}'s weak-negation operator (reproduced as (4)/(5) in @cite{wang-davidson-2026}):

• Presupposes whatever φ presupposes: φ(w)=# → EXH¹(w)=#
• Asserts φ and weakly negates all IE alternatives
• Weak negation: ~# = true, so alternatives' presuppositions do NOT project through EXH¹

Type B in @cite{wang-davidson-2026}: predicts no effect of exclusivity on presupposition filtering.

Equations

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

def Exhaustification.Trivalent.exh2 {W : Type} [BEq W] (domain : List W) (alts : List (W → Core.Duality.Truth3)) (p : W → Core.Duality.Truth3) : W → Core.Duality.Truth3

Trivalent EXH² (strong negation).

@cite{spector-sudo-2017}'s strong-negation operator (reproduced as (6)/(7) in @cite{wang-davidson-2026}):

• Presupposes whatever φ presupposes AND whatever the negated IE alternatives presuppose
• Asserts φ and strongly negates all IE alternatives
• Strong negation: ~# = #, so alternatives' presuppositions DO project through EXH²

Type A in @cite{wang-davidson-2026}: predicts that increasing exclusivity reduces presupposition filtering.

Equations

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

theorem Exhaustification.Trivalent.exh1_preserves_presup {W : Type} [BEq W] (domain : List W) (alts : List (W → Core.Duality.Truth3)) (p : W → Core.Duality.Truth3) (w : W) (h : p w = Core.Duality.Truth3.indet) : exh1 domain alts p w = Core.Duality.Truth3.indet

EXH¹ preserves the presupposition of the prejacent: if φ(w) = #, then EXH¹(φ)(w) = #.

theorem Exhaustification.Trivalent.exh2_preserves_presup {W : Type} [BEq W] (domain : List W) (alts : List (W → Core.Duality.Truth3)) (p : W → Core.Duality.Truth3) (w : W) (h : p w = Core.Duality.Truth3.indet) : exh2 domain alts p w = Core.Duality.Truth3.indet

EXH² also preserves the prejacent's presupposition.

Bathroom disjunction example

"φ or ψ" where ψ presupposes π and ¬φ entails π.

Using the four-world model from InnocentExclusion.lean (PQWorld), we add a presupposition to q: q is defined only when p is false (i.e., the presupposition π = ¬p holds). This is the "bathroom disjunction" pattern used in @cite{wang-davidson-2026}'s experiment.

inductive Exhaustification.Trivalent.BathWorld : Type

Three worlds for a bathroom disjunction:

• pOnly: p true, q's presupposition fails (#)
• qOnly: p false, q true (presupposition satisfied)
• neither: p false, q false (presupposition satisfied)

• pOnly : BathWorld
• qOnly : BathWorld
• neither : BathWorld

def Exhaustification.Trivalent.instReprBathWorld.repr : BathWorld → ℕ → Std.Format

Equations

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

instance Exhaustification.Trivalent.instReprBathWorld : Repr BathWorld

Equations

• Exhaustification.Trivalent.instReprBathWorld = { reprPrec := Exhaustification.Trivalent.instReprBathWorld.repr }

instance Exhaustification.Trivalent.instDecidableEqBathWorld : DecidableEq BathWorld

Equations

• Exhaustification.Trivalent.instDecidableEqBathWorld x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Exhaustification.Trivalent.instBEqBathWorld.beq : BathWorld → BathWorld → Bool

Equations

• Exhaustification.Trivalent.instBEqBathWorld.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Exhaustification.Trivalent.instBEqBathWorld : BEq BathWorld

Equations

• Exhaustification.Trivalent.instBEqBathWorld = { beq := Exhaustification.Trivalent.instBEqBathWorld.beq }

def Exhaustification.Trivalent.bDomain : List BathWorld

Equations

• Exhaustification.Trivalent.bDomain = [Exhaustification.Trivalent.BathWorld.pOnly, Exhaustification.Trivalent.BathWorld.qOnly, Exhaustification.Trivalent.BathWorld.neither]

def Exhaustification.Trivalent.pT3 : BathWorld → Core.Duality.Truth3

p: always defined (no presupposition).

Equations

• Exhaustification.Trivalent.pT3 Exhaustification.Trivalent.BathWorld.pOnly = Core.Duality.Truth3.true
• Exhaustification.Trivalent.pT3 x✝ = Core.Duality.Truth3.false

def Exhaustification.Trivalent.qT3 : BathWorld → Core.Duality.Truth3

q: presupposes ¬p (defined only when p is false).

Equations

• Exhaustification.Trivalent.qT3 Exhaustification.Trivalent.BathWorld.pOnly = Core.Duality.Truth3.indet
• Exhaustification.Trivalent.qT3 Exhaustification.Trivalent.BathWorld.qOnly = Core.Duality.Truth3.true
• Exhaustification.Trivalent.qT3 Exhaustification.Trivalent.BathWorld.neither = Core.Duality.Truth3.false

theorem Exhaustification.Trivalent.inclusive_allows_filtering : (pT3 BathWorld.pOnly).join (qT3 BathWorld.pOnly) = Core.Duality.Truth3.true

Inclusive disjunction under Strong Kleene allows filtering: at pOnly, p is true and q is undefined, but join returns true. The second disjunct's presupposition is "filtered".

theorem Exhaustification.Trivalent.exclusive_no_filtering : (pT3 BathWorld.pOnly).xor (qT3 BathWorld.pOnly) = Core.Duality.Truth3.indet

Exclusive disjunction does NOT allow filtering: at pOnly, xor returns undefined because q's value is unknown.

def Exhaustification.Trivalent.inclDisj : BathWorld → Core.Duality.Truth3

Inclusive disjunction as Prop3 (Strong Kleene).

Equations

• Exhaustification.Trivalent.inclDisj w = (Exhaustification.Trivalent.pT3 w).join (Exhaustification.Trivalent.qT3 w)

def Exhaustification.Trivalent.exclDisj : BathWorld → Core.Duality.Truth3

Exclusive disjunction as Prop3 (Strong Kleene).

Equations

• Exhaustification.Trivalent.exclDisj w = (Exhaustification.Trivalent.pT3 w).xor (Exhaustification.Trivalent.qT3 w)

theorem Exhaustification.Trivalent.incl_defined_at_pOnly : inclDisj BathWorld.pOnly = Core.Duality.Truth3.true

Inclusive disjunction is defined at pOnly (filtering).

theorem Exhaustification.Trivalent.excl_undef_at_pOnly : exclDisj BathWorld.pOnly = Core.Duality.Truth3.indet

Exclusive disjunction is undefined at pOnly (no filtering).

def Exhaustification.Trivalent.bathAlts : List (BathWorld → Core.Duality.Truth3)

EXH¹ applied to inclusive disjunction: the presupposition is unchanged because EXH¹ uses weak negation.

The alternatives are {p∨q, p, q, p∧q}. The conjunction alternative p∧q is the only IE alternative (by Fox 2007). Since p∧q is undefined at pOnly (q is undefined there), weak negation treats ~(p∧q) as true → no new presupposition.

Equations

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

theorem Exhaustification.Trivalent.exh1_disjunction_pOnly : exh1 bDomain bathAlts inclDisj BathWorld.pOnly = Core.Duality.Truth3.true

theorem Exhaustification.Trivalent.exh2_disjunction_pOnly : exh2 bDomain bathAlts inclDisj BathWorld.pOnly = Core.Duality.Truth3.indet

EXH² applied to inclusive disjunction: the conjunction alternative p∧q is undefined at pOnly, so strong negation makes EXH² undefined there → presupposition imported.