Documentation

Linglib.Phenomena.ScalarImplicatures.Studies.PottsEtAl2016

@cite{potts-etal-2016}: Embedded Implicatures as Pragmatic Inferences #

@cite{potts-etal-2016}

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

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. Two lexica:

Weak: "some" = "at least one" (standard lower-bound semantics)
Strong: "some" = "some but not all" (enriched semantics)

This uses the standard RSAConfig latent variable mechanism: Latent := Lexicon. No special infrastructure needed — the same mechanism handles observations (@cite{goodman-stuhlmuller-2013}), scope readings (@cite{scontras-pearl-2021}), and QUDs (@cite{kao-etal-2014-hyperbole}).

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)

inductive Phenomena.ScalarImplicatures.Studies.PottsEtAl2016.World :

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

Instances For

instance Phenomena.ScalarImplicatures.Studies.PottsEtAl2016.instDecidableEqWorld :

DecidableEq World

Equations

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

def Phenomena.ScalarImplicatures.Studies.PottsEtAl2016.instBEqWorld.beq :

World → World → Bool

Equations

Phenomena.ScalarImplicatures.Studies.PottsEtAl2016.instBEqWorld.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

instance Phenomena.ScalarImplicatures.Studies.PottsEtAl2016.instBEqWorld :

Equations

Phenomena.ScalarImplicatures.Studies.PottsEtAl2016.instBEqWorld = { beq := Phenomena.ScalarImplicatures.Studies.PottsEtAl2016.instBEqWorld.beq }

instance Phenomena.ScalarImplicatures.Studies.PottsEtAl2016.instReprWorld :

Equations

Phenomena.ScalarImplicatures.Studies.PottsEtAl2016.instReprWorld = { reprPrec := Phenomena.ScalarImplicatures.Studies.PottsEtAl2016.instReprWorld.repr }

def Phenomena.ScalarImplicatures.Studies.PottsEtAl2016.instReprWorld.repr :

World → ℕ → Std.Format

Equations

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

Instances For

instance Phenomena.ScalarImplicatures.Studies.PottsEtAl2016.instInhabitedWorld :

Inhabited World

Equations

Phenomena.ScalarImplicatures.Studies.PottsEtAl2016.instInhabitedWorld = { default := Phenomena.ScalarImplicatures.Studies.PottsEtAl2016.instInhabitedWorld.default }

def Phenomena.ScalarImplicatures.Studies.PottsEtAl2016.instInhabitedWorld.default :

Equations

Phenomena.ScalarImplicatures.Studies.PottsEtAl2016.instInhabitedWorld.default = Phenomena.ScalarImplicatures.Studies.PottsEtAl2016.World.NNN

Instances For

instance Phenomena.ScalarImplicatures.Studies.PottsEtAl2016.instFintypeWorld :

Equations

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

inductive Phenomena.ScalarImplicatures.Studies.PottsEtAl2016.ShotQ :

Inner quantifier: over a player's shots.

all : ShotQ
none_ : ShotQ
some_ : ShotQ

Instances For

instance Phenomena.ScalarImplicatures.Studies.PottsEtAl2016.instDecidableEqShotQ :

DecidableEq ShotQ

Equations

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

def Phenomena.ScalarImplicatures.Studies.PottsEtAl2016.instBEqShotQ.beq :

ShotQ → ShotQ → Bool

Equations

Phenomena.ScalarImplicatures.Studies.PottsEtAl2016.instBEqShotQ.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

instance Phenomena.ScalarImplicatures.Studies.PottsEtAl2016.instBEqShotQ :

Equations

Phenomena.ScalarImplicatures.Studies.PottsEtAl2016.instBEqShotQ = { beq := Phenomena.ScalarImplicatures.Studies.PottsEtAl2016.instBEqShotQ.beq }

instance Phenomena.ScalarImplicatures.Studies.PottsEtAl2016.instReprShotQ :

Equations

Phenomena.ScalarImplicatures.Studies.PottsEtAl2016.instReprShotQ = { reprPrec := Phenomena.ScalarImplicatures.Studies.PottsEtAl2016.instReprShotQ.repr }

def Phenomena.ScalarImplicatures.Studies.PottsEtAl2016.instReprShotQ.repr :

ShotQ → ℕ → Std.Format

Equations

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

Instances For

def Phenomena.ScalarImplicatures.Studies.PottsEtAl2016.instInhabitedShotQ.default :

Equations

Phenomena.ScalarImplicatures.Studies.PottsEtAl2016.instInhabitedShotQ.default = Phenomena.ScalarImplicatures.Studies.PottsEtAl2016.ShotQ.all

Instances For

instance Phenomena.ScalarImplicatures.Studies.PottsEtAl2016.instInhabitedShotQ :

Inhabited ShotQ

Equations

Phenomena.ScalarImplicatures.Studies.PottsEtAl2016.instInhabitedShotQ = { default := Phenomena.ScalarImplicatures.Studies.PottsEtAl2016.instInhabitedShotQ.default }

instance Phenomena.ScalarImplicatures.Studies.PottsEtAl2016.instFintypeShotQ :

Equations

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

inductive Phenomena.ScalarImplicatures.Studies.PottsEtAl2016.PlayerQ :

Outer quantifier: over players.

every : PlayerQ
exactlyOne : PlayerQ
no : PlayerQ

Instances For

instance Phenomena.ScalarImplicatures.Studies.PottsEtAl2016.instDecidableEqPlayerQ :

DecidableEq PlayerQ

Equations

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

instance Phenomena.ScalarImplicatures.Studies.PottsEtAl2016.instBEqPlayerQ :

Equations

Phenomena.ScalarImplicatures.Studies.PottsEtAl2016.instBEqPlayerQ = { beq := Phenomena.ScalarImplicatures.Studies.PottsEtAl2016.instBEqPlayerQ.beq }

def Phenomena.ScalarImplicatures.Studies.PottsEtAl2016.instBEqPlayerQ.beq :

PlayerQ → PlayerQ → Bool

Equations

Phenomena.ScalarImplicatures.Studies.PottsEtAl2016.instBEqPlayerQ.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

instance Phenomena.ScalarImplicatures.Studies.PottsEtAl2016.instReprPlayerQ :

Equations

Phenomena.ScalarImplicatures.Studies.PottsEtAl2016.instReprPlayerQ = { reprPrec := Phenomena.ScalarImplicatures.Studies.PottsEtAl2016.instReprPlayerQ.repr }

def Phenomena.ScalarImplicatures.Studies.PottsEtAl2016.instReprPlayerQ.repr :

PlayerQ → ℕ → Std.Format

Equations

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

Instances For

def Phenomena.ScalarImplicatures.Studies.PottsEtAl2016.instInhabitedPlayerQ.default :

Equations

Phenomena.ScalarImplicatures.Studies.PottsEtAl2016.instInhabitedPlayerQ.default = Phenomena.ScalarImplicatures.Studies.PottsEtAl2016.PlayerQ.every

Instances For

instance Phenomena.ScalarImplicatures.Studies.PottsEtAl2016.instInhabitedPlayerQ :

Inhabited PlayerQ

Equations

Phenomena.ScalarImplicatures.Studies.PottsEtAl2016.instInhabitedPlayerQ = { default := Phenomena.ScalarImplicatures.Studies.PottsEtAl2016.instInhabitedPlayerQ.default }

instance Phenomena.ScalarImplicatures.Studies.PottsEtAl2016.instFintypePlayerQ :

Fintype PlayerQ

Equations

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

inductive Phenomena.ScalarImplicatures.Studies.PottsEtAl2016.Utterance :

Utterance: outer quantifier × inner quantifier, plus null.

stmt : PlayerQ → ShotQ → Utterance
null : Utterance

Instances For

instance Phenomena.ScalarImplicatures.Studies.PottsEtAl2016.instDecidableEqUtterance :

DecidableEq Utterance

Equations

Phenomena.ScalarImplicatures.Studies.PottsEtAl2016.instDecidableEqUtterance = Phenomena.ScalarImplicatures.Studies.PottsEtAl2016.instDecidableEqUtterance.decEq

def Phenomena.ScalarImplicatures.Studies.PottsEtAl2016.instDecidableEqUtterance.decEq (x✝ x✝¹ : Utterance) :

Decidable (x✝ = x✝¹)

Equations

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

Instances For

instance Phenomena.ScalarImplicatures.Studies.PottsEtAl2016.instBEqUtterance :

Equations

Phenomena.ScalarImplicatures.Studies.PottsEtAl2016.instBEqUtterance = { beq := Phenomena.ScalarImplicatures.Studies.PottsEtAl2016.instBEqUtterance.beq }

def Phenomena.ScalarImplicatures.Studies.PottsEtAl2016.instBEqUtterance.beq :

Utterance → Utterance → Bool

Equations

One or more equations did not get rendered due to their size.
Phenomena.ScalarImplicatures.Studies.PottsEtAl2016.instBEqUtterance.beq x✝¹ x✝ = false

Instances For

instance Phenomena.ScalarImplicatures.Studies.PottsEtAl2016.instReprUtterance :

Equations

Phenomena.ScalarImplicatures.Studies.PottsEtAl2016.instReprUtterance = { reprPrec := Phenomena.ScalarImplicatures.Studies.PottsEtAl2016.instReprUtterance.repr }

def Phenomena.ScalarImplicatures.Studies.PottsEtAl2016.instReprUtterance.repr :

Utterance → ℕ → Std.Format

Equations

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

Instances For

def Phenomena.ScalarImplicatures.Studies.PottsEtAl2016.instInhabitedUtterance.default :

Equations

Phenomena.ScalarImplicatures.Studies.PottsEtAl2016.instInhabitedUtterance.default = Phenomena.ScalarImplicatures.Studies.PottsEtAl2016.Utterance.stmt default default

Instances For

instance Phenomena.ScalarImplicatures.Studies.PottsEtAl2016.instInhabitedUtterance :

Inhabited Utterance

Equations

Phenomena.ScalarImplicatures.Studies.PottsEtAl2016.instInhabitedUtterance = { default := Phenomena.ScalarImplicatures.Studies.PottsEtAl2016.instInhabitedUtterance.default }

instance Phenomena.ScalarImplicatures.Studies.PottsEtAl2016.instFintypeUtterance :

Fintype Utterance

Equations

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

inductive Phenomena.ScalarImplicatures.Studies.PottsEtAl2016.Lexicon :

Lexicon: how "some" is interpreted.

weak : Lexicon
strong : Lexicon

Instances For

instance Phenomena.ScalarImplicatures.Studies.PottsEtAl2016.instDecidableEqLexicon :

DecidableEq Lexicon

Equations

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

instance Phenomena.ScalarImplicatures.Studies.PottsEtAl2016.instBEqLexicon :

Equations

Phenomena.ScalarImplicatures.Studies.PottsEtAl2016.instBEqLexicon = { beq := Phenomena.ScalarImplicatures.Studies.PottsEtAl2016.instBEqLexicon.beq }

def Phenomena.ScalarImplicatures.Studies.PottsEtAl2016.instBEqLexicon.beq :

Lexicon → Lexicon → Bool

Equations

Phenomena.ScalarImplicatures.Studies.PottsEtAl2016.instBEqLexicon.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

def Phenomena.ScalarImplicatures.Studies.PottsEtAl2016.instReprLexicon.repr :

Lexicon → ℕ → Std.Format

Equations

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

Instances For

instance Phenomena.ScalarImplicatures.Studies.PottsEtAl2016.instReprLexicon :

Equations

Phenomena.ScalarImplicatures.Studies.PottsEtAl2016.instReprLexicon = { reprPrec := Phenomena.ScalarImplicatures.Studies.PottsEtAl2016.instReprLexicon.repr }

instance Phenomena.ScalarImplicatures.Studies.PottsEtAl2016.instInhabitedLexicon :

Inhabited Lexicon

Equations

Phenomena.ScalarImplicatures.Studies.PottsEtAl2016.instInhabitedLexicon = { default := Phenomena.ScalarImplicatures.Studies.PottsEtAl2016.instInhabitedLexicon.default }

def Phenomena.ScalarImplicatures.Studies.PottsEtAl2016.instInhabitedLexicon.default :

Equations

Phenomena.ScalarImplicatures.Studies.PottsEtAl2016.instInhabitedLexicon.default = Phenomena.ScalarImplicatures.Studies.PottsEtAl2016.Lexicon.weak

Instances For

instance Phenomena.ScalarImplicatures.Studies.PottsEtAl2016.instFintypeLexicon :

Fintype Lexicon

Equations

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

def Phenomena.ScalarImplicatures.Studies.PottsEtAl2016.World.numScored :

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

Equations

Instances For

def Phenomena.ScalarImplicatures.Studies.PottsEtAl2016.World.numAced :

Number of players who aced (hit all shots).

Equations

Instances For

def Phenomena.ScalarImplicatures.Studies.PottsEtAl2016.World.numScoredNotAced :

Number of players who scored but did not ace.

Equations

Instances For

def Phenomena.ScalarImplicatures.Studies.PottsEtAl2016.World.numNothing :

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

Equations

Instances For

def Phenomena.ScalarImplicatures.Studies.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

One or more equations did not get rendered due to their size.
Phenomena.ScalarImplicatures.Studies.PottsEtAl2016.predCount Phenomena.ScalarImplicatures.Studies.PottsEtAl2016.ShotQ.all lex w = w.numAced
Phenomena.ScalarImplicatures.Studies.PottsEtAl2016.predCount Phenomena.ScalarImplicatures.Studies.PottsEtAl2016.ShotQ.none_ lex w = w.numNothing

Instances For

def Phenomena.ScalarImplicatures.Studies.PottsEtAl2016.utteranceTruth (lex : Lexicon) :

Utterance → World → Bool

Truth value of an utterance in a world under a lexicon.

Equations

One or more equations did not get rendered due to their size.
Phenomena.ScalarImplicatures.Studies.PottsEtAl2016.utteranceTruth lex Phenomena.ScalarImplicatures.Studies.PottsEtAl2016.Utterance.null x✝ = true

Instances For

noncomputable def Phenomena.ScalarImplicatures.Studies.PottsEtAl2016.cfg :

RSA.RSAConfig Utterance World

@cite{potts-etal-2016} lexical uncertainty model.

Latent variable = Lexicon (weak vs strong "some"). L0: literal listener under lexicon l. S1: belief-based scoring, rpow(L0(w|u), α). L1: marginalizes over lexica with uniform prior.

Uniform priors, α = 1, no utterance cost. Qualitative predictions (DE blocking, UE enrichment) hold across a range of rationality parameters.

Equations

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

Instances For

theorem Phenomena.ScalarImplicatures.Studies.PottsEtAl2016.lexica_agree_on_all (pq : PlayerQ) (w : World) :

utteranceTruth Lexicon.weak (Utterance.stmt pq ShotQ.all) w = utteranceTruth Lexicon.strong (Utterance.stmt pq ShotQ.all) w

Lexica agree on all non-"some" utterances. The lexicon only affects the interpretation of "some"; "all" and "none" are unambiguous.

theorem Phenomena.ScalarImplicatures.Studies.PottsEtAl2016.lexica_agree_on_none (pq : PlayerQ) (w : World) :

utteranceTruth Lexicon.weak (Utterance.stmt pq ShotQ.none_) w = utteranceTruth Lexicon.strong (Utterance.stmt pq ShotQ.none_) w

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.

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.

"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 Phenomena.ScalarImplicatures.Studies.PottsEtAl2016.de_blocking_NNN_vs_NNA :

cfg.L1 (Utterance.stmt PlayerQ.no ShotQ.some_) World.NNN > cfg.L1 (Utterance.stmt PlayerQ.no ShotQ.some_) World.NNA

DE blocking: NNN > NNA.

theorem Phenomena.ScalarImplicatures.Studies.PottsEtAl2016.de_blocking_NNN_vs_NAA :

cfg.L1 (Utterance.stmt PlayerQ.no ShotQ.some_) World.NNN > cfg.L1 (Utterance.stmt PlayerQ.no ShotQ.some_) World.NAA

DE blocking: NNN > NAA.

theorem Phenomena.ScalarImplicatures.Studies.PottsEtAl2016.de_blocking_NNN_vs_AAA :

cfg.L1 (Utterance.stmt PlayerQ.no ShotQ.some_) World.NNN > cfg.L1 (Utterance.stmt PlayerQ.no ShotQ.some_) World.AAA

DE blocking: NNN > AAA.

"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 Phenomena.ScalarImplicatures.Studies.PottsEtAl2016.ue_enrichment_SSS_vs_SSA :

cfg.L1 (Utterance.stmt PlayerQ.every ShotQ.some_) World.SSS > cfg.L1 (Utterance.stmt PlayerQ.every ShotQ.some_) World.SSA

UE enrichment: SSS > SSA.

theorem Phenomena.ScalarImplicatures.Studies.PottsEtAl2016.ue_enrichment_SSS_vs_SAA :

cfg.L1 (Utterance.stmt PlayerQ.every ShotQ.some_) World.SSS > cfg.L1 (Utterance.stmt PlayerQ.every ShotQ.some_) World.SAA

UE enrichment: SSS > SAA.

theorem Phenomena.ScalarImplicatures.Studies.PottsEtAl2016.ue_enrichment_SSS_vs_AAA :

cfg.L1 (Utterance.stmt PlayerQ.every ShotQ.some_) World.SSS > cfg.L1 (Utterance.stmt PlayerQ.every ShotQ.some_) World.AAA

UE enrichment: SSS > AAA.

inductive Phenomena.ScalarImplicatures.Studies.PottsEtAl2016.Finding :

The 6 qualitative findings from the @cite{potts-etal-2016} LU model. 3 DE blocking predictions (global reading preferred under "no") + 3 UE enrichment predictions (enriched reading preferred under "every").

de_NNN_vs_NNA : Finding
de_NNN_vs_NAA : Finding
de_NNN_vs_AAA : Finding
ue_SSS_vs_SSA : Finding
ue_SSS_vs_SAA : Finding
ue_SSS_vs_AAA : Finding

Instances For

instance Phenomena.ScalarImplicatures.Studies.PottsEtAl2016.instDecidableEqFinding :

DecidableEq Finding

Equations

Phenomena.ScalarImplicatures.Studies.PottsEtAl2016.instDecidableEqFinding x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.ScalarImplicatures.Studies.PottsEtAl2016.instBEqFinding.beq :

Finding → Finding → Bool

Equations

Phenomena.ScalarImplicatures.Studies.PottsEtAl2016.instBEqFinding.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

instance Phenomena.ScalarImplicatures.Studies.PottsEtAl2016.instBEqFinding :

Equations

Phenomena.ScalarImplicatures.Studies.PottsEtAl2016.instBEqFinding = { beq := Phenomena.ScalarImplicatures.Studies.PottsEtAl2016.instBEqFinding.beq }

instance Phenomena.ScalarImplicatures.Studies.PottsEtAl2016.instReprFinding :

Equations

Phenomena.ScalarImplicatures.Studies.PottsEtAl2016.instReprFinding = { reprPrec := Phenomena.ScalarImplicatures.Studies.PottsEtAl2016.instReprFinding.repr }

def Phenomena.ScalarImplicatures.Studies.PottsEtAl2016.instReprFinding.repr :

Finding → ℕ → Std.Format

Equations

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

Instances For

def Phenomena.ScalarImplicatures.Studies.PottsEtAl2016.findings :

All findings.

Equations

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

Instances For

def Phenomena.ScalarImplicatures.Studies.PottsEtAl2016.formalize :

Finding → Prop

Map each empirical finding to the RSA model prediction that accounts for it.

Equations

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

Instances For

theorem Phenomena.ScalarImplicatures.Studies.PottsEtAl2016.all_findings_verified (f : Finding) :

The RSA model accounts for all 6 qualitative findings from @cite{potts-etal-2016}.

The outer quantifiers "every" and "no" in the @cite{potts-etal-2016} model agree with the generic quantity domain semantics from RSA.Domains.Quantity.meaning. This grounds the stipulated utteranceTruth in the shared quantifier infrastructure.

See also: GoodmanStuhlmuller2013.quantifier_meaning_grounded.

theorem Phenomena.ScalarImplicatures.Studies.PottsEtAl2016.outer_every_grounded (sq : ShotQ) (lex : Lexicon) (w : World) :

utteranceTruth lex (Utterance.stmt PlayerQ.every sq) w = RSA.Domains.Quantity.meaning 3 RSA.Domains.Quantity.Utterance.all ⟨predCount sq lex w, ⋯⟩

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

theorem Phenomena.ScalarImplicatures.Studies.PottsEtAl2016.outer_no_grounded (sq : ShotQ) (lex : Lexicon) (w : World) :

utteranceTruth lex (Utterance.stmt PlayerQ.no sq) w = RSA.Domains.Quantity.meaning 3 RSA.Domains.Quantity.Utterance.none_ ⟨predCount sq lex w, ⋯⟩

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

The @cite{potts-etal-2016} predictions connect to two other parts of linglib:

someAllBlocking (ScalarImplicatures.Basic): The empirical datum that "some" implicatures are present in UE and blocked in DE. The Potts model derives both sides: UE enrichment (§7) and DE blocking (§6).
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.
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).

theorem Phenomena.ScalarImplicatures.Studies.PottsEtAl2016.matches_someAllBlocking :

someAllBlocking.implicatureInUE = true ∧ someAllBlocking.implicatureInDE = false

The Potts model matches the someAllBlocking empirical pattern: UE enrichment present (implicatureInUE = true) and DE blocking present (implicatureInDE = false).