Conflicting Presuppositions in Disjunction

@cite{yagi-2025}

Squib-replication of @cite{yagi-2025} (S&P 18:7) on disjunctions φ_p ∨ ψ_q with p ∧ q = ⊥. Yagi argues:

(2a) the disjunction presupposes p ∨ q; (2b) it can be false (when both disjuncts are false).

§2 surveys four projection theories — Strong Kleene, two-dimensional @cite{karttunen-peters-1979}, dynamic update (@cite{heim-1982}, @cite{veltman-1996}, @cite{beaver-2001}), and @cite{schlenker-2009}'s local contexts — each failing (2b). §3 considers two reactions: @cite{beaver-krahmer-2001}'s 𝒜-operator (loses presupposition), and @cite{geurts-2005}'s flexible accommodation (captures (2a–b) at the cost of an underspecified accommodation mechanism that interacts oddly with negation, and at the cost of overgenerating non-projection in non-conflicting cases like (18)).

@cite{aloni-2022}'s bilateral state semantics is a substantively different account that also delivers a "split" disjunction; we mention it here because Yagi cites it alongside Geurts as a flexible-accommodation co-developer, but it is formalised separately at Phenomena/Modality/Studies/Aloni2022.lean and not engaged here.

Yagi's example (8) — "Either baldness is not hereditary, or all of Bill's children are bald" (@cite{karttunen-1974}) — appears in §2.2 as a counterexample to the K&P modification Π(φ ∨ ψ) := Π(φ) ∨ Π(ψ) (eq. 7). This formula is exactly what PrProp.orFlex.presup computes. The flexible-accommodation framework Yagi defends in §3.2 evades the eq. (7) problem via the χ = ω = ⊤ accommodation default, which we have not formalised here (we have only the static orFlex connective, not the parametric dynamic update s[χ][φ] ∪ s[ω][ψ] of Yagi's eq. 13).

The §3.2 discussion of how dynamic negation requires genuineness to hold within negation scope ("peculiar, given that we end up negating both disjuncts") motivated the strengthening of PrProp.genuineness from a singleton-survival check (now PrProp.liveness) to the two-conjunct definition with disjunction-update survival.

Connective inventory used

• Truth3.join (Strong Kleene): never false (strong_kleene_never_false)
• PrProp.or (classical): never defined (classical_never_defined)
• PrProp.orFilter (symmetric, positive-antecedent filtering of @cite{kalomoiros-schwarz-2021}): wrong presupposition (filter_wrong_at_kingOpens)
• PrProp.orKP (symmetric, negative-antecedent K&P of Yagi Def 2): presupposition entails assertion (kp_presup_entails_assertion)
• Semantics.Modality.Disjunction.exhaustivity_implies_uninformative: the consequence (not the derivation) of @cite{schlenker-2009} §2.4 via the Geurts-modal-disjunction substrate (truthset_uninformative_geurts_route)
• Prop3.metaAssert: allows falsity, no presupposition (metaAssert_allows_falsity, metaAssert_no_gap)
• PrProp.orFlex = PrProp.orBelnap (substrate identity from Core/Semantics/Presupposition.lean): correct (2a) and (2b), with a discriminating world noHeadOfState to prove the presupposition is non-trivial
• PrProp.orFlex.presup overgenerates trivial-truth in eq. (7) shape: eq7_too_weak_for_ex8 exhibits the empirical mismatch at world noChild
• For example (18), orFlex predicts non-projection only because the left disjunct is presuppositionless (ex18_orFlex_no_projection_via_vacuous_left, ex18_unprincipled_in_right_presup_failure); the principled K1973 asymmetric route (ex18_asymmetric_K1973_principled) goes via PrProp.disjFilterLeft_eliminates_presup_when_neg_entails

World type

@cite{yagi-2025} ex. (1c), after @cite{beaver-2001}: "Either the King of Buganda is now opening parliament or the President of Buganda is conducting the ceremony." A nation has either a king or a president (presuppositions conflict), and the head of state may or may not be performing the relevant ceremonial duty. We add a fifth world noHeadOfState so the disjunctive presupposition p ∨ q is non-trivial — without it, every world would satisfy the expected presupposition and flex_correct_presup would degenerate to True ↔ True.

inductive Yagi2025.W : Type

• kingOpens : W
• kingDoesnt : W
• presidentConducts : W
• presidentDoesnt : W
• noHeadOfState : W

@[implicit_reducible]

instance Yagi2025.instDecidableEqW : DecidableEq W

Equations

• Yagi2025.instDecidableEqW x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Yagi2025.instReprW.repr : W → ℕ → Std.Format

Equations

• Yagi2025.instReprW.repr Yagi2025.W.kingOpens prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Yagi2025.W.kingOpens")).group prec✝
• Yagi2025.instReprW.repr Yagi2025.W.kingDoesnt prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Yagi2025.W.kingDoesnt")).group prec✝
• Yagi2025.instReprW.repr Yagi2025.W.presidentConducts prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Yagi2025.W.presidentConducts")).group prec✝
• Yagi2025.instReprW.repr Yagi2025.W.presidentDoesnt prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Yagi2025.W.presidentDoesnt")).group prec✝
• Yagi2025.instReprW.repr Yagi2025.W.noHeadOfState prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Yagi2025.W.noHeadOfState")).group prec✝

@[implicit_reducible]

instance Yagi2025.instReprW : Repr W

Equations

• Yagi2025.instReprW = { reprPrec := Yagi2025.instReprW.repr }

def Yagi2025.instInhabitedW.default : W

Equations

• Yagi2025.instInhabitedW.default = Yagi2025.W.kingOpens

@[implicit_reducible]

instance Yagi2025.instInhabitedW : Inhabited W

Equations

• Yagi2025.instInhabitedW = { default := Yagi2025.instInhabitedW.default }

@[implicit_reducible]

instance Yagi2025.instFintypeW : Fintype W

Equations

• Yagi2025.instFintypeW = { elems := { val := ↑Yagi2025.W.enumList, nodup := Yagi2025.W.enumList_nodup }, complete := Yagi2025.instFintypeW._proof_1 }

def Yagi2025.hasKing : W → Prop

Presupposition p: the nation has a king.

Equations

• Yagi2025.hasKing Yagi2025.W.kingOpens = True
• Yagi2025.hasKing Yagi2025.W.kingDoesnt = True
• Yagi2025.hasKing x✝ = False

@[implicit_reducible]

instance Yagi2025.instDecidablePredWHasKing : DecidablePred hasKing

Equations

• Yagi2025.instDecidablePredWHasKing Yagi2025.W.kingOpens = isTrue trivial
• Yagi2025.instDecidablePredWHasKing Yagi2025.W.kingDoesnt = isTrue trivial
• Yagi2025.instDecidablePredWHasKing Yagi2025.W.presidentConducts = isFalse Yagi2025.instDecidablePredWHasKing._proof_1
• Yagi2025.instDecidablePredWHasKing Yagi2025.W.presidentDoesnt = isFalse Yagi2025.instDecidablePredWHasKing._proof_2
• Yagi2025.instDecidablePredWHasKing Yagi2025.W.noHeadOfState = isFalse Yagi2025.instDecidablePredWHasKing._proof_3

def Yagi2025.hasPresident : W → Prop

Presupposition q: the nation has a president.

Equations

• Yagi2025.hasPresident Yagi2025.W.presidentConducts = True
• Yagi2025.hasPresident Yagi2025.W.presidentDoesnt = True
• Yagi2025.hasPresident x✝ = False

@[implicit_reducible]

instance Yagi2025.instDecidablePredWHasPresident : DecidablePred hasPresident

Equations

• Yagi2025.instDecidablePredWHasPresident Yagi2025.W.presidentConducts = isTrue trivial
• Yagi2025.instDecidablePredWHasPresident Yagi2025.W.presidentDoesnt = isTrue trivial
• Yagi2025.instDecidablePredWHasPresident Yagi2025.W.kingOpens = isFalse Yagi2025.instDecidablePredWHasPresident._proof_1
• Yagi2025.instDecidablePredWHasPresident Yagi2025.W.kingDoesnt = isFalse Yagi2025.instDecidablePredWHasPresident._proof_2
• Yagi2025.instDecidablePredWHasPresident Yagi2025.W.noHeadOfState = isFalse Yagi2025.instDecidablePredWHasPresident._proof_3

theorem Yagi2025.presups_conflict (w : W) : ¬(hasKing w ∧ hasPresident w)

p ∧ q = ⊥: the presuppositions conflict.

def Yagi2025.kingOpensParl : Core.Presupposition.PrProp W

φ_p: "The King is opening parliament" — presupposes hasKing.

Equations

• Yagi2025.kingOpensParl = { presup := Yagi2025.hasKing, assertion := fun (w : Yagi2025.W) => w = Yagi2025.W.kingOpens }

def Yagi2025.presConductsCeremony : Core.Presupposition.PrProp W

ψ_q: "The President is conducting the ceremony" — presupposes hasPresident.

Equations

• Yagi2025.presConductsCeremony = { presup := Yagi2025.hasPresident, assertion := fun (w : Yagi2025.W) => w = Yagi2025.W.presidentConducts }

Empirical observations

@cite{yagi-2025} (2a–b). Note that (2a) is non-trivial here — the discriminating world noHeadOfState falsifies expectedPresup.

def Yagi2025.expectedPresup : W → Prop

The expected presupposition: the nation has some head of state.

Equations

• Yagi2025.expectedPresup w = (Yagi2025.hasKing w ∨ Yagi2025.hasPresident w)

@[implicit_reducible]

instance Yagi2025.instDecidablePredWExpectedPresup : DecidablePred expectedPresup

Equations

• Yagi2025.instDecidablePredWExpectedPresup w = id inferInstance

theorem Yagi2025.presup_iff_has_head_of_state (w : W) : expectedPresup w ↔ w ≠ W.noHeadOfState

(2a) holds at every world with a head of state. The fifth world noHeadOfState falsifies it — the test is now non-trivial.

theorem Yagi2025.presup_fails_at_no_head : ¬expectedPresup W.noHeadOfState

(2a) is falsified at noHeadOfState.

theorem Yagi2025.can_be_false : expectedPresup W.kingDoesnt ∧ ¬kingOpensParl.assertion W.kingDoesnt ∧ ¬presConductsCeremony.assertion W.kingDoesnt

(2b): the disjunction can be false. At kingDoesnt the presupposition is satisfied but both disjuncts fail.

Failure 1: Strong Kleene (@cite{yagi-2025} §2.1, Definition 1)

noncomputable def Yagi2025.skDisj : Core.Duality.Prop3 W

Strong Kleene disjunction of the two presuppositional propositions.

Equations

• Yagi2025.skDisj = Yagi2025.kingOpensParl.eval ⊔ Yagi2025.presConductsCeremony.eval

theorem Yagi2025.strong_kleene_never_false (w : W) : skDisj w ≠ Core.Duality.Truth3.false

Strong Kleene never produces false for this disjunction. Because presuppositions conflict, at least one disjunct is always undefined, so the table never reaches the 0 ∨ 0 = 0 row.

Failure 2: Two-dimensional semantics (@cite{yagi-2025} §2.2)

@cite{karttunen-peters-1979}, with @cite{yagi-2025}'s symmetric Definition 2 (per fn 2, citing @cite{kalomoiros-schwarz-2021} for empirical support of symmetry). The substrate PrProp.orKP matches Yagi's Def 2 directly:

Π(φ ∨ ψ) = (¬A(ψ) → Π(φ)) ∧ (¬A(φ) → Π(ψ))

PrProp.orFilter is a different symmetric variant with positive-antecedent conditionals plus an extra Π(φ) ∨ Π(ψ) disjunct, which is strictly stronger than orKP (worked counterexample: at a world with A(φ)=⊤, A(ψ)=⊥, Π(φ)=⊤, Π(ψ)=⊥, orKP is defined, orFilter is not). The two are not predictionally equivalent, and neither is the asymmetric @cite{karttunen-1973} rule (24b) used as PrProp.disjFilterLeft — see Phenomena/Presupposition/Studies/Karttunen1973.lean.

def Yagi2025.classicalDisj : Core.Presupposition.PrProp W

Classical disjunction requires both presuppositions: presup = p ∧ q.

Equations

• Yagi2025.classicalDisj = Yagi2025.kingOpensParl.or Yagi2025.presConductsCeremony

theorem Yagi2025.classical_never_defined (w : W) : ¬classicalDisj.presup w

PrProp.or is never defined when presuppositions conflict.

def Yagi2025.filterDisj : Core.Presupposition.PrProp W

The symmetric positive-antecedent filtering disjunction (PrProp.orFilter). Encodes (A(φ) → Π(ψ)) ∧ (A(ψ) → Π(φ)) ∧ (Π(φ) ∨ Π(ψ)) — strictly stronger than orKP. The conjunct Π(φ) ∨ Π(ψ) matches the eq. (7) modification discussed by @cite{yagi-2025} §2.2 (after Def 3) as a candidate fix.

Equations

• Yagi2025.filterDisj = Yagi2025.kingOpensParl.orFilter Yagi2025.presConductsCeremony

theorem Yagi2025.filter_wrong_at_kingOpens : ¬filterDisj.presup W.kingOpens

orFilter predicts presupposition failure at kingOpens, where the disjunction should clearly be true: the filtering condition demands the president-presupposition hold when the king-assertion is true.

theorem Yagi2025.expected_satisfied_at_kingOpens : expectedPresup W.kingOpens

The expected presupposition is satisfied at kingOpens.

def Yagi2025.kpDisj : Core.Presupposition.PrProp W

K&P two-dimensional disjunction applied to the Buganda scenario.

Equations

• Yagi2025.kpDisj = Yagi2025.kingOpensParl.orKP Yagi2025.presConductsCeremony

theorem Yagi2025.kp_presup_entails_assertion (w : W) : kpDisj.presup w → kpDisj.assertion w

K&P's presupposition entails the assertion when presuppositions conflict: whenever Π = 1, A = 1. Derived from the substrate PrProp.orKP_presup_entails_when_conflicting. @cite{yagi-2025} §2.2 (5)–(6).

Failure 3: Update semantics (@cite{yagi-2025} §2.3)

Bridges to Theories.Semantics.Dynamic.UpdateSemantics.Basic, which collapses the @cite{heim-1982}/@cite{veltman-1996}/@cite{beaver-2001} treatments of presuppositional disjunction into a single PUpdate.disjPresup operator.

def Yagi2025.bugandaState : Semantics.Dynamic.UpdateSemantics.State W

The ideal input state for (1c): all worlds with a head of state. The noHeadOfState world is excluded — Yagi's discussion presupposes a context where the disjunctive presupposition p ∨ q is satisfied.

Equations

• Yagi2025.bugandaState = {Yagi2025.W.kingOpens, Yagi2025.W.kingDoesnt, Yagi2025.W.presidentConducts, Yagi2025.W.presidentDoesnt}

theorem Yagi2025.hasKing_not_supported : Semantics.Dynamic.UpdateSemantics.Update.prop hasKing bugandaState ≠ bugandaState

Presupposition p (hasKing) is NOT supported in bugandaState: updating by p eliminates the president-worlds.

theorem Yagi2025.hasPresident_not_supported : Semantics.Dynamic.UpdateSemantics.Update.prop hasPresident bugandaState ≠ bugandaState

Presupposition q (hasPresident) is NOT supported in bugandaState.

theorem Yagi2025.update_yields_undefined : Semantics.Dynamic.UpdateSemantics.PUpdate.disjPresup hasKing kingOpensParl.assertion hasPresident presConductsCeremony.assertion (some bugandaState) = none

The presuppositional disjunction update yields ∗ (none) on bugandaState. @cite{yagi-2025} §2.3: the update s[φ_p ∨ ψ_q] results in undefinedness because the presupposition check for the first disjunct (s[p] = s) fails.

theorem Yagi2025.neither_presup_supported : Semantics.Dynamic.UpdateSemantics.Update.prop hasKing bugandaState ≠ bugandaState ∧ Semantics.Dynamic.UpdateSemantics.Update.prop hasPresident bugandaState ≠ bugandaState

Both presuppositions fail on bugandaState: combined with update_yields_undefined, the standard dynamic definition has no defined-and-informative output for conflicting presuppositions.

Failure 4: @cite{schlenker-2009}'s incremental evaluation

(@cite{yagi-2025} §2.4)

Yagi's §2.4 derivation: Schlenker's pragmatic condition on local contexts admits a context-world w only if w survives the local-context update of the second disjunct's presupposition; walking through the cases for the conflicting-presupposition setup, Yagi concludes that s_0 ends up containing only worlds where some disjunct's assertion-plus-presupposition holds — at which point the disjunction is trivially true and uninformative.

What we actually formalise here is the consequence, not Yagi's derivation. We stipulate the truth-set truthSet directly (kingOpens + presidentConducts — the worlds where some disjunct is defined-and-true) and show via the substrate's Semantics.Modality.Disjunction.exhaustivity_implies_uninformative that the disjunction is true throughout truthSet. This is an instance of Geurts's exhaustivity-implies-uninformativity, which Yagi argues coincides with Schlenker's verdict on the same context. The actual Schlenker local-context derivation would require a localContext operator on PUpdate (s/s[¬φ]) that we have not formalised; the present theorem is the static reduction.

Note: truthSet-uninformativity is structurally trivial — any proposition is uninformative on its own truth-set. The substantive Schlenker move is deriving that s_0 reduces to the truth-set; we punt on that derivation.

def Yagi2025.truthSet : Set W

The truth-set of the Buganda disjunction: the worlds where some disjunct's presupposition-and-assertion holds. Yagi §2.4 argues Schlenker's pragmatic condition forces s_0 ⊆ truthSet.

Equations

• Yagi2025.truthSet = {Yagi2025.W.kingOpens, Yagi2025.W.presidentConducts}

theorem Yagi2025.truthSet_exhausted : Semantics.Modality.Disjunction.exhaustivity truthSet (Semantics.Modality.Disjunction.fromPrProp kingOpensParl presConductsCeremony)

Geurts exhaustivity holds on truthSet: every truth-set world is in some disjunct's modal cell (domain ∩ content = presup ∧ assertion).

theorem Yagi2025.truthset_uninformative_geurts_route (w : W) : w ∈ truthSet → (kingOpensParl.orFlex presConductsCeremony).assertion w

Truth-set uninformativity via Geurts (the consequence of Yagi §2.4, not Schlenker's actual local-context derivation): the disjunction is true throughout the stipulated truthSet. Discharged via the substrate's exhaustivity_implies_uninformative. A faithful Schlenker formalisation would derive s_0 ⊆ truthSet from a localContext PUpdate operator we have not built.

Reaction 1: Meta-assertion (@cite{yagi-2025} §3.1, @cite{beaver-krahmer-2001})

Yagi §3.1 has two prongs: (i) the truth-functional behavior of 𝒜 (we formalize this), and (ii) the licensing constraint on when 𝒜 may be inserted (Beaver & Krahmer's condition: insert iff the formula would be undefined OR a part is replaceable by ⊥/⊤ without semantic effect). Yagi argues this constraint licenses the @cite{beaver-krahmer-2001} analysis (10) 𝒜φ_p ∨_w 𝒜ψ_q but does NOT license the Strong-Kleene counterpart (11) φ_p ∨_s 𝒜ψ_q, leaving Yagi's verdict on §3.1 partly negative ("I cannot offer a constraint now").

We formalize the truth-functional content; the licensing constraint remains prose-only because it requires a "replaceability" predicate that is itself an open theoretical question.

noncomputable def Yagi2025.metaAssertDisj : Core.Duality.Prop3 W

The disjunction 𝒜φ_p ∨ 𝒜ψ_q of Yagi (10), with 𝒜 the meta-assertion operator of Yagi Definition 6 (truth table 1↦1, 0↦0, ∗↦0). We use Prop3.or (Strong Kleene join) — since metaAssert maps each disjunct to a bivalent value, Strong and Weak Kleene agree on the result, and Yagi's discussion uses Weak Kleene (Def 7) only as a notational matter.

Equations

• Yagi2025.metaAssertDisj = Yagi2025.kingOpensParl.eval.metaAssert ⊔ Yagi2025.presConductsCeremony.eval.metaAssert

theorem Yagi2025.metaAssert_allows_falsity : metaAssertDisj W.kingDoesnt = Core.Duality.Truth3.false

Meta-assertion allows falsity (unlike Strong Kleene). Satisfies (2b).

theorem Yagi2025.metaAssert_always_defined (w : W) : (metaAssertDisj w).isDefined

Meta-assertion loses the presupposition: 𝒜φ_p has no presupposition (it maps ∗ to 0), so the Strong Kleene disjunction 𝒜φ_p ∨_s ψ_q only presupposes ¬𝒜ψ_q → p per Yagi (11), not p ∨ q.

theorem Yagi2025.metaAssert_no_gap (w : W) : metaAssertDisj w ≠ Core.Duality.Truth3.indet

The meta-assertion disjunction is bivalent — no gap, no presupposition via the standard gap mechanism.

Reaction 2: Flexible accommodation (@cite{yagi-2025} §3.2,

@cite{geurts-2005}, @cite{aloni-2022})

Uses the substrate PrProp.orFlex, with the discriminating world noHeadOfState ensuring the (2a) test is non-trivial.

def Yagi2025.flexDisj : Core.Presupposition.PrProp W

The flexible accommodation disjunction.

Equations

• Yagi2025.flexDisj = Yagi2025.kingOpensParl.orFlex Yagi2025.presConductsCeremony

theorem Yagi2025.flex_presup_fails_at_no_head : ¬flexDisj.presup W.noHeadOfState

(2a) at the discriminating world: flexDisj.presup fails at noHeadOfState. Without this world, expectedPresup would be a tautology and flex_correct_presup_iff_expected would degenerate to True ↔ True.

theorem Yagi2025.flex_presup_holds_at_kingOpens : flexDisj.presup W.kingOpens

(2a) at a head-of-state world: flexDisj.presup holds at kingOpens.

theorem Yagi2025.flex_correct_presup_iff_expected (w : W) : flexDisj.presup w ↔ expectedPresup w

(2a) globally: flexDisj.presup matches expectedPresup at every world. With noHeadOfState in the world model, this is a non-trivial biconditional (both sides fail there; both sides hold elsewhere).

theorem Yagi2025.flex_truth_table : flexDisj.eval W.kingOpens = Core.Duality.Truth3.true ∧ flexDisj.eval W.kingDoesnt = Core.Duality.Truth3.false ∧ flexDisj.eval W.presidentConducts = Core.Duality.Truth3.true ∧ flexDisj.eval W.presidentDoesnt = Core.Duality.Truth3.false

Complete truth table: flexible accommodation predicts the right value at every head-of-state world. (At noHeadOfState the disjunction is undefined.)

theorem Yagi2025.flex_undefined_at_no_head : flexDisj.eval W.noHeadOfState = Core.Duality.Truth3.indet

Flexible accommodation is undefined at the discriminating world noHeadOfState.

theorem Yagi2025.flex_can_be_false : flexDisj.eval W.kingDoesnt = Core.Duality.Truth3.false

(2b): flexDisj is false at kingDoesnt (king present but not opening).

Genuineness

@cite{yagi-2025} Definition 8 (after @cite{zimmermann-2000}): each disjunct must contribute a "live possibility" — there is w ∈ s with {w}[φ] = {w} AND w ∈ s[φ ∨ ψ]. The substrate PrProp.genuineness p q s disj parameterises on the disjunction connective disj whose update we test against; the simpler singleton-survival check is now PrProp.liveness. Under orFlex, liveness ⇒ genuineness (liveness_implies_genuineness_orFlex), so discharging genuineness reduces to discharging liveness.

theorem Yagi2025.flex_genuineness : kingOpensParl.genuineness presConductsCeremony { val := ↑[W.kingOpens, W.presidentConducts], nodup := ⋯ } flexDisj

Genuineness for the Buganda flex disjunction holds against the two-element witness state {kingOpens, presConducts}: each disjunct's witness world survives both its own update and the joint orFlex update.

Substrate observation: orFlex = orBelnap

NOT a Yagi claim — @cite{belnap-1970} is not in his references. This is an observation Core/Semantics/Presupposition.lean already makes (orFlex_eq_orBelnap) and that Theories/Semantics/Modality/Disjunction.lean extends to a three-way identity with @cite{geurts-2005}'s modal-disjunction view. We instantiate the substrate identity at the Buganda case for clarity.

theorem Yagi2025.flexDisj_eq_orBelnap : flexDisj = kingOpensParl.orBelnap presConductsCeremony

Substrate identity at the Buganda case: flexDisj = orBelnap.

Negation interaction (@cite{yagi-2025} §3.2 final paragraphs)

Yagi's static negation works fine — preserves presupposition, flips assertion. His dynamic negation s[¬(φ_p ∨ ψ_q)] = s/(s[χ][φ_p] ∪ s[χ][ψ_q]) requires genuineness to hold within the scope of negation, which Yagi calls "peculiar, given that we end up negating both disjuncts". The peculiarity surfaces only at the dynamic level — at the static PrProp.neg connective, the assertion just flips and presupposition is preserved (neg_presup); there is no genuineness check to violate.

We do not formalise the dynamic version here because it would require the Update-Semantics state operator s[¬φ] = s/s[φ] paired with the parametric flex update s[χ][φ] ∪ s[ω][ψ] of Yagi's eq. (13), neither of which we have built. The static negFlexDisj truth-table below shows the intended truth conditions (negation true at king-doesn't and president-doesn't, where both disjuncts fail); Yagi's "peculiarity" diagnosis lives at the dynamic level above this static reduction.

def Yagi2025.negFlexDisj : Core.Presupposition.PrProp W

Negation of the flexible accommodation disjunction.

Equations

• Yagi2025.negFlexDisj = Yagi2025.flexDisj.neg

theorem Yagi2025.neg_flex_presup_preserved : negFlexDisj.presup = flexDisj.presup

Static negation preserves the presupposition (substrate neg_presup).

theorem Yagi2025.neg_flex_truth_table : negFlexDisj.eval W.kingOpens = Core.Duality.Truth3.false ∧ negFlexDisj.eval W.kingDoesnt = Core.Duality.Truth3.true ∧ negFlexDisj.eval W.presidentConducts = Core.Duality.Truth3.false ∧ negFlexDisj.eval W.presidentDoesnt = Core.Duality.Truth3.true

Static negation gives the right truth values at the head-of-state worlds: true at king-doesn't and president-doesn't (both disjuncts false).

@cite{yagi-2025} example (8) Karttunen 1974: eq. (7) is too weak

@cite{yagi-2025} §2.2 (between Def 3 and §2.3) considers a modification to K&P, Π(φ ∨ ψ) := Π(φ) ∨ Π(ψ) (eq. (7)). This formula IS what PrProp.orFlex.presup computes. Yagi shows it correctly predicts (1c) Buganda but is "too weak" for (8) @cite{karttunen-1974}: "Either baldness is not hereditary, or all of Bill's children are bald." Eq. (7) predicts the tautological presupposition ⊤ ∨ Π(ψ) = ⊤, but the empirical intuition is that (8) presupposes Bill has children.

Important scope note: Yagi's §3.2 flexible-accommodation framework is NOT subject to this critique — it handles the analog (14) correctly via the χ = ω = ⊤ accommodation default (only when that violates an independent pragmatic principle does the split become non-trivial). The critique here applies to the static orFlex.presup formula (which matches eq. (7) at the presup level), not to the dynamic flex update s[χ][φ] ∪ s[ω][ψ] of eq. (13), which we have not formalised.

inductive Yagi2025.W8 : Type

Worlds for example (8).

• hasChildAllBald : W8
• hasChildSomeNotBald : W8
• noChild : W8

@[implicit_reducible]

instance Yagi2025.instDecidableEqW8 : DecidableEq W8

Equations

• Yagi2025.instDecidableEqW8 x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Yagi2025.instReprW8 : Repr W8

Equations

• Yagi2025.instReprW8 = { reprPrec := Yagi2025.instReprW8.repr }

def Yagi2025.instReprW8.repr : W8 → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Yagi2025.instReprW8.repr Yagi2025.W8.hasChildAllBald prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Yagi2025.W8.hasChildAllBald")).group prec✝
• Yagi2025.instReprW8.repr Yagi2025.W8.noChild prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Yagi2025.W8.noChild")).group prec✝

def Yagi2025.instInhabitedW8.default : W8

Equations

• Yagi2025.instInhabitedW8.default = Yagi2025.W8.hasChildAllBald

@[implicit_reducible]

instance Yagi2025.instInhabitedW8 : Inhabited W8

Equations

• Yagi2025.instInhabitedW8 = { default := Yagi2025.instInhabitedW8.default }

@[implicit_reducible]

instance Yagi2025.instFintypeW8 : Fintype W8

Equations

• Yagi2025.instFintypeW8 = { elems := { val := ↑Yagi2025.W8.enumList, nodup := Yagi2025.W8.enumList_nodup }, complete := Yagi2025.instFintypeW8._proof_1 }

def Yagi2025.billHasChild : W8 → Prop

"Bill has a child" — presupposition trigger for "all of Bill's children ...".

Equations

• Yagi2025.billHasChild Yagi2025.W8.hasChildAllBald = True
• Yagi2025.billHasChild Yagi2025.W8.hasChildSomeNotBald = True
• Yagi2025.billHasChild Yagi2025.W8.noChild = False

@[implicit_reducible]

instance Yagi2025.instDecidablePredW8BillHasChild : DecidablePred billHasChild

Equations

• Yagi2025.instDecidablePredW8BillHasChild Yagi2025.W8.hasChildAllBald = isTrue trivial
• Yagi2025.instDecidablePredW8BillHasChild Yagi2025.W8.hasChildSomeNotBald = isTrue trivial
• Yagi2025.instDecidablePredW8BillHasChild Yagi2025.W8.noChild = isFalse Yagi2025.instDecidablePredW8BillHasChild._proof_1

def Yagi2025.baldnessNotHereditary : Core.Presupposition.PrProp W8

"Baldness is not hereditary" — no presupposition.

Equations

• Yagi2025.baldnessNotHereditary = { presup := fun (x : Yagi2025.W8) => True, assertion := fun (x : Yagi2025.W8) => True }

def Yagi2025.allBillsChildrenBald : Core.Presupposition.PrProp W8

"All of Bill's children are bald" — factive on billHasChild.

Equations

• Yagi2025.allBillsChildrenBald = { presup := Yagi2025.billHasChild, assertion := fun (w : Yagi2025.W8) => w = Yagi2025.W8.hasChildAllBald }

def Yagi2025.ex8FlexDisj : Core.Presupposition.PrProp W8

The static flex disjunction for (8) — assertion ignored, only the presup formula matters here.

Equations

• Yagi2025.ex8FlexDisj = Yagi2025.baldnessNotHereditary.orFlex Yagi2025.allBillsChildrenBald

def Yagi2025.ex8ExpectedPresup : W8 → Prop

The empirical presupposition Karttunen attributes to (8): "Bill has children". This is the predicate that any adequate theory of disjunctive projection should derive.

Equations

• Yagi2025.ex8ExpectedPresup = Yagi2025.billHasChild

theorem Yagi2025.ex7_presup_trivial_for_ex8 (w : W8) : ex8FlexDisj.presup w

Eq. (7) predicts a tautological presupposition for (8): orFlex.presup is universally True because the first disjunct is presuppositionless.

theorem Yagi2025.expected_presup_fails_at_noChild : ¬ex8ExpectedPresup W8.noChild

The empirical presupposition is non-trivial: it fails at noChild.

theorem Yagi2025.eq7_too_weak_for_ex8 : ex8FlexDisj.presup ≠ ex8ExpectedPresup

@cite{yagi-2025}'s eq. (7) critique made formal: the eq. (7) formula (= orFlex.presup) does NOT match the empirical presupposition. Witness: at noChild, eq. (7) says True (presup satisfied), but the empirical intuition says False (presup failure — "Bill has children" doesn't hold). This is the contrast Yagi flags as making eq. (7) "too weak".

@cite{yagi-2025} example (18) Beaver 2001:115: the unprincipled success

"Either John didn't solve the problem or Mary realized that the problem is solved." The factive presupposition of "realize" does NOT project. @cite{yagi-2025} §3.2 final paragraphs: standard update semantics correctly predicts non-projection here, while flexible accommodation may predict it correctly but for the wrong reason — the incompatibility that motivates accommodation in (1c) and (15) is absent in (18), so genuineness should not even fire. The success is unprincipled.

Linglib's @cite{karttunen-1973} formalisation (Phenomena/Presupposition/Studies/Karttunen1973.lean) handles (18) via the asymmetric disjFilterLeft rule (24b): when ¬A entails Π(B), the presupposition is filtered. This is the principled alternative that the symmetric variants (orKP, orFilter) cannot offer.

inductive Yagi2025.W18 : Type

Worlds for example (18).

• solvedRealized : W18
• solvedNotRealized : W18
• notSolved : W18

@[implicit_reducible]

instance Yagi2025.instDecidableEqW18 : DecidableEq W18

Equations

• Yagi2025.instDecidableEqW18 x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Yagi2025.instReprW18 : Repr W18

Equations

• Yagi2025.instReprW18 = { reprPrec := Yagi2025.instReprW18.repr }

def Yagi2025.instReprW18.repr : W18 → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Yagi2025.instReprW18.repr Yagi2025.W18.solvedRealized prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Yagi2025.W18.solvedRealized")).group prec✝
• Yagi2025.instReprW18.repr Yagi2025.W18.notSolved prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Yagi2025.W18.notSolved")).group prec✝

@[implicit_reducible]

instance Yagi2025.instInhabitedW18 : Inhabited W18

Equations

• Yagi2025.instInhabitedW18 = { default := Yagi2025.instInhabitedW18.default }

def Yagi2025.instInhabitedW18.default : W18

Equations

• Yagi2025.instInhabitedW18.default = Yagi2025.W18.solvedRealized

@[implicit_reducible]

instance Yagi2025.instFintypeW18 : Fintype W18

Equations

• Yagi2025.instFintypeW18 = { elems := { val := ↑Yagi2025.W18.enumList, nodup := Yagi2025.W18.enumList_nodup }, complete := Yagi2025.instFintypeW18._proof_1 }

def Yagi2025.solved : W18 → Prop

"John solved the problem".

Equations

• Yagi2025.solved Yagi2025.W18.solvedRealized = True
• Yagi2025.solved Yagi2025.W18.solvedNotRealized = True
• Yagi2025.solved Yagi2025.W18.notSolved = False

@[implicit_reducible]

instance Yagi2025.instDecidablePredW18Solved : DecidablePred solved

Equations

• Yagi2025.instDecidablePredW18Solved Yagi2025.W18.solvedRealized = isTrue trivial
• Yagi2025.instDecidablePredW18Solved Yagi2025.W18.solvedNotRealized = isTrue trivial
• Yagi2025.instDecidablePredW18Solved Yagi2025.W18.notSolved = isFalse Yagi2025.instDecidablePredW18Solved._proof_1

def Yagi2025.maryRealized : Core.Presupposition.PrProp W18

"Mary realized the problem is solved" — factive: presupposes problem is solved.

Equations

• Yagi2025.maryRealized = { presup := Yagi2025.solved, assertion := fun (w : Yagi2025.W18) => w = Yagi2025.W18.solvedRealized }

def Yagi2025.johnDidntSolve : Core.Presupposition.PrProp W18

"John didn't solve the problem" — no presupposition.

Equations

• Yagi2025.johnDidntSolve = { presup := fun (x : Yagi2025.W18) => True, assertion := fun (w : Yagi2025.W18) => ¬Yagi2025.solved w }

theorem Yagi2025.ex18_symmetric_orFilter_overgenerates : ¬(johnDidntSolve.orFilter maryRealized).presup W18.notSolved

The symmetric positive-antecedent orFilter overgenerates here: predicts presupposition failure at notSolved, where the disjunction should be defined-and-true.

theorem Yagi2025.ex18_orFlex_no_projection_via_vacuous_left : (johnDidntSolve.orFlex maryRealized).presup W18.notSolved

orFlex predicts non-projection at notSolved. The proof goes through the LEFT disjunct of Π(φ) ∨ Π(ψ): johnDidntSolve.presup is universally True (no presupposition).

theorem Yagi2025.ex18_left_presup_vacuous (w : W18) : johnDidntSolve.presup w

The structural reason for ex18_orFlex_no_projection_via_vacuous_left: johnDidntSolve has NO presupposition, so any orFlex.presup involving it is universally satisfied — independently of maryRealized.presup.

theorem Yagi2025.ex18_unprincipled_in_right_presup_failure : ¬maryRealized.presup W18.notSolved ∧ (johnDidntSolve.orFlex maryRealized).presup W18.notSolved ∧ ∀ (w : W18), johnDidntSolve.presup w

@cite{yagi-2025} §3.2's "unprincipled success" diagnosis made structural: at notSolved, the right disjunct's presupposition solved fails, so (orFlex _ maryRealized).presup would have NO support if the left disjunct also had a presupposition. The success at (18) rides entirely on the left disjunct being presuppositionless — which is an accident of (18)'s lexical content, not a consequence of genuineness or accommodation. The contrast: in (1c) Buganda, BOTH disjuncts carry presuppositions, so orFlex.presup provides genuine accommodation work; in (18), only the right disjunct does, so the left disjunct's vacuous True carries the prediction unilaterally.

theorem Yagi2025.ex18_asymmetric_K1973_principled : (Core.Presupposition.PrProp.disjFilterLeft (fun (w : W18) => ¬solved w) maryRealized).presup = fun (x : W18) => True

@cite{karttunen-1973}'s asymmetric rule (24b) — formalised in Phenomena/Presupposition/Studies/Karttunen1973.lean as PrProp.disjFilterLeft — gives a principled derivation: ¬(¬solved) = solved entails the factive presupposition, so it is filtered. We invoke the K1973 sibling theorem Karttunen1973.disjFilterLeft_eliminates_presup_when_neg_entails.

Summary

Compact API restating the core verdicts. We keep only the headline results — the per-failure detail theorems above already document the content.

theorem Yagi2025.orFlex_satisfies_both : (∀ (w : W), flexDisj.presup w ↔ expectedPresup w) ∧ flexDisj.eval W.kingDoesnt = Core.Duality.Truth3.false

orFlex satisfies both Yagi headline observations: (2a) correct presupposition at the discriminating world, (2b) can be false.

theorem Yagi2025.orFlex_eq_orBelnap_at_buganda : Core.Presupposition.PrProp.orFlex = Core.Presupposition.PrProp.orBelnap

The substrate-canonical orFlex / orBelnap / Geurts three-way identity, instantiated at the Buganda case. The substrate-side identity is Core.Presupposition.PrProp.orFlex_eq_orBelnap and Theories.Semantics.Modality.Disjunction.fromPrProp_cell_iff_orBelnap.