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 Exhaustification.innocent.excluded (mathlib-canonical Finset version). 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.

Pointwise lift of Truth3.toBoolOrFalse.

Equations

• Exhaustification.Trivalent.classicalPart p = Core.Duality.Truth3.toBoolOrFalse ∘ p

def Exhaustification.Trivalent.exh1 {W : Type} [Fintype W] [DecidableEq 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} [Fintype W] [DecidableEq 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} [Fintype W] [DecidableEq W] (alts : List (W → Core.Duality.Truth3)) (p : W → Core.Duality.Truth3) (w : W) (h : p w = Core.Duality.Truth3.indet) : exh1 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} [Fintype W] [DecidableEq W] (alts : List (W → Core.Duality.Truth3)) (p : W → Core.Duality.Truth3) (w : W) (h : p w = Core.Duality.Truth3.indet) : exh2 alts p w = Core.Duality.Truth3.indet

EXH² also preserves the prejacent's presupposition.