Blind Mandatory Scalar Implicatures

@cite{magri-2009}

@cite{magri-2009}. Natural Language Semantics 17(3): 245–297. DOI: 10.1007/s11050-009-9042-x.

Three pieces form the substantive core of the paper:

1. Blindness Hypothesis (BH) (§3.2.2, eq. (32)): The exhaustivity operator EXH computes the strengthened meaning using logical entailment (→W), not entailment given common knowledge (→{W_ck}).

2. Mismatch Hypothesis (MH) (§3.2.2, eq. (33)): If the blind strengthened meaning EXH(φ) is a contradiction given common knowledge (EXH(φ) ∩ W_ck = ∅), then φ sounds odd.

3. Mandatoriness machinery (§3.2.5, eq. (41)–(43)): EXH is mandatory in matrix clauses (eq. 41); a contextual relevance variable R subject to (43a) "uttered ⇒ relevant" and (43b) "relevance closed under contextual equivalence" makes mismatching SIs mandatory while leaving standard SIs non-mandatory. The mandatoriness is the load-bearing premise — without it, the SI could be cancelled and the deviance rescued (Magri's §1 "robustness" claim).

Substrate split

BlindScenario + strengthened + blindOdd capture (1) and (2): the outcome of mismatching SIs. The deviance prediction is correct under mandatoriness as an external assumption.

RelevantBlindScenario adds R as a structure field with (43a)/(43b) as laws, and strengthenedR implements the R-relativized EXH (eq. (42)). The substantive theorem mismatching_alt_relevant proves Magri's mandatoriness consequence: when target and alternative are CK-equivalent, R cannot block the alternative — the SI is mandatory.

Introductory Example

"# Some Italians come from a warm country" (ex. (2))

• Literal: some Italians come from a warm country
• Strengthened (blind, via BH): some BUT NOT ALL Italians come from a warm country
• CK: Italy is warm → all Italians come from a warm country
• Strengthened ∩ CK = ∅ → odd (via MH)
• "Some" and "all" are CK-equivalent (both denote {allWarm} in CK) → R(all) = R(some) = 1 → SI is mandatory (eq. 43a + 43b consequence).

Application to Individual-Level Predicates

The paper's main contribution (§4) derives properties of individual-level predicates (ILPs) from BH + MH via assumption (70): ILPs are homogeneous — if an i-predicate holds at any time in W_ck, it holds at all times. This homogeneity makes blind strengthening systematically contradict CK for i-predicate constructions.

Key applications: "#Sometimes, John is tall" (§4.1), bare plural subject restrictions (§4.2), embedding under universal quantifiers (§4.3), and German word order (§4.5). See §5 below for the Q-adverb formalization.

The ILP/SLP distinction is @cite{carlson-1977}'s PredicateLevel: individual-level predicates trigger homogeneity (assumption (70)), while stage-level predicates do not.

Naming note: BPSWorld

Section §6 below uses BPSWorld for Bare Plural Subjects, the empirical phenomenon @cite{magri-2009} extends his account to. This is unrelated to the Bassi–Del Pinal–Sauerland 2021 Presuppositional EXH abbreviation also used in this project (bpsToImplicature, .bpsPresuppositional). Different BPS, different file.

structure Magri2009.BlindScenario (W U : Type) [Fintype W] [DecidableEq W] : Type

A scenario for blind scalar implicature computation.

@cite{magri-2009}'s mechanism needs only literal meanings, scalar alternatives, and common knowledge — no QUD or complexity ordering.

• meaning : U → W → Bool

  Literal meaning of each utterance at each world.

• alternatives : U → List U

  All scalar alternatives for each utterance. @cite{fox-2007}'s innocent exclusion algorithm determines which alternatives are excludable — weaker alternatives (e.g., "some" when the prejacent is "all") are automatically filtered out.

• context : W → Bool

  Common knowledge: which worlds are CK-compatible.

def Magri2009.BlindScenario.cWorlds {W U : Type} [Fintype W] [DecidableEq W] (s : BlindScenario W U) : Finset W

CK-compatible worlds.

Equations

• s.cWorlds = {w : W | s.context w = true}

def Magri2009.BlindScenario.strengthened {W U : Type} [Fintype W] [DecidableEq W] (s : BlindScenario W U) (u : U) (w : W) : Bool

Strengthened meaning via @cite{fox-2007}'s exhaustivity operator.

Implements the Blindness Hypothesis (BH): EXH computes the strengthened meaning using logical entailment over W, not entailment given common knowledge W_ck. The grammar strengthens automatically, even when the result contradicts what speaker and hearer both know.

Equations

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

def Magri2009.BlindScenario.blindOdd {W U : Type} [Fintype W] [DecidableEq W] (s : BlindScenario W U) (u : U) : Bool

Blind oddness: the exhaustivity operator produced a non-vacuous implicature, yet the strengthened meaning is false at every CK world.

Implements the Mismatch Hypothesis (MH): if EXH(φ) ∩ W_ck = ∅ (the blind strengthened meaning contradicts common knowledge), then φ sounds odd.

Equations

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

theorem Magri2009.BlindScenario.blindOdd_excludes_cWorlds {W U : Type} [Fintype W] [DecidableEq W] (s : BlindScenario W U) (u : U) (h : s.blindOdd u = true) (w : W) : w ∈ s.cWorlds → w ∉ Exhaustification.innocent.exh (Exhaustification.altsFromPreds (List.map s.meaning (s.alternatives u))) (Exhaustification.predToFinset (s.meaning u))

Structural extraction of the second blindOdd conjunct: when the strengthened meaning is blindOdd, every CK-compatible world is excluded by the EXH operator. This is the load-bearing fact for the "strengthened meaning has no CK-realizer" claim — strengthened u w = true means w ∈ innocent.exh ..., but blindOdd says no CK world is in that set. Lifting this lemma to the BlindScenario level (rather than inlining it at every consumer site) decouples the proof from the specific shape of blindOdd.

theorem Magri2009.BlindScenario.mem_cWorlds_of_context {W U : Type} [Fintype W] [DecidableEq W] (s : BlindScenario W U) (w : W) (h : s.context w = true) : w ∈ s.cWorlds

Membership in cWorlds reflects context truth. Convenience for callers that have a s.context w = true hypothesis and need w ∈ s.cWorlds.

def Magri2009.BlindScenario.ignoranceContradictsCK {W U : Type} [Fintype W] [DecidableEq W] (s : BlindScenario W U) (u : U) : Bool

Ignorance-based oddness: alternatives exist that are NOT innocently excludable (so ignorance inferences are derived), yet CK settles every alternative (all true at every CK world, or all false at every CK world). The speaker cannot be genuinely ignorant → contradiction → deviant.

This complements blindOdd: blindOdd detects when scalar implicatures contradict CK (EXH(φ) ∩ W_ck = ∅), while ignoranceContradictsCK detects when ignorance inferences contradict CK (alternatives are relevant but CK-settled).

@cite{denic-2023} §6: deviance of "#Each of those three girls is Mary, Susan, or Jane" arises because ignorance inferences about singleton- denoting predicates contradict CK.

Equations

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

R-relativized exhaustification: the mandatoriness mechanism

§3.2.2 (BH+MH above) states the outcome of @cite{magri-2009}'s account: blind EXH mismatches CK, sentence sounds odd. §3.2.5 is the mechanism explaining why mismatching SIs are mandatory while standard SIs (e.g. the answer to (40c) "John is usually available after dinner") are not. The key is a contextually-supplied relevance predicate R, an R-relativized EXH operator (eq. (42)), and two postulates on R (eq. (43)).

The mandatoriness consequence (p. 263): for mismatching SIs, the target φ and its scalar alternative ψ are contextually equivalent (φ ↔_{W_ck} ψ — common knowledge forces them to denote the same set within W_ck). By postulate (43b), R is closed under contextual equivalence, so R(ψ) = R(φ). By postulate (43a), R(φ) = 1 (the uttered proposition is always relevant). Hence R(ψ) = 1, and EXHᴿ(φ) negates ψ no matter how the context assigns R to other propositions. The SI is mandatory.

For standard SIs (φ and alternatives NOT contextually equivalent), R can be set independently — the context can make ψ irrelevant (R(ψ) = 0), in which case EXHᴿ(φ) does not negate ψ and the SI is not derived. Hence the SI is non-mandatory.

Without this machinery, BlindScenario's blindOdd over-predicts deviance: it fires whenever any logically stronger CK-incompatible alternative exists, regardless of whether R would block it. The substrate below adds R as a field with the postulates as structure laws, and proves that for CK-equivalent (target, alternative) pairs the SI is mandatory.

structure Magri2009.RelevantBlindScenario (W U : Type) [Fintype W] [DecidableEq W] extends Magri2009.BlindScenario W U : Type

Magri's relevance predicate, contextually supplied (@cite{magri-2009} §3.2.5). A property R : Finset W → Bool of propositions (extensions, as Finsets of CK-compatible-or-not worlds) satisfying:

• (43a) Maximize Relevance: an uttered proposition's denotation is relevant. Hardwires the Gricean Maxim of Relevance.
• (43b) Contextual closure: if two propositions are equivalent given common knowledge (p ∩ W_ck = q ∩ W_ck), they share their relevance status. Captures that R is a contextual variable.

Together with mandatory EXH (eq. (41), an external assumption — Magri states it as a stipulation about matrix clauses), R determines whether SIs are mandatory: see mismatching_alt_relevant below.

• meaning : U → W → Bool
• alternatives : U → List U
• context : W → Bool
• relevant : Finset W → Bool

  R: which propositions (as Finsets of worlds) are contextually relevant.

• uttered_relevant (u : U) : self.relevant (Exhaustification.predToFinset (self.meaning u)) = true

  @cite{magri-2009} eq. (43a): every uttered proposition's denotation is relevant.

• relevant_ck_closed (p q : Finset W) : p ∩ self.cWorlds = q ∩ self.cWorlds → self.relevant p = self.relevant q

  @cite{magri-2009} eq. (43b): R is closed under common-knowledge equivalence. Two propositions agreeing on every CK-compatible world have the same R-value.

def Magri2009.RelevantBlindScenario.strengthenedR {W U : Type} [Fintype W] [DecidableEq W] (s : RelevantBlindScenario W U) (u : U) (w : W) : Bool

@cite{magri-2009} eq. (42): R-relativized exhaustification. EXHᴿ(φ) := φ ∧ ⋀_{ψ ∈ Excl(φ)} (¬ψ ∨ ¬R(ψ)). A world w survives iff w ∈ φ AND, for every excludable alternative ψ, either w ∉ ψ or ψ is irrelevant. Equivalently: w ∈ φ and every relevant excludable alternative is false at w.

Reduces to plain strengthened (Fox 2007 IE) when all excludable alternatives are relevant.

Equations

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

theorem Magri2009.RelevantBlindScenario.mismatching_alt_relevant {W U : Type} [Fintype W] [DecidableEq W] (s : RelevantBlindScenario W U) (u alt : U) (h_ck_equiv : Exhaustification.predToFinset (s.meaning u) ∩ s.cWorlds = Exhaustification.predToFinset (s.meaning alt) ∩ s.cWorlds) : s.relevant (Exhaustification.predToFinset (s.meaning alt)) = true

Mandatoriness consequence of (43a) + (43b) for mismatching SIs. When the uttered prejacent's denotation and an alternative's denotation are contextually equivalent (= agree on every CK-compatible world), postulate (43b) lifts the alternative's relevance to match the prejacent's, and (43a) forces the prejacent's relevance to 1. So the alternative is mandatorily relevant — no contextual choice of R can block it.

This is the formal core of @cite{magri-2009}'s argument on p. 263: mismatching SIs are mandatory because the alternative cannot be R-blocked. The contrast with non-mismatching SIs (where φ and ψ are not CK-equivalent, so R(ψ) is free) explains why standard SIs are non-mandatory.

"# Some Italians come from a warm country" (@cite{magri-2009})

Three worlds are needed because the strengthened meaning "some but not all" requires a world where some but not all Italians come from a warm country.

CK: Italy is a warm country → all Italians come from a warm country. Only allWarm is CK-compatible.

inductive Magri2009.ItalyWorld₃ : Type

• allWarm : ItalyWorld₃
• someNotAll : ItalyWorld₃
• noneWarm : ItalyWorld₃

@[implicit_reducible]

instance Magri2009.instDecidableEqItalyWorld₃ : DecidableEq ItalyWorld₃

Equations

• Magri2009.instDecidableEqItalyWorld₃ x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Magri2009.instReprItalyWorld₃.repr : ItalyWorld₃ → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Magri2009.instReprItalyWorld₃ : Repr ItalyWorld₃

Equations

• Magri2009.instReprItalyWorld₃ = { reprPrec := Magri2009.instReprItalyWorld₃.repr }

@[implicit_reducible]

instance Magri2009.instFintypeItalyWorld₃ : Fintype ItalyWorld₃

Equations

• Magri2009.instFintypeItalyWorld₃ = { elems := { val := ↑Magri2009.ItalyWorld₃.enumList, nodup := Magri2009.ItalyWorld₃.enumList_nodup }, complete := Magri2009.instFintypeItalyWorld₃._proof_1 }

inductive Magri2009.ItalyUtt : Type

• some_ : ItalyUtt
• all_ : ItalyUtt

@[implicit_reducible]

instance Magri2009.instDecidableEqItalyUtt : DecidableEq ItalyUtt

Equations

• Magri2009.instDecidableEqItalyUtt x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Magri2009.instReprItalyUtt : Repr ItalyUtt

Equations

• Magri2009.instReprItalyUtt = { reprPrec := Magri2009.instReprItalyUtt.repr }

def Magri2009.instReprItalyUtt.repr : ItalyUtt → ℕ → Std.Format

Equations

• Magri2009.instReprItalyUtt.repr Magri2009.ItalyUtt.some_ prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Magri2009.ItalyUtt.some_")).group prec✝
• Magri2009.instReprItalyUtt.repr Magri2009.ItalyUtt.all_ prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Magri2009.ItalyUtt.all_")).group prec✝

@[implicit_reducible]

instance Magri2009.instFintypeItalyUtt : Fintype ItalyUtt

Equations

• Magri2009.instFintypeItalyUtt = { elems := { val := ↑Magri2009.ItalyUtt.enumList, nodup := Magri2009.ItalyUtt.enumList_nodup }, complete := Magri2009.instFintypeItalyUtt._proof_1 }

def Magri2009.italianScenario : BlindScenario ItalyWorld₃ ItalyUtt

Equations

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

def Magri2009.italianRelevantScenario : RelevantBlindScenario ItalyWorld₃ ItalyUtt

Lift italianScenario to a RelevantBlindScenario by adding a canonical relevance predicate: R(p) := 1 iff p's CK-projection matches that of some uttered alternative. This is the minimal R satisfying both (43a) and (43b) — and crucially, it forces R(meaning all_) = R(meaning some_) = 1 because both denote {allWarm} in CK.

Equations

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

theorem Magri2009.some_strengthened_false_at_ck : italianScenario.strengthened ItalyUtt.some_ ItalyWorld₃.allWarm = false

Strengthened "some" at allWarm is false: some(allWarm) ∧ ¬all(allWarm) = true ∧ false = false. The blind implicature "not all" kills the literal meaning at the CK world.

theorem Magri2009.some_strengthened_true_at_nonck : italianScenario.strengthened ItalyUtt.some_ ItalyWorld₃.someNotAll = true

Strengthened "some" at someNotAll is true: some(someNotAll) ∧ ¬all(someNotAll) = true ∧ true = true. But someNotAll is ruled out by CK — no help.

theorem Magri2009.italian_some_blind_odd : italianScenario.blindOdd ItalyUtt.some_ = true

@cite{magri-2009} prediction: "some Italians" is odd. The blind implicature "not all" contradicts CK (Italy is warm).

theorem Magri2009.italian_all_not_odd : italianScenario.blindOdd ItalyUtt.all_ = false

"all Italians" is not odd: no stronger alternative to negate, so no blind implicature is generated.

@cite{magri-2009} ex. (3)/(72b): "# Sometimes, John is tall"

The paper's main contribution derives oddness of Q-adverbs with individual-level predicates (ILPs) from BH + MH. The key assumption homogeneity (assumption (70)): if an i-predicate holds of an individual at any time in W_ck, it holds at all times. This rules out mixed worlds (tall at some times but not all) from the common ground.

• Literal: at some times, John is tall
• Strengthened (blind, via BH): at some but NOT ALL times, John is tall
• CK: "tall" is an ILP → homogeneity → John is either always tall or never tall. The "sometimes but not always" world is CK-incompatible.
• Strengthened ∩ CK = ∅ → odd (via MH)

Contrast with the stage-level predicate "Sometimes, John is available": since availability can genuinely vary over time, the "sometimes but not always" world is CK-compatible → strengthened meaning is satisfiable → OK.

The ILP/SLP distinction is @cite{carlson-1977}'s PredicateLevel: individual-level → homogeneity → oddness; stage-level → no homogeneity → fine.

inductive Magri2009.TallWorld : Type

• alwaysTall : TallWorld
• sometimesOnly : TallWorld
• neverTall : TallWorld

@[implicit_reducible]

instance Magri2009.instDecidableEqTallWorld : DecidableEq TallWorld

Equations

• Magri2009.instDecidableEqTallWorld x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Magri2009.instReprTallWorld : Repr TallWorld

Equations

• Magri2009.instReprTallWorld = { reprPrec := Magri2009.instReprTallWorld.repr }

def Magri2009.instReprTallWorld.repr : TallWorld → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Magri2009.instFintypeTallWorld : Fintype TallWorld

Equations

• Magri2009.instFintypeTallWorld = { elems := { val := ↑Magri2009.TallWorld.enumList, nodup := Magri2009.TallWorld.enumList_nodup }, complete := Magri2009.instFintypeTallWorld._proof_1 }

inductive Magri2009.QAdvUtt : Type

• sometimes_ : QAdvUtt
• always_ : QAdvUtt

@[implicit_reducible]

instance Magri2009.instDecidableEqQAdvUtt : DecidableEq QAdvUtt

Equations

• Magri2009.instDecidableEqQAdvUtt x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Magri2009.instReprQAdvUtt.repr : QAdvUtt → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Magri2009.instReprQAdvUtt.repr Magri2009.QAdvUtt.always_ prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Magri2009.QAdvUtt.always_")).group prec✝

@[implicit_reducible]

instance Magri2009.instReprQAdvUtt : Repr QAdvUtt

Equations

• Magri2009.instReprQAdvUtt = { reprPrec := Magri2009.instReprQAdvUtt.repr }

def Magri2009.tallScenario : BlindScenario TallWorld QAdvUtt

@cite{magri-2009} §4.1: Q-adverbs with individual-level predicates.

"Sometimes" and "always" form a ⟨sometimes, always⟩ scale analogous to ⟨some, all⟩. Homogeneity (assumption (70)) rules out sometimesOnly from the common ground.

Equations

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

theorem Magri2009.tall_sometimes_strengthened_false : tallScenario.strengthened QAdvUtt.sometimes_ TallWorld.alwaysTall = false

Strengthened "sometimes" at alwaysTall is false: sometimes(alwaysTall) ∧ ¬always(alwaysTall) = true ∧ false = false.

theorem Magri2009.tall_sometimes_strengthened_false_never : tallScenario.strengthened QAdvUtt.sometimes_ TallWorld.neverTall = false

Strengthened "sometimes" at neverTall is also false: sometimes(neverTall) = false.

theorem Magri2009.tall_sometimes_blind_odd : tallScenario.blindOdd QAdvUtt.sometimes_ = true

@cite{magri-2009} prediction: "# Sometimes, John is tall" is odd. The blind implicature "not always" contradicts homogeneity (70).

theorem Magri2009.tall_always_not_odd : tallScenario.blindOdd QAdvUtt.always_ = false

"Always, John is tall" is fine: no stronger alternative exists.

def Magri2009.homogeneity : Semantics.Kinds.SortedOntology.PredicateLevel → TallWorld → Bool

Homogeneity determines which worlds are CK-compatible.

@cite{magri-2009} assumption (70): if an i-predicate holds of an individual at any time in a CK-compatible world, it holds at all times within that individual's lifespan. This makes the predicate "homogeneous."

This maps @cite{carlson-1977}'s PredicateLevel to a CK context:

• Individual-level → only homogeneous worlds are CK-compatible
• Stage-level → all worlds are CK-compatible (the predicate can genuinely vary over time)

Equations

• One or more equations did not get rendered due to their size.
• Magri2009.homogeneity Semantics.Kinds.SortedOntology.PredicateLevel.stageLevel = fun (x : Magri2009.TallWorld) => true

theorem Magri2009.tall_context_from_ilp : tallScenario.context = homogeneity Semantics.Kinds.SortedOntology.PredicateLevel.individualLevel

The context function of tallScenario is exactly what ILP homogeneity predicts for individual-level predicates.

def Magri2009.availableScenario : BlindScenario TallWorld QAdvUtt

Stage-level contrast scenario: "Sometimes, John is available."

Same literal semantics and scale as the tall scenario, but CK admits all worlds because availability is stage-level — it CAN genuinely vary over time. The homogeneity assumption (70) does not apply.

Equations

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

theorem Magri2009.available_context_from_slp : availableScenario.context = homogeneity Semantics.Kinds.SortedOntology.PredicateLevel.stageLevel

The context of availableScenario matches stage-level homogeneity: all worlds are CK-compatible.

theorem Magri2009.available_sometimes_not_odd : availableScenario.blindOdd QAdvUtt.sometimes_ = false

"Sometimes, John is available" is NOT odd. Stage-level predicates don't trigger homogeneity (70), so sometimesOnly is CK-compatible and the strengthened meaning is satisfiable.

theorem Magri2009.predicate_level_determines_oddness : tallScenario.blindOdd QAdvUtt.sometimes_ = true ∧ availableScenario.blindOdd QAdvUtt.sometimes_ = false

The ILP/SLP distinction determines oddness: individual-level + "sometimes" → odd; stage-level + "sometimes" → fine.

This is the structural prediction: @cite{carlson-1977}'s PredicateLevel feeds into @cite{magri-2009}'s blindness mechanism via homogeneity (70).

theorem Magri2009.scenarios_share_semantics : tallScenario.meaning = availableScenario.meaning ∧ tallScenario.alternatives = availableScenario.alternatives

The tall and available scenarios share literal semantics and alternatives — they differ ONLY in the CK context.

theorem Magri2009.contexts_differ_at_sometimesOnly : tallScenario.context TallWorld.sometimesOnly ≠ availableScenario.context TallWorld.sometimesOnly

The contexts genuinely differ: sometimesOnly is CK-incompatible for individual-level (tall) but CK-compatible for stage-level (available).

theorem Magri2009.homogeneity_necessary_and_sufficient : tallScenario.meaning = availableScenario.meaning ∧ tallScenario.alternatives = availableScenario.alternatives ∧ tallScenario.context ≠ availableScenario.context ∧ tallScenario.blindOdd QAdvUtt.sometimes_ ≠ availableScenario.blindOdd QAdvUtt.sometimes_

Homogeneity (70) is necessary and sufficient for Q-adverb oddness.

The two scenarios have identical literal semantics, identical scale structure, and identical worlds. The ONLY difference is the CK context, which is determined by @cite{carlson-1977}'s PredicateLevel via homogeneity. Yet this single difference flips the oddness prediction:

• Individual-level ("tall"): context rules out sometimesOnly → strengthened meaning contradicts CK → odd
• Stage-level ("available"): context admits sometimesOnly → strengthened meaning satisfiable at CK world → fine

This proves that @cite{carlson-1977}'s predicate-level classification is doing genuine explanatory work in @cite{magri-2009}'s system: it is the SOLE factor determining oddness for Q-adverb sentences.

Context characterization theorem

The existing proofs show that specific context functions (homogeneity, stage-level) produce or prevent oddness. But what characterizes the oddness- producing contexts in general?

For the ⟨sometimes, always⟩ scale, oddness of "sometimes" depends on a single Boolean condition: whether the "mixed" world (sometimesOnly) is CK-compatible. This is because the strengthened meaning "sometimes but not always" is true only at the mixed world — so EXH(φ) ∩ W_ck = ∅ iff the mixed world is excluded from CK.

This theorem is universally quantified over all possible context functions, not just the two tested above. It explains why @cite{carlson-1977}'s predicate-level classification does the right work: individual-level predicates produce oddness precisely because homogeneity rules out the mixed world.

theorem Magri2009.oddness_iff_mixed_excluded (ctx : TallWorld → Bool) : (have __src := tallScenario; { meaning := __src.meaning, alternatives := __src.alternatives, context := ctx }).blindOdd QAdvUtt.sometimes_ = !ctx TallWorld.sometimesOnly

For any context function on the ⟨sometimes, always⟩ scale, oddness of "sometimes" is equivalent to ruling out the mixed world from CK.

This characterizes EXACTLY which contexts produce oddness, independently of any specific predicate-level classification. The proof factors the abstract context into its 3 constructor values (8 cases) and verifies each computationally.

theorem Magri2009.ilp_rules_out_mixed : homogeneity Semantics.Kinds.SortedOntology.PredicateLevel.individualLevel TallWorld.sometimesOnly = false

Homogeneity (70) produces oddness because it rules out the mixed world.

theorem Magri2009.slp_admits_mixed : homogeneity Semantics.Kinds.SortedOntology.PredicateLevel.stageLevel TallWorld.sometimesOnly = true

SLP permits "sometimes" because it admits the mixed world.

Bare plural subject restrictions

@cite{magri-2009} §4.2: the BPS firemen of the s-predicate available admits both the existential and generic readings (ex. (84a)):

• ∃-BPS: "There are firemen who are available"
• GEN-BPS: "Firemen are generally available"

But the BPS of the i-predicate tall lacks the existential reading (84b):

• #∃-BPS: "There are firemen who are tall"
• GEN-BPS: "Firemen are (generally) tall"

@cite{magri-2009}'s key insight: the ∃-BPS reading of an ILP has the SAME abstract structure as "#Sometimes, John is tall" (§4.1). This is because existential BPs always take narrowest scope (@cite{carlson-1977}), making narrow-scope ∃ over times equivalent to "sometimes." The definite description alternative plays the role of "always." Homogeneity (70) rules out the partial world, so the strengthened meaning contradicts CK.

We model this with independent types and prove the meaning table is isomorphic to the Q-adverb scenario from §5.

inductive Magri2009.BPSWorld : Type

Worlds for the bare plural ∃-reading of "Firemen are tall."

@cite{magri-2009} §4.2: the truth conditions (91b)/(92b) involve ∃ over firemen and time. The three worlds correspond to whether any fireman is tall throughout his lifespan within the contextually supplied restrictor.

• allThroughout : BPSWorld
• partialOnly : BPSWorld
• noneTall : BPSWorld

@[implicit_reducible]

instance Magri2009.instDecidableEqBPSWorld : DecidableEq BPSWorld

Equations

• Magri2009.instDecidableEqBPSWorld x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Magri2009.instReprBPSWorld : Repr BPSWorld

Equations

• Magri2009.instReprBPSWorld = { reprPrec := Magri2009.instReprBPSWorld.repr }

def Magri2009.instReprBPSWorld.repr : BPSWorld → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Magri2009.instFintypeBPSWorld : Fintype BPSWorld

Equations

• Magri2009.instFintypeBPSWorld = { elems := { val := ↑Magri2009.BPSWorld.enumList, nodup := Magri2009.BPSWorld.enumList_nodup }, complete := Magri2009.instFintypeBPSWorld._proof_1 }

inductive Magri2009.BPSReading : Type

The bare plural reading and its definite-description alternative.

Following the Heim-Diesing framework: the BP introduces a free variable bound by a default existential operator (DEO) with VP scope.

The Horn scale is ⟨bare plural, definite description⟩ (eq. (94)): the BP firemen alternates with the fireman P for each specific fireman P. In the 3-world model, the definite-description alternative ψ (eq. (95)) is extensionally equivalent to the GEN-BPS reading φ (eq. (91b)), so we model both as generic_.

• existential_ : BPSReading
• generic_ : BPSReading

@[implicit_reducible]

instance Magri2009.instDecidableEqBPSReading : DecidableEq BPSReading

Equations

• Magri2009.instDecidableEqBPSReading x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Magri2009.instReprBPSReading.repr : BPSReading → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Magri2009.instReprBPSReading : Repr BPSReading

Equations

• Magri2009.instReprBPSReading = { reprPrec := Magri2009.instReprBPSReading.repr }

def Magri2009.bpsScenario : BlindScenario BPSWorld BPSReading

@cite{magri-2009} §4.2: bare plural existential reading of an ILP.

• existential_ (φ', (92b)): ∃_t[C̄(t)][∃x(fireman(x) ∧ tall(x,t))] "for some time t in C̄, there exists a fireman who is tall at t"
• generic_ (φ, (91b)): GEN_t[C̄(t)][∃x(fireman(x) ∧ tall(x,t))] "for generically all times t in C̄, there exists a fireman who is tall at t"

Homogeneity (70) rules out partialOnly: if fireman d is tall at any time, d is tall at ALL times within his lifespan.

Equations

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

theorem Magri2009.bps_existential_ilp_odd : bpsScenario.blindOdd BPSReading.existential_ = true

The ∃-BPS reading of ILP "Firemen are tall" is odd. Blind strengthening derives "∃ fireman tall at some times BUT no fireman tall throughout" — contradicting homogeneity (70).

theorem Magri2009.bps_generic_not_odd : bpsScenario.blindOdd BPSReading.generic_ = false

The GEN-BPS reading of ILP "Firemen are tall" is fine.

def Magri2009.bpsSLPScenario : BlindScenario BPSWorld BPSReading

Stage-level counterpart: ∃-BPS reading of "Firemen are available."

Same meaning structure, but all worlds CK-compatible because availability can genuinely vary over time (no homogeneity).

Equations

• Magri2009.bpsSLPScenario = { meaning := Magri2009.bpsScenario.meaning, alternatives := Magri2009.bpsScenario.alternatives, context := fun (x : Magri2009.BPSWorld) => true }

theorem Magri2009.bps_existential_slp_not_odd : bpsSLPScenario.blindOdd BPSReading.existential_ = false

The ∃-BPS reading of SLP "Firemen are available" is fine.

theorem Magri2009.bps_meaning_matches_qadverb (u : BPSReading) (w : BPSWorld) : bpsScenario.meaning u w = tallScenario.meaning (match u with | BPSReading.existential_ => QAdvUtt.sometimes_ | BPSReading.generic_ => QAdvUtt.always_) (match w with | BPSWorld.allThroughout => TallWorld.alwaysTall | BPSWorld.partialOnly => TallWorld.sometimesOnly | BPSWorld.noneTall => TallWorld.neverTall)

The BPS scenario's meaning table is isomorphic to the Q-adverb scenario: "∃-BPS at world w" has the same truth value as "sometimes at the corresponding Q-adverb world."

This is @cite{magri-2009}'s reduction (p. 275): "the existential reading of the BPS of sentence (84b) can be ruled out in exactly the same way as sentence (46a)."

theorem Magri2009.bps_context_matches_qadverb (w : BPSWorld) : bpsScenario.context w = tallScenario.context (match w with | BPSWorld.allThroughout => TallWorld.alwaysTall | BPSWorld.partialOnly => TallWorld.sometimesOnly | BPSWorld.noneTall => TallWorld.neverTall)

The context functions match: homogeneity rules out the same "mixed" world in both scenarios.

Universal quantifier rescue

@cite{magri-2009} §4.3, building on @cite{fox-1995}: the ∃-BPS reading of an i-predicate becomes available when the BP is embedded under a universal quantifier.

• (102a) "Jewish women are related to Chomsky" — no ∃ reading
• (102b) "Jewish women are related to every Jewish man" — ∃ reading available

In (102b) the existential over Jewish women takes wide scope over both the generic operator AND the universal quantifier every Jewish man. This creates a "distributed witnesses" world — woman a₁ related to man b₁, a₂ to b₂ — where EXH(φ) = φ ∧ ¬ψ is satisfiable.

Under homogeneity, "related" is permanent: once a₁ is related to b₁, she always is. But this doesn't prevent different women from being related to different men. The distributed-witnesses world is CK-compatible, so the strengthened meaning is not vacuous at CK worlds → not odd.

The structural insight: the rescue scenario has the SAME context as the stage-level scenario (all worlds CK-compatible), despite a different reason. For SLPs, variability over time admits the mixed world. For universal embedding, distributed witnesses admit the mixed world. @cite{magri-2009}'s mechanism produces the correct prediction in both cases: the mixed world survives in CK.

def Magri2009.universalRescueScenario : BlindScenario TallWorld QAdvUtt

@cite{magri-2009} §4.3: universal quantifier rescue of ∃-BPS reading.

The meaning table matches the ⟨some, all⟩ pattern:

• sometimes_ (φ): "for every Jewish man, ∃ a related Jewish woman"
• always_ (ψ): "∃ a Jewish woman related to EVERY Jewish man"

The three worlds under the correspondence:

• alwaysTall → "concentrated": one woman related to all men (φ ∧ ψ)
• sometimesOnly → "distributed": different women for different men (φ ∧ ¬ψ)
• neverTall → "none": some man has no related woman (¬φ ∧ ¬ψ)

All worlds are CK-compatible because homogeneity for "related" (each woman-man relationship is permanent) is compatible with distributed witnesses.

Equations

• Magri2009.universalRescueScenario = { meaning := Magri2009.tallScenario.meaning, alternatives := Magri2009.tallScenario.alternatives, context := fun (x : Magri2009.TallWorld) => true }

theorem Magri2009.universal_rescue_not_odd : universalRescueScenario.blindOdd QAdvUtt.sometimes_ = false

The ∃-BPS reading under a universal quantifier is NOT odd. The distributed-witnesses world is CK-compatible, so the strengthened meaning is satisfiable at a CK world.

theorem Magri2009.rescue_shares_semantics : tallScenario.meaning = universalRescueScenario.meaning ∧ tallScenario.alternatives = universalRescueScenario.alternatives

The rescue scenario shares literal semantics and scale with the ILP Q-adverb scenario — the ONLY difference is the CK context.

theorem Magri2009.rescue_context_equals_slp : universalRescueScenario.context = availableScenario.context

The rescue context matches the SLP context: both admit all worlds.

For SLPs: the predicate can genuinely vary over time → no worlds ruled out. For universal rescue: distributed witnesses are CK-compatible → no worlds ruled out. Different reasons, same abstract effect.

theorem Magri2009.three_way_contrast : tallScenario.meaning = availableScenario.meaning ∧ tallScenario.meaning = universalRescueScenario.meaning ∧ tallScenario.alternatives = availableScenario.alternatives ∧ tallScenario.alternatives = universalRescueScenario.alternatives ∧ tallScenario.blindOdd QAdvUtt.sometimes_ = true ∧ availableScenario.blindOdd QAdvUtt.sometimes_ = false ∧ universalRescueScenario.blindOdd QAdvUtt.sometimes_ = false ∧ tallScenario.context TallWorld.sometimesOnly = false ∧ availableScenario.context TallWorld.sometimesOnly = true ∧ universalRescueScenario.context TallWorld.sometimesOnly = true

Three-way structural comparison:

Scenario	Context type	Mixed world CK?	Odd?
ILP Q-adverb	Homogeneity (70)	No	Yes
SLP Q-adverb	All worlds	Yes	No
ILP + ∀	All worlds	Yes	No

All three share the same meaning table and alternatives. Oddness is entirely determined by whether the context rules out the mixed world — as proved by oddness_iff_mixed_excluded.

BH_prs and MH_prs

@cite{magri-2009} extends BH and MH to presuppositions (§3.4, eqs. 64–66):

1. BH_prs (65): The strengthened presupposition EXH_prs(φ) is computed using logical entailment, not entailment given common knowledge.

2. MH_prs (66): If the blind strengthened presupposition contradicts common knowledge (EXH_prs(φ) ∩ W_ck = ∅), then φ sounds odd.

The strengthened presupposition mirrors standard EXH but operates on the presupposition dimension:

EXH_prs(φ) = φ_prs ∧ ∧_{ψ ∈ Excl_prs(φ)} ¬ψ_prs

where Excl_prs uses @cite{fox-2007}'s innocent exclusion applied to presuppositions. This reuses exhB/ieIndices directly — the same algorithm, applied to a different dimension of meaning.

structure Magri2009.BlindPresupScenario (W U : Type) [Fintype W] [DecidableEq W] extends Magri2009.BlindScenario W U : Type

A scenario with both meanings and presuppositions for blind SI computation.

@cite{magri-2009} §3.4: presupposition strengthening runs in parallel to meaning strengthening, using the same @cite{fox-2007} algorithm.

• meaning : U → W → Bool
• alternatives : U → List U
• context : W → Bool
• presup : U → W → Bool

  Presupposition carried by each utterance.

def Magri2009.BlindPresupScenario.strengthenedPresup {W U : Type} [Fintype W] [DecidableEq W] (s : BlindPresupScenario W U) (u : U) (w : W) : Bool

Strengthened presupposition via @cite{fox-2007}'s EXH applied to presuppositions.

Implements BH_prs: the strengthening uses logical entailment over W, not entailment given common knowledge.

Equations

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

def Magri2009.BlindPresupScenario.blindOddPrs {W U : Type} [Fintype W] [DecidableEq W] (s : BlindPresupScenario W U) (u : U) : Bool

Blind presuppositional oddness: EXH_prs(φ) ∩ W_ck = ∅.

Implements MH_prs (66): if the blind strengthened presupposition contradicts common knowledge, the sentence sounds odd.

Equations

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

"#John is always tall" via presuppositional mismatch

@cite{magri-2009} §4.6: always and covert GEN are Horn-mates with the same denotation but different presuppositions. Overt always carries no homogeneity presupposition; covert GEN carries the homogeneity presupposition (eq. (137)): either ALL atomic parts of the restrictor satisfy the scope or NONE do (YES ∪ NO).

The oddness of "#John is always tall" is derived via MH_prs (66):

1. φ_prs (always) = W (trivial presupposition)
2. ψ_prs (GEN) = YES ∪ NO (homogeneity presupposition)
3. ψ_prs asymmetrically entails φ_prs (YES ∪ NO ⊂ W)
4. EXH_prs(φ) = φ_prs ∧ ¬ψ_prs = ¬(YES ∪ NO) = mixed worlds only
5. CK (from assumption (70)): W_ck = YES ∪ NO (homogeneity for ILPs)
6. EXH_prs(φ) ∩ W_ck = ∅ → odd via MH_prs

The contrast with "John is tall" (= covert GEN): GEN has no stronger presuppositional alternative, so EXH_prs is vacuous and no mismatch arises.

The reuse of TallWorld is structural: the three worlds — alwaysTall, sometimesOnly, neverTall — serve double duty across meaning (§5) and presupposition (§10).

inductive Magri2009.AlwaysGENUtt : Type

Utterance type for the ⟨always, GEN⟩ Horn scale.

• always_ : AlwaysGENUtt
• gen_ : AlwaysGENUtt

@[implicit_reducible]

instance Magri2009.instDecidableEqAlwaysGENUtt : DecidableEq AlwaysGENUtt

Equations

• Magri2009.instDecidableEqAlwaysGENUtt x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Magri2009.instReprAlwaysGENUtt : Repr AlwaysGENUtt

Equations

• Magri2009.instReprAlwaysGENUtt = { reprPrec := Magri2009.instReprAlwaysGENUtt.repr }

def Magri2009.instReprAlwaysGENUtt.repr : AlwaysGENUtt → ℕ → Std.Format

Equations

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

def Magri2009.alwaysGENScenario : BlindPresupScenario TallWorld AlwaysGENUtt

@cite{magri-2009} §4.6: always vs covert GEN.

The two utterances have IDENTICAL denotation (both mean "at all times, John is tall") but DIFFERENT presuppositions:

• always: φ_prs = W (no homogeneity presupposition)
• GEN: ψ_prs = {alwaysTall, neverTall} (homogeneity: YES ∪ NO)

Equations

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

theorem Magri2009.gen_presup_matches_context (w : TallWorld) : alwaysGENScenario.presup AlwaysGENUtt.gen_ w = alwaysGENScenario.context w

GEN's presupposition matches homogeneity: the same predicate as the CK context. This is not coincidence — assumption (70) says W_ck is exactly the set of homogeneous worlds, and GEN presupposes homogeneity.

theorem Magri2009.always_presup_trivial (w : TallWorld) : alwaysGENScenario.presup AlwaysGENUtt.always_ w = true

always has trivial (universal) presupposition.

theorem Magri2009.always_strengthened_presup_false_at_ck : alwaysGENScenario.strengthenedPresup AlwaysGENUtt.always_ TallWorld.alwaysTall = false ∧ alwaysGENScenario.strengthenedPresup AlwaysGENUtt.always_ TallWorld.neverTall = false

The strengthened presupposition of always asserts ¬(YES ∪ NO), i.e., that there ARE mixed worlds — which is exactly what homogeneity rules out.

theorem Magri2009.always_tall_blind_odd_prs : alwaysGENScenario.blindOddPrs AlwaysGENUtt.always_ = true

@cite{magri-2009} §4.6: "#John is always tall" is odd via MH_prs.

The blind strengthened presupposition (= ¬homogeneity = mixed worlds only) contradicts CK (= homogeneity = no mixed worlds).

theorem Magri2009.gen_tall_not_odd_prs : alwaysGENScenario.blindOddPrs AlwaysGENUtt.gen_ = false

"John is tall" (= covert GEN) is NOT odd via MH_prs.

GEN has no stronger presuppositional alternative — always is presuppositionally weaker (trivial presupposition ⊂ homogeneity presupposition is backwards). Since GEN's presupposition entails always's, always is not excludable w.r.t. GEN.

theorem Magri2009.always_gen_same_meaning_different_presup : alwaysGENScenario.meaning AlwaysGENUtt.always_ = alwaysGENScenario.meaning AlwaysGENUtt.gen_ ∧ alwaysGENScenario.presup AlwaysGENUtt.always_ ≠ alwaysGENScenario.presup AlwaysGENUtt.gen_ ∧ alwaysGENScenario.blindOddPrs AlwaysGENUtt.always_ ≠ alwaysGENScenario.blindOddPrs AlwaysGENUtt.gen_

Meanings are identical but oddness differs — the presupposition is doing ALL the work. This is a pure presuppositional effect: the same mechanism (BH + MH) applied to a different dimension of meaning.

Predictions match empirical BPS data

@cite{magri-2009}'s theory predicts that individual-level predicates block the existential reading of bare plural subjects. The data in Phenomena.Generics.BarePlurals independently records these judgments as empirical observations (@cite{cohen-erteschik-shir-2002}).

The bridge theorems verify that every ILP datum with existentialOK = false is correctly predicted by the BH+MH mechanism, and every SLP-with-locative-argument datum with existentialOK = true is correctly predicted as non-odd.

theorem Magri2009.ilp_data_matches_magri_prediction : (Phenomena.Generics.BarePlurals.iLevelData.all fun (d : Phenomena.Generics.BarePlurals.BarePluralDatum) => d.predicateLevel == Semantics.Kinds.SortedOntology.PredicateLevel.individualLevel && !d.existentialOK) = true

All individual-level predicates in the BarePlurals data lack the existential reading — matching @cite{magri-2009}'s prediction that the ∃-BPS of an ILP is odd (BH + MH + homogeneity).

theorem Magri2009.slp_argument_data_matches_magri_prediction : (Phenomena.Generics.BarePlurals.sLevelArgumentData.all fun (d : Phenomena.Generics.BarePlurals.SLevelDatum) => d.predicateLevel == Semantics.Kinds.SortedOntology.PredicateLevel.stageLevel && d.existentialOK) = true

All stage-level predicates with locative arguments in the BarePlurals data HAVE the existential reading — matching @cite{magri-2009}'s prediction that the ∃-BPS of an SLP is fine (no homogeneity → no mismatch).

theorem Magri2009.magri_predicts_ilp_no_existential : bpsScenario.blindOdd BPSReading.existential_ = true ∧ (Phenomena.Generics.BarePlurals.iLevelData.all fun (d : Phenomena.Generics.BarePlurals.BarePluralDatum) => !d.existentialOK) = true

The BPS scenario for ILPs is odd, AND the ILP data independently confirms no existential reading. Cross-validation between theory (BH+MH) and empirical observation.

theorem Magri2009.magri_predicts_slp_existential : bpsSLPScenario.blindOdd BPSReading.existential_ = false ∧ (Phenomena.Generics.BarePlurals.sLevelArgumentData.all fun (d : Phenomena.Generics.BarePlurals.SLevelDatum) => d.existentialOK) = true

The BPS scenario for SLPs is fine, AND the SLP-argument data independently confirms existential reading available.

German BPS word order matches BH+MH predictions

@cite{magri-2009} §4.5 argues that @cite{diesing-1992}'s German BPS word order contrast (BPS left vs right of ja doch) follows from BH+MH:

• S-predicate BPS both positions OK → BH+MH: no mismatch (SLP)
• I-predicate BPS left only → BH+MH: right-of-ja doch = VP-internal = existential reading only → mismatch with homogeneity → odd

The data in Fragments.German.BarePluralWordOrder independently records this pattern. The bridge theorem confirms that the oddness pattern in the German data aligns with the model scenarios.

theorem Magri2009.german_data_matches_magri : (Fragments.German.BarePluralWordOrder.allJaDochData.all fun (d : Fragments.German.BarePluralWordOrder.JaDochDatum) => d.acceptable == !(d.predicateLevel == Semantics.Kinds.SortedOntology.PredicateLevel.individualLevel && d.bpsPosition == Fragments.German.BarePluralWordOrder.BPSPosition.rightOfJaDoch)) = true ∧ bpsScenario.blindOdd BPSReading.existential_ = true ∧ bpsSLPScenario.blindOdd BPSReading.existential_ = false

The German ja doch data confirms the same ILP/SLP split: the ONLY unacceptable configuration is ILP + right of ja doch (= VP-internal = existential-only reading).

• ILP right of ja doch → odd: matches bpsScenario.blindOdd .existential_
• SLP both positions → fine: matches bpsSLPScenario.blindOdd .existential_
• ILP left of ja doch → fine: the GEN reading is available (not blocked)

"Firemen are always tall" is fine (§4.6.2 Remark)

@cite{magri-2009} §4.6.2: "#John is always tall" is odd (§10 above), but "Firemen are always tall" is FINE when the definite John is replaced by a bare plural.

The key difference: with a bare plural subject, the strengthened presupposition ¬ψ_prs asserts that homogeneity fails for the restrictor (some firemen are tall, others aren't). This is NOT a contradiction given common knowledge — there are CK-compatible worlds where some firemen are tall and others aren't.

This shows the presuppositional mechanism is sensitive to the logical form of the subject: definite subjects (John) produce oddness because homogeneity must hold for a single individual; bare plural subjects (firemen) don't because different individuals can differ.

inductive Magri2009.BPAlwaysWorld : Type

Worlds for "Firemen are always tall" with bare plural subject.

With a bare plural, the homogeneity presupposition of GEN quantifies over firemen: either ALL firemen are tall or NONE are. But CK for a bare plural does NOT rule out mixed worlds (some tall, some not).

• allTall : BPAlwaysWorld
• mixedFiremen : BPAlwaysWorld
• noneTall : BPAlwaysWorld

@[implicit_reducible]

instance Magri2009.instDecidableEqBPAlwaysWorld : DecidableEq BPAlwaysWorld

Equations

• Magri2009.instDecidableEqBPAlwaysWorld x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Magri2009.instReprBPAlwaysWorld : Repr BPAlwaysWorld

Equations

• Magri2009.instReprBPAlwaysWorld = { reprPrec := Magri2009.instReprBPAlwaysWorld.repr }

def Magri2009.instReprBPAlwaysWorld.repr : BPAlwaysWorld → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Magri2009.instFintypeBPAlwaysWorld : Fintype BPAlwaysWorld

Equations

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

def Magri2009.bpAlwaysScenario : BlindPresupScenario BPAlwaysWorld AlwaysGENUtt

@cite{magri-2009} §4.6.2: always vs GEN with bare plural subject.

Meanings are identical (both: "all firemen are always tall"), but presuppositions differ. GEN's homogeneity presupposition says either all firemen are tall or none are (YES ∪ NO). But with a bare plural, the mixed world (some tall, some not) IS CK-compatible.

Equations

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

theorem Magri2009.bp_always_not_odd_prs : bpAlwaysScenario.blindOddPrs AlwaysGENUtt.always_ = false

"Firemen are always tall" is NOT odd via MH_prs.

The strengthened presupposition ¬ψ_prs = {mixedFiremen} is satisfiable at a CK world (mixedFiremen is CK-compatible for bare plurals), so MH_prs does not fire.

theorem Magri2009.definite_vs_bp_always_contrast : alwaysGENScenario.blindOddPrs AlwaysGENUtt.always_ = true ∧ bpAlwaysScenario.blindOddPrs AlwaysGENUtt.always_ = false

Contrast: same logical structure, different subjects, different oddness.

• "#John is always tall" (definite): odd via MH_prs (§10)
• "Firemen are always tall" (bare plural): fine (§4.6.2)

The difference: CK for a definite (John) rules out the mixed world (homogeneity for one individual), while CK for a bare plural does not (different firemen can differ).

@[implicit_reducible]

instance Magri2009.instAlternativeSourceItalyUtt : Alternatives.AlternativeSource ItalyUtt

AlternativeSource instance for the Italian ⟨some, all⟩ scale.

Equations

• Magri2009.instAlternativeSourceItalyUtt = { alternatives := fun (x : Magri2009.ItalyUtt) => [Magri2009.ItalyUtt.some_, Magri2009.ItalyUtt.all_] }

theorem Magri2009.strengthened_eq_alternativeSource (w : ItalyWorld₃) : italianScenario.strengthened ItalyUtt.some_ w = decide (w ∈ Exhaustification.innocent.exh (Exhaustification.altsFromPreds (List.map italianScenario.meaning (Alternatives.AlternativeSource.alternatives ItalyUtt.some_))) (Exhaustification.predToFinset (italianScenario.meaning ItalyUtt.some_)))

Exhaustifying via AlternativeSource agrees with BlindScenario.strengthened.

BlindScenario carries its own alternatives field; here we show that deriving alternatives from the AlternativeSource typeclass produces the same exhaustified meaning. The key: including the assertion in the alternative list (AlternativeSource convention) doesn't change the result — exhIE filters it out via the non-weaker check.

Bridge: blind SI as Implicature W Prop

Wraps a BlindScenario-derived strengthened meaning as an Implicature value over the same world type, exercising the cross-mechanism spine in Theories/Pragmatics/Implicature/Defs.lean. The Bool-valued strengthening becomes a Prop-valued implicature content via s.strengthened u w = true.

Why NOT a non-cancellability theorem

The @cite{magri-2009} obligatoriness claim does not translate cleanly into Implicature.IsCancellable failure, even CK-relativized. For "#Some Italians come from a warm country" with CK = {allWarm}, "in fact all" is a consistent continuation at the CK world that contradicts the EXH'd implicature — so IsCancellable (and IsCancellableInContext) both hold. The contentful Magri claim is a different diagnostic: the strengthened meaning has no CK-realizer. That is the theorem delivered here. See Theories/Pragmatics/Implicature/Diagnostics.lean docstring for the extended discussion of why Magri obligatoriness ≠ IsCancellable failure.

def Magri2009.magriToImplicature {W U : Type} [Fintype W] [DecidableEq W] (s : BlindScenario W U) (u : U) : Implicature W Prop

Wrap a BlindScenario-derived strengthened meaning as an Implicature W Prop. The content is s.strengthened u · = true (the EXH'd meaning at each world); the mechanism is .exhIE — @cite{magri-2009} uses Fox's innocent-exclusion operator only (innocent.exh in Theories/Semantics/Exhaustification/Excluder.lean, implementing @cite{fox-2007}'s IE algorithm), not the Bar-Lev–Fox 2020 IE+II extension that postdates the paper by 11 years.

Equations

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

theorem Magri2009.magri_blindOdd_no_ck_realizer {W U : Type} [Fintype W] [DecidableEq W] (s : BlindScenario W U) (u : U) (h : s.blindOdd u = true) : ¬∃ (w : W), s.context w = true ∧ (magriToImplicature s u).content w

Magri's mismatch consequence, restated against the implicature spine. When EXH is applied to φ blind to CK (@cite{magri-2009} §3.2.2 eq. (32), the Blindness Hypothesis), and the resulting strengthened meaning has no CK-realizer (eq. (33), the Mismatch Hypothesis), then the wrapped implicature's content has no CK-compatible realizer.

The deviance @cite{magri-2009} predicts is not Sadock truth-conditional non-cancellability — for the "Some Italians" example, the continuation "in fact all" IS truth-conditionally consistent with the literal "some" and DOES contradict the EXH'd "not all" implicature, so IsCancellable holds. The load-bearing premise is @cite{magri-2009} §3.2.5 eq. (41) "EXH is mandatory in matrix clauses" combined with the R-postulates (43a)/(43b): the speaker is grammatically committed to the SI even when uttering a cancellation continuation, and this commitment is what creates the deviance. The mandatoriness machinery is formalized below in RelevantBlindScenario; this theorem only states the outcome (eq. (33) antecedent) translated to the implicature spine.