@cite{franke-bergen-2020} — GI-RSA for Nested Aristotelians

@cite{franke-bergen-2020} @cite{fox-2007} @cite{franke-2011}

"Theory-driven statistical modeling for semantics and pragmatics: A case study on grammatically generated implicature readings"

The Model

Domain: Nested Aristotelian sentences "Q₁ of the aliens drank Q₂ of their water" with Q₁, Q₂ ∈ {none, some, all}. 7 world states based on which alien types exist (none-drinkers, some-drinkers, all-drinkers). 8 grammatical parses (subsets of {M, O, I} EXH positions) as latent variables.

The Global Intentions (GI) model treats the parse as a latent variable: the speaker chooses both an utterance and a parse, the listener marginalizes over parses to recover the world state.

• L0: L0(w|u,g) ∝ ⟦u⟧ᵍ(w) (meaning under parse g)
• S1: S1(u,g|w) ∝ L0(w|u,g)^α · P(g)
• L1: L1(w|u) ∝ P(w) · Σ_g S1(u,g|w)

Exhaustification uses compositional enrichment at inner/outer quantifier positions: Exh(Q) conjoins Q with the negation of all strictly stronger lexical alternatives on the {some, all} scale (@cite{fox-2007}). Only Exh(some) = "some but not all" is non-vacuous; Exh(all) and Exh(none) have no strictly stronger alternative.

At matrix position, EXH uses exh_MW (eq. A2): negate the LITERAL meanings of sentential alternatives that are strictly stronger than the sub-matrix enriched meaning, with a noncontradictory fallback. Sentential alternatives are the cross-product of scale-mate substitutions ({some, all}) for each on-scale quantifier. "none" is treated as off-scale; the paper notes (fn. 7) that including "not all" as an alternative to "none" has negligible effect on predictions.

Parameters: α = 2 (modeling choice; the paper estimates α jointly with cost and error parameters, reporting MLE ≈ 1.3 for GI), uniform priors. The paper's cost term c(u) for "none"-initial utterances and error term ε are omitted; the qualitative predictions below are robust to these simplifications.

Qualitative Findings

#	Finding	Theorem
1	SS exhaustifies inner Q	ss_inner_exh
2	SS exhaustifies outer Q	ss_outer_exh
3	AA identifies unique world	aa_identifies
4	AS exhaustifies inner Q	as_inner_exh
5	Full EXH preferred for SS	ss_parse_pref
6	Vanilla gets SS wrong (prefers wNA)	vanilla_ss_prefers_wNA
7	GI gets SS right (prefers wNS)	gi_ss_prefers_wNS
8	LU gets SS→wNS right	lu_ss_prefers_wNS
9	LI derives outer exh for SS	li_ss_outer_exh
10	LI also gets SS→wNS right	li_ss_prefers_wNS

Model Comparison

All four models from the paper are formalized as RSAConfig instances differing only in Latent type:

• Vanilla (§3.1): Latent := Unit — literal semantics only
• LU (§3.2): Latent := LULex (2 lexica) — simplified to L1 (the paper adds an S2/L2 layer, eqs. 14a-14b, following @cite{potts-etal-2016}; our L1-only approximation suffices for qualitative predictions)
• LI (§3.3): Latent := LIParse (4 parses) — speaker chooses parse
• GI (§3.4): Latent := Parse (8 parses) — full parse space

Bayesian model comparison: GI achieves 0.956 posterior probability, LI = 0.033, LU = 0.010, vanilla = 0.

inductive Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.AristQuant : Type

Aristotelian quantifiers: none, some, all.

• none : AristQuant
• some_ : AristQuant
• all : AristQuant

instance Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.instDecidableEqAristQuant : DecidableEq AristQuant

Equations

• Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.instDecidableEqAristQuant x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.instBEqAristQuant.beq : AristQuant → AristQuant → Bool

Equations

• Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.instBEqAristQuant.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.instBEqAristQuant : BEq AristQuant

Equations

• Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.instBEqAristQuant = { beq := Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.instBEqAristQuant.beq }

instance Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.instReprAristQuant : Repr AristQuant

Equations

• Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.instReprAristQuant = { reprPrec := Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.instReprAristQuant.repr }

def Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.instReprAristQuant.repr : AristQuant → ℕ → Std.Format

Equations

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

def Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.instInhabitedAristQuant.default : AristQuant

Equations

• Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.instInhabitedAristQuant.default = Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.AristQuant.none

instance Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.instInhabitedAristQuant : Inhabited AristQuant

Equations

• Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.instInhabitedAristQuant = { default := Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.instInhabitedAristQuant.default }

instance Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.instFintypeAristQuant : Fintype AristQuant

Equations

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

inductive Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.World : Type

The 7 world states, distinguished by which alien types exist. Three types: N (drank none), S (drank some but not all), A (drank all). Worlds are the 7 non-empty subsets of {N, S, A}.

• wN : World
• wNS : World
• wNA : World
• wNSA : World
• wS : World
• wSA : World
• wA : World

instance Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.instDecidableEqWorld : DecidableEq World

Equations

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

instance Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.instBEqWorld : BEq World

Equations

• Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.instBEqWorld = { beq := Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.instBEqWorld.beq }

def Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.instBEqWorld.beq : World → World → Bool

Equations

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

def Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.instReprWorld.repr : World → ℕ → Std.Format

Equations

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

instance Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.instReprWorld : Repr World

Equations

• Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.instReprWorld = { reprPrec := Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.instReprWorld.repr }

instance Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.instInhabitedWorld : Inhabited World

Equations

• Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.instInhabitedWorld = { default := Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.instInhabitedWorld.default }

def Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.instInhabitedWorld.default : World

Equations

• Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.instInhabitedWorld.default = Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.World.wN

instance Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.instFintypeWorld : Fintype World

Equations

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

inductive Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.Utterance : Type

The 9 nested Aristotelian utterances: Q_outer × Q_inner.

• nn : Utterance
• ns : Utterance
• na : Utterance
• sn : Utterance
• ss : Utterance
• sa : Utterance
• an : Utterance
• as_ : Utterance
• aa : Utterance

instance Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.instDecidableEqUtterance : DecidableEq Utterance

Equations

• Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.instDecidableEqUtterance x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.instBEqUtterance.beq : Utterance → Utterance → Bool

Equations

• Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.instBEqUtterance.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.instBEqUtterance : BEq Utterance

Equations

• Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.instBEqUtterance = { beq := Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.instBEqUtterance.beq }

instance Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.instReprUtterance : Repr Utterance

Equations

• Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.instReprUtterance = { reprPrec := Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.instReprUtterance.repr }

def Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.instReprUtterance.repr : Utterance → ℕ → Std.Format

Equations

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

instance Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.instInhabitedUtterance : Inhabited Utterance

Equations

• Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.instInhabitedUtterance = { default := Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.instInhabitedUtterance.default }

def Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.instInhabitedUtterance.default : Utterance

Equations

• Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.instInhabitedUtterance.default = Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.Utterance.nn

instance Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.instFintypeUtterance : Fintype Utterance

Equations

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

inductive Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.Parse : Type

The 8 grammatical parses: subsets of {M, O, I} EXH positions.

• none : Parse
• m : Parse
• o : Parse
• i : Parse
• mo : Parse
• mi : Parse
• oi : Parse
• moi : Parse

instance Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.instDecidableEqParse : DecidableEq Parse

Equations

• Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.instDecidableEqParse x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.instBEqParse.beq : Parse → Parse → Bool

Equations

• Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.instBEqParse.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.instBEqParse : BEq Parse

Equations

• Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.instBEqParse = { beq := Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.instBEqParse.beq }

def Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.instReprParse.repr : Parse → ℕ → Std.Format

Equations

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

instance Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.instReprParse : Repr Parse

Equations

• Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.instReprParse = { reprPrec := Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.instReprParse.repr }

def Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.instInhabitedParse.default : Parse

Equations

• Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.instInhabitedParse.default = Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.Parse.none

instance Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.instInhabitedParse : Inhabited Parse

Equations

• Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.instInhabitedParse = { default := Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.instInhabitedParse.default }

instance Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.instFintypeParse : Fintype Parse

Equations

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

def Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.World.hasN : World → Bool

Whether N-type aliens (drank none) exist.

Equations

• Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.World.wN.hasN = true
• Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.World.wNS.hasN = true
• Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.World.wNA.hasN = true
• Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.World.wNSA.hasN = true
• x✝.hasN = false

def Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.World.hasS : World → Bool

Whether S-type aliens (drank some but not all) exist.

Equations

• Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.World.wS.hasS = true
• Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.World.wNS.hasS = true
• Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.World.wSA.hasS = true
• Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.World.wNSA.hasS = true
• x✝.hasS = false

def Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.World.hasA : World → Bool

Whether A-type aliens (drank all) exist.

Equations

• Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.World.wA.hasA = true
• Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.World.wNA.hasA = true
• Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.World.wSA.hasA = true
• Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.World.wNSA.hasA = true
• x✝.hasA = false

def Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.Utterance.outer : Utterance → AristQuant

Outer quantifier of an utterance.

Equations

• Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.Utterance.nn.outer = Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.AristQuant.none
• Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.Utterance.ns.outer = Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.AristQuant.none
• Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.Utterance.na.outer = Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.AristQuant.none
• Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.Utterance.sn.outer = Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.AristQuant.some_
• Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.Utterance.ss.outer = Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.AristQuant.some_
• Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.Utterance.sa.outer = Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.AristQuant.some_
• Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.Utterance.an.outer = Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.AristQuant.all
• Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.Utterance.as_.outer = Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.AristQuant.all
• Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.Utterance.aa.outer = Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.AristQuant.all

def Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.Utterance.inner : Utterance → AristQuant

Inner quantifier of an utterance.

Equations

• Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.Utterance.nn.inner = Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.AristQuant.none
• Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.Utterance.sn.inner = Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.AristQuant.none
• Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.Utterance.an.inner = Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.AristQuant.none
• Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.Utterance.ns.inner = Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.AristQuant.some_
• Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.Utterance.ss.inner = Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.AristQuant.some_
• Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.Utterance.as_.inner = Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.AristQuant.some_
• Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.Utterance.na.inner = Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.AristQuant.all
• Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.Utterance.sa.inner = Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.AristQuant.all
• Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.Utterance.aa.inner = Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.AristQuant.all

def Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.Utterance.mk : AristQuant → AristQuant → Utterance

Construct an utterance from outer × inner quantifiers.

Equations

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

def Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.AristQuant.onScale : AristQuant → Bool

Whether a quantifier is on the lexical scale {some, all}.

Equations

• Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.AristQuant.some_.onScale = true
• Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.AristQuant.all.onScale = true
• Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.AristQuant.none.onScale = false

def Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.Parse.hasI : Parse → Bool

Whether parse includes EXH at inner position.

Equations

• Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.Parse.i.hasI = true
• Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.Parse.mi.hasI = true
• Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.Parse.oi.hasI = true
• Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.Parse.moi.hasI = true
• x✝.hasI = false

def Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.Parse.hasO : Parse → Bool

Whether parse includes EXH at outer position.

Equations

• Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.Parse.o.hasO = true
• Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.Parse.mo.hasO = true
• Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.Parse.oi.hasO = true
• Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.Parse.moi.hasO = true
• x✝.hasO = false

def Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.Parse.hasM : Parse → Bool

Whether parse includes EXH at matrix position.

Equations

• Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.Parse.m.hasM = true
• Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.Parse.mo.hasM = true
• Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.Parse.mi.hasM = true
• Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.Parse.moi.hasM = true
• x✝.hasM = false

def Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.innerTypeSat (qi : AristQuant) : Bool × Bool × Bool

Inner VP satisfaction: which alien types satisfy "drank Q"?

• Q = none: N-types satisfy (drank none of their water)
• Q = some: S-types and A-types satisfy (drank some)
• Q = all: only A-types satisfy (drank all)

Equations

• Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.innerTypeSat Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.AristQuant.none = (true, false, false)
• Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.innerTypeSat Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.AristQuant.some_ = (false, true, true)
• Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.innerTypeSat Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.AristQuant.all = (false, false, true)

def Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.outerEval (qo : AristQuant) (nSat sSat aSat : Bool) (w : World) : Bool

Outer quantifier evaluation: does the world satisfy "Q_outer of the aliens [satisfy inner VP]"? nSat, sSat, aSat indicate which alien types satisfy the inner VP.

Equations

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

def Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.literalMeaning (u : Utterance) (w : World) : Bool

Literal meaning: compose inner VP satisfaction with outer quantifier.

Equations

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

def Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.allWorlds : List World

All 7 worlds for enumeration.

Equations

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

def Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.enrichedInnerTypeSat (qi : AristQuant) (hasI : Bool) : Bool × Bool × Bool

Inner VP satisfaction after EXH enrichment. Only "some" is enrichable: Exh(some) = "some but not all" — satisfied by S-types only (not A-types). Exh(none) and Exh(all) are vacuous (no strictly stronger alternative).

Equations

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

def Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.scale : List AristQuant

The lexical scale: {some, all}.

Equations

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

def Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.matrixAlts (u : Utterance) : List Utterance

Sentential alternatives at matrix position: cross-product of scale-mate substitutions for each scalar item in the utterance. Non-scalar positions are held fixed.

Equations

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

def Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.exhMeaning (p : Parse) (u : Utterance) : World → Bool

Exhaustified meaning under a given parse, using compositional enrichment.

Inner/outer EXH enrich quantifiers in situ (at the quantifier level, not the sentence level), following the paper's Appendix. Only "some" → "some but not all" is a meaningful enrichment; Exh(all) and Exh(none) are vacuous (no strictly stronger lexical alternative on the scale).

Matrix EXH uses exh_MW with a strength filter: negate the LITERAL meanings of sentential alternatives that are strictly stronger than the enriched (sub-matrix) meaning. Fall back to no matrix EXH if the conjunction is contradictory (eq. A2).

Equations

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

theorem Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.ss_literal_count : (List.filter (literalMeaning Utterance.ss) allWorlds).length = 6

Literal SS is true at 6 of 7 worlds (all except wN).

theorem Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.exh_i_ss : exhMeaning Parse.i Utterance.ss World.wNS = true ∧ exhMeaning Parse.i Utterance.ss World.wNSA = true ∧ exhMeaning Parse.i Utterance.ss World.wS = true ∧ exhMeaning Parse.i Utterance.ss World.wSA = true ∧ exhMeaning Parse.i Utterance.ss World.wN = false ∧ exhMeaning Parse.i Utterance.ss World.wNA = false ∧ exhMeaning Parse.i Utterance.ss World.wA = false

EXH_I(SS) = worlds with S-types (compositional: "some aliens drank some but not all"). Inner EXH enriches "some" to "some but not all", so S-types satisfy the VP but A-types do not. The outer "some" requires at least one S-type, giving {wNS, wNSA, wS, wSA}.

theorem Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.exh_oi_ss : exhMeaning Parse.oi Utterance.ss World.wNS = true ∧ exhMeaning Parse.oi Utterance.ss World.wNSA = true ∧ exhMeaning Parse.oi Utterance.ss World.wSA = true ∧ exhMeaning Parse.oi Utterance.ss World.wS = false

EXH_OI(SS) = {wNS, wNSA, wSA} — outer "some but not all" alien types satisfy the enriched inner predicate. wS excluded because at wS all types (just S) satisfy the inner pred, so "all" would be true.

theorem Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.exh_moi_ss (w : World) : exhMeaning Parse.moi Utterance.ss w = exhMeaning Parse.oi Utterance.ss w

EXH_MOI(SS) = EXH_OI(SS) = {wNS, wNSA, wSA} — matrix EXH is vacuous here because no sentential alternative is strictly stronger than the OI-enriched meaning.

theorem Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.aa_singleton (p : Parse) (w : World) : exhMeaning p Utterance.aa w = (w == World.wA)

AA is true only at wA under all parses.

theorem Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.table1_ss : List.map (exhMeaning Parse.none Utterance.ss) allWorlds = [false, true, true, true, true, true, true] ∧ List.map (exhMeaning Parse.i Utterance.ss) allWorlds = [false, true, false, true, true, true, false] ∧ List.map (exhMeaning Parse.oi Utterance.ss) allWorlds = [false, true, false, true, false, true, false] ∧ List.map (exhMeaning Parse.moi Utterance.ss) allWorlds = [false, true, false, true, false, true, false]

Full truth table for SS across key parses, matching Table 1 of the paper. Format: (parse, [wN, wNS, wNA, wNSA, wS, wSA, wA]).

noncomputable def Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.giConfig : RSA.RSAConfig Utterance World

GI-RSA model for nested Aristotelians. Parse is the latent variable; meaning under each parse is determined by compositional exhaustification. α = 2 is a modeling choice for qualitative predictions (the paper estimates α ≈ 1.3 jointly with cost and error parameters).

Equations

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

theorem Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.ss_inner_exh : giConfig.L1 Utterance.ss World.wNS > giConfig.L1 Utterance.ss World.wNSA

SS exhaustifies inner quantifier: L1 prefers wNS (N and S types, no A) over wNSA (all three types including A). Inner EXH negates "some drank all", disfavoring worlds with A-type aliens.

theorem Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.ss_outer_exh : giConfig.L1 Utterance.ss World.wNS > giConfig.L1 Utterance.ss World.wS

SS exhaustifies outer quantifier: L1 prefers wNS (mixed N+S types) over wS (only S-type). At wS, "all aliens drank some but not all" would be true, but outer EXH negates the "all" reading, preferring worlds where not all alien types are uniform.

theorem Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.aa_identifies : giConfig.L1 Utterance.aa World.wA > giConfig.L1 Utterance.aa World.wSA

AA correctly identifies the unique world where all aliens drank all.

theorem Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.as_inner_exh : giConfig.L1 Utterance.as_ World.wS > giConfig.L1 Utterance.as_ World.wA

AS exhaustifies inner: L1 prefers wS (all aliens are "some" drinkers) over wA (all aliens are "all" drinkers).

theorem Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.ss_parse_pref : giConfig.L1_latent Utterance.ss Parse.moi > giConfig.L1_latent Utterance.ss Parse.none

Full exhaustification is preferred: L1 assigns more probability to the fully exhaustified parse (MOI) than to the literal parse for SS.

noncomputable def Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.vanillaConfig : RSA.RSAConfig Utterance World

Vanilla RSA (§3.1): literal semantics only, no grammatical enrichment. Each utterance has a single reading; no latent parse variable.

Equations

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

inductive Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.LULex : Type

LU lexicon: literal or OI (inner + outer EXH). Each speaker has a fixed lexicon; listeners marginalize over the two lexica to infer the world state. Mirrors the @cite{potts-etal-2016} architecture (Latent := Lexicon).

• lit : LULex
• oi : LULex

instance Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.instDecidableEqLULex : DecidableEq LULex

Equations

• Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.instDecidableEqLULex x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.instBEqLULex.beq : LULex → LULex → Bool

Equations

• Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.instBEqLULex.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.instBEqLULex : BEq LULex

Equations

• Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.instBEqLULex = { beq := Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.instBEqLULex.beq }

instance Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.instReprLULex : Repr LULex

Equations

• Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.instReprLULex = { reprPrec := Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.instReprLULex.repr }

def Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.instReprLULex.repr : LULex → ℕ → Std.Format

Equations

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

def Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.instInhabitedLULex.default : LULex

Equations

• Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.instInhabitedLULex.default = Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.LULex.lit

instance Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.instInhabitedLULex : Inhabited LULex

Equations

• Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.instInhabitedLULex = { default := Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.instInhabitedLULex.default }

instance Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.instFintypeLULex : Fintype LULex

Equations

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

def Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.LULex.toParse : LULex → Parse

Map LU lexicon to the corresponding Parse.

Equations

• Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.LULex.lit.toParse = Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.Parse.none
• Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.LULex.oi.toParse = Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.Parse.oi

noncomputable def Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.luConfig : RSA.RSAConfig Utterance World

Lexical Uncertainty model (§3.2): speaker has a fixed lexicon (lit or OI), listener marginalizes over lexica. Simplified to L1 — the paper adds an S2/L2 layer (eqs. 14a-14b) for production predictions.

Equations

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

inductive Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.LIParse : Type

LI parse: lit, I, O, or OI. The speaker actively chooses a parse per utterance (unlike LU, where each speaker has a fixed lexicon).

• lit : LIParse
• i : LIParse
• o : LIParse
• oi : LIParse

instance Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.instDecidableEqLIParse : DecidableEq LIParse

Equations

• Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.instDecidableEqLIParse x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.instBEqLIParse : BEq LIParse

Equations

• Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.instBEqLIParse = { beq := Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.instBEqLIParse.beq }

def Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.instBEqLIParse.beq : LIParse → LIParse → Bool

Equations

• Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.instBEqLIParse.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.instReprLIParse : Repr LIParse

Equations

• Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.instReprLIParse = { reprPrec := Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.instReprLIParse.repr }

def Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.instReprLIParse.repr : LIParse → ℕ → Std.Format

Equations

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

def Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.instInhabitedLIParse.default : LIParse

Equations

• Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.instInhabitedLIParse.default = Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.LIParse.lit

instance Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.instInhabitedLIParse : Inhabited LIParse

Equations

• Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.instInhabitedLIParse = { default := Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.instInhabitedLIParse.default }

instance Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.instFintypeLIParse : Fintype LIParse

Equations

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

def Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.LIParse.toParse : LIParse → Parse

Map LI parse to the full Parse type.

Equations

• Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.LIParse.lit.toParse = Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.Parse.none
• Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.LIParse.i.toParse = Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.Parse.i
• Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.LIParse.o.toParse = Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.Parse.o
• Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.LIParse.oi.toParse = Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.Parse.oi

noncomputable def Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.liConfig : RSA.RSAConfig Utterance World

Lexical Intentions model (§3.3): speaker chooses (utterance, parse) jointly from {lit, I, O, OI}, listener marginalizes over parses.

Equations

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

The paper's key empirical finding: GI predicts SS→wNS (the state where N-types and S-types coexist), matching production data. Vanilla RSA cannot access the exhaustified reading ⟦SS⟧^MOI = {wNS, wNSA, wSA} and instead predicts wNA (N+A types) for hearing SS.

theorem Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.vanilla_ss_prefers_wNA : vanillaConfig.L1 Utterance.ss World.wNA > vanillaConfig.L1 Utterance.ss World.wNS

Vanilla RSA hearing SS: prefers wNA over wNS. Without exhaustification, SS is literally true at 6/7 worlds. At wNA, the competing utterances (SN, SA) are less informative than at wNS (where NA is a strong competitor), so SS "wins" more of the S1 score at wNA.

This is the wrong prediction — production data shows SS is used for state wNS, not wNA. Evidence for grammatical enrichment.

theorem Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.gi_ss_prefers_wNS : giConfig.L1 Utterance.ss World.wNS > giConfig.L1 Utterance.ss World.wNA

GI correctly predicts the opposite: SS→wNS, not wNA. The exhaustified parses concentrate probability on worlds with S-types but not A-types, overriding the literal-meaning signal.

theorem Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.lu_ss_prefers_wNS : luConfig.L1 Utterance.ss World.wNS > luConfig.L1 Utterance.ss World.wNA

LU also gets the key SS prediction right: wNS > wNA. The OI lexicon gives ⟦SS⟧^OI = {wNS, wNSA, wSA}, which excludes wNA. The lit lexicon includes both, but OI's exclusion of wNA is enough to tip the balance. Same architecture as @cite{potts-etal-2016} (Latent := Lexicon).

theorem Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.li_ss_outer_exh : liConfig.L1 Utterance.ss World.wNS > liConfig.L1 Utterance.ss World.wS

LI derives outer exhaustification for SS via the OI parse: ⟦SS⟧^OI = {wNS, wNSA, wSA} pins down worlds with mixed types.

theorem Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.li_ss_prefers_wNS : liConfig.L1 Utterance.ss World.wNS > liConfig.L1 Utterance.ss World.wNA

LI also gets the wNS > wNA ordering that vanilla misses.

theorem Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.table1_nn (p : Parse) : List.map (exhMeaning p Utterance.nn) allWorlds = [false, false, false, false, true, true, true]

NN is vacuously exhaustified: "none" is off-scale, so EXH at any position has no alternatives to exclude. All parses agree.

theorem Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.table1_an (p : Parse) : List.map (exhMeaning p Utterance.an) allWorlds = [true, false, false, false, false, false, false]

AN is maximally informative: all types must satisfy "drank none." Only wN (all N-types) works. All parses agree.

theorem Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.table1_aa (p : Parse) : List.map (exhMeaning p Utterance.aa) allWorlds = [false, false, false, false, false, false, true]

AA is maximally informative: all types must satisfy "drank all." Only wA works. All parses agree (already proved in aa_singleton).

theorem Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.table1_ns : List.map (exhMeaning Parse.none Utterance.ns) allWorlds = [true, false, false, false, false, false, false]

NS lit = {wN}: "none drank some" requires no type to satisfy "drank some." S-types and A-types satisfy, so they must be absent. Only wN (all N-types) works.

theorem Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.table1_sa : List.map (exhMeaning Parse.none Utterance.sa) allWorlds = [false, false, true, true, false, true, true] ∧ List.map (exhMeaning Parse.o Utterance.sa) allWorlds = [false, false, true, true, false, true, false]

SA: "some drank all" requires ≥1 A-type. EXH_I vacuous (inner=all). EXH_O enriches outer "some" to "some but not all," excluding wA (where all types are A → "all" would hold).

theorem Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.table1_na : List.map (exhMeaning Parse.none Utterance.na) allWorlds = [true, true, false, false, true, false, false] ∧ List.map (exhMeaning Parse.m Utterance.na) allWorlds = [false, true, false, false, true, false, false]

NA: "none drank all" requires no A-types. True at {wN, wNS, wS}. Matrix EXH negates the stronger alternative NS (= "none drank some" = {wN}), removing wN.

theorem Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.table1_sn : List.map (exhMeaning Parse.none Utterance.sn) allWorlds = [true, true, true, true, false, false, false] ∧ List.map (exhMeaning Parse.o Utterance.sn) allWorlds = [false, true, true, true, false, false, false]

SN: "some drank none" requires ≥1 N-type. True at {wN, wNS, wNA, wNSA}. EXH_O enriches outer "some" to "some but not all," negating AN = {wN}. Matrix EXH gives the same result (M ⊆ O for SN).

theorem Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.table1_as_full : List.map (exhMeaning Parse.none Utterance.as_) allWorlds = [false, false, false, false, true, true, true] ∧ List.map (exhMeaning Parse.i Utterance.as_) allWorlds = [false, false, false, false, true, false, false] ∧ List.map (exhMeaning Parse.m Utterance.as_) allWorlds = [false, false, false, false, true, true, false]

AS: "all drank some" requires every type to satisfy "drank some." EXH_I enriches to "all drank [some but not all]" — only S-types satisfy, so only wS (all S-types) works. Matrix EXH without I negates AA, excluding wA (where "all drank all" holds).

theorem Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.literal_eq_exh_none (u : Utterance) (w : World) : literalMeaning u w = exhMeaning Parse.none u w

Literal meaning equals exhaustified meaning under the empty parse.

theorem Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.m_ss_singleton (w : World) : exhMeaning Parse.m Utterance.ss w = (w == World.wNS)

⟦SS⟧^M = {wNS}: matrix EXH narrows SS to a single world. This is the paper's key finding (§6): the M reading "uniquely singles out this world state" (p. e86, eq. 22), giving GI its decisive advantage over LI and LU.

theorem Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.li_excludes_matrix (l : LIParse) : l.toParse.hasM = false

LI cannot access M-containing parses: none of {lit, I, O, OI} include matrix EXH. This excludes ⟦SS⟧^M from LI's parse space.

theorem Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.lu_excludes_matrix (l : LULex) : l.toParse.hasM = false

LU cannot access M-containing parses: neither lit nor OI include matrix EXH. This excludes ⟦SS⟧^M from LU's parse space.

theorem Phenomena.ScalarImplicatures.Studies.FrankeBergen2020.latent_space_hierarchy : Fintype.card Unit = 1 ∧ Fintype.card LULex = 2 ∧ Fintype.card LIParse = 4 ∧ Fintype.card Parse = 8

The latent space grows across models: 1 → 2 → 4 → 8.

Connection to @cite{potts-etal-2016}

The LU model here uses Latent := LULex (2 lexica: lit, OI), the same RSAConfig architecture as @cite{potts-etal-2016}'s Latent := Lexicon (weak, strong "some"). Both implement Bergen et al.'s lexical uncertainty via RSAConfig's latent variable mechanism — no special LUScenario infrastructure needed. Our LU uses L1 only; the paper adds an S2/L2 layer (eqs. 14a-14b) for production predictions.

Connection to @cite{cremers-wilcox-spector-2023}

Cremers et al. test 9 model variants, including EXH-LU and RSA-LI, which correspond to our luConfig and liConfig. Their key finding — grammatical models (EXH-LU, RSA-LI) block anti-exhaustivity regardless of prior bias — is consistent with our LU and LI predictions: both correctly derive exhaustification for SS (lu_ss_prefers_wNS, li_ss_outer_exh), concentrating probability on the exhaustified worlds.

Connection to @cite{franke-2011}

The matrix EXH in exhMeaning uses exh_MW: conjoin the sub-matrix meaning with the negation of all strictly stronger alternatives' literal meanings. @cite{franke-2011} proves that IBR fixed points equal exh_MW for scalar games (Franke2011.r1_eq_exhMW_under_totality). This grounds the matrix position of our GI model in game-theoretic equilibrium semantics.

Connection to @cite{fox-2007}

The exhaustification implementation uses compositional enrichment at inner/outer quantifier positions (scale-mate substitution on {some, all}) and MW-style sentential alternative negation at matrix position. The models differ only in which EXH positions are available to the speaker/listener, demonstrating that the key theoretical question is not HOW to exhaustify but WHERE EXH can be inserted and WHO controls the insertion (grammar vs. speaker vs. listener).

Why GI wins (§6)

The decisive advantage of GI over LI and LU is the M parse: m_ss_singleton proves ⟦SS⟧^M = {wNS}, and li_excludes_matrix / lu_excludes_matrix prove that M-containing parses are structurally unavailable to the smaller models. Only GI can access the reading that uniquely identifies wNS, explaining its superior production predictions for SS (Figure 5, Figure 7c).