Documentation

Linglib.Phenomena.Quantification.Studies.ScontrasPearl2021TwoNot

@cite{scontras-pearl-2021} §4 — Two-Not RSA Model @cite{scontras-pearl-2021} @cite{kennedy-2015} @cite{musolino-2004} #

The two-not model extends the every-not model (§3) to "two horses didn't jump" with n=4 horses. The key innovation: when n exceeds the numeral's value, exact vs at-least numeral semantics produce different truth conditions and thus different RSA predictions.

Model Structure (eqs 5–11) #

Domain: "Two horses didn't jump" with n=4 horses. 5 world states (0–4 jumped). 2 utterances (null, twoNot). 10 latent states (2 scopes × 5 QUDs).

L0: L0(w|u,i) ∝ ⟦u⟧ᵢ(w) (literal semantics)
S1: S1(u|w,i,q) ∝ [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) ∝ L1(w|u) (endorsement)

Parameters: α = 1. P(w) = Binomial(4, b_suc).

QUDs (eq 7) #

Five QUD partitions over 5-world domain:

how-many?: identity — {w0}, {w1}, {w2}, {w3}, {w4}
all?: did all jump? — {w0,w1,w2,w3} vs {w4}
none?: did none jump? — {w0} vs {w1,w2,w3,w4}
two=?: did exactly two jump? — {w2} vs {w0,w1,w3,w4}
two≥?: did at least two jump? — {w0,w1} vs {w2,w3,w4}

Central Claim (§4.2) #

Under exact semantics, surface scope pinpoints w=2 as the unique true world, giving maximum informativity → high S2 endorsement at w=2. Under at-least semantics, surface scope is true at {w0,w1,w2}, diluting informativity → lower S2 endorsement at w=2.

This predicts that adults endorse "two horses didn't jump" more readily in 2-of-4 contexts under exact numeral semantics — converging with @cite{kennedy-2015} and acquisition data from @cite{musolino-2004}.

instance Phenomena.Quantification.Studies.ScontrasPearl2021TwoNot.instFintypeJumpOutcome4 :

Fintype ScontrasPearl2021.JumpOutcome4

Equations

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

instance Phenomena.Quantification.Studies.ScontrasPearl2021TwoNot.instFintypeScopeReading :

Fintype ScontrasPearl2021.ScopeReading

Equations

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

instance Phenomena.Quantification.Studies.ScontrasPearl2021TwoNot.instFintypeNumeralReading :

Fintype ScontrasPearl2021.NumeralReading

Equations

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

inductive Phenomena.Quantification.Studies.ScontrasPearl2021TwoNot.Utt :

Utterances: null (silence) or "two horses didn't jump".

null : Utt
twoNot : Utt

Instances For

instance Phenomena.Quantification.Studies.ScontrasPearl2021TwoNot.instDecidableEqUtt :

DecidableEq Utt

Equations

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

def Phenomena.Quantification.Studies.ScontrasPearl2021TwoNot.instBEqUtt.beq :

Utt → Utt → Bool

Equations

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

Instances For

instance Phenomena.Quantification.Studies.ScontrasPearl2021TwoNot.instBEqUtt :

Equations

Phenomena.Quantification.Studies.ScontrasPearl2021TwoNot.instBEqUtt = { beq := Phenomena.Quantification.Studies.ScontrasPearl2021TwoNot.instBEqUtt.beq }

def Phenomena.Quantification.Studies.ScontrasPearl2021TwoNot.instReprUtt.repr :

Utt → ℕ → Std.Format

Equations

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

Instances For

instance Phenomena.Quantification.Studies.ScontrasPearl2021TwoNot.instReprUtt :

Equations

Phenomena.Quantification.Studies.ScontrasPearl2021TwoNot.instReprUtt = { reprPrec := Phenomena.Quantification.Studies.ScontrasPearl2021TwoNot.instReprUtt.repr }

def Phenomena.Quantification.Studies.ScontrasPearl2021TwoNot.instInhabitedUtt.default :

Equations

Phenomena.Quantification.Studies.ScontrasPearl2021TwoNot.instInhabitedUtt.default = Phenomena.Quantification.Studies.ScontrasPearl2021TwoNot.Utt.null

Instances For

instance Phenomena.Quantification.Studies.ScontrasPearl2021TwoNot.instInhabitedUtt :

Equations

Phenomena.Quantification.Studies.ScontrasPearl2021TwoNot.instInhabitedUtt = { default := Phenomena.Quantification.Studies.ScontrasPearl2021TwoNot.instInhabitedUtt.default }

instance Phenomena.Quantification.Studies.ScontrasPearl2021TwoNot.instFintypeUtt :

Equations

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

inductive Phenomena.Quantification.Studies.ScontrasPearl2021TwoNot.QUD5 :

QUDs for the two-not model (eq 7). Five partitions over the 5-world domain. The two numeral-specific QUDs (two=?, two≥?) are added because explicitly mentioning a numeral makes that cardinality potentially relevant to the topic of conversation.

howMany : QUD5
all_ : QUD5
none_ : QUD5
twoExact : QUD5
twoAtLeast : QUD5

Instances For

instance Phenomena.Quantification.Studies.ScontrasPearl2021TwoNot.instDecidableEqQUD5 :

DecidableEq QUD5

Equations

Phenomena.Quantification.Studies.ScontrasPearl2021TwoNot.instDecidableEqQUD5 x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.Quantification.Studies.ScontrasPearl2021TwoNot.instBEqQUD5.beq :

QUD5 → QUD5 → Bool

Equations

Phenomena.Quantification.Studies.ScontrasPearl2021TwoNot.instBEqQUD5.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

instance Phenomena.Quantification.Studies.ScontrasPearl2021TwoNot.instBEqQUD5 :

Equations

Phenomena.Quantification.Studies.ScontrasPearl2021TwoNot.instBEqQUD5 = { beq := Phenomena.Quantification.Studies.ScontrasPearl2021TwoNot.instBEqQUD5.beq }

instance Phenomena.Quantification.Studies.ScontrasPearl2021TwoNot.instReprQUD5 :

Equations

Phenomena.Quantification.Studies.ScontrasPearl2021TwoNot.instReprQUD5 = { reprPrec := Phenomena.Quantification.Studies.ScontrasPearl2021TwoNot.instReprQUD5.repr }

def Phenomena.Quantification.Studies.ScontrasPearl2021TwoNot.instReprQUD5.repr :

QUD5 → ℕ → Std.Format

Equations

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

Instances For

instance Phenomena.Quantification.Studies.ScontrasPearl2021TwoNot.instInhabitedQUD5 :

Equations

Phenomena.Quantification.Studies.ScontrasPearl2021TwoNot.instInhabitedQUD5 = { default := Phenomena.Quantification.Studies.ScontrasPearl2021TwoNot.instInhabitedQUD5.default }

def Phenomena.Quantification.Studies.ScontrasPearl2021TwoNot.instInhabitedQUD5.default :

Equations

Phenomena.Quantification.Studies.ScontrasPearl2021TwoNot.instInhabitedQUD5.default = Phenomena.Quantification.Studies.ScontrasPearl2021TwoNot.QUD5.howMany

Instances For

instance Phenomena.Quantification.Studies.ScontrasPearl2021TwoNot.instFintypeQUD5 :

Equations

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

inductive Phenomena.Quantification.Studies.ScontrasPearl2021TwoNot.Latent10 :

Flattened latent variable: scope reading × QUD. 2 scopes × 5 QUDs = 10 constructors.

surfHowMany : Latent10
surfAll : Latent10
surfNone : Latent10
surfTwoExact : Latent10
surfTwoAtLeast : Latent10
invHowMany : Latent10
invAll : Latent10
invNone : Latent10
invTwoExact : Latent10
invTwoAtLeast : Latent10

Instances For

instance Phenomena.Quantification.Studies.ScontrasPearl2021TwoNot.instDecidableEqLatent10 :

DecidableEq Latent10

Equations

Phenomena.Quantification.Studies.ScontrasPearl2021TwoNot.instDecidableEqLatent10 x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.Quantification.Studies.ScontrasPearl2021TwoNot.instBEqLatent10.beq :

Latent10 → Latent10 → Bool

Equations

Phenomena.Quantification.Studies.ScontrasPearl2021TwoNot.instBEqLatent10.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

instance Phenomena.Quantification.Studies.ScontrasPearl2021TwoNot.instBEqLatent10 :

Equations

Phenomena.Quantification.Studies.ScontrasPearl2021TwoNot.instBEqLatent10 = { beq := Phenomena.Quantification.Studies.ScontrasPearl2021TwoNot.instBEqLatent10.beq }

def Phenomena.Quantification.Studies.ScontrasPearl2021TwoNot.instReprLatent10.repr :

Latent10 → ℕ → Std.Format

Equations

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

Instances For

instance Phenomena.Quantification.Studies.ScontrasPearl2021TwoNot.instReprLatent10 :

Equations

Phenomena.Quantification.Studies.ScontrasPearl2021TwoNot.instReprLatent10 = { reprPrec := Phenomena.Quantification.Studies.ScontrasPearl2021TwoNot.instReprLatent10.repr }

def Phenomena.Quantification.Studies.ScontrasPearl2021TwoNot.instInhabitedLatent10.default :

Equations

Phenomena.Quantification.Studies.ScontrasPearl2021TwoNot.instInhabitedLatent10.default = Phenomena.Quantification.Studies.ScontrasPearl2021TwoNot.Latent10.surfHowMany

Instances For

instance Phenomena.Quantification.Studies.ScontrasPearl2021TwoNot.instInhabitedLatent10 :

Inhabited Latent10

Equations

Phenomena.Quantification.Studies.ScontrasPearl2021TwoNot.instInhabitedLatent10 = { default := Phenomena.Quantification.Studies.ScontrasPearl2021TwoNot.instInhabitedLatent10.default }

instance Phenomena.Quantification.Studies.ScontrasPearl2021TwoNot.instFintypeLatent10 :

Fintype Latent10

Equations

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

def Phenomena.Quantification.Studies.ScontrasPearl2021TwoNot.Latent10.scope :

Latent10 → ScontrasPearl2021.ScopeReading

Extract scope reading from latent variable.

Equations

Instances For

def Phenomena.Quantification.Studies.ScontrasPearl2021TwoNot.Latent10.qud :

Latent10 → QUD5

Extract QUD from latent variable.

Equations

Instances For

def Phenomena.Quantification.Studies.ScontrasPearl2021TwoNot.uttMeaning (nr : ScontrasPearl2021.NumeralReading) :

ScontrasPearl2021.ScopeReading → Utt → ScontrasPearl2021.JumpOutcome4 → Bool

RSA meaning for the two-not model, parameterized by numeral reading. Null utterance is always true (uninformative baseline).

Equations

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

Instances For

theorem Phenomena.Quantification.Studies.ScontrasPearl2021TwoNot.exact_truth_table :

uttMeaning ScontrasPearl2021.NumeralReading.exact ScontrasPearl2021.ScopeReading.surface Utt.twoNot ScontrasPearl2021.JumpOutcome4.w0 = false ∧ uttMeaning ScontrasPearl2021.NumeralReading.exact ScontrasPearl2021.ScopeReading.surface Utt.twoNot ScontrasPearl2021.JumpOutcome4.w1 = false ∧ uttMeaning ScontrasPearl2021.NumeralReading.exact ScontrasPearl2021.ScopeReading.surface Utt.twoNot ScontrasPearl2021.JumpOutcome4.w2 = true ∧ uttMeaning ScontrasPearl2021.NumeralReading.exact ScontrasPearl2021.ScopeReading.surface Utt.twoNot ScontrasPearl2021.JumpOutcome4.w3 = false ∧ uttMeaning ScontrasPearl2021.NumeralReading.exact ScontrasPearl2021.ScopeReading.surface Utt.twoNot ScontrasPearl2021.JumpOutcome4.w4 = false ∧ uttMeaning ScontrasPearl2021.NumeralReading.exact ScontrasPearl2021.ScopeReading.inverse Utt.twoNot ScontrasPearl2021.JumpOutcome4.w0 = true ∧ uttMeaning ScontrasPearl2021.NumeralReading.exact ScontrasPearl2021.ScopeReading.inverse Utt.twoNot ScontrasPearl2021.JumpOutcome4.w1 = true ∧ uttMeaning ScontrasPearl2021.NumeralReading.exact ScontrasPearl2021.ScopeReading.inverse Utt.twoNot ScontrasPearl2021.JumpOutcome4.w2 = false ∧ uttMeaning ScontrasPearl2021.NumeralReading.exact ScontrasPearl2021.ScopeReading.inverse Utt.twoNot ScontrasPearl2021.JumpOutcome4.w3 = true ∧ uttMeaning ScontrasPearl2021.NumeralReading.exact ScontrasPearl2021.ScopeReading.inverse Utt.twoNot ScontrasPearl2021.JumpOutcome4.w4 = true

Exact semantics truth table (eq 6a).

theorem Phenomena.Quantification.Studies.ScontrasPearl2021TwoNot.atLeast_truth_table :

uttMeaning ScontrasPearl2021.NumeralReading.atLeast ScontrasPearl2021.ScopeReading.surface Utt.twoNot ScontrasPearl2021.JumpOutcome4.w0 = true ∧ uttMeaning ScontrasPearl2021.NumeralReading.atLeast ScontrasPearl2021.ScopeReading.surface Utt.twoNot ScontrasPearl2021.JumpOutcome4.w1 = true ∧ uttMeaning ScontrasPearl2021.NumeralReading.atLeast ScontrasPearl2021.ScopeReading.surface Utt.twoNot ScontrasPearl2021.JumpOutcome4.w2 = true ∧ uttMeaning ScontrasPearl2021.NumeralReading.atLeast ScontrasPearl2021.ScopeReading.surface Utt.twoNot ScontrasPearl2021.JumpOutcome4.w3 = false ∧ uttMeaning ScontrasPearl2021.NumeralReading.atLeast ScontrasPearl2021.ScopeReading.surface Utt.twoNot ScontrasPearl2021.JumpOutcome4.w4 = false ∧ uttMeaning ScontrasPearl2021.NumeralReading.atLeast ScontrasPearl2021.ScopeReading.inverse Utt.twoNot ScontrasPearl2021.JumpOutcome4.w0 = true ∧ uttMeaning ScontrasPearl2021.NumeralReading.atLeast ScontrasPearl2021.ScopeReading.inverse Utt.twoNot ScontrasPearl2021.JumpOutcome4.w1 = true ∧ uttMeaning ScontrasPearl2021.NumeralReading.atLeast ScontrasPearl2021.ScopeReading.inverse Utt.twoNot ScontrasPearl2021.JumpOutcome4.w2 = false ∧ uttMeaning ScontrasPearl2021.NumeralReading.atLeast ScontrasPearl2021.ScopeReading.inverse Utt.twoNot ScontrasPearl2021.JumpOutcome4.w3 = false ∧ uttMeaning ScontrasPearl2021.NumeralReading.atLeast ScontrasPearl2021.ScopeReading.inverse Utt.twoNot ScontrasPearl2021.JumpOutcome4.w4 = false

At-least semantics truth table (eq 6b).

def Phenomena.Quantification.Studies.ScontrasPearl2021TwoNot.qudProject (q : QUD5) (f : ScontrasPearl2021.JumpOutcome4 → ℝ) (w : ScontrasPearl2021.JumpOutcome4) :

QUD projection for the 5-world domain (eq 4, extended). Explicit case analysis, kernel-reducible.

Equations

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

Instances For

theorem Phenomena.Quantification.Studies.ScontrasPearl2021TwoNot.qudProject_nonneg {q : QUD5} {f : ScontrasPearl2021.JumpOutcome4 → ℝ} {w : ScontrasPearl2021.JumpOutcome4} (hf : ∀ (w : ScontrasPearl2021.JumpOutcome4), 0 ≤ f w) :

0 ≤ qudProject q f w

noncomputable def Phenomena.Quantification.Studies.ScontrasPearl2021TwoNot.cfg (nr : ScontrasPearl2021.NumeralReading) (worldPr : ScontrasPearl2021.JumpOutcome4 → ℝ) (hwp : ∀ (w : ScontrasPearl2021.JumpOutcome4), 0 ≤ worldPr w) (scopePr : ScontrasPearl2021.ScopeReading → ℝ) (hsp : ∀ (s : ScontrasPearl2021.ScopeReading), 0 ≤ scopePr s) (qudPr : QUD5 → ℝ) (hqp : ∀ (q : QUD5), 0 ≤ qudPr q) :

RSA.RSAConfig Utt ScontrasPearl2021.JumpOutcome4

Two-not RSA model, parameterized by numeral reading and priors. Same architecture as the every-not model: S1 uses QUD-projected rpow with α = 1, L0 does not incorporate the world prior.

Equations

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

Instances For

World priors follow Binomial(4, b_suc), unnormalized.

The paper's central 2-of-4 predictions (Figure 7) use b_suc = 0.1
with low P(inverse) = 0.1 (surface scope bias), matching the baseline
parameters from the every-not model that produce low 1-of-2 endorsement.

Binomial(4, 0.1) ∝ C(4,k) · 1^k · 9^(4-k) = (6561, 2916, 486, 36, 1).

@[reducible, inline]

noncomputable abbrev Phenomena.Quantification.Studies.ScontrasPearl2021TwoNot.exactBaselineCfg :

RSA.RSAConfig Utt ScontrasPearl2021.JumpOutcome4

Baseline exact config: b_suc = 0.1, P(inv) = 0.1 (surface scope bias). Matches Figure 7 right panel, red bar (S2 ≈ 0.8).

Equations

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

Instances For

@[reducible, inline]

noncomputable abbrev Phenomena.Quantification.Studies.ScontrasPearl2021TwoNot.atleastBaselineCfg :

RSA.RSAConfig Utt ScontrasPearl2021.JumpOutcome4

Baseline at-least config: same parameters, at-least numeral semantics. Matches Figure 7 left panel, red bar (S2 ≈ 0.1).

Equations

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

Instances For

@[reducible, inline]

noncomputable abbrev Phenomena.Quantification.Studies.ScontrasPearl2021TwoNot.exactSymCfg :

RSA.RSAConfig Utt ScontrasPearl2021.JumpOutcome4

Symmetric exact config: b_suc = 0.5, uniform scope/QUD. Binomial(4, 0.5) ∝ (1, 4, 6, 4, 1).

Equations

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

Instances For

@[reducible, inline]

noncomputable abbrev Phenomena.Quantification.Studies.ScontrasPearl2021TwoNot.atleastSymCfg :

RSA.RSAConfig Utt ScontrasPearl2021.JumpOutcome4

Symmetric at-least config: b_suc = 0.5, uniform scope/QUD.

Equations

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

Instances For

The paper's central claims for the 2-of-4 context (Figure 7).

Under exact semantics with low base rate (b_suc = 0.1) and surface scope
bias (P(inv) = 0.1), surface scope pinpoints w=2 as the unique true world,
giving maximum informativity → high S2 endorsement at w=2.

Under at-least semantics with the same parameters, surface scope is true
at {w0,w1,w2}, diluting informativity → low S2 endorsement at w=2.

The 1-of-2 vs 2-of-4 asymmetry: these SAME "baseline" parameters produce
low endorsement (27.5%) in the 1-of-2 context but high endorsement in the
2-of-4 context, but ONLY under exact numeral semantics. This is the
paper's key argument for exact semantics as the basic numeral meaning.

S2 predictions may require sorry because the state space
(5 worlds × 10 latents × 2 utterances = 100 S1 scores) exceeds
the heartbeat budget for kernel-level proof checking.

theorem Phenomena.Quantification.Studies.ScontrasPearl2021TwoNot.exact_baseline_endorsement_high :

exactBaselineCfg.S2 ScontrasPearl2021.JumpOutcome4.w2 Utt.twoNot > 1 / 2

Under exact semantics with baseline parameters (b_suc=0.1, P(inv)=0.1), S2 endorsement of "two horses didn't jump" at w=2 exceeds 1/2. Surface scope pinpoints w=2 as the unique true world, giving maximum informativity (Figure 7 right, red bar ≈ 0.8).

theorem Phenomena.Quantification.Studies.ScontrasPearl2021TwoNot.exact_vs_atleast_endorsement :

exactBaselineCfg.S2 ScontrasPearl2021.JumpOutcome4.w2 Utt.twoNot > atleastBaselineCfg.S2 ScontrasPearl2021.JumpOutcome4.w2 Utt.twoNot

Under at-least semantics with baseline parameters, S2 endorsement at w=2 is lower than under exact semantics. Exact surface has 1 true world; at-least surface has 3. (Figure 7: right panel > left panel at matching P(inv).)

theorem Phenomena.Quantification.Studies.ScontrasPearl2021TwoNot.exact_surface_singleton :

(List.filter (uttMeaning ScontrasPearl2021.NumeralReading.exact ScontrasPearl2021.ScopeReading.surface Utt.twoNot) [ScontrasPearl2021.JumpOutcome4.w0 , ScontrasPearl2021.JumpOutcome4.w1 , ScontrasPearl2021.JumpOutcome4.w2 , ScontrasPearl2021.JumpOutcome4.w3 , ScontrasPearl2021.JumpOutcome4.w4 ]).length = 1

The key informativity contrast: under exact semantics, surface scope has exactly 1 true world (w2), while under at-least it has 3 (w0–w2). This drives the endorsement difference via S1 informativity.

theorem Phenomena.Quantification.Studies.ScontrasPearl2021TwoNot.exact_inverse_quad :

(List.filter (uttMeaning ScontrasPearl2021.NumeralReading.exact ScontrasPearl2021.ScopeReading.inverse Utt.twoNot) [ScontrasPearl2021.JumpOutcome4.w0 , ScontrasPearl2021.JumpOutcome4.w1 , ScontrasPearl2021.JumpOutcome4.w2 , ScontrasPearl2021.JumpOutcome4.w3 , ScontrasPearl2021.JumpOutcome4.w4 ]).length = 4

Exact inverse has 4 true worlds (w0,w1,w3,w4) — very uninformative. Since w2 is the only world where surface scope is true, inverse scope contributes nothing at w2 (it's false there), explaining why surface scope dominates the S2 prediction under exact semantics.

theorem Phenomena.Quantification.Studies.ScontrasPearl2021TwoNot.atLeast_inverse_double :

(List.filter (uttMeaning ScontrasPearl2021.NumeralReading.atLeast ScontrasPearl2021.ScopeReading.inverse Utt.twoNot) [ScontrasPearl2021.JumpOutcome4.w0 , ScontrasPearl2021.JumpOutcome4.w1 , ScontrasPearl2021.JumpOutcome4.w2 , ScontrasPearl2021.JumpOutcome4.w3 , ScontrasPearl2021.JumpOutcome4.w4 ]).length = 2

At-least inverse has 2 true worlds (w0,w1) — more informative than exact inverse's 4, but still less informative than exact surface's 1.