Yagi (2025): Conflicting Presuppositions in Disjunction

This file formalizes Yagi's survey of disjunctions whose disjuncts carry contradictory presuppositions (Conflict), Either the King of Buganda is opening parliament or the President of Buganda is conducting the ceremony. Such a disjunction presupposes the disjunction of the two presuppositions and is false when that holds and both disjuncts are false. Four theories fail the second observation. Under Strong Kleene disjunction the sentence is true whenever defined, so it is never false and its negation never true (sup_ne_neg_one, neg_sup_ne_one); the symmetric two-dimensional disjunction in the tradition of Karttunen and Peters has a presupposition that entails the assertion (orKPSymmetric_ne_neg_one), and replacing it by the disjunction of the presuppositions (orPresupOr) fixes the case but predicts a tautologous presupposition for either baldness is not hereditary or all of Bill's children are bald (orPresupOr_notAtIssue_of_left); the update semantics of Heim and Beaver, with failure as a designated state, is defined only when the first disjunct already holds throughout the input, so it is uninformative wherever defined (mem_disj_iff); and Schlenker's local contexts admit only worlds where one disjunct is true (local_contexts_force_truth). Of the two reactions, Beaver and Krahmer's meta-assertion operator makes the disjunction false, but also where neither presupposition holds, and leaves it presuppositionless (joinWeak_ofProp_eq_one_eq_neg_one_iff, joinWeak_ofProp_eq_one_ne_zero); inserting it on one disjunct under Strong Kleene yields only a conditional presupposition (sup_ofProp_eq_one_ne_zero_iff).

Flexible accommodation evaluates each disjunct in the input restricted by an accommodated proposition (flex). The standard update is the case where the second disjunct's proposition is the negation of the first (flex_univ_eq_disj), which gives the conditional presupposition of Either Bill has no child or all of Bill's children are bald (admits_flex_univ_iff, bill). With tautologies accommodated the update is never defined under conflict (not_admits_flex_univ_univ) and is not genuine when a presupposition contradicts the other disjunct (not_genuine_flex_univ_univ); accommodating each disjunct's negated rival presupposition derives both observations (mem_flex_rival_iff, neg_flex_rival, buganda), at the cost of demanding accommodation where the standard update filters the presupposition away (exists_admits_disj_not_admits_flex_univ_univ).

Implementation notes

The disjunctions in the tradition of Karttunen and Peters read a disjunct's at-issue content where its presupposition fails, so they are two-dimensional meanings (ConventionalImplicature.TwoDim), evaluated by TwoDim.toTrivalent; the other theories take trivalent propositions. The designated undefined state of the update semantics is the undefined value of Part, the updates being the substrate's partial context change potentials of trivalent propositions. The meta-assertion operator is Bochvar's assertion operator applied pointwise, fun w ↦ SignType.ofProp (φ w = 1). The licensing constraint on the operator is not modelled. The paper's examples are the rows of Data.Examples.Yagi2025; (1c) and (4) are modelled by the Buganda input and (15a) by the Bill input.

References

• [Yag25]
• [Bea01]
• [BK01]
• [Geu05]
• [Hei82a]
• [KP79]
• [KS12]
• [Sch09a]
• [Zim00]

def Yagi2025.Conflict {W : Type u_1} (φ ψ : W → SignType) : Prop

Two trivalent propositions have conflicting presuppositions when at every world one of them is undefined.

Equations

• Yagi2025.Conflict φ ψ = ∀ (w : W), φ w = 0 ∨ ψ w = 0

Strong Kleene and two-dimensional disjunction

theorem Yagi2025.sup_ne_neg_one {W : Type u_1} {φ ψ : W → SignType} (h : Conflict φ ψ) (w : W) : (φ ⊔ ψ) w ≠ -1

Under conflict the Strong Kleene disjunction is never false, its presupposition entailing its assertion.

theorem Yagi2025.neg_sup_ne_one {W : Type u_1} {φ ψ : W → SignType} (h : Conflict φ ψ) (w : W) : (-(φ ⊔ ψ)) w ≠ 1

Its negation is never true.

theorem Yagi2025.orKPSymmetric_ne_neg_one {W : Type u_1} {p q : ConventionalImplicature.TwoDim W (W → Prop)} (h : Conflict p.toTrivalent q.toTrivalent) (w : W) : (p.orKPSymmetric q).toTrivalent w ≠ -1

The symmetric two-dimensional disjunction is never false either.

def Yagi2025.orPresupOr {W : Type u_1} (p q : ConventionalImplicature.TwoDim W (W → Prop)) : ConventionalImplicature.TwoDim W (W → Prop)

The two-dimensional disjunction whose presupposition is the disjunction of the presuppositions, (7).

Equations

• Yagi2025.orPresupOr p q = { atIssue := fun (w : W) => p.atIssue w ∨ q.atIssue w, notAtIssue := fun (w : W) => p.notAtIssue w ∨ q.notAtIssue w }

theorem Yagi2025.orPresupOr_toTrivalent_eq_neg_one_iff {W : Type u_1} {p q : ConventionalImplicature.TwoDim W (W → Prop)} (w : W) : (orPresupOr p q).toTrivalent w = -1 ↔ (p.notAtIssue w ∨ q.notAtIssue w) ∧ ¬p.atIssue w ∧ ¬q.atIssue w

It is false exactly where a presupposition holds and both assertions fail.

theorem Yagi2025.orPresupOr_notAtIssue_of_left {W : Type u_1} {p q : ConventionalImplicature.TwoDim W (W → Prop)} (h : ∀ (w : W), p.notAtIssue w) (w : W) : (orPresupOr p q).notAtIssue w

With a presuppositionless first disjunct it presupposes nothing, (8).

Update semantics with a designated undefined state

theorem Yagi2025.mem_disj_iff {W : Type u_1} {φ ψ : W → SignType} (h : Conflict φ ψ) (s t : Set W) : t ∈ (DynamicSemantics.CCP.Partial.ofTrivalent φ).disj (DynamicSemantics.CCP.Partial.ofTrivalent ψ) s ↔ (∀ w ∈ s, φ w = 1) ∧ t = s

Under conflict the update by the disjunction is defined only when the first disjunct already holds throughout the input, and then it returns the input, so it is defined only if uninformative.

Local contexts

theorem Yagi2025.local_contexts_force_truth {W : Type u_1} {φ ψ : W → SignType} (h : Conflict φ ψ) (s : Set W) (h₁ : ∀ w ∈ s, φ w ≠ 1 → ψ w ≠ 0) (h₂ : ∀ w ∈ s, ψ w ≠ 1 → φ w ≠ 0) (w : W) : w ∈ s → φ w = 1 ∨ ψ w = 1

If each disjunct's presupposition is entailed by its local context, the negation of the other disjunct within the global context, then under conflict every world of the global context makes some disjunct true.

The meta-assertion operator

theorem Yagi2025.joinWeak_ofProp_eq_one_ne_zero {W : Type u_1} {φ ψ : W → SignType} (w : W) : (SignType.ofProp (φ w = 1)).joinWeak (SignType.ofProp (ψ w = 1)) ≠ 0

The disjunction of two meta-asserted disjuncts has no presupposition.

theorem Yagi2025.joinWeak_ofProp_eq_one_eq_neg_one_iff {W : Type u_1} {φ ψ : W → SignType} (w : W) : (SignType.ofProp (φ w = 1)).joinWeak (SignType.ofProp (ψ w = 1)) = -1 ↔ φ w ≠ 1 ∧ ψ w ≠ 1

It is false whenever neither disjunct is true, so also where neither presupposition holds.

theorem Yagi2025.sup_ofProp_eq_one_ne_zero_iff {W : Type u_1} {φ ψ : W → SignType} (w : W) : max (φ w) (SignType.ofProp (ψ w = 1)) ≠ 0 ↔ ψ w ≠ 1 → φ w ≠ 0

Meta-asserting one disjunct under Strong Kleene yields the conditional presupposition that the first presupposition holds unless the second disjunct is true.

Flexible accommodation

def Yagi2025.flex {W : Type u_1} (χ ω : Set W) (φ ψ : DynamicSemantics.CCP.Partial W) : DynamicSemantics.CCP.Partial W

Under flexible accommodation, (13), each disjunct updates the input restricted by its accommodated proposition, and the results join.

Equations

• Yagi2025.flex χ ω φ ψ s = (φ (s ∩ χ)).bind fun (a : Set W) => Part.map (fun (x : Set W) => a ∪ x) (ψ (s ∩ ω))

theorem Yagi2025.gapExt_union_gapExt_of_conflict {W : Type u_1} {φ ψ : W → SignType} (h : Conflict φ ψ) : Trivalent.gapExt ψ ∪ Trivalent.gapExt φ = Set.univ

(13) requires that the accommodated propositions cover the input. Under conflict each disjunct's negated rival presupposition covers every input.

def Yagi2025.Genuine {W : Type u_1} (u φ ψ : DynamicSemantics.CCP.Partial W) (s : Set W) : Prop

Genuineness, Definition 8, requires each disjunct to be true at some world of the input that survives the update.

Equations

• Yagi2025.Genuine u φ ψ s = ((∃ w ∈ s, {w} ∈ φ {w} ∧ ∃ t ∈ u s, w ∈ t) ∧ ∃ w ∈ s, {w} ∈ ψ {w} ∧ ∃ t ∈ u s, w ∈ t)

theorem Yagi2025.flex_univ_eq_disj {W : Type u_1} {φ : W → SignType} (ψ : DynamicSemantics.CCP.Partial W) : flex Set.univ (Trivalent.posExt φ)ᶜ (DynamicSemantics.CCP.Partial.ofTrivalent φ) ψ = (DynamicSemantics.CCP.Partial.ofTrivalent φ).disj ψ

The standard update is flexible accommodation of the negation of the first disjunct for the second.

theorem Yagi2025.admits_flex_univ_iff {W : Type u_1} {φ ψ : W → SignType} (s : Set W) : DynamicSemantics.PartialUpdate.Admits (flex Set.univ (Trivalent.posExt φ)ᶜ (DynamicSemantics.CCP.Partial.ofTrivalent φ) (DynamicSemantics.CCP.Partial.ofTrivalent ψ)) s ↔ ∀ w ∈ s, φ w ≠ 0 ∧ (φ w ≠ 1 → ψ w ≠ 0)

Accommodating the negation of the first disjunct for the second, (15), the update presupposes the first presupposition and, where the first disjunct fails, the second. This is the conditional presupposition Katzir and Singh observe, fn. 6.

theorem Yagi2025.mem_flex_univ_univ_iff {W : Type u_1} {φ ψ : W → SignType} (s t : Set W) : t ∈ flex Set.univ Set.univ (DynamicSemantics.CCP.Partial.ofTrivalent φ) (DynamicSemantics.CCP.Partial.ofTrivalent ψ) s ↔ (∀ w ∈ s, φ w ≠ 0) ∧ (∀ w ∈ s, ψ w ≠ 0) ∧ t = {w : W | w ∈ s ∧ φ w = 1} ∪ {w : W | w ∈ s ∧ ψ w = 1}

With tautologies accommodated the update is defined exactly when both presuppositions hold throughout, and returns the worlds verifying either disjunct.

theorem Yagi2025.not_admits_flex_univ_univ {W : Type u_1} {φ ψ : W → SignType} (h : Conflict φ ψ) {s : Set W} (hs : s.Nonempty) : ¬DynamicSemantics.PartialUpdate.Admits (flex Set.univ Set.univ (DynamicSemantics.CCP.Partial.ofTrivalent φ) (DynamicSemantics.CCP.Partial.ofTrivalent ψ)) s

Under conflict that update is never defined on a nonempty input, (16).

theorem Yagi2025.not_genuine_flex_univ_univ {W : Type u_1} {φ ψ : W → SignType} (h : ∀ (w : W), φ w = 1 → ψ w = 0) (s : Set W) : ¬Genuine (flex Set.univ Set.univ (DynamicSemantics.CCP.Partial.ofTrivalent φ) (DynamicSemantics.CCP.Partial.ofTrivalent ψ)) (DynamicSemantics.CCP.Partial.ofTrivalent φ) (DynamicSemantics.CCP.Partial.ofTrivalent ψ) s

When the first disjunct contradicts the second presupposition, (15), the update with tautologies accommodated is not genuine, since where defined it presupposes the second presupposition throughout, which leaves the first disjunct no world.

theorem Yagi2025.mem_flex_rival_iff {W : Type u_1} {φ ψ : W → SignType} (h : Conflict φ ψ) (s t : Set W) : t ∈ flex (Trivalent.gapExt ψ) (Trivalent.gapExt φ) (DynamicSemantics.CCP.Partial.ofTrivalent φ) (DynamicSemantics.CCP.Partial.ofTrivalent ψ) s ↔ (∀ w ∈ s, φ w ≠ 0 ∨ ψ w ≠ 0) ∧ t = {w : W | w ∈ s ∧ (φ w = 1 ∨ ψ w = 1)}

Accommodating each disjunct's negated rival presupposition, (17), the update is defined exactly when some presupposition holds at every world of the input, and returns the worlds where a disjunct is true.

theorem Yagi2025.neg_flex_rival {W : Type u_1} {φ ψ : W → SignType} (h : Conflict φ ψ) {s : Set W} (hs : ∀ w ∈ s, φ w ≠ 0 ∨ ψ w ≠ 0) : (flex (Trivalent.gapExt ψ) (Trivalent.gapExt φ) (DynamicSemantics.CCP.Partial.ofTrivalent φ) (DynamicSemantics.CCP.Partial.ofTrivalent ψ)).neg s = Part.some {w : W | w ∈ s ∧ φ w ≠ 1 ∧ ψ w ≠ 1}

The negation of that update removes exactly the worlds where both disjuncts are true, so the disjunction can be false.

theorem Yagi2025.exists_admits_disj_not_admits_flex_univ_univ {W : Type u_1} {φ ψ : W → SignType} (hφ : ∀ (w : W), φ w ≠ 0) (hf : ∀ (w : W), φ w ≠ 1 → ψ w ≠ 0) {w : W} (hq : ψ w = 0) : DynamicSemantics.PartialUpdate.Admits ((DynamicSemantics.CCP.Partial.ofTrivalent φ).disj (DynamicSemantics.CCP.Partial.ofTrivalent ψ)) {w} ∧ ¬DynamicSemantics.PartialUpdate.Admits (flex Set.univ Set.univ (DynamicSemantics.CCP.Partial.ofTrivalent φ) (DynamicSemantics.CCP.Partial.ofTrivalent ψ)) {w}

The standard update filters a presupposition entailed by the negation of the first disjunct, (18), where accommodating tautologies still demands it, at a world where the first disjunct holds and the second presupposition fails.

The ideal inputs

@[reducible, inline]

abbrev Yagi2025.Buganda : Type

The Buganda input of (1c) has four worlds, in which the king opens parliament, the king does not open it, the president conducts the ceremony, and the president does not conduct it.

Equations

• Yagi2025.Buganda = Fin 4

noncomputable def Yagi2025.kingOpens : Buganda → SignType

The King of Buganda is opening parliament.

Equations

• Yagi2025.kingOpens = {w : Yagi2025.Buganda | w < 2}.indicator fun (w : Yagi2025.Buganda) => SignType.ofProp (w = 0)

noncomputable def Yagi2025.presidentConducts : Buganda → SignType

The President of Buganda is conducting the ceremony.

Equations

• Yagi2025.presidentConducts = {w : Yagi2025.Buganda | 2 ≤ w}.indicator fun (w : Yagi2025.Buganda) => SignType.ofProp (w = 2)

theorem Yagi2025.conflict_buganda : Conflict kingOpens presidentConducts

theorem Yagi2025.buganda : flex (Trivalent.gapExt presidentConducts) (Trivalent.gapExt kingOpens) (DynamicSemantics.CCP.Partial.ofTrivalent kingOpens) (DynamicSemantics.CCP.Partial.ofTrivalent presidentConducts) Set.univ = Part.some {0, 2} ∧ (flex (Trivalent.gapExt presidentConducts) (Trivalent.gapExt kingOpens) (DynamicSemantics.CCP.Partial.ofTrivalent kingOpens) (DynamicSemantics.CCP.Partial.ofTrivalent presidentConducts)).neg Set.univ = Part.some {1, 3}

On the Buganda input the update with the rival presuppositions accommodated keeps the worlds where the head of state performs the duty, and its negation, (4), the others.

@[reducible, inline]

abbrev Yagi2025.Bill : Type

The Bill input of (15a) has three worlds, in which Bill has no child, has children who are all bald, or has children who are not all bald.

Equations

• Yagi2025.Bill = Fin 3

def Yagi2025.noChild : Bill → SignType

Bill has no child.

Equations

• Yagi2025.noChild w = SignType.ofProp (w = 0)

noncomputable def Yagi2025.allBald : Bill → SignType

All of Bill's children are bald, presupposing that Bill has children.

Equations

• Yagi2025.allBald = {w : Yagi2025.Bill | w ≠ 0}.indicator fun (w : Yagi2025.Bill) => SignType.ofProp (w = 1)

theorem Yagi2025.bill : ¬DynamicSemantics.PartialUpdate.Admits (flex Set.univ Set.univ (DynamicSemantics.CCP.Partial.ofTrivalent noChild) (DynamicSemantics.CCP.Partial.ofTrivalent allBald)) Set.univ ∧ {0, 1} ∈ flex Set.univ (Trivalent.posExt noChild)ᶜ (DynamicSemantics.CCP.Partial.ofTrivalent noChild) (DynamicSemantics.CCP.Partial.ofTrivalent allBald) Set.univ ∧ Genuine (flex Set.univ (Trivalent.posExt noChild)ᶜ (DynamicSemantics.CCP.Partial.ofTrivalent noChild) (DynamicSemantics.CCP.Partial.ofTrivalent allBald)) (DynamicSemantics.CCP.Partial.ofTrivalent noChild) (DynamicSemantics.CCP.Partial.ofTrivalent allBald) Set.univ

On the Bill input the update with tautologies accommodated is undefined, while accommodating the negation of the first disjunct for the second, (15), is defined and genuine, keeping the worlds where Bill has no child or his children are all bald.