[PLLF16]: Embedded Implicatures as Pragmatic Inferences

[PLLF16] [CS11]

"Embedded Implicatures as Pragmatic Inferences under Compositional Lexical Uncertainty." Journal of Semantics 33(4): 755–802.

Empirical anchor: [CS11]

The 3-players × 3-outcomes architecture is structurally the same as CS11's every/exactly one/no × some/all design (CS11 uses 6 letters × 3 cell-states for Exp 1, 3 letters for Exp 2). The LU model's predictions — DE prefers weak lexicon (NNN reading), UE prefers strong (SSS embedded SI) — match CS11's qualitative findings: STRONG > WEAK in universal contexts (Exp 1) and LOCAL > FALSE in non-monotonic (Exp 2). The LU model is silent on the attitude-verb gradient that CS11 doesn't test (think > want > all > must, from [GP09]).

The Puzzle

Scalar implicatures interact asymmetrically with logical operators:

• UE (upward-entailing): "Every player hit some of his shots" → embedded implicature "some but not all" (enriched reading SSS preferred)
• DE (downward-entailing): "No player hit some of his shots" → global reading preferred, no embedded implicature (NNN preferred)

The Model: Compositional Lexical Uncertainty

The key innovation is lexical uncertainty: L1 marginalizes over possible lexica (refinements of "some") rather than using a fixed literal semantics. This file formalizes the paper's neo-Gricean refinement model variant (their (19d), refining only "some" to the two-element set {⟦some⟧, ⟦some and not all⟧} of (14)) — not their unconstrained-refinement model (19c), whose listener marginalizes over the full refinement lattice ℘(⟦some⟧) ∖ ∅. The two refinements are:

• Weak: "some" = "at least one" (the unrefined lower-bound ⟦some⟧)
• Strong: "some" = "some but not all" (the maximal enrichment)

The PMF stack mirrors [GS13]'s latent-uncertainty model on mathlib PMF, with Latent := Lexicon:

• L0 lex u : PMF World — RSA.L0OfBoolMeaning (uniform on the extension).
• S1 lex w : PMF Utterance — RSA.S1Belief (L0 lex) (fun _ => 1) 1 w (α = 1, no utterance cost): normalises L0 lex u w over utterances.
• marginalSpeaker w : PMF Utterance — RSA.marginalizeKernel of S1 against the uniform Lexicon prior.
• L1 u : PMF World — PMF.posterior marginalSpeaker (uniform World) u.

Architecture

The experiment (Section 6) uses 3 players, each with outcome N (nothing) / S (scored but not aced) / A (aced). The 10 equivalence classes are the multisets of 3 outcomes. Utterances are PlayerQ × ShotQ (outer × inner quantifier): "every/exactly one/no player hit all/none/some of his shots."

Predictions

The asymmetry arises from monotonicity:

• DE (under "no"): strong "some" widens the true-world set → less informative → L1 prefers weak lexicon → global reading (NNN)
• UE (under "every"): strong "some" narrows the true-world set → more informative → L1 prefers strong lexicon → enriched reading (SSS)

Domain types

inductive PottsEtAl2016.World : Type

World state as equivalence class over 3 players' outcomes. Each player's outcome: N (nothing), S (scored but not aced), A (aced). 10 classes = multisets of size 3 from {N, S, A}.

• NNN : World
• NNS : World
• NNA : World
• NSS : World
• NSA : World
• NAA : World
• SSS : World
• SSA : World
• SAA : World
• AAA : World

@[implicit_reducible]

instance PottsEtAl2016.instDecidableEqWorld : DecidableEq World

Equations

• PottsEtAl2016.instDecidableEqWorld x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def PottsEtAl2016.instReprWorld.repr : World → ℕ → Std.Format

Equations

• PottsEtAl2016.instReprWorld.repr PottsEtAl2016.World.NNN prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "PottsEtAl2016.World.NNN")).group prec✝
• PottsEtAl2016.instReprWorld.repr PottsEtAl2016.World.NNS prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "PottsEtAl2016.World.NNS")).group prec✝
• PottsEtAl2016.instReprWorld.repr PottsEtAl2016.World.NNA prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "PottsEtAl2016.World.NNA")).group prec✝
• PottsEtAl2016.instReprWorld.repr PottsEtAl2016.World.NSS prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "PottsEtAl2016.World.NSS")).group prec✝
• PottsEtAl2016.instReprWorld.repr PottsEtAl2016.World.NSA prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "PottsEtAl2016.World.NSA")).group prec✝
• PottsEtAl2016.instReprWorld.repr PottsEtAl2016.World.NAA prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "PottsEtAl2016.World.NAA")).group prec✝
• PottsEtAl2016.instReprWorld.repr PottsEtAl2016.World.SSS prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "PottsEtAl2016.World.SSS")).group prec✝
• PottsEtAl2016.instReprWorld.repr PottsEtAl2016.World.SSA prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "PottsEtAl2016.World.SSA")).group prec✝
• PottsEtAl2016.instReprWorld.repr PottsEtAl2016.World.SAA prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "PottsEtAl2016.World.SAA")).group prec✝
• PottsEtAl2016.instReprWorld.repr PottsEtAl2016.World.AAA prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "PottsEtAl2016.World.AAA")).group prec✝

@[implicit_reducible]

instance PottsEtAl2016.instReprWorld : Repr World

Equations

• PottsEtAl2016.instReprWorld = { reprPrec := PottsEtAl2016.instReprWorld.repr }

@[implicit_reducible]

instance PottsEtAl2016.instInhabitedWorld : Inhabited World

Equations

• PottsEtAl2016.instInhabitedWorld = { default := PottsEtAl2016.instInhabitedWorld.default }

@[implicit_reducible]

instance PottsEtAl2016.instFintypeWorld : Fintype World

Equations

• PottsEtAl2016.instFintypeWorld = { elems := { val := ↑PottsEtAl2016.World.enumList, nodup := PottsEtAl2016.World.enumList_nodup }, complete := PottsEtAl2016.instFintypeWorld._proof_1 }

inductive PottsEtAl2016.ShotQ : Type

Inner quantifier: over a player's shots.

• all : ShotQ
• none_ : ShotQ
• some_ : ShotQ

@[implicit_reducible]

instance PottsEtAl2016.instDecidableEqShotQ : DecidableEq ShotQ

Equations

• PottsEtAl2016.instDecidableEqShotQ x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def PottsEtAl2016.instReprShotQ.repr : ShotQ → ℕ → Std.Format

Equations

• PottsEtAl2016.instReprShotQ.repr PottsEtAl2016.ShotQ.all prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "PottsEtAl2016.ShotQ.all")).group prec✝
• PottsEtAl2016.instReprShotQ.repr PottsEtAl2016.ShotQ.none_ prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "PottsEtAl2016.ShotQ.none_")).group prec✝
• PottsEtAl2016.instReprShotQ.repr PottsEtAl2016.ShotQ.some_ prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "PottsEtAl2016.ShotQ.some_")).group prec✝

@[implicit_reducible]

instance PottsEtAl2016.instReprShotQ : Repr ShotQ

Equations

• PottsEtAl2016.instReprShotQ = { reprPrec := PottsEtAl2016.instReprShotQ.repr }

@[implicit_reducible]

instance PottsEtAl2016.instInhabitedShotQ : Inhabited ShotQ

Equations

• PottsEtAl2016.instInhabitedShotQ = { default := PottsEtAl2016.instInhabitedShotQ.default }

@[implicit_reducible]

instance PottsEtAl2016.instFintypeShotQ : Fintype ShotQ

Equations

• PottsEtAl2016.instFintypeShotQ = { elems := { val := ↑PottsEtAl2016.ShotQ.enumList, nodup := PottsEtAl2016.ShotQ.enumList_nodup }, complete := PottsEtAl2016.instFintypeShotQ._proof_1 }

inductive PottsEtAl2016.PlayerQ : Type

Outer quantifier: over players.

• every : PlayerQ
• exactlyOne : PlayerQ
• no : PlayerQ

@[implicit_reducible]

instance PottsEtAl2016.instDecidableEqPlayerQ : DecidableEq PlayerQ

Equations

• PottsEtAl2016.instDecidableEqPlayerQ x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance PottsEtAl2016.instReprPlayerQ : Repr PlayerQ

Equations

• PottsEtAl2016.instReprPlayerQ = { reprPrec := PottsEtAl2016.instReprPlayerQ.repr }

def PottsEtAl2016.instReprPlayerQ.repr : PlayerQ → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance PottsEtAl2016.instInhabitedPlayerQ : Inhabited PlayerQ

Equations

• PottsEtAl2016.instInhabitedPlayerQ = { default := PottsEtAl2016.instInhabitedPlayerQ.default }

@[implicit_reducible]

instance PottsEtAl2016.instFintypePlayerQ : Fintype PlayerQ

Equations

• PottsEtAl2016.instFintypePlayerQ = { elems := { val := ↑PottsEtAl2016.PlayerQ.enumList, nodup := PottsEtAl2016.PlayerQ.enumList_nodup }, complete := PottsEtAl2016.instFintypePlayerQ._proof_1 }

@[reducible, inline]

abbrev PottsEtAl2016.Stmt : Type

Statement: outer quantifier × inner quantifier.

Equations

• PottsEtAl2016.Stmt = (PottsEtAl2016.PlayerQ × PottsEtAl2016.ShotQ)

@[reducible, inline]

abbrev PottsEtAl2016.Utterance : Type

Utterance: a statement, or silence (none) — the null utterance, true at every world.

Equations

• PottsEtAl2016.Utterance = RSA.WithSilence PottsEtAl2016.Stmt

inductive PottsEtAl2016.Lexicon : Type

Lexicon: how "some" is interpreted.

• weak : Lexicon
• strong : Lexicon

@[implicit_reducible]

instance PottsEtAl2016.instDecidableEqLexicon : DecidableEq Lexicon

Equations

• PottsEtAl2016.instDecidableEqLexicon x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def PottsEtAl2016.instReprLexicon.repr : Lexicon → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance PottsEtAl2016.instReprLexicon : Repr Lexicon

Equations

• PottsEtAl2016.instReprLexicon = { reprPrec := PottsEtAl2016.instReprLexicon.repr }

@[implicit_reducible]

instance PottsEtAl2016.instInhabitedLexicon : Inhabited Lexicon

Equations

• PottsEtAl2016.instInhabitedLexicon = { default := PottsEtAl2016.instInhabitedLexicon.default }

@[implicit_reducible]

instance PottsEtAl2016.instFintypeLexicon : Fintype Lexicon

Equations

• PottsEtAl2016.instFintypeLexicon = { elems := { val := ↑PottsEtAl2016.Lexicon.enumList, nodup := PottsEtAl2016.Lexicon.enumList_nodup }, complete := PottsEtAl2016.instFintypeLexicon._proof_1 }

World count functions

def PottsEtAl2016.World.numScored : World → ℕ

Number of players who scored (hit ≥ 1 shot, i.e. S or A).

Equations

• PottsEtAl2016.World.NNN.numScored = 0
• PottsEtAl2016.World.NNS.numScored = 1
• PottsEtAl2016.World.NNA.numScored = 1
• PottsEtAl2016.World.NSS.numScored = 2
• PottsEtAl2016.World.NSA.numScored = 2
• PottsEtAl2016.World.NAA.numScored = 2
• PottsEtAl2016.World.SSS.numScored = 3
• PottsEtAl2016.World.SSA.numScored = 3
• PottsEtAl2016.World.SAA.numScored = 3
• PottsEtAl2016.World.AAA.numScored = 3

def PottsEtAl2016.World.numAced : World → ℕ

Number of players who aced (hit all shots).

Equations

• PottsEtAl2016.World.NNN.numAced = 0
• PottsEtAl2016.World.NNS.numAced = 0
• PottsEtAl2016.World.NNA.numAced = 1
• PottsEtAl2016.World.NSS.numAced = 0
• PottsEtAl2016.World.NSA.numAced = 1
• PottsEtAl2016.World.NAA.numAced = 2
• PottsEtAl2016.World.SSS.numAced = 0
• PottsEtAl2016.World.SSA.numAced = 1
• PottsEtAl2016.World.SAA.numAced = 2
• PottsEtAl2016.World.AAA.numAced = 3

def PottsEtAl2016.World.numScoredNotAced : World → ℕ

Number of players who scored but did not ace.

Equations

• PottsEtAl2016.World.NNN.numScoredNotAced = 0
• PottsEtAl2016.World.NNS.numScoredNotAced = 1
• PottsEtAl2016.World.NNA.numScoredNotAced = 0
• PottsEtAl2016.World.NSS.numScoredNotAced = 2
• PottsEtAl2016.World.NSA.numScoredNotAced = 1
• PottsEtAl2016.World.NAA.numScoredNotAced = 0
• PottsEtAl2016.World.SSS.numScoredNotAced = 3
• PottsEtAl2016.World.SSA.numScoredNotAced = 2
• PottsEtAl2016.World.SAA.numScoredNotAced = 1
• PottsEtAl2016.World.AAA.numScoredNotAced = 0

def PottsEtAl2016.World.numNothing : World → ℕ

Number of players who did nothing (hit 0 shots).

Equations

• PottsEtAl2016.World.NNN.numNothing = 3
• PottsEtAl2016.World.NNS.numNothing = 2
• PottsEtAl2016.World.NNA.numNothing = 2
• PottsEtAl2016.World.NSS.numNothing = 1
• PottsEtAl2016.World.NSA.numNothing = 1
• PottsEtAl2016.World.NAA.numNothing = 1
• PottsEtAl2016.World.SSS.numNothing = 0
• PottsEtAl2016.World.SSA.numNothing = 0
• PottsEtAl2016.World.SAA.numNothing = 0
• PottsEtAl2016.World.AAA.numNothing = 0

Truth conditions (lexicon-parameterized)

def PottsEtAl2016.predCount (sq : ShotQ) (lex : Lexicon) (w : World) : ℕ

Count of players satisfying the inner predicate, under a given lexicon.

• all: number who aced
• none_: number who did nothing
• some_: depends on lexicon:
  • weak: number who scored (≥ 1 shot)
  • strong: number who scored but did not ace

Equations

• PottsEtAl2016.predCount PottsEtAl2016.ShotQ.all lex w = w.numAced
• PottsEtAl2016.predCount PottsEtAl2016.ShotQ.none_ lex w = w.numNothing
• PottsEtAl2016.predCount PottsEtAl2016.ShotQ.some_ PottsEtAl2016.Lexicon.weak w = w.numScored
• PottsEtAl2016.predCount PottsEtAl2016.ShotQ.some_ PottsEtAl2016.Lexicon.strong w = w.numScoredNotAced

def PottsEtAl2016.stmtTruth (lex : Lexicon) : Stmt → World → Bool

Truth value of a statement in a world under a lexicon.

Equations

• PottsEtAl2016.stmtTruth lex (PottsEtAl2016.PlayerQ.every, sq) x✝ = (PottsEtAl2016.predCount sq lex x✝ == 3)
• PottsEtAl2016.stmtTruth lex (PottsEtAl2016.PlayerQ.exactlyOne, sq) x✝ = (PottsEtAl2016.predCount sq lex x✝ == 1)
• PottsEtAl2016.stmtTruth lex (PottsEtAl2016.PlayerQ.no, sq) x✝ = (PottsEtAl2016.predCount sq lex x✝ == 0)

def PottsEtAl2016.utteranceTruth (lex : Lexicon) : Utterance → World → Bool

Truth value of an utterance under a lexicon: stmtTruth with silence true at every world.

Equations

• PottsEtAl2016.utteranceTruth lex = RSA.liftMeaning (PottsEtAl2016.stmtTruth lex)

Structural properties

The lexicon affects only "some"; "all" and "none" are unambiguous. The DE/UE asymmetry is a widening vs. narrowing fact about the strong lexicon's extension under each outer quantifier.

theorem PottsEtAl2016.lexica_agree_on_all (pq : PlayerQ) (w : World) : utteranceTruth Lexicon.weak (some (pq, ShotQ.all)) w = utteranceTruth Lexicon.strong (some (pq, ShotQ.all)) w

Lexica agree on all "all"-utterances; the lexicon only refines "some".

theorem PottsEtAl2016.lexica_agree_on_none (pq : PlayerQ) (w : World) : utteranceTruth Lexicon.weak (some (pq, ShotQ.none_)) w = utteranceTruth Lexicon.strong (some (pq, ShotQ.none_)) w

Lexica agree on all "none"-utterances.

theorem PottsEtAl2016.de_enrichment_widens : {w : World | utteranceTruth Lexicon.weak (some (PlayerQ.no, ShotQ.some_)) w = true}.card < {w : World | utteranceTruth Lexicon.strong (some (PlayerQ.no, ShotQ.some_)) w = true}.card

DE context: strong "some" widens the set of true worlds relative to weak. Under "no player hit some of his shots":

• Weak "some": only NNN satisfies (1 world)
• Strong "some": NNN, NNA, NAA, AAA satisfy (4 worlds) Widening makes the utterance less informative under the strong lexicon.

theorem PottsEtAl2016.ue_enrichment_narrows : {w : World | utteranceTruth Lexicon.strong (some (PlayerQ.every, ShotQ.some_)) w = true}.card < {w : World | utteranceTruth Lexicon.weak (some (PlayerQ.every, ShotQ.some_)) w = true}.card

UE context: strong "some" narrows the set of true worlds relative to weak. Under "every player hit some of his shots":

• Weak "some": SSS, SSA, SAA, AAA satisfy (4 worlds)
• Strong "some": only SSS satisfies (1 world) Narrowing makes the utterance more informative under the strong lexicon.

Literal listener L0

Per-lexicon literal listener via RSA.L0OfBoolMeaning: uniform on the extension of the (lexicon-parameterised) meaning function. Every utterance has a non-empty extension (every quantifier is true at some world, and null is true everywhere), so the Nonempty precondition is universal.

theorem PottsEtAl2016.ext_nonempty (lex : Lexicon) (u : Utterance) : (RSA.extensionOf (utteranceTruth lex) u).Nonempty

Every (lexicon, utterance) has a non-empty extension.

noncomputable def PottsEtAl2016.L0 (lex : Lexicon) (u : Utterance) : PMF World

Per-lexicon literal listener: uniform on the extension.

Equations

• PottsEtAl2016.L0 lex u = RSA.L0OfBoolMeaning (PottsEtAl2016.utteranceTruth lex) u ⋯

theorem PottsEtAl2016.L0_apply (lex : Lexicon) (u : Utterance) (w : World) : (L0 lex u) w = if utteranceTruth lex u w = true then ENNReal.ofReal (↑(RSA.extensionOf (utteranceTruth lex) u).card)⁻¹ else 0

Closed-form L0 value: ENNReal.ofReal (1 / |extension|) at true worlds, 0 otherwise. The pmf_eval_simps-friendly if-form.

theorem PottsEtAl2016.L0_null (lex : Lexicon) (w : World) : (L0 lex none) w = ENNReal.ofReal 10⁻¹

L0 lex none w = ofReal (1/10): silence is true at every world, so its extension is all 10 worlds. Used to discharge the speaker normaliser's positivity hypothesis.

theorem PottsEtAl2016.Utterance_sum_univ {β : Type u_1} [AddCommMonoid β] (f : Utterance → β) : ∑ i : Utterance, f i = f none + (f (some (PlayerQ.every, ShotQ.all)) + (f (some (PlayerQ.every, ShotQ.none_)) + (f (some (PlayerQ.every, ShotQ.some_)) + (f (some (PlayerQ.exactlyOne, ShotQ.all)) + (f (some (PlayerQ.exactlyOne, ShotQ.none_)) + (f (some (PlayerQ.exactlyOne, ShotQ.some_)) + (f (some (PlayerQ.no, ShotQ.all)) + (f (some (PlayerQ.no, ShotQ.none_)) + (f (some (PlayerQ.no, ShotQ.some_)) + 0)))))))))

Sum-over-Utterance unfolder (silence + the 9 statements), proved by rfl. Local-tagged for pmf_eval_simps so partition sums reduce to a concrete 10-term sum.

Extension cardinalities

Per-(lexicon, utterance) extension sizes, decide-checked and locally tagged for pmf_eval_simps so L0_apply reduces to concrete ofReal((c)⁻¹) values. The local tag keeps these private paper-specific cards out of the substrate simp set (audit hygiene rule, following GoodmanStuhlmuller2013).

Speaker normaliser Z

S1Belief with α = 1 and unit cost has score (L0 u w)^1 · 1 = L0 u w, so the partition function is Z lex w = ∑' u, L0 lex u w. Each value is ofReal of a rational; the closed forms below are computed by simp +decide only [pmf_eval_simps, ...] (reducing to a sum of concrete ofReal (c⁻¹) terms) followed by explicit ENNReal.ofReal_add folding and norm_num.

theorem PottsEtAl2016.score_eq (lex : Lexicon) (w : World) (u : Utterance) : (L0 lex u) w ^ 1 * 1 = (L0 lex u) w

With α = 1 and unit cost, the speaker score is just L0 lex u w.

noncomputable def PottsEtAl2016.Z (lex : Lexicon) (w : World) : ENNReal

The S1Belief normaliser at (lexicon, world).

Equations

• PottsEtAl2016.Z lex w = ∑' (u : PottsEtAl2016.Utterance), (PottsEtAl2016.L0 lex u) w ^ 1 * 1

theorem PottsEtAl2016.Z_eq_sum (lex : Lexicon) (w : World) : Z lex w = ∑' (u : Utterance), (L0 lex u) w

theorem PottsEtAl2016.Z_ne_top (lex : Lexicon) (w : World) : Z lex w ≠ ⊤

theorem PottsEtAl2016.Z_ne_zero (lex : Lexicon) (w : World) : ∑' (u : Utterance), (L0 lex u) w ^ 1 * 1 ≠ 0

The speaker normaliser is non-zero: null is true everywhere, contributing ofReal (1/10) ≠ 0.

Per-lexicon speaker S1

RSA.S1Belief (L0 lex) (fun _ => 1) 1 w: normalises L0 lex u w over utterances at the fixed world w. The closed-form values are ofReal (L0-value · Z⁻¹).

noncomputable def PottsEtAl2016.S1 (lex : Lexicon) (w : World) : PMF Utterance

Per-lexicon speaker (α = 1, no cost).

Equations

• PottsEtAl2016.S1 lex w = RSA.S1Belief (PottsEtAl2016.L0 lex) (fun (x : PottsEtAl2016.Utterance) => 1) 1 w ⋯ ⋯

theorem PottsEtAl2016.S1_apply (lex : Lexicon) (w : World) (u : Utterance) : (S1 lex w) u = (L0 lex u) w ^ 1 * 1 * (Z lex w)⁻¹

Marginal speaker over lexica

RSA.marginalizeKernel against the uniform Lexicon prior. Over the 2-element Lexicon, marginalSpeaker w u = (1/2)·S1 weak w u + (1/2)·S1 strong w u.

noncomputable def PottsEtAl2016.marginalSpeaker (w : World) : PMF Utterance

Marginal speaker: marginalises S1 over a uniform Lexicon prior.

Equations

• PottsEtAl2016.marginalSpeaker w = RSA.marginalizeKernel (PMF.uniformOfFintype PottsEtAl2016.Lexicon) (fun (lex : PottsEtAl2016.Lexicon) (w : PottsEtAl2016.World) => PottsEtAl2016.S1 lex w) w

theorem PottsEtAl2016.marginalSpeaker_apply (w : World) (u : Utterance) : (marginalSpeaker w) u = ENNReal.ofReal (1 / 2) * (S1 Lexicon.weak w) u + (ENNReal.ofReal (1 / 2) * (S1 Lexicon.strong w) u + 0)

Marginal speaker as the explicit (1/2, 1/2)-weighted lexicon mixture.

Marginal-speaker closed forms (per prediction cell)

The 8 cells the predictions compare, each ofReal of a rational. DE worlds under "no … some"; UE worlds under "every … some". Values match the LU model's hand-computation (α = 1, uniform priors).

Pragmatic listener L1

PMF.posterior marginalSpeaker (uniform World) u. The marginal positivity hypotheses are discharged via PMF.marginal_ne_zero with the target world as witness (marginalSpeaker w u ≠ 0 for the relevant (w, u)).

noncomputable def PottsEtAl2016.L1 (u : Utterance) (h : PMF.marginal marginalSpeaker (PMF.uniformOfFintype World) u ≠ 0) : PMF World

Pragmatic listener: Bayesian inversion of marginalSpeaker against the uniform world prior.

Equations

• PottsEtAl2016.L1 u h = PMF.posterior PottsEtAl2016.marginalSpeaker (PMF.uniformOfFintype PottsEtAl2016.World) u h

Predictions: DE blocking

"No player hit some of his shots" → NNN preferred.

Under the weak lexicon, only NNN makes the utterance true (1 world, maximally informative). Under the strong lexicon, NNN, NNA, NAA, and AAA all make it true (4 worlds, less informative). L1 marginalizes over lexica weighted by informativity, preferring the weak lexicon for this utterance. Result: NNN receives the highest posterior — the global reading.

theorem PottsEtAl2016.de_blocking_NNN_vs_NNA : (L1 (some (PlayerQ.no, ShotQ.some_)) PottsEtAl2016.hMarg_DE✝) World.NNN > (L1 (some (PlayerQ.no, ShotQ.some_)) PottsEtAl2016.hMarg_DE✝) World.NNA

DE blocking: NNN > NNA.

theorem PottsEtAl2016.de_blocking_NNN_vs_NAA : (L1 (some (PlayerQ.no, ShotQ.some_)) PottsEtAl2016.hMarg_DE✝) World.NNN > (L1 (some (PlayerQ.no, ShotQ.some_)) PottsEtAl2016.hMarg_DE✝) World.NAA

DE blocking: NNN > NAA.

theorem PottsEtAl2016.de_blocking_NNN_vs_AAA : (L1 (some (PlayerQ.no, ShotQ.some_)) PottsEtAl2016.hMarg_DE✝) World.NNN > (L1 (some (PlayerQ.no, ShotQ.some_)) PottsEtAl2016.hMarg_DE✝) World.AAA

DE blocking: NNN > AAA.

Predictions: UE enrichment

"Every player hit some of his shots" → SSS preferred.

Under the strong lexicon, only SSS makes the utterance true (1 world, maximally informative). Under the weak lexicon, SSS, SSA, SAA, and AAA all make it true (4 worlds, less informative). L1 marginalizes and prefers the informative strong lexicon for this utterance. Result: SSS receives the highest posterior — the embedded implicature.

theorem PottsEtAl2016.ue_enrichment_SSS_vs_SSA : (L1 (some (PlayerQ.every, ShotQ.some_)) PottsEtAl2016.hMarg_UE✝) World.SSS > (L1 (some (PlayerQ.every, ShotQ.some_)) PottsEtAl2016.hMarg_UE✝) World.SSA

UE enrichment: SSS > SSA.

theorem PottsEtAl2016.ue_enrichment_SSS_vs_SAA : (L1 (some (PlayerQ.every, ShotQ.some_)) PottsEtAl2016.hMarg_UE✝) World.SSS > (L1 (some (PlayerQ.every, ShotQ.some_)) PottsEtAl2016.hMarg_UE✝) World.SAA

UE enrichment: SSS > SAA.

theorem PottsEtAl2016.ue_enrichment_SSS_vs_AAA : (L1 (some (PlayerQ.every, ShotQ.some_)) PottsEtAl2016.hMarg_UE✝) World.SSS > (L1 (some (PlayerQ.every, ShotQ.some_)) PottsEtAl2016.hMarg_UE✝) World.AAA

UE enrichment: SSS > AAA.

Grounding: outer quantifiers

The outer quantifiers "every" and "no" in the [PLLF16] model agree with the shared quantifier semantics Alternatives.Quantifiers.worldMeaning. This grounds the stipulated utteranceTruth in the shared quantifier infrastructure.

Compare GoodmanStuhlmuller2013's qMeaning, an independent implementation of the same count-threshold semantics.

theorem PottsEtAl2016.outer_every_grounded (sq : ShotQ) (lex : Lexicon) (w : World) : utteranceTruth lex (some (PlayerQ.every, sq)) w = Alternatives.Quantifiers.worldMeaning 3 Alternatives.Quantifiers.QuantExpr.all { count := ⟨predCount sq lex w, ⋯⟩ }

"Every player hit X" ↔ worldMeaning 3 .all applied to predCount.

theorem PottsEtAl2016.outer_no_grounded (sq : ShotQ) (lex : Lexicon) (w : World) : utteranceTruth lex (some (PlayerQ.no, sq)) w = Alternatives.Quantifiers.worldMeaning 3 Alternatives.Quantifiers.QuantExpr.none_ { count := ⟨predCount sq lex w, ⋯⟩ }

"No player hit X" ↔ worldMeaning 3 .none_ applied to predCount.

Cross-study connections

The [PLLF16] predictions connect to two other parts of linglib:

1. Geurts2010 (ScalarImplicatures.Studies.Geurts2010): Notes that the minimal LU model inverts the predictions, but "the full Potts et al. model derives the correct pattern." The theorems here are the formal backing.

2. EmbeddedSIPrediction (LexicalUncertainty.Compositional): Tracks embedded SI predictions by context type. The Potts model demonstrates the negation case: local reading dispreferred in DE (global NNN preferred).