@cite{scontras-pearl-2021} — Scope Ambiguity RSA Model

@cite{scontras-pearl-2021} "When pragmatics matters more for truth-value judgments: An investigation of quantifier scope ambiguity" Glossa 6(1): 110.

The Model (§3.1)

Domain: "Every horse didn't jump" with n=2 horses. 3 world states (0, 1, 2 jumped). 2 utterances (null, everyNot). 6 latent states (2 scopes × 3 QUDs).

• L0: L0(w|u,i) ∝ δ_{⟦u⟧ⁱ(w)} (literal semantics, no world prior; footnote 6)
• S1: S1(u|w,i,q) ∝ exp(α · log L0(⟦q⟧(w)|u,i,q)) (QUD-projected)
• L1: L1(w,i,q|u) ∝ P(w) · P(i) · P(q) · S1(u|w,i,q)
• S2: S2(u|w) ∝ exp(log Σ_{i,q} L1(w,i,q|u)) = L1(w|u)
• Endorsement: P(endorse u | w_obs) = S2(u|w_obs)

Parameters: α = 1 (§3.2, p.15). P(w) = Binomial(n, b_suc).

QUDs (eqs 3–4)

Three QUD partitions over worlds:

• how-many?: identity — partitions {w0}, {w1}, {w2}
• all?: w = n? — partitions {w0,w1} vs {w2}
• none?: w = 0? — partitions {w0} vs {w1,w2}

S2 vs L1 (eq 8)

The paper models endorsement as S2, not L1. S2(u|w) ∝ P_{L1}(w|u), using the normalized L1 posterior. This matters because:

• L1 conditions on the heard utterance (same normalizer for all worlds)
• S2 conditions on the observed world (different normalizer per world)
• worldPrior enters S2 through L1's normalization denominator, so different worldPriors produce different S2 values

The S2 ordering S2(everyNot|w0) > S2(everyNot|w1) > S2(everyNot|w2) is robust across all prior configurations, even when L1 orderings vary (e.g., highBaseCfg reverses L1 ordering but preserves S2 ordering).

Compositional Grounding

The truth conditions scopeTruth are grounded in linglib's formal semantics infrastructure via every_sem (Quantifier.lean), ScopeConfig/ScopeDerivation (Montague/Scope.lean), and FiniteModel/Model (Montague/Basic.lean):

• Surface (∀>¬): every_sem horseModel horse_sem (λh.¬jump(h))(w)
• Inverse (¬>∀): ¬(every_sem horseModel horse_sem (jump)(w))

See surface_from_every_sem, inverse_from_every_sem, and scopeDerivation_matches_scopeTruth.

Key Findings (Figure 2)

S2 endorsement for "every horse didn't jump" in the partial world (w=1). The "Paper value" column is S&P's computed model predictions (not experimental data — S&P is a modeling paper explaining @cite{musolino-lidz-2003} findings):

Config	S2(everyNot	w=1)
b_suc=0.1 (baseline)	0.288	~0.29
b_suc=0.5 (default)	0.506	~0.48
b_suc=0.9 (high base rate)	0.796	~0.80

The S2 ordering w0 > w1 > w2 is robust across all prior configurations, even when L1 orderings vary (e.g., highBaseCfg reverses L1 ordering).

Developmental Continuity (§3.3)

The same model architecture explains both child and adult behavior. Children's isomorphic (surface-scope) preference follows from low b_suc priors. Adult-like inverse scope access emerges from supportive contexts (high b_suc, all?-biased QUD) — the same model, different priors.

instance Phenomena.Quantification.Studies.ScontrasPearl2021RSA.instFintypeJumpOutcome : Fintype ScontrasPearl2021.JumpOutcome

Equations

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

instance Phenomena.Quantification.Studies.ScontrasPearl2021RSA.instFintypeScopeReading : Fintype ScontrasPearl2021.ScopeReading

Equations

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

inductive Phenomena.Quantification.Studies.ScontrasPearl2021RSA.Utt : Type

Utterances: null (silence) or "Every horse didn't jump".

• null : Utt
• everyNot : Utt

instance Phenomena.Quantification.Studies.ScontrasPearl2021RSA.instDecidableEqUtt : DecidableEq Utt

Equations

• Phenomena.Quantification.Studies.ScontrasPearl2021RSA.instDecidableEqUtt x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Phenomena.Quantification.Studies.ScontrasPearl2021RSA.instBEqUtt : BEq Utt

Equations

• Phenomena.Quantification.Studies.ScontrasPearl2021RSA.instBEqUtt = { beq := Phenomena.Quantification.Studies.ScontrasPearl2021RSA.instBEqUtt.beq }

def Phenomena.Quantification.Studies.ScontrasPearl2021RSA.instBEqUtt.beq : Utt → Utt → Bool

Equations

• Phenomena.Quantification.Studies.ScontrasPearl2021RSA.instBEqUtt.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Quantification.Studies.ScontrasPearl2021RSA.instReprUtt : Repr Utt

Equations

• Phenomena.Quantification.Studies.ScontrasPearl2021RSA.instReprUtt = { reprPrec := Phenomena.Quantification.Studies.ScontrasPearl2021RSA.instReprUtt.repr }

def Phenomena.Quantification.Studies.ScontrasPearl2021RSA.instReprUtt.repr : Utt → ℕ → Std.Format

Equations

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

instance Phenomena.Quantification.Studies.ScontrasPearl2021RSA.instInhabitedUtt : Inhabited Utt

Equations

• Phenomena.Quantification.Studies.ScontrasPearl2021RSA.instInhabitedUtt = { default := Phenomena.Quantification.Studies.ScontrasPearl2021RSA.instInhabitedUtt.default }

def Phenomena.Quantification.Studies.ScontrasPearl2021RSA.instInhabitedUtt.default : Utt

Equations

• Phenomena.Quantification.Studies.ScontrasPearl2021RSA.instInhabitedUtt.default = Phenomena.Quantification.Studies.ScontrasPearl2021RSA.Utt.null

instance Phenomena.Quantification.Studies.ScontrasPearl2021RSA.instFintypeUtt : Fintype Utt

Equations

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

inductive Phenomena.Quantification.Studies.ScontrasPearl2021RSA.QUD : Type

QUDs partition worlds by the question under discussion (eqs 3–4). Three QUD partitions for n=2 worlds.

• howMany : QUD
• all_ : QUD
• none_ : QUD

instance Phenomena.Quantification.Studies.ScontrasPearl2021RSA.instDecidableEqQUD : DecidableEq QUD

Equations

• Phenomena.Quantification.Studies.ScontrasPearl2021RSA.instDecidableEqQUD x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.Quantification.Studies.ScontrasPearl2021RSA.instBEqQUD.beq : QUD → QUD → Bool

Equations

• Phenomena.Quantification.Studies.ScontrasPearl2021RSA.instBEqQUD.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Quantification.Studies.ScontrasPearl2021RSA.instBEqQUD : BEq QUD

Equations

• Phenomena.Quantification.Studies.ScontrasPearl2021RSA.instBEqQUD = { beq := Phenomena.Quantification.Studies.ScontrasPearl2021RSA.instBEqQUD.beq }

instance Phenomena.Quantification.Studies.ScontrasPearl2021RSA.instReprQUD : Repr QUD

Equations

• Phenomena.Quantification.Studies.ScontrasPearl2021RSA.instReprQUD = { reprPrec := Phenomena.Quantification.Studies.ScontrasPearl2021RSA.instReprQUD.repr }

def Phenomena.Quantification.Studies.ScontrasPearl2021RSA.instReprQUD.repr : QUD → ℕ → Std.Format

Equations

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

def Phenomena.Quantification.Studies.ScontrasPearl2021RSA.instInhabitedQUD.default : QUD

Equations

• Phenomena.Quantification.Studies.ScontrasPearl2021RSA.instInhabitedQUD.default = Phenomena.Quantification.Studies.ScontrasPearl2021RSA.QUD.howMany

instance Phenomena.Quantification.Studies.ScontrasPearl2021RSA.instInhabitedQUD : Inhabited QUD

Equations

• Phenomena.Quantification.Studies.ScontrasPearl2021RSA.instInhabitedQUD = { default := Phenomena.Quantification.Studies.ScontrasPearl2021RSA.instInhabitedQUD.default }

instance Phenomena.Quantification.Studies.ScontrasPearl2021RSA.instFintypeQUD : Fintype QUD

Equations

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

inductive Phenomena.Quantification.Studies.ScontrasPearl2021RSA.Latent : Type

Flattened latent variable: scope reading × QUD. Flat inductive avoids Prod, keeping proof terms tractable for the kernel checker.

• surfHowMany : Latent
• surfAll : Latent
• surfNone : Latent
• invHowMany : Latent
• invAll : Latent
• invNone : Latent

instance Phenomena.Quantification.Studies.ScontrasPearl2021RSA.instDecidableEqLatent : DecidableEq Latent

Equations

• Phenomena.Quantification.Studies.ScontrasPearl2021RSA.instDecidableEqLatent x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.Quantification.Studies.ScontrasPearl2021RSA.instBEqLatent.beq : Latent → Latent → Bool

Equations

• Phenomena.Quantification.Studies.ScontrasPearl2021RSA.instBEqLatent.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Quantification.Studies.ScontrasPearl2021RSA.instBEqLatent : BEq Latent

Equations

• Phenomena.Quantification.Studies.ScontrasPearl2021RSA.instBEqLatent = { beq := Phenomena.Quantification.Studies.ScontrasPearl2021RSA.instBEqLatent.beq }

instance Phenomena.Quantification.Studies.ScontrasPearl2021RSA.instReprLatent : Repr Latent

Equations

• Phenomena.Quantification.Studies.ScontrasPearl2021RSA.instReprLatent = { reprPrec := Phenomena.Quantification.Studies.ScontrasPearl2021RSA.instReprLatent.repr }

def Phenomena.Quantification.Studies.ScontrasPearl2021RSA.instReprLatent.repr : Latent → ℕ → Std.Format

Equations

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

instance Phenomena.Quantification.Studies.ScontrasPearl2021RSA.instInhabitedLatent : Inhabited Latent

Equations

• Phenomena.Quantification.Studies.ScontrasPearl2021RSA.instInhabitedLatent = { default := Phenomena.Quantification.Studies.ScontrasPearl2021RSA.instInhabitedLatent.default }

def Phenomena.Quantification.Studies.ScontrasPearl2021RSA.instInhabitedLatent.default : Latent

Equations

• Phenomena.Quantification.Studies.ScontrasPearl2021RSA.instInhabitedLatent.default = Phenomena.Quantification.Studies.ScontrasPearl2021RSA.Latent.surfHowMany

instance Phenomena.Quantification.Studies.ScontrasPearl2021RSA.instFintypeLatent : Fintype Latent

Equations

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

def Phenomena.Quantification.Studies.ScontrasPearl2021RSA.Latent.scope : Latent → ScontrasPearl2021.ScopeReading

Extract scope reading from latent variable.

Equations

• Phenomena.Quantification.Studies.ScontrasPearl2021RSA.Latent.surfHowMany.scope = Phenomena.Quantification.Studies.ScontrasPearl2021.ScopeReading.surface
• Phenomena.Quantification.Studies.ScontrasPearl2021RSA.Latent.surfAll.scope = Phenomena.Quantification.Studies.ScontrasPearl2021.ScopeReading.surface
• Phenomena.Quantification.Studies.ScontrasPearl2021RSA.Latent.surfNone.scope = Phenomena.Quantification.Studies.ScontrasPearl2021.ScopeReading.surface
• Phenomena.Quantification.Studies.ScontrasPearl2021RSA.Latent.invHowMany.scope = Phenomena.Quantification.Studies.ScontrasPearl2021.ScopeReading.inverse
• Phenomena.Quantification.Studies.ScontrasPearl2021RSA.Latent.invAll.scope = Phenomena.Quantification.Studies.ScontrasPearl2021.ScopeReading.inverse
• Phenomena.Quantification.Studies.ScontrasPearl2021RSA.Latent.invNone.scope = Phenomena.Quantification.Studies.ScontrasPearl2021.ScopeReading.inverse

def Phenomena.Quantification.Studies.ScontrasPearl2021RSA.Latent.qud : Latent → QUD

Extract QUD from latent variable.

Equations

• Phenomena.Quantification.Studies.ScontrasPearl2021RSA.Latent.surfHowMany.qud = Phenomena.Quantification.Studies.ScontrasPearl2021RSA.QUD.howMany
• Phenomena.Quantification.Studies.ScontrasPearl2021RSA.Latent.invHowMany.qud = Phenomena.Quantification.Studies.ScontrasPearl2021RSA.QUD.howMany
• Phenomena.Quantification.Studies.ScontrasPearl2021RSA.Latent.surfAll.qud = Phenomena.Quantification.Studies.ScontrasPearl2021RSA.QUD.all_
• Phenomena.Quantification.Studies.ScontrasPearl2021RSA.Latent.invAll.qud = Phenomena.Quantification.Studies.ScontrasPearl2021RSA.QUD.all_
• Phenomena.Quantification.Studies.ScontrasPearl2021RSA.Latent.surfNone.qud = Phenomena.Quantification.Studies.ScontrasPearl2021RSA.QUD.none_
• Phenomena.Quantification.Studies.ScontrasPearl2021RSA.Latent.invNone.qud = Phenomena.Quantification.Studies.ScontrasPearl2021RSA.QUD.none_

def Phenomena.Quantification.Studies.ScontrasPearl2021RSA.uttMeaning : ScontrasPearl2021.ScopeReading → Utt → ScontrasPearl2021.JumpOutcome → Bool

RSA meaning derived from the data file's scopeTruth. Null utterance is always true (uninformative baseline).

Equations

• One or more equations did not get rendered due to their size.
• Phenomena.Quantification.Studies.ScontrasPearl2021RSA.uttMeaning x✝¹ Phenomena.Quantification.Studies.ScontrasPearl2021RSA.Utt.null x✝ = true

theorem Phenomena.Quantification.Studies.ScontrasPearl2021RSA.truth_table : uttMeaning ScontrasPearl2021.ScopeReading.surface Utt.everyNot ScontrasPearl2021.JumpOutcome.zero = true ∧ uttMeaning ScontrasPearl2021.ScopeReading.surface Utt.everyNot ScontrasPearl2021.JumpOutcome.one = false ∧ uttMeaning ScontrasPearl2021.ScopeReading.surface Utt.everyNot ScontrasPearl2021.JumpOutcome.two = false ∧ uttMeaning ScontrasPearl2021.ScopeReading.inverse Utt.everyNot ScontrasPearl2021.JumpOutcome.zero = true ∧ uttMeaning ScontrasPearl2021.ScopeReading.inverse Utt.everyNot ScontrasPearl2021.JumpOutcome.one = true ∧ uttMeaning ScontrasPearl2021.ScopeReading.inverse Utt.everyNot ScontrasPearl2021.JumpOutcome.two = false

Truth table verification against the paper's equations (3a-b).

inductive Phenomena.Quantification.Studies.ScontrasPearl2021RSA.Horse : Type

2-horse domain for grounding truth conditions in quantifier semantics.

• h1 : Horse
• h2 : Horse

instance Phenomena.Quantification.Studies.ScontrasPearl2021RSA.instDecidableEqHorse : DecidableEq Horse

Equations

• Phenomena.Quantification.Studies.ScontrasPearl2021RSA.instDecidableEqHorse x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.Quantification.Studies.ScontrasPearl2021RSA.jumpIn : ScontrasPearl2021.JumpOutcome → Horse → Bool

Jump predicate for each world state. In the 1-horse world, exactly h1 jumped (the choice is arbitrary; only cardinality matters for the universally quantified sentence).

Equations

• One or more equations did not get rendered due to their size.
• Phenomena.Quantification.Studies.ScontrasPearl2021RSA.jumpIn Phenomena.Quantification.Studies.ScontrasPearl2021.JumpOutcome.zero x✝ = false
• Phenomena.Quantification.Studies.ScontrasPearl2021RSA.jumpIn Phenomena.Quantification.Studies.ScontrasPearl2021.JumpOutcome.two x✝ = true

@[reducible, inline]

abbrev Phenomena.Quantification.Studies.ScontrasPearl2021RSA.horseModel : Semantics.Montague.Model

Horse model as a Montague Model.

Equations

• Phenomena.Quantification.Studies.ScontrasPearl2021RSA.horseModel = { Entity := Phenomena.Quantification.Studies.ScontrasPearl2021RSA.Horse, decEq := inferInstance }

instance Phenomena.Quantification.Studies.ScontrasPearl2021RSA.instFintypeEntityHorseModel : Fintype horseModel.Entity

Equations

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

def Phenomena.Quantification.Studies.ScontrasPearl2021RSA.horse_sem : horseModel.interpTy (Semantics.Montague.Ty.e ⇒ Semantics.Montague.Ty.t)

Restrictor: all entities are horses (trivial for this model).

Equations

• Phenomena.Quantification.Studies.ScontrasPearl2021RSA.horse_sem x✝ = true

def Phenomena.Quantification.Studies.ScontrasPearl2021RSA.jumpIn_sem (w : ScontrasPearl2021.JumpOutcome) : horseModel.interpTy (Semantics.Montague.Ty.e ⇒ Semantics.Montague.Ty.t)

Scope predicate: did entity h jump in world w?

Equations

• Phenomena.Quantification.Studies.ScontrasPearl2021RSA.jumpIn_sem w h = Phenomena.Quantification.Studies.ScontrasPearl2021RSA.jumpIn w h

def Phenomena.Quantification.Studies.ScontrasPearl2021RSA.everyNotJumped_surface (w : ScontrasPearl2021.JumpOutcome) : Bool

Surface scope: ⟦every⟧(horse)(λx.¬jump(x))(w).

Equations

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

def Phenomena.Quantification.Studies.ScontrasPearl2021RSA.everyNotJumped_inverse (w : ScontrasPearl2021.JumpOutcome) : Bool

Inverse scope: ¬⟦every⟧(horse)(jump)(w).

Equations

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

theorem Phenomena.Quantification.Studies.ScontrasPearl2021RSA.surface_from_every_sem (w : ScontrasPearl2021.JumpOutcome) : ScontrasPearl2021.scopeTruth ScontrasPearl2021.ScopeReading.surface w = Semantics.Lexical.Determiner.Quantifier.every_sem horseModel horse_sem fun (h : horseModel.interpTy Semantics.Montague.Ty.e) => !jumpIn_sem w h

Surface scope grounding: scopeTruth.surface derives from compositional ⟦every⟧(horse)(λx.¬jump(x)), not stipulation.

theorem Phenomena.Quantification.Studies.ScontrasPearl2021RSA.inverse_from_every_sem (w : ScontrasPearl2021.JumpOutcome) : ScontrasPearl2021.scopeTruth ScontrasPearl2021.ScopeReading.inverse w = !Semantics.Lexical.Determiner.Quantifier.every_sem horseModel horse_sem (jumpIn_sem w)

Inverse scope grounding: scopeTruth.inverse derives from negating the compositional ⟦every⟧(horse)(jump).

def Phenomena.Quantification.Studies.ScontrasPearl2021RSA.scopeConfigToReading : Semantics.Scope.ScopeConfig → ScontrasPearl2021.ScopeReading

Map Montague ScopeConfig to data file's ScopeReading.

Equations

• Phenomena.Quantification.Studies.ScontrasPearl2021RSA.scopeConfigToReading Semantics.Scope.ScopeConfig.surface = Phenomena.Quantification.Studies.ScontrasPearl2021.ScopeReading.surface
• Phenomena.Quantification.Studies.ScontrasPearl2021RSA.scopeConfigToReading Semantics.Scope.ScopeConfig.inverse = Phenomena.Quantification.Studies.ScontrasPearl2021.ScopeReading.inverse

def Phenomena.Quantification.Studies.ScontrasPearl2021RSA.readingToScopeConfig : ScontrasPearl2021.ScopeReading → Semantics.Scope.ScopeConfig

Map data file's ScopeReading to Montague ScopeConfig.

Equations

• Phenomena.Quantification.Studies.ScontrasPearl2021RSA.readingToScopeConfig Phenomena.Quantification.Studies.ScontrasPearl2021.ScopeReading.surface = Semantics.Scope.ScopeConfig.surface
• Phenomena.Quantification.Studies.ScontrasPearl2021RSA.readingToScopeConfig Phenomena.Quantification.Studies.ScontrasPearl2021.ScopeReading.inverse = Semantics.Scope.ScopeConfig.inverse

def Phenomena.Quantification.Studies.ScontrasPearl2021RSA.everyHorseDidntJump (w : ScontrasPearl2021.JumpOutcome) : Semantics.Scope.ScopeDerivation horseModel Semantics.Montague.Ty.t

"Every horse didn't jump" as a ScopeDerivation: a single syntactic form with multiple semantic values indexed by scope configuration.

Equations

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

theorem Phenomena.Quantification.Studies.ScontrasPearl2021RSA.scopeDerivation_matches_scopeTruth (s : Semantics.Scope.ScopeConfig) (w : ScontrasPearl2021.JumpOutcome) : (everyHorseDidntJump w).meaningAt s = ScontrasPearl2021.scopeTruth (scopeConfigToReading s) w

The ScopeDerivation's meaningAt matches scopeTruth for both readings.

theorem Phenomena.Quantification.Studies.ScontrasPearl2021RSA.rsa_meaning_from_scope_derivation (lat : Latent) (w : ScontrasPearl2021.JumpOutcome) : uttMeaning lat.scope Utt.everyNot w = (everyHorseDidntJump w).meaningAt (readingToScopeConfig lat.scope)

RSA meaning is grounded in ScopeDerivation: the meaning function used by the RSA config matches the compositional scope derivation.

theorem Phenomena.Quantification.Studies.ScontrasPearl2021RSA.every_not_scope_entailment : Semantics.Scope.classifyScopeEntailment [ScontrasPearl2021.JumpOutcome.zero, ScontrasPearl2021.JumpOutcome.one, ScontrasPearl2021.JumpOutcome.two] (ScontrasPearl2021.scopeTruth ScontrasPearl2021.ScopeReading.surface) (ScontrasPearl2021.scopeTruth ScontrasPearl2021.ScopeReading.inverse) = Semantics.Scope.ScopeEntailment.surfaceEntailsInverse

The every-not scope pair has surface-entails-inverse structure: surface scope (none jumped) is a strict subset of inverse scope (not all jumped). This makes universals non-diagnostic for scope preferences — no TVJ context can distinguish isomorphic from non-isomorphic behavior.

def Phenomena.Quantification.Studies.ScontrasPearl2021RSA.qudAnswer : QUD → ScontrasPearl2021.JumpOutcome → Fin 3

QUD answer function: q(w) → equivalence class identifier (eq 4). For howMany, each world is its own class (identity partition).

Equations

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

def Phenomena.Quantification.Studies.ScontrasPearl2021RSA.qudProjectInline (q : QUD) (f : ScontrasPearl2021.JumpOutcome → ℝ) (w : ScontrasPearl2021.JumpOutcome) : ℝ

Inline QUD projection: explicit case analysis, kernel-reducible. For howMany, each world is its own equivalence class (identity partition). For all?/none?, worlds sharing an answer are aggregated.

Equations

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

theorem Phenomena.Quantification.Studies.ScontrasPearl2021RSA.qudProjectInline_nonneg {q : QUD} {f : ScontrasPearl2021.JumpOutcome → ℝ} {w : ScontrasPearl2021.JumpOutcome} (hf : ∀ (w : ScontrasPearl2021.JumpOutcome), 0 ≤ f w) : 0 ≤ qudProjectInline q f w

noncomputable def Phenomena.Quantification.Studies.ScontrasPearl2021RSA.cfg (worldPr : ScontrasPearl2021.JumpOutcome → ℝ) (hwp : ∀ (w : ScontrasPearl2021.JumpOutcome), 0 ≤ worldPr w) (scopePr : ScontrasPearl2021.ScopeReading → ℝ) (hsp : ∀ (s : ScontrasPearl2021.ScopeReading), 0 ≤ scopePr s) (qudPr : QUD → ℝ) (hqp : ∀ (q : QUD), 0 ≤ qudPr q) : RSA.RSAConfig Utt ScontrasPearl2021.JumpOutcome

@cite{scontras-pearl-2021} RSA model, parametric in three priors. S1 uses QUD-projected rpow with α = 1 (§3.2). L0 does not incorporate the world prior (footnote 6).

Equations

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

World priors follow Binomial(2, b_suc), unnormalized: - b_suc = 0.1: P(w) ∝ (81, 18, 1) — horses unlikely to jump - b_suc = 0.5: P(w) ∝ (1, 2, 1) — symmetric - b_suc = 0.9: P(w) ∝ (1, 18, 81) — horses likely to jump

@[reducible, inline]

noncomputable abbrev Phenomena.Quantification.Studies.ScontrasPearl2021RSA.baselineCfg : RSA.RSAConfig Utt ScontrasPearl2021.JumpOutcome

Baseline: low base rate (b_suc = 0.1), uniform scope, uniform QUD. Best fit to adult Experiment 1 data (§3.2, Figure 2 left).

Equations

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

@[reducible, inline]

noncomputable abbrev Phenomena.Quantification.Studies.ScontrasPearl2021RSA.defaultCfg : RSA.RSAConfig Utt ScontrasPearl2021.JumpOutcome

Default: symmetric prior (b_suc = 0.5), uniform scope, uniform QUD. Binomial(2, 0.5) ∝ (1, 2, 1). Paper's default parameter setting.

Equations

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

@[reducible, inline]

noncomputable abbrev Phenomena.Quantification.Studies.ScontrasPearl2021RSA.highBaseCfg : RSA.RSAConfig Utt ScontrasPearl2021.JumpOutcome

High base rate: b_suc = 0.9, uniform scope, uniform QUD. Tests robustness of S2 ordering to prior manipulation (Figure 2 left).

Equations

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

@[reducible, inline]

noncomputable abbrev Phenomena.Quantification.Studies.ScontrasPearl2021RSA.supportiveCfg : RSA.RSAConfig Utt ScontrasPearl2021.JumpOutcome

Supportive context: b_suc = 0.9 + all?-biased QUD (1:18:1 ≈ 0.05:0.9:0.05). Models the @cite{gualmini-etal-2008} early-success manipulation, where context pragmatically supports inverse scope (§3.3, Figure 3).

Equations

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

@[reducible, inline]

noncomputable abbrev Phenomena.Quantification.Studies.ScontrasPearl2021RSA.surfaceOnlyCfg : RSA.RSAConfig Utt ScontrasPearl2021.JumpOutcome

Surface-only: P(inverse) = 0. Tests whether scope ambiguity is needed to produce intermediate endorsement.

Equations

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

S2 endorsement (eq 8) uses the generic RSAConfig.S2 from Theories/Pragmatics/RSA/Core/Config.lean: S2(u|w) = S2agent.policy(w, u) where S2agent.score(w, u) = cfg.L1(u, w) (the normalized L1 posterior).

The `rsa_predict` tactic handles S2 cross-world goals via `policy_gt_cross`,
building compositional QInterval proofs for the cross-product comparison. 

theorem Phenomena.Quantification.Studies.ScontrasPearl2021RSA.baseline_L1_w0_gt_w1 : baselineCfg.L1 Utt.everyNot ScontrasPearl2021.JumpOutcome.zero > baselineCfg.L1 Utt.everyNot ScontrasPearl2021.JumpOutcome.one

Baseline L1: 0-jumped > 1-jumped. Both scopes agree w=0 is true; high prior weight (81 vs 18).

theorem Phenomena.Quantification.Studies.ScontrasPearl2021RSA.baseline_L1_w1_gt_w2 : baselineCfg.L1 Utt.everyNot ScontrasPearl2021.JumpOutcome.one > baselineCfg.L1 Utt.everyNot ScontrasPearl2021.JumpOutcome.two

Baseline L1: 1-jumped > 2-jumped. Inverse scope makes w=1 true; moderate prior advantage (18 vs 1).

theorem Phenomena.Quantification.Studies.ScontrasPearl2021RSA.ambiguity_boosts_partial : baselineCfg.L1 Utt.everyNot ScontrasPearl2021.JumpOutcome.one > surfaceOnlyCfg.L1 Utt.everyNot ScontrasPearl2021.JumpOutcome.one

Scope ambiguity boosts partial-world endorsement. With both scopes active, L1(w=1) is higher than surface-only, because inverse scope directly makes w=1 true.

theorem Phenomena.Quantification.Studies.ScontrasPearl2021RSA.baseline_S2_w0_gt_w1 : baselineCfg.S2 ScontrasPearl2021.JumpOutcome.zero Utt.everyNot > baselineCfg.S2 ScontrasPearl2021.JumpOutcome.one Utt.everyNot

Baseline S2: w0 > w1. The model predicts higher endorsement of "every horse didn't jump" when no horses jumped (none-scenario) than when one horse jumped (not-all scenario).

theorem Phenomena.Quantification.Studies.ScontrasPearl2021RSA.baseline_S2_w1_gt_w2 : baselineCfg.S2 ScontrasPearl2021.JumpOutcome.one Utt.everyNot > baselineCfg.S2 ScontrasPearl2021.JumpOutcome.two Utt.everyNot

Baseline S2: w1 > w2. Endorsement in the not-all scenario exceeds the all scenario.

theorem Phenomena.Quantification.Studies.ScontrasPearl2021RSA.highBase_S2_w0_gt_w1 : highBaseCfg.S2 ScontrasPearl2021.JumpOutcome.zero Utt.everyNot > highBaseCfg.S2 ScontrasPearl2021.JumpOutcome.one Utt.everyNot

S2 ordering robust to high base rate (b_suc = 0.9). Even when L1 reverses (w1 > w2 > w0 at L1), S2 still orders w0 > w1.

theorem Phenomena.Quantification.Studies.ScontrasPearl2021RSA.highBase_S2_w1_gt_w2 : highBaseCfg.S2 ScontrasPearl2021.JumpOutcome.one Utt.everyNot > highBaseCfg.S2 ScontrasPearl2021.JumpOutcome.two Utt.everyNot

S2 ordering robust to high base rate: w1 > w2.

theorem Phenomena.Quantification.Studies.ScontrasPearl2021RSA.default_S2_w0_gt_w1 : defaultCfg.S2 ScontrasPearl2021.JumpOutcome.zero Utt.everyNot > defaultCfg.S2 ScontrasPearl2021.JumpOutcome.one Utt.everyNot

S2 ordering robust to symmetric prior (b_suc = 0.5).

theorem Phenomena.Quantification.Studies.ScontrasPearl2021RSA.default_S2_w1_gt_w2 : defaultCfg.S2 ScontrasPearl2021.JumpOutcome.one Utt.everyNot > defaultCfg.S2 ScontrasPearl2021.JumpOutcome.two Utt.everyNot

theorem Phenomena.Quantification.Studies.ScontrasPearl2021RSA.supportive_S2_w0_gt_w1 : supportiveCfg.S2 ScontrasPearl2021.JumpOutcome.zero Utt.everyNot > supportiveCfg.S2 ScontrasPearl2021.JumpOutcome.one Utt.everyNot

S2 ordering robust under supportive context (b_suc = 0.9, all?-biased QUD).

theorem Phenomena.Quantification.Studies.ScontrasPearl2021RSA.supportive_S2_w1_gt_w2 : supportiveCfg.S2 ScontrasPearl2021.JumpOutcome.one Utt.everyNot > supportiveCfg.S2 ScontrasPearl2021.JumpOutcome.two Utt.everyNot