Probabilities and Logic in Implicature Computation

@cite{denic-2023}

Denić, M. (2023). Probabilities and logic in implicature computation: Two puzzles with embedded disjunction. Semantics and Pragmatics 16, Article 4: 1–48.

Two Puzzles

Inference puzzle (§2): Quantified sentences with embedded disjunction trigger inferences sensitive to (i) the cardinality of the restrictor and (ii) the number of disjuncts:

• ALL-20-OR ("All 20 of Mary's friends are French or Spanish") preferably triggers distributive inferences (at least one is French, at least one is Spanish)
• ALL-2-OR ("Both of Mary's friends are French or Spanish") preferably triggers ignorance inferences (speaker is ignorant about whether at least one is French/Spanish)

This contrast is surprising: the two sentences stand in identical entailment relations to their alternatives, so any entailment-based theory (@cite{fox-2007} exhaustification, neo-Gricean) predicts the same implicatures for both.

Deviance puzzle (§5–6): Certain sentences with embedded disjunction under universal quantifiers are deviant:

• "#Each of these three girls is Mary, Susan, or Jane" (DEVIANT-BE)
• "Each of those three girls is called Mary, Susan, or Jane" (fine)

The key property: the identity copula + proper name is singleton- denoting (given CK, only one individual can be Mary), while "is called" is not. Deviance arises because ignorance inferences of singleton- denoting predicates contradict common knowledge — extending @cite{magri-2009}'s blindness hypothesis.

Proposal

Two components:

1. Informativeness-based pruning (§4, proposal (30)): Alternative pruning is sensitive to probabilistic informativeness — the probability of pruning alternative A from ALT(S) increases with P(A|S). This is in addition to contextual relevance (@cite{fox-katzir-2011}).

2. Blind informativeness (§7.3): The informativeness computation that feeds pruning is blind to (most of) common knowledge — only logical structure (domain size, number of disjuncts) matters.

Key connections

• @cite{fox-2007}: innocent exclusion (IE) algorithm — innocent.exh, innocent.excluded, IsMCSet from Innocent.lean
• @cite{magri-2009}: blindness hypothesis + mismatch hypothesis — BlindScenario, blindOdd from Magri2009.lean
• @cite{fox-katzir-2011}: contextual constraint on alternatives
• @cite{franke-2011}: IBR = exhMW result (inherits the puzzle)
• @cite{chierchia-2004}: embedded scalar items and disjunction

inductive Denic2023.InferenceType : Type

The two inference types that embedded disjunction can trigger.

@cite{denic-2023} §2: the central empirical observation is that the same sentence structure preferably triggers different inference types depending on domain size and disjunct count.

• distributive : InferenceType

  Distributive: "at least one is A, at least one is B." Derived when existential alternatives are pruned from ALT.

• ignorance : InferenceType

  Ignorance: "the speaker is ignorant about whether at least one is A (B)." Derived when existential alternatives remain in ALT.

@[implicit_reducible]

instance Denic2023.instDecidableEqInferenceType : DecidableEq InferenceType

Equations

• Denic2023.instDecidableEqInferenceType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Denic2023.instReprInferenceType.repr : InferenceType → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Denic2023.instReprInferenceType : Repr InferenceType

Equations

• Denic2023.instReprInferenceType = { reprPrec := Denic2023.instReprInferenceType.repr }

structure Denic2023.InferenceDatum : Type

An empirical datum from @cite{denic-2023} §2.

• label : String

  Human-readable label.

• restrictorSize : ℕ

  Cardinality of the restrictor of the universal quantifier.

• disjunctCount : ℕ

  Number of disjuncts.

• preferred : InferenceType

  The preferably triggered inference type.

def Denic2023.instReprInferenceDatum.repr : InferenceDatum → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Denic2023.instReprInferenceDatum : Repr InferenceDatum

Equations

• Denic2023.instReprInferenceDatum = { reprPrec := Denic2023.instReprInferenceDatum.repr }

def Denic2023.all20or : InferenceDatum

ALL-20-OR: "All 20 of Mary's friends are French or Spanish." @cite{denic-2023} ex. (6): preferably triggers distributive inferences.

Equations

• Denic2023.all20or = { label := "ALL-20-OR", restrictorSize := 20, disjunctCount := 2, preferred := Denic2023.InferenceType.distributive }

def Denic2023.all2or : InferenceDatum

ALL-2-OR: "Both of Mary's friends are French or Spanish." @cite{denic-2023} ex. (7): preferably triggers ignorance inferences.

Equations

• Denic2023.all2or = { label := "ALL-2-OR", restrictorSize := 2, disjunctCount := 2, preferred := Denic2023.InferenceType.ignorance }

def Denic2023.simpleDisj : InferenceDatum

SIMPLE-DISJ: "All four of Mary's friends are French or Spanish." @cite{denic-2023} ex. (8): distributive more natural than COMPLEX-DISJ.

Equations

• Denic2023.simpleDisj = { label := "SIMPLE-DISJ", restrictorSize := 4, disjunctCount := 2, preferred := Denic2023.InferenceType.distributive }

def Denic2023.complexDisj : InferenceDatum

COMPLEX-DISJ: "All four of Mary's friends are French, Spanish, German, or Dutch." @cite{denic-2023} ex. (9): ignorance more natural than SIMPLE-DISJ.

Equations

• Denic2023.complexDisj = { label := "COMPLEX-DISJ", restrictorSize := 4, disjunctCount := 4, preferred := Denic2023.InferenceType.ignorance }

def Denic2023.inferencePuzzleData : List InferenceDatum

The four key data points from @cite{denic-2023} §2.

Equations

• Denic2023.inferencePuzzleData = [Denic2023.all20or, Denic2023.all2or, Denic2023.simpleDisj, Denic2023.complexDisj]

def Denic2023.thresholdPrediction (T : ℕ) (d : InferenceDatum) : InferenceType

Threshold generalization (@cite{denic-2023} (10)): when the ratio of restrictor cardinality to disjunct count exceeds a threshold T ≥ 1, distributive inferences are preferably derived.

Equations

• Denic2023.thresholdPrediction T d = if d.restrictorSize / d.disjunctCount ≥ T then Denic2023.InferenceType.distributive else Denic2023.InferenceType.ignorance

def Denic2023.ratio (d : InferenceDatum) : ℕ

Gradient generalization (@cite{denic-2023} (11)): the larger the ratio of restrictor to disjuncts, the greater the preference for distributive over ignorance.

Equations

• Denic2023.ratio d = d.restrictorSize / d.disjunctCount

theorem Denic2023.ratio_ordering : ratio all20or > ratio simpleDisj ∧ ratio simpleDisj > ratio all2or ∧ ratio all2or = ratio complexDisj

The ratio ordering matches the inference pattern: ALL-20-OR (ratio 10) > SIMPLE-DISJ (ratio 2) > ALL-2-OR = COMPLEX-DISJ (ratio 1). Higher ratio → distributive; lower ratio → ignorance.

theorem Denic2023.threshold_2_correct : (inferencePuzzleData.all fun (d : InferenceDatum) => thresholdPrediction 2 d == d.preferred) = true

The threshold generalization with T = 2 correctly classifies all four data points.

Why entailment-based theories fail

@cite{denic-2023} §3.2–3.4: ALL-20-OR and ALL-2-OR activate the same structural alternatives (up to domain-size relabeling). Since entailment relations between a sentence and its alternatives are invariant under domain size, any approach where implicatures are a function of entailment relations (@cite{fox-2007} exhaustification, neo-Gricean) predicts identical inferences.

The unembedded baseline (disjunction without universal quantifier) is handled in InnocentExclusion.lean: disj_exh_eq_exor shows Exh(Alt)(p∨q) = p ⊻ q. The puzzle arises specifically when disjunction is embedded under a universal quantifier.

inductive Denic2023.GroupWorld : Type

Worlds for ALL-n-OR with 2 disjuncts (French, Spanish).

For the entailment structure, only the proportions matter, not individual assignments. We model the 4 possible group compositions.

• allFrench : GroupWorld

  All are French (and possibly Spanish).

• allSpanish : GroupWorld

  All are Spanish (and possibly French).

• mixed : GroupWorld

  Mixed: some French, some Spanish, satisfying both ∃ constraints.

• allBoth : GroupWorld

  All are French AND Spanish (bilingual).

@[implicit_reducible]

instance Denic2023.instDecidableEqGroupWorld : DecidableEq GroupWorld

Equations

• Denic2023.instDecidableEqGroupWorld x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Denic2023.instReprGroupWorld : Repr GroupWorld

Equations

• Denic2023.instReprGroupWorld = { reprPrec := Denic2023.instReprGroupWorld.repr }

def Denic2023.instReprGroupWorld.repr : GroupWorld → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Denic2023.instFintypeGroupWorld : Fintype GroupWorld

Equations

• Denic2023.instFintypeGroupWorld = { elems := { val := ↑Denic2023.GroupWorld.enumList, nodup := Denic2023.GroupWorld.enumList_nodup }, complete := Denic2023.instFintypeGroupWorld._proof_1 }

theorem Denic2023.altOr_both_ie : Exhaustification.innocent.excluded (Exhaustification.altsFromPreds Denic2023.altOr✝) (Exhaustification.predToFinset Denic2023.allForS✝) = Exhaustification.altsFromPreds Denic2023.altOr✝

With ALT-or, both alternatives are IE: each can be negated consistently with the prejacent. Negating both yields distributive inferences: "some are French, some are Spanish."

theorem Denic2023.altOr_exh_distributive : Exhaustification.innocent.exh (Exhaustification.altsFromPreds Denic2023.altOr✝) (Exhaustification.predToFinset Denic2023.allForS✝) = {GroupWorld.mixed}

The exhaustified meaning with ALT-or: "All are F∨S, NOT all French, NOT all Spanish" — true only at mixed, the distributive reading where some are French AND some are Spanish.

This connects to Spector2016.disj_exh_eq_exor (unembedded disjunction yields exclusive or); embedding under ∀ + domain structure gives the distributive reading.

theorem Denic2023.altAllOr_no_ie : Exhaustification.innocent.excluded (Exhaustification.altsFromPreds Denic2023.altAllOr✝) (Exhaustification.predToFinset Denic2023.allForS✝) = ∅

With ALT-all-or, NO alternative is IE: three different maximal consistent exclusions exist, and no alternative appears in all three. Result: no distributive inferences; ignorance inferences are derived.

Note: this is a distinct mechanism from symmetric_not_ie in Symmetric.lean. The alternatives here are NOT symmetric in the @cite{fox-katzir-2011} partition sense (see altAllOr_not_symmetric below) — the IE emptiness arises from the MCE structure, not from alternative pairs partitioning the prejacent.

theorem Denic2023.altAllOr_exh_vacuous : Exhaustification.innocent.exh (Exhaustification.altsFromPreds Denic2023.altAllOr✝) (Exhaustification.predToFinset Denic2023.allForS✝) = Exhaustification.predToFinset Denic2023.allForS✝

IE collapse for ALT-all-or: with three incompatible maximal consistent exclusions (@cite{denic-2023} (26a–c)), no alternative survives in every MC-set. Consequently exhIE returns the prejacent unchanged — exhaustification is vacuous.

The MCEs in Denić's notation are

• {allS, someS}: negate → all French
• {allF, someF}: negate → all Spanish
• {allF, allS}: negate → mixed

No proposition appears in all three → IE = {prejacent} → exhIE = prejacent.

theorem Denic2023.altAllOr_not_symmetric : Alternatives.Symmetric.isSymmetric [GroupWorld.allFrench, GroupWorld.allSpanish, GroupWorld.mixed, GroupWorld.allBoth] Denic2023.allForS✝ Denic2023.someFrenchAlt✝ Denic2023.someSpanishAlt✝ = false ∧ Alternatives.Symmetric.isSymmetric [GroupWorld.allFrench, GroupWorld.allSpanish, GroupWorld.mixed, GroupWorld.allBoth] Denic2023.allForS✝ Denic2023.allFrenchAlt✝ Denic2023.allSpanishAlt✝ = false

The existential alternatives ("some are French" / "some are Spanish") are NOT symmetric in the @cite{fox-katzir-2011} sense: they overlap at mixed and allBoth worlds (both alternatives true), so they do not partition the prejacent's denotation.

This matters because it means the IE emptiness (above) cannot be derived from Symmetric.symmetric_not_ie — it requires the full MCE computation showing three incompatible exclusion sets.

theorem Denic2023.entailment_invariant_across_domain_size : Exhaustification.innocent.excluded (Exhaustification.altsFromPreds Denic2023.altOr✝) (Exhaustification.predToFinset Denic2023.allForS✝) = Exhaustification.altsFromPreds Denic2023.altOr✝ ∧ Exhaustification.innocent.excluded (Exhaustification.altsFromPreds Denic2023.altAllOr✝) (Exhaustification.predToFinset Denic2023.allForS✝) = ∅

The core negative result: the IE computation is identical for any domain size when the same abstract alternative structure is used.

The 4-world model above is domain-size-invariant: it captures the entailment structure of both ALL-20-OR and ALL-2-OR. The alternatives stand in the same entailment relations regardless of whether n = 2 or n = 20. Therefore, the IE set — and hence the predicted implicatures — are identical.

This is @cite{denic-2023}'s argument in §3.2 (final paragraph): "ALL-20-OR and ALL-2-OR activate comparable sets of alternatives, [so] they stand in the same entailment relations to them, and will thus necessarily be predicted to have the same implicatures."

Since @cite{franke-2011}'s IBR converges to exhMW for scalar games (ibr_equals_exhMW in ScalarGames.lean), IBR inherits the same inability to distinguish ALL-20-OR from ALL-2-OR.

Informativeness-based alternative pruning

@cite{denic-2023} proposal (30): the probability of pruning alternative A from ALT(S) increases with P(A|S) — the conditional probability that A is true given S. Informativeness is inversely related: the more likely A is given S (the less informative A is relative to S), the more likely A is to be pruned.

The key insight: P(Some of n are A | All n are A or B) increases with n, because having more individuals makes it more likely that at least one satisfies A. So existential alternatives are more likely pruned for larger domains, yielding ALT-or (→ distributive) for ALL-20-OR and ALT-all-or (→ ignorance) for ALL-2-OR.

We make this precise using the uniform conditional probability model: P(∃x. A(x) | ∀x. disjunction of m predicates) = 1 − ((m−1)/m)^n.

def Denic2023.uniformCondProb (n m : ℕ) : ℚ

Conditional probability P(∃x∈D. A(x) | ∀x∈D. A(x)∨B₁(x)∨...∨Bₘ₋₁(x)) under uniform independent assignment to m equally likely predicates.

With m predicates and n individuals independently assigned, each individual is assigned to A with probability 1/m, so:

• P(no individual is A) = ((m−1)/m)^n
• P(∃x. A(x)) = 1 − ((m−1)/m)^n

@cite{denic-2023} §4: the critical observation is that this probability increases with n (more individuals → more likely someone is A) and decreases with m (more disjuncts → less likely any given one holds).

Equations

• Denic2023.uniformCondProb n m = 1 - (↑(↑m - 1) / ↑↑m) ^ n

theorem Denic2023.condProb_values : uniformCondProb 20 2 = ↑1048575 / 1048576 ∧ uniformCondProb 4 2 = ↑15 / 16 ∧ uniformCondProb 2 2 = ↑3 / 4 ∧ uniformCondProb 4 4 = ↑175 / 256

Conditional probability values for the four data points.

• ALL-20-OR (n=20, m=2): 1 − (1/2)²⁰ = 1048575/1048576
• SIMPLE-DISJ (n=4, m=2): 1 − (1/2)⁴ = 15/16
• ALL-2-OR (n=2, m=2): 1 − (1/2)² = 3/4
• COMPLEX-DISJ (n=4, m=4): 1 − (3/4)⁴ = 175/256

Higher condProb → more pruning → more likely distributive. Lower condProb → less pruning → more likely ignorance.

theorem Denic2023.condProb_ordering : uniformCondProb 20 2 > uniformCondProb 4 2 ∧ uniformCondProb 4 2 > uniformCondProb 2 2 ∧ uniformCondProb 2 2 > uniformCondProb 4 4

The conditional probability ordering matches the inference pattern: ALL-20-OR > SIMPLE-DISJ > ALL-2-OR > COMPLEX-DISJ.

Distributive sentences have higher condProb (existential alternatives are less informative, more likely pruned); ignorance sentences have lower condProb (existential alternatives are more informative, less likely pruned).

Any pruning threshold between 175/256 ≈ 0.68 and 3/4 = 0.75 correctly classifies all four data points.

theorem Denic2023.domain_size_distinguishes : all20or.restrictorSize > all2or.restrictorSize ∧ all20or.preferred = InferenceType.distributive ∧ all2or.preferred = InferenceType.ignorance

The proposal correctly predicts the ALL-20-OR vs ALL-2-OR contrast.

Under the uniform model, existential alternatives are more likely pruned for ALL-20-OR (condProb ≈ 1) than ALL-2-OR (condProb = 3/4):

• ALL-20-OR: existentials likely pruned → ALT-or → distributive ✓
• ALL-2-OR: existentials likely retained → ALT-all-or → ignorance ✓

theorem Denic2023.disjunct_count_distinguishes : complexDisj.disjunctCount > simpleDisj.disjunctCount ∧ simpleDisj.restrictorSize = complexDisj.restrictorSize ∧ simpleDisj.preferred = InferenceType.distributive ∧ complexDisj.preferred = InferenceType.ignorance

The proposal correctly predicts the SIMPLE-DISJ vs COMPLEX-DISJ contrast.

Under the uniform model, existential alternatives are more likely pruned for SIMPLE-DISJ (condProb = 15/16) than COMPLEX-DISJ (condProb = 175/256):

• SIMPLE-DISJ: existentials likely pruned → ALT-or → distributive ✓
• COMPLEX-DISJ: existentials likely retained → ALT-all-or → ignorance ✓

Singleton-denoting predicates and deviance

@cite{denic-2023} §5: a predicate (in context) is singleton-denoting if, given common knowledge, it can only be true of a unique individual.

• "is Mary" is singleton-denoting: CK says only one person IS Mary
• "is called Mary" is NOT singleton-denoting: multiple people can be called Mary

Deviance arises when ignorance inferences of singleton-denoting predicates contradict CK. This extends @cite{magri-2009}'s blind oddness mechanism.

def Denic2023.singletonDenoting {α : Type} (predDomain : List α) (predicate context : α → Bool) : Bool

Whether a predicate is singleton-denoting in context.

@cite{denic-2023} §5: a (complex) predicate is singleton-denoting if, given common knowledge, it can only be true of a unique (singular or plural) individual. Examples:

• "is Mary" + domain of individuals → singleton-denoting
• "wrote Anna Karenina" + domain of authors → singleton-denoting
• "is called Mary" + domain of individuals → NOT singleton-denoting
• "read Anna Karenina" + domain of students → NOT singleton-denoting

Equations

• Denic2023.singletonDenoting predDomain predicate context = decide ((List.filter predicate (List.filter context predDomain)).length ≤ 1)

@[implicit_reducible]

instance Denic2023.instDecidableEqGirl : DecidableEq Denic2023.Girl✝

Equations

• Denic2023.instDecidableEqGirl x✝ y✝ = if h : Denic2023.Girl.ctorIdx✝ x✝ = Denic2023.Girl.ctorIdx✝ y✝ then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Denic2023.instFintypeGirl : Fintype Denic2023.Girl✝

Equations

• Denic2023.instFintypeGirl = { elems := { val := ↑Denic2023.Girl.enumList✝, nodup := Denic2023.Girl.enumList_nodup✝ }, complete := Denic2023.instFintypeGirl._proof_1 }

theorem Denic2023.isMary_singleton : singletonDenoting Denic2023.girls✝ Denic2023.isMary✝ Denic2023.allGirls✝ = true

Identity predicates ("is Mary") are singleton-denoting.

theorem Denic2023.isSusan_singleton : singletonDenoting Denic2023.girls✝ Denic2023.isSusan✝ Denic2023.allGirls✝ = true

theorem Denic2023.isCalledMary_not_singleton : singletonDenoting Denic2023.girls✝ Denic2023.isCalledMary✝ Denic2023.allGirls✝ = false

"Is called" predicates are NOT singleton-denoting.

structure Denic2023.DevianceDatum : Type

A deviance datum from @cite{denic-2023} §5.

• label : String
• isDeviant : Bool
• isSingletonDenoting : Bool

def Denic2023.instReprDevianceDatum.repr : DevianceDatum → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Denic2023.instReprDevianceDatum : Repr DevianceDatum

Equations

• Denic2023.instReprDevianceDatum = { reprPrec := Denic2023.instReprDevianceDatum.repr }

def Denic2023.deviantBe : DevianceDatum

DEVIANT-BE: "#Each of those three girls is Mary, Susan, or Jane." @cite{denic-2023} ex. (31).

Equations

• Denic2023.deviantBe = { label := "DEVIANT-BE", isDeviant := true, isSingletonDenoting := true }

def Denic2023.nonDeviantCalled : DevianceDatum

NON-DEVIANT-CALLED: "Each of those three girls is called Mary, Susan, or Jane." @cite{denic-2023} ex. (32).

Equations

• Denic2023.nonDeviantCalled = { label := "NON-DEVIANT-CALLED", isDeviant := false, isSingletonDenoting := false }

def Denic2023.deviantWrite : DevianceDatum

DEVIANT-WRITE: "#Each of those three writers wrote Anna Karenina, Germinal, or Harry Potter." @cite{denic-2023} ex. (33).

Equations

• Denic2023.deviantWrite = { label := "DEVIANT-WRITE", isDeviant := true, isSingletonDenoting := true }

def Denic2023.nonDeviantRead : DevianceDatum

NON-DEVIANT-READ: "Each of those three students read Anna Karenina, Germinal, or Harry Potter." @cite{denic-2023} ex. (34).

Equations

• Denic2023.nonDeviantRead = { label := "NON-DEVIANT-READ", isDeviant := false, isSingletonDenoting := false }

def Denic2023.deviancePuzzleData : List DevianceDatum

The four deviance data points from @cite{denic-2023} §5.

Equations

• Denic2023.deviancePuzzleData = [Denic2023.deviantBe, Denic2023.nonDeviantCalled, Denic2023.deviantWrite, Denic2023.nonDeviantRead]

theorem Denic2023.deviance_iff_singleton : (deviancePuzzleData.all fun (d : DevianceDatum) => d.isDeviant == d.isSingletonDenoting) = true

Deviance tracks singleton-denotation exactly.

Concrete model: DEVIANT-BE

"#Each of those three girls is Mary, Susan, or Jane."

We model this as a BlindScenario and show that blindOdd correctly predicts deviance. The key: since "is Mary/Susan/Jane" is singleton- denoting, the ignorance inferences ("the speaker is ignorant about whether at least one girl is Mary") contradict CK (the speaker must know which girl is which).

This is exactly @cite{magri-2009}'s mechanism (BH + MH) applied to a new empirical domain, as @cite{denic-2023} proposes in §6.

inductive Denic2023.DeviantBEWorld : Type

Worlds for DEVIANT-BE.

Three girls, each is exactly one of Mary, Susan, Jane. By CK (singleton- denoting), each name maps to exactly one girl. The only question is which permutation. We model 3 representative worlds.

• msj : DeviantBEWorld

  Girl 1 = Mary, Girl 2 = Susan, Girl 3 = Jane.

• mjs : DeviantBEWorld

  Girl 1 = Mary, Girl 2 = Jane, Girl 3 = Susan.

• smj : DeviantBEWorld

  Girl 1 = Susan, Girl 2 = Mary, Girl 3 = Jane.

@[implicit_reducible]

instance Denic2023.instDecidableEqDeviantBEWorld : DecidableEq DeviantBEWorld

Equations

• Denic2023.instDecidableEqDeviantBEWorld x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Denic2023.instReprDeviantBEWorld.repr : DeviantBEWorld → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Denic2023.instReprDeviantBEWorld : Repr DeviantBEWorld

Equations

• Denic2023.instReprDeviantBEWorld = { reprPrec := Denic2023.instReprDeviantBEWorld.repr }

@[implicit_reducible]

instance Denic2023.instFintypeDeviantBEWorld : Fintype DeviantBEWorld

Equations

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

inductive Denic2023.DeviantBEUtt : Type

Utterances: the target sentence and its individual-disjunct alternatives.

• eachOrDisj : DeviantBEUtt

  "Each is Mary, Susan, or Jane" (the target).

• someIsMary : DeviantBEUtt

  "At least one is Mary" (existential alternative).

• someIsSusan : DeviantBEUtt

  "At least one is Susan."

• someIsJane : DeviantBEUtt

  "At least one is Jane."

@[implicit_reducible]

instance Denic2023.instDecidableEqDeviantBEUtt : DecidableEq DeviantBEUtt

Equations

• Denic2023.instDecidableEqDeviantBEUtt x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Denic2023.instReprDeviantBEUtt : Repr DeviantBEUtt

Equations

• Denic2023.instReprDeviantBEUtt = { reprPrec := Denic2023.instReprDeviantBEUtt.repr }

def Denic2023.instReprDeviantBEUtt.repr : DeviantBEUtt → ℕ → Std.Format

Equations

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

def Denic2023.deviantBEScenario : Magri2009.BlindScenario DeviantBEWorld DeviantBEUtt

Blind scenario for DEVIANT-BE.

The target sentence is trivially true at all CK worlds (each girl IS one of Mary/Susan/Jane by construction). The existential alternatives are also all true at every CK world (in every permutation, at least one girl is Mary, at least one is Susan, etc.). This means the alternatives are not excludable — but the ignorance inferences (the speaker doesn't know whether one of them is Mary) contradict CK.

Equations

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

theorem Denic2023.deviantBE_no_ie : Exhaustification.innocent.excluded (Exhaustification.altsFromPreds (List.map deviantBEScenario.meaning (deviantBEScenario.alternatives DeviantBEUtt.eachOrDisj))) (Exhaustification.predToFinset (deviantBEScenario.meaning DeviantBEUtt.eachOrDisj)) = ∅

No alternative is IE for DEVIANT-BE: all alternatives are entailed by the prejacent (trivially true everywhere), so none can be excluded.

theorem Denic2023.deviantBE_not_blindOdd_directly : deviantBEScenario.blindOdd DeviantBEUtt.eachOrDisj = false

DEVIANT-BE is NOT blindOdd in this direct model, because IE is empty (no implicature is generated at all). The deviance comes not from scalar implicatures contradicting CK, but from ignorance inferences contradicting CK — a subtlety that requires grammatical ignorance inferences (K_speaker in the grammar, or Gricean quantity reasoning).

@cite{denic-2023} §6–7: deviance is due to ignorance inferences (derived via the maxim of quantity or grammatically via K_speaker) contradicting CK. Since all alternatives are true at all CK worlds, claiming ignorance about any of them contradicts CK.

theorem Denic2023.deviantBE_ignorance_contradicts_ck : deviantBEScenario.ignoranceContradictsCK DeviantBEUtt.eachOrDisj = true

DEVIANT-BE triggers ignorance inferences that contradict CK.

Non-IE alternatives exist (the speaker should be ignorant about them), but CK settles all of them (every existential alternative is true at every CK world). The speaker CANNOT be ignorant → contradiction → deviant.

This is @cite{denic-2023}'s proposal (40): "Sentences DEVIANT-BE and DEVIANT-WRITE are deviant because they trigger ignorance inferences which contradict common knowledge."

NON-DEVIANT-CALLED: "Each is called Mary, Susan, or Jane"

"is called Mary" is NOT singleton-denoting: multiple individuals can be called Mary. So ignorance about "at least one is called Mary" is consistent with CK — the speaker genuinely might not know.

inductive Denic2023.CalledWorld : Type

Worlds for NON-DEVIANT-CALLED.

Since "is called" is not singleton-denoting, there are CK-compatible worlds where NOT everyone called Mary exists in the group.

• allDifferent : CalledWorld

  All three are called different names (one Mary, one Susan, one Jane).

• allMary : CalledWorld

  All three are called Mary.

• noJane : CalledWorld

  Some called Mary, some called Susan, none called Jane.

@[implicit_reducible]

instance Denic2023.instDecidableEqCalledWorld : DecidableEq CalledWorld

Equations

• Denic2023.instDecidableEqCalledWorld x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Denic2023.instReprCalledWorld.repr : CalledWorld → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Denic2023.instReprCalledWorld : Repr CalledWorld

Equations

• Denic2023.instReprCalledWorld = { reprPrec := Denic2023.instReprCalledWorld.repr }

@[implicit_reducible]

instance Denic2023.instFintypeCalledWorld : Fintype CalledWorld

Equations

• Denic2023.instFintypeCalledWorld = { elems := { val := ↑Denic2023.CalledWorld.enumList, nodup := Denic2023.CalledWorld.enumList_nodup }, complete := Denic2023.instFintypeCalledWorld._proof_1 }

def Denic2023.nonDeviantCalledScenario : Magri2009.BlindScenario CalledWorld DeviantBEUtt

Blind scenario for NON-DEVIANT-CALLED.

Unlike DEVIANT-BE, the existential alternatives are NOT all true at every CK world — it is genuinely possible that none is called Jane (multiple people can share the name Mary or Susan).

Equations

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

theorem Denic2023.nonDeviantCalled_ignorance_ok : nonDeviantCalledScenario.ignoranceContradictsCK DeviantBEUtt.eachOrDisj = false

NON-DEVIANT-CALLED: ignorance does NOT contradict CK.

The speaker CAN be genuinely ignorant about "at least one is called Jane" because there exist CK worlds where it's true (allDifferent) and where it's false (allMary, noJane).

theorem Denic2023.deviance_contrast : deviantBEScenario.ignoranceContradictsCK DeviantBEUtt.eachOrDisj = true ∧ nonDeviantCalledScenario.ignoranceContradictsCK DeviantBEUtt.eachOrDisj = false

The deviance contrast: singleton-denoting predicates trigger CK- contradicting ignorance inferences; non-singleton-denoting ones don't.

@cite{denic-2023} §5–6: the property distinguishing DEVIANT-BE from NON-DEVIANT-CALLED is exactly whether the predicate is singleton- denoting.

Blindness extends to informativeness computation

@cite{denic-2023} §7.3: the informativeness computation feeding pruning must itself be blind to common knowledge. The argument:

1. @cite{magri-2009}: EXH is blind to CK (BH) — formalized via BlindScenario.strengthened, which uses logical entailment, not CK-relativized entailment.

2. @cite{denic-2023}: informativeness evaluation for pruning is ALSO blind to CK. If it weren't, then for DEVIANT-BE, CK would tell us P(at least one is Mary | Each is Mary, Susan, or Jane) = 1 — ALL existential alternatives would have condProb = 1 given CK, so all would be pruned → no ignorance inference → no deviance. But DEVIANT-BE IS deviant, so the pruning mechanism cannot use CK.

Together: the entire implicature computation pipeline — from alternative generation through informativeness evaluation to exhaustification — operates without consulting predicate-specific common knowledge. Only structural features (domain size, disjunct count, quantifier type) enter the computation.

theorem Denic2023.deviantBE_all_alts_ck_settled (alt : DeviantBEUtt) : alt ∈ deviantBEScenario.alternatives DeviantBEUtt.eachOrDisj → ∀ w ∈ deviantBEScenario.cWorlds, deviantBEScenario.meaning alt w = true

If CK were used to evaluate informativeness for DEVIANT-BE, every existential alternative would have condProb = 1 (all true at all CK worlds). Under monotone pruning, all alternatives with maximal condProb would be pruned, leaving no active alternatives for exhaustification.

We verify the premise: all existential alternatives ARE true at all CK worlds in the DEVIANT-BE scenario.

theorem Denic2023.ck_pruning_would_be_vacuous : Exhaustification.innocent.exh (Exhaustification.altsFromPreds []) (Exhaustification.predToFinset (deviantBEScenario.meaning DeviantBEUtt.eachOrDisj)) = Exhaustification.predToFinset (deviantBEScenario.meaning DeviantBEUtt.eachOrDisj)

The counterfactual: if we pruned all existential alternatives (as CK-informed informativeness would recommend), exhaustification would be vacuous — no alternatives to negate. This produces no ignorance inferences and incorrectly predicts non-deviance.

But DEVIANT-BE IS deviant (deviantBE_ignorance_contradicts_ck), so CK must be screened off from the informativeness computation.

The two puzzles constrain each other

@cite{denic-2023} §7: the deviance puzzle constrains the solution to the inference puzzle. The deviance data requires blindness of informativeness to CK (§5). Combined with the inference puzzle's requirement that informativeness guides pruning (§3), we get:

Pruning is guided by informativeness computed blindly to CK.

This is stronger than either puzzle requires alone:

• Inference puzzle alone: informativeness guides pruning (could use CK)
• Deviance puzzle alone: implicatures are blind to CK (could not involve pruning)
• Together: informativeness-guided pruning that is blind to CK

theorem Denic2023.puzzles_connected : Exhaustification.innocent.excluded (Exhaustification.altsFromPreds Denic2023.altAllOr✝) (Exhaustification.predToFinset Denic2023.allForS✝) = ∅ ∧ Exhaustification.innocent.excluded (Exhaustification.altsFromPreds Denic2023.altOr✝) (Exhaustification.predToFinset Denic2023.allForS✝) = Exhaustification.altsFromPreds Denic2023.altOr✝ ∧ uniformCondProb 20 2 > uniformCondProb 2 2 ∧ deviantBEScenario.ignoranceContradictsCK DeviantBEUtt.eachOrDisj = true ∧ nonDeviantCalledScenario.ignoranceContradictsCK DeviantBEUtt.eachOrDisj = false

The combined prediction: both puzzles are resolved by a single mechanism (informativeness-based pruning blind to CK). The two puzzle types are not independent — their solutions constrain each other.

• Inference puzzle ← informativeness-based pruning (§3): condProb ordering (condProb_ordering) separates cases that entailment cannot (entailment_invariant_across_domain_size)
• Deviance puzzle ← blindness of informativeness to CK (§5): CK-informed pruning would vacuously remove all alternatives (ck_pruning_would_be_vacuous), preventing the ignorance inferences that cause deviance (deviantBE_ignorance_contradicts_ck)
• Combined ← blind informativeness-based pruning