Documentation

Linglib.Phenomena.ScalarImplicatures.Studies.PottsEtAl2016

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

@cite{potts-etal-2016} @cite{chemla-spector-2011}

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

Empirical anchor: @cite{chemla-spector-2011} #

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 @cite{geurts-pouscoulous-2009}).

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 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

@[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✝

Instances For

@[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 }

def PottsEtAl2016.instInhabitedWorld.default :

Equations

PottsEtAl2016.instInhabitedWorld.default = PottsEtAl2016.World.NNN

Instances For

@[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 :

Inner quantifier: over a player's shots.

all : ShotQ
none_ : ShotQ
some_ : ShotQ

Instances For

@[implicit_reducible]

instance PottsEtAl2016.instDecidableEqShotQ :

DecidableEq ShotQ

Equations

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

@[implicit_reducible]

instance PottsEtAl2016.instReprShotQ :

Repr ShotQ

Equations

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

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✝

Instances For

def PottsEtAl2016.instInhabitedShotQ.default :

Equations

PottsEtAl2016.instInhabitedShotQ.default = PottsEtAl2016.ShotQ.all

Instances For

@[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 :

Outer quantifier: over players.

every : PlayerQ
exactlyOne : PlayerQ
no : PlayerQ

Instances For

@[implicit_reducible]

instance PottsEtAl2016.instDecidableEqPlayerQ :

DecidableEq PlayerQ

Equations

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

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✝

Instances For

@[implicit_reducible]

instance PottsEtAl2016.instReprPlayerQ :

Equations

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

@[implicit_reducible]

instance PottsEtAl2016.instInhabitedPlayerQ :

Inhabited PlayerQ

Equations

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

def PottsEtAl2016.instInhabitedPlayerQ.default :

Equations

PottsEtAl2016.instInhabitedPlayerQ.default = PottsEtAl2016.PlayerQ.every

Instances For

@[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 }

inductive PottsEtAl2016.Utterance :

Utterance: outer quantifier × inner quantifier, plus null.

stmt : PlayerQ → ShotQ → Utterance
null : Utterance

Instances For

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

Decidable (x✝ = x✝¹)

Equations

One or more equations did not get rendered due to their size.
PottsEtAl2016.instDecidableEqUtterance.decEq (PottsEtAl2016.Utterance.stmt a a_1) PottsEtAl2016.Utterance.null = isFalse ⋯
PottsEtAl2016.instDecidableEqUtterance.decEq PottsEtAl2016.Utterance.null (PottsEtAl2016.Utterance.stmt a a_1) = isFalse ⋯
PottsEtAl2016.instDecidableEqUtterance.decEq PottsEtAl2016.Utterance.null PottsEtAl2016.Utterance.null = isTrue ⋯

Instances For

@[implicit_reducible]

instance PottsEtAl2016.instDecidableEqUtterance :

DecidableEq Utterance

Equations

PottsEtAl2016.instDecidableEqUtterance = PottsEtAl2016.instDecidableEqUtterance.decEq

def PottsEtAl2016.instReprUtterance.repr :

Utterance → ℕ → Std.Format

Equations

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

Instances For

@[implicit_reducible]

instance PottsEtAl2016.instReprUtterance :

Equations

PottsEtAl2016.instReprUtterance = { reprPrec := PottsEtAl2016.instReprUtterance.repr }

def PottsEtAl2016.instInhabitedUtterance.default :

Equations

PottsEtAl2016.instInhabitedUtterance.default = PottsEtAl2016.Utterance.stmt default default

Instances For

@[implicit_reducible]

instance PottsEtAl2016.instInhabitedUtterance :

Inhabited Utterance

Equations

PottsEtAl2016.instInhabitedUtterance = { default := PottsEtAl2016.instInhabitedUtterance.default }

@[implicit_reducible]

instance PottsEtAl2016.instFintypeUtterance :

Fintype Utterance

Equations

PottsEtAl2016.instFintypeUtterance = Fintype.ofEquiv ((_ : PottsEtAl2016.PlayerQ) × PottsEtAl2016.ShotQ ⊕ Unit) PottsEtAl2016.Utterance.proxyTypeEquiv

inductive PottsEtAl2016.Lexicon :

Lexicon: how "some" is interpreted.

weak : Lexicon
strong : Lexicon

Instances For

@[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.

Instances For

@[implicit_reducible]

instance PottsEtAl2016.instReprLexicon :

Equations

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

def PottsEtAl2016.instInhabitedLexicon.default :

Equations

PottsEtAl2016.instInhabitedLexicon.default = PottsEtAl2016.Lexicon.weak

Instances For

@[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 }

def PottsEtAl2016.World.numScored :

World → ℕ

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

Equations

Instances For

def PottsEtAl2016.World.numAced :

World → ℕ

Number of players who aced (hit all shots).

Equations

Instances For

def PottsEtAl2016.World.numScoredNotAced :

World → ℕ

Number of players who scored but did not ace.

Equations

Instances For

def PottsEtAl2016.World.numNothing :

World → ℕ

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

Equations

Instances For

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

Instances For

def PottsEtAl2016.utteranceTruth (lex : Lexicon) :

Utterance → World → Bool

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

Equations

PottsEtAl2016.utteranceTruth lex PottsEtAl2016.Utterance.null x✝ = true
PottsEtAl2016.utteranceTruth lex (PottsEtAl2016.Utterance.stmt PottsEtAl2016.PlayerQ.every sq) x✝ = (PottsEtAl2016.predCount sq lex x✝ == 3)
PottsEtAl2016.utteranceTruth lex (PottsEtAl2016.Utterance.stmt PottsEtAl2016.PlayerQ.exactlyOne sq) x✝ = (PottsEtAl2016.predCount sq lex x✝ == 1)
PottsEtAl2016.utteranceTruth lex (PottsEtAl2016.Utterance.stmt PottsEtAl2016.PlayerQ.no sq) x✝ = (PottsEtAl2016.predCount sq lex x✝ == 0)

Instances For

noncomputable def 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 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 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

theorem PottsEtAl2016.de_enrichment_widens :

{w : World | utteranceTruth Lexicon.weak (Utterance.stmt PlayerQ.no ShotQ.some_) w = true}.card < {w : World | utteranceTruth Lexicon.strong (Utterance.stmt 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 (Utterance.stmt PlayerQ.every ShotQ.some_) w = true}.card < {w : World | utteranceTruth Lexicon.weak (Utterance.stmt 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.

"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 :

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 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 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 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 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 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 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

@[implicit_reducible]

instance PottsEtAl2016.instDecidableEqFinding :

DecidableEq Finding

Equations

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

@[implicit_reducible]

instance PottsEtAl2016.instReprFinding :

Equations

PottsEtAl2016.instReprFinding = { reprPrec := PottsEtAl2016.instReprFinding.repr }

def PottsEtAl2016.instReprFinding.repr :

Finding → ℕ → Std.Format

Equations

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

Instances For

def PottsEtAl2016.findings :

All findings.

Equations

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

Instances For

def 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 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 Phenomena.ScalarImplicatures.QuantityDomain.meaning. This grounds the stipulated utteranceTruth in the shared quantifier infrastructure.

See also: GoodmanStuhlmuller2013PMF's qMeaning definition (uses the same QuantityDomain.meaning-derived shape).

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

utteranceTruth lex (Utterance.stmt PlayerQ.every sq) w = Phenomena.ScalarImplicatures.QuantityDomain.meaning 3 Phenomena.ScalarImplicatures.QuantityDomain.Utterance.all ⟨predCount sq lex w, ⋯⟩

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

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

utteranceTruth lex (Utterance.stmt PlayerQ.no sq) w = Phenomena.ScalarImplicatures.QuantityDomain.meaning 3 Phenomena.ScalarImplicatures.QuantityDomain.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 PottsEtAl2016.matches_someAllBlocking :

Phenomena.ScalarImplicatures.someAllBlocking.implicatureInUE = true ∧ Phenomena.ScalarImplicatures.someAllBlocking.implicatureInDE = false

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