Wang & Davidson (2026): Presupposition Filtering in Disjunction

Wang and Davidson survey what fully semantic implementations of exclusive disjunction predict for presupposition projection. Under Strong Kleene an inclusive disjunction is true when one disjunct is, whatever the other, so a true disjunct filters the other's presupposition, whereas an exclusive disjunction is undefined whenever a disjunct is (Filters, not_filters_xor). Fox's bivalent exhaustification strengthens a disjunction to its exclusive reading (exh_or), so once the strengthened truth conditions feed the projection computation three projection theories agree that an exclusive disjunction projects uniformly: Strong Kleene, as Mayr and Romoli apply it; George's algorithm, rendered as george over any classical connective, which agrees with Strong Kleene on inclusive and exclusive disjunction (george_or, george_xor) while filtering conjunction only from left to right; and dynamic semantics, where each of the eight context change potentials that Rothschild's restrictions allow for exclusive disjunction is admitted only by a context satisfying both presuppositions (xorCCPs_admits). Spector and Sudo's trivalent exhaustifiers split: weak-negation EXH¹ is undefined exactly where its prejacent is, so it leaves projection alone, while strong-negation EXH² is undefined wherever an innocently excludable alternative is, and for a disjunction the conjunction alternative's presupposition together with the disjunction's is both disjuncts' (sup_inf_ne_zero_iff). The theories predicting that more exclusive readings mean less filtering are the paper's Type A; the paper's Mandarin experiment on huozhe finds no such effect.

Implementation notes

Strong Kleene exclusive disjunction is -(a * b), since multiplication on SignType is the Strong Kleene biconditional. The exhaustification identity is checked on the four valuations of two atoms, the free model of a propositional identity. George's algorithm is stated as the paper renders it, on the set of classical values a trivalent argument leaves open. The experiment's ratings are not formalized; its stimuli are in Data.Examples.WangDavidson2026.

References

• [WD26]
• [Fox07]
• [Geo08]
• [KS24]
• [MR16a]
• [Rot11]
• [SS17]

Filtering by a trivalent connective

def WangDavidson2026.FiltersLR (f : SignType → SignType → SignType) : Prop

A trivalent connective filters from left to right when a defined left argument can make the whole defined with an undefined right argument.

Equations

• WangDavidson2026.FiltersLR f = ∃ (a : SignType), f a 0 ≠ 0

def WangDavidson2026.FiltersRL (f : SignType → SignType → SignType) : Prop

Filtering from right to left.

Equations

• WangDavidson2026.FiltersRL f = ∃ (b : SignType), f 0 b ≠ 0

def WangDavidson2026.Filters (f : SignType → SignType → SignType) : Prop

A connective filters when it does so in either direction.

Equations

• WangDavidson2026.Filters f = (WangDavidson2026.FiltersLR f ∨ WangDavidson2026.FiltersRL f)

theorem WangDavidson2026.filtersLR_sup : FiltersLR fun (x1 x2 : SignType) => max x1 x2

Strong Kleene inclusive disjunction filters in both directions (Table 1).

theorem WangDavidson2026.filtersRL_sup : FiltersRL fun (x1 x2 : SignType) => max x1 x2

theorem WangDavidson2026.not_filters_xor : ¬Filters fun (a b : SignType) => -(a * b)

Strong Kleene exclusive disjunction never filters (Table 2).

Bivalent exhaustification yields exclusive disjunction

@[reducible, inline]

abbrev WangDavidson2026.Val : Type

The valuations of two atoms.

Equations

• WangDavidson2026.Val = (Bool × Bool)

def WangDavidson2026.orAlts : Finset (Finset Val)

The alternatives of p ∨ q are p, q and p ∧ q (3a).

Equations

• WangDavidson2026.orAlts = Exhaustification.altsFromPreds [fun (v : WangDavidson2026.Val) => v.1 || v.2, Prod.fst, Prod.snd, fun (v : WangDavidson2026.Val) => v.1 && v.2]

theorem WangDavidson2026.excluded_or : Exhaustification.innocent.excluded orAlts (Exhaustification.predToFinset fun (v : Val) => v.1 || v.2) = {Exhaustification.predToFinset fun (v : Val) => v.1 && v.2}

Only the conjunction is innocently excludable (3b).

theorem WangDavidson2026.exh_or : Exhaustification.innocent.exh orAlts (Exhaustification.predToFinset fun (v : Val) => v.1 || v.2) = Exhaustification.predToFinset fun (v : Val) => v.1 ^^ v.2

Bivalent exhaustification of p ∨ q is p xor q (3c).

George's algorithm

def WangDavidson2026.values : SignType → Finset Bool

The classical values a trivalent value leaves open.

Equations

• WangDavidson2026.values SignType.pos = {true}
• WangDavidson2026.values SignType.neg = {false}
• WangDavidson2026.values SignType.zero = Finset.univ

def WangDavidson2026.george (f : Bool → Bool → Bool) (a b : SignType) : SignType

[Geo08]'s algorithm computes the trivalent table of a classical connective, as [KS24] render it. If the left argument settles the value, that is the value; otherwise, if some value of the right argument could make the sentence true, the two arguments settle the value or the sentence is undefined; otherwise it is undefined.

Equations

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

theorem WangDavidson2026.george_or : (george fun (x1 x2 : Bool) => x1 || x2) = fun (x1 x2 : SignType) => max x1 x2

On inclusive disjunction George's algorithm is Strong Kleene.

theorem WangDavidson2026.george_xor : (george fun (x1 x2 : Bool) => x1 ^^ x2) = fun (a b : SignType) => -(a * b)

On exclusive disjunction George's algorithm is Strong Kleene too.

theorem WangDavidson2026.filtersLR_george_and : FiltersLR (george fun (x1 x2 : Bool) => x1 && x2)

George's algorithm filters conjunction from left to right only.

theorem WangDavidson2026.not_filtersRL_george_and : ¬FiltersRL (george fun (x1 x2 : Bool) => x1 && x2)

theorem WangDavidson2026.not_filters_george_xor : ¬Filters (george fun (x1 x2 : Bool) => x1 ^^ x2)

Dynamic semantics

def WangDavidson2026.lit {W : Type u_1} : Bool → (W → SignType) → DynamicSemantics.CCP.Partial W

Update with a proposition or with its negation.

Equations

• WangDavidson2026.lit true x✝ = DynamicSemantics.CCP.Partial.ofTrivalent x✝
• WangDavidson2026.lit false x✝ = (DynamicSemantics.CCP.Partial.ofTrivalent x✝).neg

def WangDavidson2026.chain {W : Type u_1} (b₁ : Bool) (p : W → SignType) (b₂ : Bool) (q : W → SignType) : DynamicSemantics.CCP.Partial W

The context C[p][q], for p and q propositions or their negations.

Equations

• WangDavidson2026.chain b₁ p b₂ q = DynamicSemantics.PartialUpdate.seq (WangDavidson2026.lit b₁ p) (WangDavidson2026.lit b₂ q)

def WangDavidson2026.union {W : Type u_1} (φ ψ : DynamicSemantics.CCP.Partial W) : DynamicSemantics.CCP.Partial W

The union of two updates, defined when both are.

Equations

• WangDavidson2026.union φ ψ s = { Dom := (φ s).Dom ∧ (ψ s).Dom, get := fun (h : (φ s).Dom ∧ (ψ s).Dom) => (φ s).get ⋯ ∪ (ψ s).get ⋯ }

def WangDavidson2026.diff {W : Type u_1} (φ ψ : DynamicSemantics.CCP.Partial W) : DynamicSemantics.CCP.Partial W

The context minus two updates, defined when both are.

Equations

• WangDavidson2026.diff φ ψ s = { Dom := (φ s).Dom ∧ (ψ s).Dom, get := fun (h : (φ s).Dom ∧ (ψ s).Dom) => (s \ (φ s).get ⋯) \ (ψ s).get ⋯ }

def WangDavidson2026.xorCCPs {W : Type u_1} (α β : W → SignType) : List (DynamicSemantics.CCP.Partial W)

The eight context change potentials for α xor β (Table 3).

Equations

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

theorem WangDavidson2026.subset_support_of_split {W : Type u_1} (α β : W → SignType) {s : Set W} (h₁ : {w : W | w ∈ s ∧ α w = 1} ⊆ Function.support β) (h₂ : s \ {w : W | w ∈ s ∧ α w = 1} ⊆ Function.support β) : s ⊆ Function.support β

A presupposition satisfied on C[α] and on C[¬α] is satisfied on C.

theorem WangDavidson2026.xorCCPs_admits {W : Type u_1} (α β : W → SignType) {s : Set W} (u : DynamicSemantics.CCP.Partial W) : u ∈ xorCCPs α β → DynamicSemantics.PartialUpdate.Admits u s → s ⊆ Function.support α ∧ s ⊆ Function.support β

Every context change potential for exclusive disjunction is admitted only by a context satisfying both presuppositions, so exclusive disjunction does not filter.

theorem WangDavidson2026.exists_disj_admits_not_admits : ∃ (α : Bool → SignType) (β : Bool → SignType), DynamicSemantics.PartialUpdate.Admits ((DynamicSemantics.CCP.Partial.ofTrivalent α).disj (DynamicSemantics.CCP.Partial.ofTrivalent β)) Set.univ ∧ ¬Set.univ ⊆ Function.support β

Inclusive dynamic disjunction, by contrast, filters, since a context can admit α ∨ β without satisfying β's presupposition.

Trivalent exhaustification

theorem WangDavidson2026.sup_inf_ne_zero_iff (a b : SignType) : max a b ≠ 0 ∧ min a b ≠ 0 ↔ a ≠ 0 ∧ b ≠ 0

The presupposition of α ∨ β together with that of α ∧ β is that of both disjuncts under Strong Kleene (8), so EXH², which imports the conjunction alternative's presupposition, makes an exhaustified disjunction project uniformly.

def WangDavidson2026.bathLeft : Val → SignType

A bathroom disjunction on the valuations of two atoms — bathLeft is always defined and bathRight presupposes its negation.

Equations

• WangDavidson2026.bathLeft v = SignType.ofProp (v.1 = true)

def WangDavidson2026.bathRight : Val → SignType

Equations

• WangDavidson2026.bathRight v = if v.1 = true then 0 else SignType.ofProp (v.2 = true)

def WangDavidson2026.bathAlts : List (Val → SignType)

The alternatives of the bathroom disjunction.

Equations

• WangDavidson2026.bathAlts = [WangDavidson2026.bathLeft, WangDavidson2026.bathRight, fun (v : WangDavidson2026.Val) => min (WangDavidson2026.bathLeft v) (WangDavidson2026.bathRight v)]

def WangDavidson2026.bathOr : Val → SignType

The inclusive bathroom disjunction.

Equations

• WangDavidson2026.bathOr v = max (WangDavidson2026.bathLeft v) (WangDavidson2026.bathRight v)

theorem WangDavidson2026.exh1_bathOr : Exhaustification.Trivalent.exh1 bathAlts bathOr (true, false) = 1

EXH¹ keeps the filtering — where the left disjunct is true and the right undefined, the exhaustified disjunction is true.

theorem WangDavidson2026.exh2_bathOr : Exhaustification.Trivalent.exh2 bathAlts bathOr (true, false) = 0

EXH² undoes it — the undefined conjunction alternative makes the exhaustified disjunction undefined there.