Wang & Davidson (2026): Presupposition Filtering in Disjunction

@cite{wang-davidson-2026}

Yiqian Wang and Kathryn Davidson, "Presupposition filtering in disjunction: The role of exclusive interpretation." Proceedings of Sinn und Bedeutung 30.

Summary

The paper asks whether exclusive interpretation of disjunction (via scalar implicature / exhaustification) affects presupposition projection. The answer, both theoretically and empirically, is:

Most theories predict yes, but the experiment finds no.

Theoretical Contribution (§3)

The paper surveys combinations of:

• Exhaustification theories: bivalent EXH, trivalent EXH¹, EXH²
• Projection theories: Strong Kleene, George 2008, classic dynamic semantics

These divide into two classes:

• Type A: increasing exclusivity reduces filtering (bivalent EXH + SK/George/dynamic; EXH² + any projection)
• Type B: exclusivity has no effect on filtering (EXH¹ + any projection)

The core mechanism: under Strong Kleene, inclusive disjunction (Truth3.join) can return .true even when one disjunct is undefined — so a true first disjunct "filters" the second's presupposition failure. Exclusive disjunction (Truth3.xor) cannot: it returns .indet whenever either input is .indet.

Feed-forward assumption (§5)

The Type A prediction for bivalent EXH depends on a feed-forward assumption: the strengthened (exclusive) truth conditions must be computed early enough to be visible to the projection computation. Without this, bivalent EXH + SK would not predict Type A because the projection computation would see only the original inclusive truth conditions. This assumption is architecturally non-trivial — see @cite{wang-davidson-2026} §5.

Empirical Contribution (§4)

Mandarin experiment using huozhe ('or'), manipulating exclusivity via environmental monotonicity (UE → more exclusive, DE → less). Two presupposition triggers: jie 'quit' and zhidao 'know'.

Key result: PREDICATE × MONOTONICITY interaction is not significant (p = .30, BF₁₀ = 0.52). No evidence that exclusivity modulates filtering. This challenges Type A theories and is consistent with Type B (EXH¹).

Secondary finding: filtering (a)symmetry depends on trigger. jie shows asymmetric filtering (PREDICATE × ORDER: p = .01); zhidao shows symmetric filtering (uniform, p = .99 for PREDICATE).

Inclusive vs exclusive disjunction under Strong Kleene

The fundamental asymmetry: inclusive disjunction can "see past" an undefined disjunct when the other is true. Exclusive cannot.

This single fact drives the Type A prediction for bivalent EXH + SK: since bivalent_exh_yields_xor shows Exh strengthens ∨ to ⊻, and Truth3.xor_indet_iff shows ⊻ propagates undefinedness unconditionally, exhaustification eliminates filtering.

theorem WangDavidson2026.sk_inclusive_filters : max Core.Duality.Truth3.true Core.Duality.Truth3.indet = Core.Duality.Truth3.true

Inclusive disjunction allows filtering: a true first disjunct absorbs the second's presupposition failure.

theorem WangDavidson2026.sk_exclusive_no_filter : Core.Duality.Truth3.true.xor Core.Duality.Truth3.indet = Core.Duality.Truth3.indet

Exclusive disjunction does not filter: even when one disjunct is true, an undefined partner makes the result undefined.

theorem WangDavidson2026.sk_filtering_symmetric : max Core.Duality.Truth3.indet Core.Duality.Truth3.true = Core.Duality.Truth3.true ∧ Core.Duality.Truth3.indet.xor Core.Duality.Truth3.true = Core.Duality.Truth3.indet

The filtering contrast is symmetric: both join and xor are commutative, so the direction doesn't matter for SK.

This is what @cite{kalomoiros-schwarz-2024} call "symmetric projection" — filtering is equally (un)available in both directions.

PrProp exclusive disjunction

PrProp.xor requires both presuppositions to hold — it never filters presupposition failure from either disjunct. This mirrors the SK XOR truth table (Figure 2 in the paper).

Note: SK inclusive filtering (Truth3.join .true .indet = .true) is an emergent property of the SK truth table, not a PrProp connective. The contrast is between Truth3.join (filters) and Truth3.xor (does not filter), verified in §1 above.

theorem WangDavidson2026.prprop_exclusive_no_filter {W : Type u_1} (p q : Core.Presupposition.PrProp W) (w : W) (hq : ¬q.presup w) : (p.xor q).eval w = Core.Duality.Truth3.indet

PrProp.xor does not filter: when q's presupposition fails, the result is always undefined regardless of p.

inductive WangDavidson2026.TheoryClass : Type

Theory classification from §3.3: theories are grouped by their prediction about the effect of exclusivity on presupposition filtering across disjunction.

• typeA : TheoryClass

  Increasing exclusivity reduces filtering.

• typeB : TheoryClass

  Exclusivity has no effect on filtering.

@[implicit_reducible]

instance WangDavidson2026.instDecidableEqTheoryClass : DecidableEq TheoryClass

Equations

• WangDavidson2026.instDecidableEqTheoryClass x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def WangDavidson2026.instReprTheoryClass.repr : TheoryClass → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance WangDavidson2026.instReprTheoryClass : Repr TheoryClass

Equations

• WangDavidson2026.instReprTheoryClass = { reprPrec := WangDavidson2026.instReprTheoryClass.repr }

inductive WangDavidson2026.ExhStrategy : Type

Exhaustification strategy: bivalent (@cite{fox-2007}) or trivalent (@cite{spector-sudo-2017}).

• bivalent : ExhStrategy
• exh1 : ExhStrategy
• exh2 : ExhStrategy

@[implicit_reducible]

instance WangDavidson2026.instDecidableEqExhStrategy : DecidableEq ExhStrategy

Equations

• WangDavidson2026.instDecidableEqExhStrategy x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance WangDavidson2026.instReprExhStrategy : Repr ExhStrategy

Equations

• WangDavidson2026.instReprExhStrategy = { reprPrec := WangDavidson2026.instReprExhStrategy.repr }

def WangDavidson2026.instReprExhStrategy.repr : ExhStrategy → ℕ → Std.Format

Equations

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

inductive WangDavidson2026.ProjectionTheory : Type

Semantic presupposition projection theory.

• strongKleene : ProjectionTheory
• george2008 : ProjectionTheory
• dynamicSemantics : ProjectionTheory

@[implicit_reducible]

instance WangDavidson2026.instDecidableEqProjectionTheory : DecidableEq ProjectionTheory

Equations

• WangDavidson2026.instDecidableEqProjectionTheory x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance WangDavidson2026.instReprProjectionTheory : Repr ProjectionTheory

Equations

• WangDavidson2026.instReprProjectionTheory = { reprPrec := WangDavidson2026.instReprProjectionTheory.repr }

def WangDavidson2026.instReprProjectionTheory.repr : ProjectionTheory → ℕ → Std.Format

Equations

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

def WangDavidson2026.classify (exh : ExhStrategy) (_proj : ProjectionTheory) : TheoryClass

Classify a combination of exhaustification + projection theory into Type A or Type B.

Type A (exclusivity reduces filtering):

• bivalent EXH + any of the three projection theories
• EXH² + any projection theory

Type B (no effect of exclusivity):

• EXH¹ + any projection theory

Equations

• WangDavidson2026.classify WangDavidson2026.ExhStrategy.bivalent _proj = WangDavidson2026.TheoryClass.typeA
• WangDavidson2026.classify WangDavidson2026.ExhStrategy.exh2 _proj = WangDavidson2026.TheoryClass.typeA
• WangDavidson2026.classify WangDavidson2026.ExhStrategy.exh1 _proj = WangDavidson2026.TheoryClass.typeB

theorem WangDavidson2026.exh1_always_typeB (proj : ProjectionTheory) : classify ExhStrategy.exh1 proj = TheoryClass.typeB

EXH¹ is always Type B regardless of projection theory.

theorem WangDavidson2026.bivalent_always_typeA (proj : ProjectionTheory) : classify ExhStrategy.bivalent proj = TheoryClass.typeA

Bivalent EXH is always Type A regardless of projection theory.

theorem WangDavidson2026.exh2_always_typeA (proj : ProjectionTheory) : classify ExhStrategy.exh2 proj = TheoryClass.typeA

EXH² is always Type A regardless of projection theory.

Bivalent EXH strengthens inclusive to exclusive

The bridge from bivalent EXH to the SK prediction:

1. bivalent_exh_yields_xor: Exh(Alt)(p∨q) = p ⊕ q
2. The exclusive truth conditions, when lifted to Truth3 via SK, yield Truth3.xor — which propagates # unconditionally
3. Therefore: bivalent EXH + SK → no filtering (Type A prediction)

This chain depends on the feed-forward assumption (§5): the strengthened exclusive truth conditions must be visible to the projection computation. Without it, projection would see only the original inclusive conditions and filtering would be unaffected.

inductive WangDavidson2026.PQWorld : Type

Four propositional worlds with two atomic propositions.

• pOnly : PQWorld
• qOnly : PQWorld
• both : PQWorld
• neither : PQWorld

@[implicit_reducible]

instance WangDavidson2026.instReprPQWorld : Repr PQWorld

Equations

• WangDavidson2026.instReprPQWorld = { reprPrec := WangDavidson2026.instReprPQWorld.repr }

def WangDavidson2026.instReprPQWorld.repr : PQWorld → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance WangDavidson2026.instDecidableEqPQWorld : DecidableEq PQWorld

Equations

• WangDavidson2026.instDecidableEqPQWorld x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance WangDavidson2026.instFintypePQWorld : Fintype PQWorld

Equations

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

def WangDavidson2026.pProp : PQWorld → Bool

Equations

• WangDavidson2026.pProp WangDavidson2026.PQWorld.pOnly = true
• WangDavidson2026.pProp WangDavidson2026.PQWorld.both = true
• WangDavidson2026.pProp x✝ = false

def WangDavidson2026.qProp : PQWorld → Bool

Equations

• WangDavidson2026.qProp WangDavidson2026.PQWorld.qOnly = true
• WangDavidson2026.qProp WangDavidson2026.PQWorld.both = true
• WangDavidson2026.qProp x✝ = false

def WangDavidson2026.pOrQ : PQWorld → Bool

Equations

• WangDavidson2026.pOrQ WangDavidson2026.PQWorld.neither = false
• WangDavidson2026.pOrQ x✝ = true

def WangDavidson2026.pAndQ : PQWorld → Bool

Equations

• WangDavidson2026.pAndQ WangDavidson2026.PQWorld.both = true
• WangDavidson2026.pAndQ x✝ = false

theorem WangDavidson2026.bivalent_exh_yields_xor : Exhaustification.innocent.exh WangDavidson2026.disjAltsF✝ WangDavidson2026.pOrQF✝ = Exhaustification.predToFinset fun (w : PQWorld) => pOrQ w && !pAndQ w

Bivalent EXH on inclusive disjunction yields exclusive disjunction: exh(p ∨ q) is the set of worlds where exactly one of p, q holds.

theorem WangDavidson2026.bool_xor_lifts_to_sk (a b : Bool) : (Core.Duality.Truth3.ofBool a).xor (Core.Duality.Truth3.ofBool b) = Core.Duality.Truth3.ofBool (a ^^ b)

The classical exclusive disjunction (Bool XOR) agrees with Strong Kleene XOR on defined inputs.

Bathroom disjunction model

"φ or ψ" where ψ presupposes π and ¬φ entails π. We instantiate the generic trivalent EXH¹/EXH² operators on a 3-world toy model that captures the experiment's critical configuration.

inductive WangDavidson2026.BathWorld : Type

Three worlds for the 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

@[implicit_reducible]

instance WangDavidson2026.instReprBathWorld : Repr BathWorld

Equations

• WangDavidson2026.instReprBathWorld = { reprPrec := WangDavidson2026.instReprBathWorld.repr }

def WangDavidson2026.instReprBathWorld.repr : BathWorld → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance WangDavidson2026.instDecidableEqBathWorld : DecidableEq BathWorld

Equations

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

@[implicit_reducible]

instance WangDavidson2026.instFintypeBathWorld : Fintype BathWorld

Equations

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

def WangDavidson2026.pT3 : BathWorld → Core.Duality.Truth3

p: always defined (no presupposition).

Equations

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

def WangDavidson2026.qT3 : BathWorld → Core.Duality.Truth3

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

Equations

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

theorem WangDavidson2026.inclusive_allows_filtering : max (pT3 BathWorld.pOnly) (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 WangDavidson2026.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 WangDavidson2026.inclDisj : BathWorld → Core.Duality.Truth3

Inclusive disjunction as Prop3 (Strong Kleene).

Equations

• WangDavidson2026.inclDisj w = max (WangDavidson2026.pT3 w) (WangDavidson2026.qT3 w)

def WangDavidson2026.exclDisj : BathWorld → Core.Duality.Truth3

Exclusive disjunction as Prop3 (Strong Kleene).

Equations

• WangDavidson2026.exclDisj w = (WangDavidson2026.pT3 w).xor (WangDavidson2026.qT3 w)

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

Inclusive disjunction is defined at pOnly (filtering).

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

Exclusive disjunction is undefined at pOnly (no filtering).

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

Alternative set for the bathroom disjunction: {p∨q, p, q, p∧q}. The conjunction alternative p ∧ q is the only IE alternative (by @cite{fox-2007}).

Equations

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

EXH¹ vs EXH² on the bathroom disjunction

EXH¹ uses weak negation (~# = true), so the conjunction alternative's undefinedness at pOnly is harmlessly "negated": EXH¹ preserves filtering (Type B).

EXH² uses strong negation (~# = #), so the conjunction alternative's undefinedness propagates upward as a new presupposition requirement: EXH² destroys filtering (Type A).

theorem WangDavidson2026.exh1_preserves_filtering : Exhaustification.Trivalent.exh1 bathAlts inclDisj BathWorld.pOnly = Core.Duality.Truth3.true

EXH¹ preserves filtering at the critical world (Type B).

theorem WangDavidson2026.exh2_destroys_filtering : Exhaustification.Trivalent.exh2 bathAlts inclDisj BathWorld.pOnly = Core.Duality.Truth3.indet

EXH² destroys filtering at the critical world (Type A).

inductive WangDavidson2026.Monotonicity : Type

Monotonicity environment, used as between-subjects factor. UE = unembedded disjunction (more exclusive readings); DE = disjunction in conditional antecedent (fewer exclusive readings).

• UE : Monotonicity
• DE : Monotonicity

@[implicit_reducible]

instance WangDavidson2026.instDecidableEqMonotonicity : DecidableEq Monotonicity

Equations

• WangDavidson2026.instDecidableEqMonotonicity x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def WangDavidson2026.instReprMonotonicity.repr : Monotonicity → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance WangDavidson2026.instReprMonotonicity : Repr Monotonicity

Equations

• WangDavidson2026.instReprMonotonicity = { reprPrec := WangDavidson2026.instReprMonotonicity.repr }

inductive WangDavidson2026.Predicate : Type

Predicate type: whether test sentence contains presupposition trigger.

• ps : Predicate
• noPs : Predicate

@[implicit_reducible]

instance WangDavidson2026.instDecidableEqPredicate : DecidableEq Predicate

Equations

• WangDavidson2026.instDecidableEqPredicate x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance WangDavidson2026.instReprPredicate : Repr Predicate

Equations

• WangDavidson2026.instReprPredicate = { reprPrec := WangDavidson2026.instReprPredicate.repr }

def WangDavidson2026.instReprPredicate.repr : Predicate → ℕ → Std.Format

Equations

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

inductive WangDavidson2026.Order : Type

Order of trigger in disjunction.

• first : Order
• second : Order

@[implicit_reducible]

instance WangDavidson2026.instDecidableEqOrder : DecidableEq Order

Equations

• WangDavidson2026.instDecidableEqOrder x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance WangDavidson2026.instReprOrder : Repr Order

Equations

• WangDavidson2026.instReprOrder = { reprPrec := WangDavidson2026.instReprOrder.repr }

def WangDavidson2026.instReprOrder.repr : Order → ℕ → Std.Format

Equations

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

inductive WangDavidson2026.Trigger : Type

Presupposition triggers used in the experiment.

• jie : Trigger
• zhidao : Trigger

@[implicit_reducible]

instance WangDavidson2026.instDecidableEqTrigger : DecidableEq Trigger

Equations

• WangDavidson2026.instDecidableEqTrigger x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def WangDavidson2026.instReprTrigger.repr : Trigger → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance WangDavidson2026.instReprTrigger : Repr Trigger

Equations

• WangDavidson2026.instReprTrigger = { reprPrec := WangDavidson2026.instReprTrigger.repr }

structure WangDavidson2026.Finding : Type

Experimental finding summary.

• description : String
• significant : Bool

def WangDavidson2026.normingValidation : Finding

Norming task validation: the monotonicity manipulation successfully modulates exclusivity (Fisher's exact test, p = .011). UE: 23.3% exclusive responses; DE: 0% exclusive responses.

Equations

• WangDavidson2026.normingValidation = { description := "Norming task: exclusive responses UE 23.3% vs DE 0%, p = .011", significant := true }

def WangDavidson2026.mainResult : Finding

The critical null result: PREDICATE × MONOTONICITY is not significant. p = .30 (frequentist), BF₁₀ = 0.52 (Bayesian). No evidence that exclusivity modulates filtering.

Equations

• WangDavidson2026.mainResult = { description := "PREDICATE × MONOTONICITY interaction: p = .30, BF₁₀ = 0.52", significant := false }

def WangDavidson2026.controlValidation : Finding

Control validation: the paradigm detects presuppositional definedness costs. CONTEXT manipulation is significant (p < .001).

Equations

• WangDavidson2026.controlValidation = { description := "CONTEXT (EI vs S) main effect: p < .001", significant := true }

def WangDavidson2026.jieAsymmetry : Finding

jie shows asymmetric filtering: PREDICATE × ORDER is significant (β = −1.81, SE = 0.72, p = .01). R-to-L filtering is weaker than L-to-R.

Equations

• WangDavidson2026.jieAsymmetry = { description := "jie PREDICATE × ORDER: β = −1.81, SE = 0.72, p = .01", significant := true }

def WangDavidson2026.zhidaoSymmetry : Finding

zhidao shows symmetric filtering: PREDICATE × ORDER is not significant (p = .40), and PREDICATE main effect p = .99 (uniform filtering).

Equations

• WangDavidson2026.zhidaoSymmetry = { description := "zhidao PREDICATE × ORDER: p = .40; PREDICATE: p = .99", significant := false }

theorem WangDavidson2026.norming_validates_manipulation : normingValidation.significant = true

The norming task confirms the manipulation is effective.

theorem WangDavidson2026.null_result_consistent_with_typeB : mainResult.significant = false

The null result is consistent with Type B theories (EXH¹).

theorem WangDavidson2026.null_result_challenges_typeA : mainResult.significant = false ∧ classify ExhStrategy.bivalent ProjectionTheory.strongKleene = TheoryClass.typeA ∧ classify ExhStrategy.bivalent ProjectionTheory.george2008 = TheoryClass.typeA ∧ classify ExhStrategy.bivalent ProjectionTheory.dynamicSemantics = TheoryClass.typeA ∧ classify ExhStrategy.exh2 ProjectionTheory.strongKleene = TheoryClass.typeA

The null result challenges all Type A theories: three bivalent EXH + projection combinations and EXH² + any.

theorem WangDavidson2026.end_to_end_bivalent_sk_challenged : (Exhaustification.innocent.exh WangDavidson2026.disjAltsF✝ WangDavidson2026.pOrQF✝ = Exhaustification.predToFinset fun (w : PQWorld) => pOrQ w && !pAndQ w) ∧ Core.Duality.Truth3.true.xor Core.Duality.Truth3.indet = Core.Duality.Truth3.indet ∧ classify ExhStrategy.bivalent ProjectionTheory.strongKleene = TheoryClass.typeA ∧ mainResult.significant = false

End-to-end argumentation chain: Fox 2007 computes exclusive truth conditions → SK propagates undefinedness → Type A predicted → experiment finds no effect → challenges bivalent EXH + SK.

This links bivalent_exh_yields_xor, Truth3.xor_indet_iff, the Type A classification, and the null experimental result.