@cite{goodman-stuhlmuller-2013}: Empirical Data

@cite{goodman-stuhlmuller-2013}

"Knowledge and Implicature: Modeling Language Understanding as Social Cognition" Topics in Cognitive Science 5(1): 173-184

Paradigm

Three objects that may have a property. Speaker observes a subset (access = 1, 2, or 3) and makes a quantified or numeral statement. Listener divides $100 among world states (0-3 objects have property). Speaker access is common knowledge.

Trials with knowledgeability bet <= 70 excluded from primary analysis.

Qualitative Findings

The paper's central finding: scalar implicature and upper-bounded numeral interpretations are modulated by speaker knowledge. When the speaker has full access, listeners draw upper-bounded inferences; when access is partial, these inferences weaken or disappear.

#	Finding	Word	Access	Comparison	Evidence
1	Implicature present	"some"	3	state 2 > state 3	t(43)=-10.2, p<.001
2	Implicature canceled	"some"	1	state 2 not > state 3	t(31)=0.77, p=.78
3	Implicature canceled	"some"	2	state 2 not > state 3	t(28)=-0.82, p=.21
4	Upper-bounded	"two"	3	state 2 > state 3	t(43)=-10.2, p<.001
5	Not upper-bounded	"two"	2	state 2 not > state 3	t(24)=1.1, p=.87
6	Upper-bounded	"one"	3	state 1 > state 2	t(42)=-13.1, p<.001
7	Upper-bounded	"one"	3	state 1 > state 3	t(42)=-17.1, p<.001
8	Not upper-bounded	"one"	1	state 1 not > state 2	t(24)=1.9, p=.96
9	Not upper-bounded	"one"	1	state 1 not > state 3	t(24)=3.2, p=1.0
10	Partial	"one"	2	state 1 > state 3	t(25)=-3.9, p<.001
11	Partial	"one"	2	state 1 not > state 2	t(25)=1.5, p=.92

def Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.nPerExperiment : ℕ

Equations

• Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.nPerExperiment = 50

def Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.nObjects : ℕ

Equations

• Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.nObjects = 3

inductive Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.Finding : Type

The 11 qualitative findings from @cite{goodman-stuhlmuller-2013} Experiments 1-2. Each finding is a pairwise bet comparison between world states under a specific (word, access) condition.

• some_full_implicature : Finding

  Full access: bets on state 2 > state 3 (scalar implicature present). Evidence: t(43) = -10.2, p < .001.

• some_minimal_canceled : Finding

  Minimal access (a=1): state 2 does not exceed state 3 (canceled). Evidence: t(31) = 0.77, p = .78.

• some_partial_canceled : Finding

  Partial access (a=2): state 2 does not exceed state 3 (canceled). Evidence: t(28) = -0.82, p = .21.

• two_full_upper_bounded : Finding

  Full access: "two" -> state 2 > state 3 (upper-bounded reading). Evidence: t(43) = -10.2, p < .001.

• two_partial_weakened : Finding

  Partial access (a=2): state 2 does not exceed state 3 (weakened). Evidence: t(24) = 1.1, p = .87.

• one_full_1v2 : Finding

  Full access: "one" -> state 1 > state 2. Evidence: t(42) = -13.1, p < .001.

• one_full_1v3 : Finding

  Full access: "one" -> state 1 > state 3. Evidence: t(42) = -17.1, p < .001.

• one_minimal_1v2_canceled : Finding

  Minimal access (a=1): state 1 does not exceed state 2 (canceled). Evidence: t(24) = 1.9, p = .96.

• one_minimal_1v3_canceled : Finding

  Minimal access (a=1): state 1 does not exceed state 3 (canceled). Evidence: t(24) = 3.2, p = 1.0.

• one_partial_1v3 : Finding

  Partial access (a=2): state 1 > state 3 (partial implicature holds). Evidence: t(25) = -3.9, p < .001.

• one_partial_1v2_canceled : Finding

  Partial access (a=2): state 1 does not exceed state 2 (still canceled). Evidence: t(25) = 1.5, p = .92.

instance Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.instDecidableEqFinding : DecidableEq Finding

Equations

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

def Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.instBEqFinding.beq : Finding → Finding → Bool

Equations

• Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.instBEqFinding.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.instBEqFinding : BEq Finding

Equations

• Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.instBEqFinding = { beq := Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.instBEqFinding.beq }

def Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.instReprFinding.repr : Finding → ℕ → Std.Format

Equations

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

instance Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.instReprFinding : Repr Finding

Equations

• Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.instReprFinding = { reprPrec := Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.instReprFinding.repr }

def Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.findings : List Finding

All findings from the paper.

Equations

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

structure Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.BetComparison : Type

A pairwise comparison of bets on two world states in a condition.

The key observable: did participants allocate significantly more money to world state stateA than to stateB? A theory that predicts the listener's posterior P(state | word, access) can be checked against this.

• experiment : ℕ
• word : String
• access : ℕ

  How many of 3 objects the speaker observed

• stateA : ℕ
• stateB : ℕ
• aExceedsB : Bool

  Did bets on stateA significantly exceed bets on stateB?

• evidence : String

def Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.instReprBetComparison.repr : BetComparison → ℕ → Std.Format

Equations

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

instance Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.instReprBetComparison : Repr BetComparison

Equations

• Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.instReprBetComparison = { reprPrec := Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.instReprBetComparison.repr }

def Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.exp1_some_a3_2v3 : BetComparison

Access = 3: bets on state 2 > bets on state 3.

Equations

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

def Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.exp1_some_a1_2v3 : BetComparison

Access = 1: bets on state 2 did NOT exceed bets on state 3.

Equations

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

def Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.exp1_some_a2_2v3 : BetComparison

Access = 2: bets on state 2 did NOT exceed bets on state 3.

Equations

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

def Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.exp1_a3_vs_a1_on_state3 : BetComparison

Bets on state 3 at access = 3 significantly lower than at access = 1.

Equations

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

def Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.exp2_two_a3_2v3 : BetComparison

"two", access = 3: bets on state 2 > bets on state 3.

Equations

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

def Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.exp2_two_a2_2v3 : BetComparison

"two", access = 2: bets on state 2 did NOT exceed bets on state 3.

Equations

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

def Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.exp2_one_a3_1v2 : BetComparison

"one", access = 3: bets on state 1 > bets on state 2.

Equations

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

def Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.exp2_one_a3_1v3 : BetComparison

"one", access = 3: bets on state 1 > bets on state 3.

Equations

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

def Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.exp2_one_a1_1v2 : BetComparison

"one", access = 1: bets on state 1 did NOT exceed bets on state 2.

Equations

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

def Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.exp2_one_a1_1v3 : BetComparison

"one", access = 1: bets on state 1 did NOT exceed bets on state 3.

Equations

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

def Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.exp2_one_a2_1v3 : BetComparison

"one", access = 2: bets on state 1 > bets on state 3 (partial).

Equations

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

def Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.exp2_one_a2_1v2 : BetComparison

"one", access = 2: bets on state 1 did NOT exceed bets on state 2.

Equations

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

structure Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.OmnibusTest : Type

• description : String
• testType : String
• statistic : Float
• p : Float

def Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.instReprOmnibusTest.repr : OmnibusTest → ℕ → Std.Format

Equations

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

instance Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.instReprOmnibusTest : Repr OmnibusTest

Equations

• Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.instReprOmnibusTest = { reprPrec := Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.instReprOmnibusTest.repr }

def Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.exp1_access_effect : OmnibusTest

Equations

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

def Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.exp2_access_main : OmnibusTest

Equations

• Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.exp2_access_main = { description := "Main effect of access", testType := "ANOVA, F(2, 205)", statistic := 6.57, p := 1e-2 }

def Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.exp2_word_main : OmnibusTest

Equations

• Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.exp2_word_main = { description := "Main effect of word", testType := "ANOVA, F(2, 205)", statistic := 269.8, p := 1e-3 }

def Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.exp2_interaction : OmnibusTest

Equations

• Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.exp2_interaction = { description := "Word x access interaction", testType := "ANOVA, F(1, 205)", statistic := 34.7, p := 1e-3 }

structure Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.KnowledgeabilityCheck : Type

• access : ℕ
• meanBet : Float
• sd : Float

instance Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.instReprKnowledgeabilityCheck : Repr KnowledgeabilityCheck

Equations

• Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.instReprKnowledgeabilityCheck = { reprPrec := Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.instReprKnowledgeabilityCheck.repr }

def Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.instReprKnowledgeabilityCheck.repr : KnowledgeabilityCheck → ℕ → Std.Format

Equations

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

def Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.knowledge_a1 : KnowledgeabilityCheck

Equations

• Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.knowledge_a1 = { access := 1, meanBet := 27.1, sd := 4.9 }

def Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.knowledge_a2 : KnowledgeabilityCheck

Equations

• Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.knowledge_a2 = { access := 2, meanBet := 34.8, sd := 5.7 }

def Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.knowledge_a3 : KnowledgeabilityCheck

Equations

• Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.knowledge_a3 = { access := 3, meanBet := 93.0, sd := 2.7 }

def Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.Finding.evidence : Finding → BetComparison

The statistical evidence for each finding.

Equations

• Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.Finding.some_full_implicature.evidence = Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.exp1_some_a3_2v3
• Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.Finding.some_minimal_canceled.evidence = Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.exp1_some_a1_2v3
• Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.Finding.some_partial_canceled.evidence = Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.exp1_some_a2_2v3
• Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.Finding.two_full_upper_bounded.evidence = Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.exp2_two_a3_2v3
• Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.Finding.two_partial_weakened.evidence = Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.exp2_two_a2_2v3
• Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.Finding.one_full_1v2.evidence = Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.exp2_one_a3_1v2
• Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.Finding.one_full_1v3.evidence = Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.exp2_one_a3_1v3
• Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.Finding.one_minimal_1v2_canceled.evidence = Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.exp2_one_a1_1v2
• Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.Finding.one_minimal_1v3_canceled.evidence = Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.exp2_one_a1_1v3
• Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.Finding.one_partial_1v3.evidence = Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.exp2_one_a2_1v3
• Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.Finding.one_partial_1v2_canceled.evidence = Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.exp2_one_a2_1v2

def Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.Finding.predicted : Finding → Bool

Does this finding predict that the comparison holds (stateA > stateB)?

Equations

• Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.Finding.some_full_implicature.predicted = true
• Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.Finding.two_full_upper_bounded.predicted = true
• Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.Finding.one_full_1v2.predicted = true
• Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.Finding.one_full_1v3.predicted = true
• Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.Finding.one_partial_1v3.predicted = true
• x✝.predicted = false

theorem Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.evidence_matches_prediction (f : Finding) : f.evidence.aExceedsB = f.predicted

The statistical evidence matches the predicted direction for every finding.

Bridge content (merged from Bridge.lean)

@cite{goodman-stuhlmuller-2013}: RSA Bridge

@cite{goodman-stuhlmuller-2013}

The paper's RSA model applied to the experimental data. A single gsCfg constructor parametric in the meaning function serves both experiments (quantifiers and lower-bound numerals). They share the same observation model, speaker belief, and S1 structure — the only thing that varies is the utterance type and literal semantics.

Architecture (Eq. 1–5)

F_w : s → {0, 1} truth function for utterance w (§1)
P_lex(s | w) ∝ δ_{F_w(s)} literal interpretation (§1)
U(w; s) = ln P_lex(s | w) informativity (negative surprisal) (Eq. 3)
P(s | o, a) speaker's belief state (hypergeometric)
S1(w | o, a) ∝ exp(α · E_{P(s|o,a)}[U(w; s)]) (Eq. 2)
             = exp(α · Σ_s P(s | o, a) · ln P_lex(s | w))
S1(w | s, a) = Σ_o S1(w | o, a) · P(o | a, s) (Eq. 4)
L1(s | w, a) ∝ S1(w | s, a) · P(s) (Eq. 1)

The speaker observes a subset of objects (hypergeometric sampling), forms a belief P(s | o, a), and soft-max optimizes expected informativity under that belief. L1 marginalizes over observations weighted by P(o | a, s).

The quality filter (utterance must be true at all worlds the speaker considers possible) is explicit because Real.log 0 = 0 in Lean/Mathlib, unlike WebPPL where log(0) = -∞ makes quality emerge from the score.

The model reproduces all 11 findings. All proofs use rsa_predict.

Data source: GoodmanStuhlmuller2013.Data Theories used: Theories.Pragmatics.RSA.Core.Config, Theories.Pragmatics.RSA.Quantities, Theories.Semantics.Lexical.Numeral.Semantics

inductive Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.WorldState : Type

World states: how many of 3 objects have the property.

• s0 : WorldState
• s1 : WorldState
• s2 : WorldState
• s3 : WorldState

instance Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.instDecidableEqWorldState : DecidableEq WorldState

Equations

• Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.instDecidableEqWorldState x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.instBEqWorldState.beq : WorldState → WorldState → Bool

Equations

• Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.instBEqWorldState.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.instBEqWorldState : BEq WorldState

Equations

• Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.instBEqWorldState = { beq := Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.instBEqWorldState.beq }

instance Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.instReprWorldState : Repr WorldState

Equations

• Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.instReprWorldState = { reprPrec := Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.instReprWorldState.repr }

def Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.instReprWorldState.repr : WorldState → ℕ → Std.Format

Equations

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

instance Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.instInhabitedWorldState : Inhabited WorldState

Equations

• Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.instInhabitedWorldState = { default := Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.instInhabitedWorldState.default }

def Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.instInhabitedWorldState.default : WorldState

Equations

• Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.instInhabitedWorldState.default = Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.WorldState.s0

instance Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.instFintypeWorldState : Fintype WorldState

Equations

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

def Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.WorldState.toNat : WorldState → ℕ

Equations

• Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.WorldState.s0.toNat = 0
• Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.WorldState.s1.toNat = 1
• Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.WorldState.s2.toNat = 2
• Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.WorldState.s3.toNat = 3

inductive Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.Access : Type

Speaker access: how many of 3 objects the speaker can observe.

• a1 : Access
• a2 : Access
• a3 : Access

instance Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.instDecidableEqAccess : DecidableEq Access

Equations

• Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.instDecidableEqAccess x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.instBEqAccess : BEq Access

Equations

• Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.instBEqAccess = { beq := Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.instBEqAccess.beq }

def Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.instBEqAccess.beq : Access → Access → Bool

Equations

• Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.instBEqAccess.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.instReprAccess : Repr Access

Equations

• Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.instReprAccess = { reprPrec := Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.instReprAccess.repr }

def Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.instReprAccess.repr : Access → ℕ → Std.Format

Equations

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

inductive Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.Obs : Type

Observations: (number seen with property, access level). Latent variable in L1 — L1 marginalizes over observations.

• o0a1 : Obs
• o1a1 : Obs
• o0a2 : Obs
• o1a2 : Obs
• o2a2 : Obs
• o0a3 : Obs
• o1a3 : Obs
• o2a3 : Obs
• o3a3 : Obs

instance Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.instDecidableEqObs : DecidableEq Obs

Equations

• Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.instDecidableEqObs x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.instBEqObs : BEq Obs

Equations

• Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.instBEqObs = { beq := Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.instBEqObs.beq }

def Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.instBEqObs.beq : Obs → Obs → Bool

Equations

• Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.instBEqObs.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.instReprObs : Repr Obs

Equations

• Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.instReprObs = { reprPrec := Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.instReprObs.repr }

def Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.instReprObs.repr : Obs → ℕ → Std.Format

Equations

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

def Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.instInhabitedObs.default : Obs

Equations

• Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.instInhabitedObs.default = Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.Obs.o0a1

instance Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.instInhabitedObs : Inhabited Obs

Equations

• Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.instInhabitedObs = { default := Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.instInhabitedObs.default }

instance Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.instFintypeObs : Fintype Obs

Equations

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

def Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.Obs.access : Obs → Access

Equations

• Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.Obs.o0a1.access = Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.Access.a1
• Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.Obs.o1a1.access = Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.Access.a1
• Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.Obs.o0a2.access = Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.Access.a2
• Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.Obs.o1a2.access = Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.Access.a2
• Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.Obs.o2a2.access = Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.Access.a2
• Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.Obs.o0a3.access = Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.Access.a3
• Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.Obs.o1a3.access = Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.Access.a3
• Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.Obs.o2a3.access = Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.Access.a3
• Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.Obs.o3a3.access = Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.Access.a3

def Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.Obs.count : Obs → ℕ

Number of objects with the property in the sample.

Equations

• Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.Obs.o0a1.count = 0
• Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.Obs.o0a2.count = 0
• Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.Obs.o0a3.count = 0
• Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.Obs.o1a1.count = 1
• Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.Obs.o1a2.count = 1
• Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.Obs.o1a3.count = 1
• Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.Obs.o2a2.count = 2
• Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.Obs.o2a3.count = 2
• Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.Obs.o3a3.count = 3

def Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.Obs.sampleSize : Obs → ℕ

Sample size (= access level as ℕ).

Equations

• Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.Obs.o0a1.sampleSize = 1
• Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.Obs.o1a1.sampleSize = 1
• Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.Obs.o0a2.sampleSize = 2
• Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.Obs.o1a2.sampleSize = 2
• Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.Obs.o2a2.sampleSize = 2
• Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.Obs.o0a3.sampleSize = 3
• Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.Obs.o1a3.sampleSize = 3
• Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.Obs.o2a3.sampleSize = 3
• Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.Obs.o3a3.sampleSize = 3

def Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.obsCompatible (obs : Obs) (s : WorldState) : Bool

Hypergeometric feasibility: can you draw obs.count successes when sampling obs.sampleSize from a population of 3 with s.toNat successes? True iff C(K, k) > 0 and C(3−K, n−k) > 0, i.e. k ≤ K and n−k ≤ 3−K. Derived from the combinatorial constraint rather than stipulated.

Equations

• Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.obsCompatible obs s = (decide (obs.count ≤ s.toNat) && decide (obs.sampleSize - obs.count ≤ 3 - s.toNat))

noncomputable def Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.obsPriorTable (a : Access) (w : WorldState) (obs : Obs) : ℝ

P(obs | access, world). Hypergeometric probability of observing k successes when sampling n from 3 total with K successes: P(k | N=3, K, n) = C(K,k) · C(3−K, n−k) / C(3,n). Instantiates Core.Distributions.hypergeometric for N=3.

Equations

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

theorem Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.obsPriorTable_eq_hypergeometric (a : Access) (w : WorldState) (obs : Obs) (h : obs.access = a) : obsPriorTable a w obs = ↑(Core.Distributions.hypergeometric 3 w.toNat obs.sampleSize obs.count)

The observation model is an instance of the general hypergeometric from Core.Distributions (N=3). The ℝ-arithmetic form is used for rsa_predict compatibility; this theorem witnesses the equivalence.

noncomputable def Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.speakerBelief (obs : Obs) (s : WorldState) : ℝ

Speaker's posterior over world states given observation: P(state | obs) ∝ P(obs | state, access) · P(state). With uniform world prior, this is the normalized hypergeometric. The access level is derived from the observation itself.

Equations

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

def Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.qualityOk {U : Type u_1} (meaning : U → WorldState → Bool) (obs : Obs) (u : U) : Bool

Quality filter: utterance u must be true at every world the speaker considers possible given observation obs. Explicit because Real.log 0 = 0 in Lean; in WebPPL, log(0) = -∞ makes quality emerge from the score.

Equations

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

noncomputable def Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.gsCfg {U : Type u_1} [Fintype U] (meaning : U → WorldState → Bool) (a : Access) : RSA.RSAConfig U WorldState

GS2013 model parametric in utterance type and meaning function.

Eq. 1–4 from the paper: P_lex(s | w) ∝ ⟦w⟧(s) (literal listener) U(w; s) = ln P_lex(s | w) (Eq. 3) S1(w | o, a) ∝ exp(α · Σ_s P(s | o, a) · U(w; s)) (Eq. 2) S1(w | s, a) = Σ_o S1(w | o, a) · P(o | a, s) (Eq. 4) L1(s | w, a) ∝ S1(w | s, a) · P(s) (Eq. 1)

The quality filter ensures the speaker only considers utterances true at all worlds compatible with their observation. L1 marginalizes over observations via latentPrior w obs = P(obs | a, w).

Equations

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

inductive Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.QUtt : Type

• none_ : QUtt
• some_ : QUtt
• all : QUtt

instance Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.instDecidableEqQUtt : DecidableEq QUtt

Equations

• Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.instDecidableEqQUtt x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.instBEqQUtt.beq : QUtt → QUtt → Bool

Equations

• Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.instBEqQUtt.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.instBEqQUtt : BEq QUtt

Equations

• Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.instBEqQUtt = { beq := Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.instBEqQUtt.beq }

def Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.instReprQUtt.repr : QUtt → ℕ → Std.Format

Equations

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

instance Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.instReprQUtt : Repr QUtt

Equations

• Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.instReprQUtt = { reprPrec := Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.instReprQUtt.repr }

instance Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.instInhabitedQUtt : Inhabited QUtt

Equations

• Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.instInhabitedQUtt = { default := Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.instInhabitedQUtt.default }

def Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.instInhabitedQUtt.default : QUtt

Equations

• Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.instInhabitedQUtt.default = Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.QUtt.none_

instance Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.instFintypeQUtt : Fintype QUtt

Equations

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

def Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.qMeaning : QUtt → WorldState → Bool

Equations

• Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.qMeaning Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.QUtt.none_ x✝ = (x✝.toNat == 0)
• Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.qMeaning Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.QUtt.some_ x✝ = decide (x✝.toNat ≥ 1)
• Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.qMeaning Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.QUtt.all x✝ = (x✝.toNat == 3)

@[reducible, inline]

noncomputable abbrev Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.gsCfgQ (a : Access) : RSA.RSAConfig QUtt WorldState

Quantifier RSA model: {none, some, all} × speaker access.

Equations

• Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.gsCfgQ = Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.gsCfg Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.qMeaning

inductive Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.NumUtt : Type

• one : NumUtt
• two : NumUtt
• three : NumUtt

instance Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.instDecidableEqNumUtt : DecidableEq NumUtt

Equations

• Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.instDecidableEqNumUtt x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.instBEqNumUtt.beq : NumUtt → NumUtt → Bool

Equations

• Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.instBEqNumUtt.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.instBEqNumUtt : BEq NumUtt

Equations

• Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.instBEqNumUtt = { beq := Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.instBEqNumUtt.beq }

def Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.instReprNumUtt.repr : NumUtt → ℕ → Std.Format

Equations

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

instance Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.instReprNumUtt : Repr NumUtt

Equations

• Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.instReprNumUtt = { reprPrec := Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.instReprNumUtt.repr }

def Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.instInhabitedNumUtt.default : NumUtt

Equations

• Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.instInhabitedNumUtt.default = Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.NumUtt.one

instance Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.instInhabitedNumUtt : Inhabited NumUtt

Equations

• Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.instInhabitedNumUtt = { default := Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.instInhabitedNumUtt.default }

instance Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.instFintypeNumUtt : Fintype NumUtt

Equations

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

def Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.lbMeaning : NumUtt → WorldState → Bool

Equations

• Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.lbMeaning Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.NumUtt.one x✝ = decide (x✝.toNat ≥ 1)
• Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.lbMeaning Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.NumUtt.two x✝ = decide (x✝.toNat ≥ 2)
• Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.lbMeaning Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.NumUtt.three x✝ = decide (x✝.toNat ≥ 3)

@[reducible, inline]

noncomputable abbrev Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.gsCfgN (a : Access) : RSA.RSAConfig NumUtt WorldState

Lower-bound numeral RSA model: {one, two, three} × speaker access.

Equations

• Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.gsCfgN = Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.gsCfg Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.lbMeaning

theorem Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.quantifier_meaning_grounded (u : QUtt) (s : WorldState) : qMeaning u s = RSA.Domains.Quantity.meaning 3 (match u with | QUtt.none_ => RSA.Domains.Quantity.Utterance.none_ | QUtt.some_ => RSA.Domains.Quantity.Utterance.some_ | QUtt.all => RSA.Domains.Quantity.Utterance.all) ⟨s.toNat, ⋯⟩

Quantifier meaning derives from Montague semantics (not stipulated).

theorem Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.lb_meaning_grounded (u : NumUtt) (s : WorldState) : lbMeaning u s = Semantics.Lexical.Numeral.LowerBound.meaning (match u with | NumUtt.one => Semantics.Lexical.Numeral.BareNumeral.one | NumUtt.two => Semantics.Lexical.Numeral.BareNumeral.two | NumUtt.three => Semantics.Lexical.Numeral.BareNumeral.three) s.toNat

Lower-bound numeral meaning derives from NumeralTheory.meaning.

theorem Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.some_full_implicature : (gsCfgQ Access.a3).L1 QUtt.some_ WorldState.s2 > (gsCfgQ Access.a3).L1 QUtt.some_ WorldState.s3

Full access: L1 infers state 2 over state 3 — scalar implicature present.

theorem Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.some_minimal_canceled : ¬(gsCfgQ Access.a1).L1 QUtt.some_ WorldState.s2 > (gsCfgQ Access.a1).L1 QUtt.some_ WorldState.s3

Minimal access (a=1): implicature canceled — state 2 does not exceed state 3.

theorem Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.some_partial_canceled : ¬(gsCfgQ Access.a2).L1 QUtt.some_ WorldState.s2 > (gsCfgQ Access.a2).L1 QUtt.some_ WorldState.s3

Partial access (a=2): implicature canceled — state 2 does not exceed state 3.

theorem Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.two_full_upper_bounded : (gsCfgN Access.a3).L1 NumUtt.two WorldState.s2 > (gsCfgN Access.a3).L1 NumUtt.two WorldState.s3

Full access: "two" → upper-bounded reading, state 2 > state 3.

theorem Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.two_partial_weakened : ¬(gsCfgN Access.a2).L1 NumUtt.two WorldState.s2 > (gsCfgN Access.a2).L1 NumUtt.two WorldState.s3

Partial access (a=2): upper bound weakened — state 2 does not exceed state 3.

theorem Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.one_full_1v2 : (gsCfgN Access.a3).L1 NumUtt.one WorldState.s1 > (gsCfgN Access.a3).L1 NumUtt.one WorldState.s2

Full access: "one" → state 1 preferred over state 2.

theorem Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.one_full_1v3 : (gsCfgN Access.a3).L1 NumUtt.one WorldState.s1 > (gsCfgN Access.a3).L1 NumUtt.one WorldState.s3

Full access: "one" → state 1 preferred over state 3.

theorem Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.one_minimal_1v2_canceled : ¬(gsCfgN Access.a1).L1 NumUtt.one WorldState.s1 > (gsCfgN Access.a1).L1 NumUtt.one WorldState.s2

Minimal access (a=1): canceled — state 1 does not exceed state 2.

theorem Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.one_minimal_1v3_canceled : ¬(gsCfgN Access.a1).L1 NumUtt.one WorldState.s1 > (gsCfgN Access.a1).L1 NumUtt.one WorldState.s3

Minimal access (a=1): canceled — state 1 does not exceed state 3.

theorem Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.one_partial_1v3 : (gsCfgN Access.a2).L1 NumUtt.one WorldState.s1 > (gsCfgN Access.a2).L1 NumUtt.one WorldState.s3

Partial access (a=2): state 1 > state 3 (partial implicature persists).

theorem Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.one_partial_1v2_canceled : ¬(gsCfgN Access.a2).L1 NumUtt.one WorldState.s1 > (gsCfgN Access.a2).L1 NumUtt.one WorldState.s2

Partial access (a=2): state 1 does not exceed state 2 (still canceled).

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

theorem Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.all_findings_verified (f : Finding) : formalize f

The RSA model accounts for all 11 empirical findings from @cite{goodman-stuhlmuller-2013}.