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 InnocentExclusion.disj_exh_eq_exor shows Exh strengthens ∨ to ⊻, and Truth3.xor_indet_iff shows ⊻ propagates undefinedness unconditionally, exhaustification eliminates filtering.

theorem Phenomena.Presupposition.Studies.WangDavidson2026.sk_inclusive_filters : Core.Duality.Truth3.true.join Core.Duality.Truth3.indet = Core.Duality.Truth3.true

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

theorem Phenomena.Presupposition.Studies.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 Phenomena.Presupposition.Studies.WangDavidson2026.sk_filtering_symmetric : Core.Duality.Truth3.indet.join 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 Phenomena.Presupposition.Studies.WangDavidson2026.prprop_exclusive_no_filter {W : Type u_1} (p q : Core.Presupposition.PrProp W) (w : W) (hq : q.presup w = false) : (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 Phenomena.Presupposition.Studies.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.

instance Phenomena.Presupposition.Studies.WangDavidson2026.instDecidableEqTheoryClass : DecidableEq TheoryClass

Equations

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

def Phenomena.Presupposition.Studies.WangDavidson2026.instReprTheoryClass.repr : TheoryClass → ℕ → Std.Format

Equations

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

instance Phenomena.Presupposition.Studies.WangDavidson2026.instReprTheoryClass : Repr TheoryClass

Equations

• Phenomena.Presupposition.Studies.WangDavidson2026.instReprTheoryClass = { reprPrec := Phenomena.Presupposition.Studies.WangDavidson2026.instReprTheoryClass.repr }

instance Phenomena.Presupposition.Studies.WangDavidson2026.instBEqTheoryClass : BEq TheoryClass

Equations

• Phenomena.Presupposition.Studies.WangDavidson2026.instBEqTheoryClass = { beq := Phenomena.Presupposition.Studies.WangDavidson2026.instBEqTheoryClass.beq }

def Phenomena.Presupposition.Studies.WangDavidson2026.instBEqTheoryClass.beq : TheoryClass → TheoryClass → Bool

Equations

• Phenomena.Presupposition.Studies.WangDavidson2026.instBEqTheoryClass.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

inductive Phenomena.Presupposition.Studies.WangDavidson2026.ExhStrategy : Type

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

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

instance Phenomena.Presupposition.Studies.WangDavidson2026.instDecidableEqExhStrategy : DecidableEq ExhStrategy

Equations

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

def Phenomena.Presupposition.Studies.WangDavidson2026.instReprExhStrategy.repr : ExhStrategy → ℕ → Std.Format

Equations

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

instance Phenomena.Presupposition.Studies.WangDavidson2026.instReprExhStrategy : Repr ExhStrategy

Equations

• Phenomena.Presupposition.Studies.WangDavidson2026.instReprExhStrategy = { reprPrec := Phenomena.Presupposition.Studies.WangDavidson2026.instReprExhStrategy.repr }

def Phenomena.Presupposition.Studies.WangDavidson2026.instBEqExhStrategy.beq : ExhStrategy → ExhStrategy → Bool

Equations

• Phenomena.Presupposition.Studies.WangDavidson2026.instBEqExhStrategy.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Presupposition.Studies.WangDavidson2026.instBEqExhStrategy : BEq ExhStrategy

Equations

• Phenomena.Presupposition.Studies.WangDavidson2026.instBEqExhStrategy = { beq := Phenomena.Presupposition.Studies.WangDavidson2026.instBEqExhStrategy.beq }

inductive Phenomena.Presupposition.Studies.WangDavidson2026.ProjectionTheory : Type

Semantic presupposition projection theory.

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

instance Phenomena.Presupposition.Studies.WangDavidson2026.instDecidableEqProjectionTheory : DecidableEq ProjectionTheory

Equations

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

def Phenomena.Presupposition.Studies.WangDavidson2026.instReprProjectionTheory.repr : ProjectionTheory → ℕ → Std.Format

Equations

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

instance Phenomena.Presupposition.Studies.WangDavidson2026.instReprProjectionTheory : Repr ProjectionTheory

Equations

• Phenomena.Presupposition.Studies.WangDavidson2026.instReprProjectionTheory = { reprPrec := Phenomena.Presupposition.Studies.WangDavidson2026.instReprProjectionTheory.repr }

instance Phenomena.Presupposition.Studies.WangDavidson2026.instBEqProjectionTheory : BEq ProjectionTheory

Equations

• Phenomena.Presupposition.Studies.WangDavidson2026.instBEqProjectionTheory = { beq := Phenomena.Presupposition.Studies.WangDavidson2026.instBEqProjectionTheory.beq }

def Phenomena.Presupposition.Studies.WangDavidson2026.instBEqProjectionTheory.beq : ProjectionTheory → ProjectionTheory → Bool

Equations

• Phenomena.Presupposition.Studies.WangDavidson2026.instBEqProjectionTheory.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Phenomena.Presupposition.Studies.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

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

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

EXH¹ is always Type B regardless of projection theory.

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

Bivalent EXH is always Type A regardless of projection theory.

theorem Phenomena.Presupposition.Studies.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. InnocentExclusion.disj_exh_eq_exor: 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.

theorem Phenomena.Presupposition.Studies.WangDavidson2026.bivalent_exh_yields_xor (w : Exhaustification.InnocentExclusion.PQWorld) : Exhaustification.InnocentExclusion.exhB Exhaustification.InnocentExclusion.pqDomain Exhaustification.InnocentExclusion.disjAlts Exhaustification.InnocentExclusion.pOrQ w = (Exhaustification.InnocentExclusion.pOrQ w && !Exhaustification.InnocentExclusion.pAndQ w)

Fox 2007 already proves that bivalent EXH strengthens inclusive to exclusive disjunction (reexported for context).

theorem Phenomena.Presupposition.Studies.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.

Trivalent exhaustification and presupposition inheritance

The bathroom disjunction verification from Trivalent.lean shows:

• EXH¹ preserves filtering at the critical world (pOnly)
• EXH² destroys filtering at the critical world (pOnly)

This drives the Type A/B split. The mechanism:

• EXH¹ uses weak negation (~# = true), so the conjunction alternative's undefinedness at pOnly is harmlessly "negated"
• EXH² uses strong negation (~# = #), so the conjunction alternative's undefinedness propagates upward as a new presupposition requirement

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

Re-export: EXH¹ preserves filtering (Type B).

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

Re-export: EXH² destroys filtering (Type A).

inductive Phenomena.Presupposition.Studies.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

instance Phenomena.Presupposition.Studies.WangDavidson2026.instDecidableEqMonotonicity : DecidableEq Monotonicity

Equations

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

def Phenomena.Presupposition.Studies.WangDavidson2026.instReprMonotonicity.repr : Monotonicity → ℕ → Std.Format

Equations

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

instance Phenomena.Presupposition.Studies.WangDavidson2026.instReprMonotonicity : Repr Monotonicity

Equations

• Phenomena.Presupposition.Studies.WangDavidson2026.instReprMonotonicity = { reprPrec := Phenomena.Presupposition.Studies.WangDavidson2026.instReprMonotonicity.repr }

def Phenomena.Presupposition.Studies.WangDavidson2026.instBEqMonotonicity.beq : Monotonicity → Monotonicity → Bool

Equations

• Phenomena.Presupposition.Studies.WangDavidson2026.instBEqMonotonicity.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Presupposition.Studies.WangDavidson2026.instBEqMonotonicity : BEq Monotonicity

Equations

• Phenomena.Presupposition.Studies.WangDavidson2026.instBEqMonotonicity = { beq := Phenomena.Presupposition.Studies.WangDavidson2026.instBEqMonotonicity.beq }

inductive Phenomena.Presupposition.Studies.WangDavidson2026.Predicate : Type

Predicate type: whether test sentence contains presupposition trigger.

• ps : Predicate
• noPs : Predicate

instance Phenomena.Presupposition.Studies.WangDavidson2026.instDecidableEqPredicate : DecidableEq Predicate

Equations

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

instance Phenomena.Presupposition.Studies.WangDavidson2026.instReprPredicate : Repr Predicate

Equations

• Phenomena.Presupposition.Studies.WangDavidson2026.instReprPredicate = { reprPrec := Phenomena.Presupposition.Studies.WangDavidson2026.instReprPredicate.repr }

def Phenomena.Presupposition.Studies.WangDavidson2026.instReprPredicate.repr : Predicate → ℕ → Std.Format

Equations

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

instance Phenomena.Presupposition.Studies.WangDavidson2026.instBEqPredicate : BEq Predicate

Equations

• Phenomena.Presupposition.Studies.WangDavidson2026.instBEqPredicate = { beq := Phenomena.Presupposition.Studies.WangDavidson2026.instBEqPredicate.beq }

def Phenomena.Presupposition.Studies.WangDavidson2026.instBEqPredicate.beq : Predicate → Predicate → Bool

Equations

• Phenomena.Presupposition.Studies.WangDavidson2026.instBEqPredicate.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

inductive Phenomena.Presupposition.Studies.WangDavidson2026.Order : Type

Order of trigger in disjunction.

• first : Order
• second : Order

instance Phenomena.Presupposition.Studies.WangDavidson2026.instDecidableEqOrder : DecidableEq Order

Equations

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

def Phenomena.Presupposition.Studies.WangDavidson2026.instReprOrder.repr : Order → ℕ → Std.Format

Equations

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

instance Phenomena.Presupposition.Studies.WangDavidson2026.instReprOrder : Repr Order

Equations

• Phenomena.Presupposition.Studies.WangDavidson2026.instReprOrder = { reprPrec := Phenomena.Presupposition.Studies.WangDavidson2026.instReprOrder.repr }

def Phenomena.Presupposition.Studies.WangDavidson2026.instBEqOrder.beq : Order → Order → Bool

Equations

• Phenomena.Presupposition.Studies.WangDavidson2026.instBEqOrder.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Presupposition.Studies.WangDavidson2026.instBEqOrder : BEq Order

Equations

• Phenomena.Presupposition.Studies.WangDavidson2026.instBEqOrder = { beq := Phenomena.Presupposition.Studies.WangDavidson2026.instBEqOrder.beq }

inductive Phenomena.Presupposition.Studies.WangDavidson2026.Trigger : Type

Presupposition triggers used in the experiment.

• jie : Trigger
• zhidao : Trigger

instance Phenomena.Presupposition.Studies.WangDavidson2026.instDecidableEqTrigger : DecidableEq Trigger

Equations

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

def Phenomena.Presupposition.Studies.WangDavidson2026.instReprTrigger.repr : Trigger → ℕ → Std.Format

Equations

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

instance Phenomena.Presupposition.Studies.WangDavidson2026.instReprTrigger : Repr Trigger

Equations

• Phenomena.Presupposition.Studies.WangDavidson2026.instReprTrigger = { reprPrec := Phenomena.Presupposition.Studies.WangDavidson2026.instReprTrigger.repr }

instance Phenomena.Presupposition.Studies.WangDavidson2026.instBEqTrigger : BEq Trigger

Equations

• Phenomena.Presupposition.Studies.WangDavidson2026.instBEqTrigger = { beq := Phenomena.Presupposition.Studies.WangDavidson2026.instBEqTrigger.beq }

def Phenomena.Presupposition.Studies.WangDavidson2026.instBEqTrigger.beq : Trigger → Trigger → Bool

Equations

• Phenomena.Presupposition.Studies.WangDavidson2026.instBEqTrigger.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

structure Phenomena.Presupposition.Studies.WangDavidson2026.Finding : Type

Experimental finding summary.

• description : String
• significant : Bool

def Phenomena.Presupposition.Studies.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

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

def Phenomena.Presupposition.Studies.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

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

def Phenomena.Presupposition.Studies.WangDavidson2026.controlValidation : Finding

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

Equations

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

def Phenomena.Presupposition.Studies.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

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

def Phenomena.Presupposition.Studies.WangDavidson2026.zhidaoSymmetry : Finding

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

Equations

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

theorem Phenomena.Presupposition.Studies.WangDavidson2026.norming_validates_manipulation : normingValidation.significant = true

The norming task confirms the manipulation is effective.

theorem Phenomena.Presupposition.Studies.WangDavidson2026.null_result_consistent_with_typeB : mainResult.significant = false

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

theorem Phenomena.Presupposition.Studies.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 Phenomena.Presupposition.Studies.WangDavidson2026.end_to_end_bivalent_sk_challenged : (∀ (w : Exhaustification.InnocentExclusion.PQWorld), Exhaustification.InnocentExclusion.exhB Exhaustification.InnocentExclusion.pqDomain Exhaustification.InnocentExclusion.disjAlts Exhaustification.InnocentExclusion.pOrQ w = (Exhaustification.InnocentExclusion.pOrQ w && !Exhaustification.InnocentExclusion.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 InnocentExclusion.disj_exh_eq_exor, Truth3.xor_indet_iff, the Type A classification, and the null experimental result.