Documentation

Linglib.Phenomena.Quantification.Studies.ScontrasPearl2021

@cite{scontras-pearl-2021}: Quantifier Scope Ambiguity @cite{musolino-lidz-2003} #

"When pragmatics matters more for truth-value judgments: An investigation of quantifier scope ambiguity" Glossa 6(1): 110.

S&P is a modeling paper — it explains endorsement patterns from @cite{musolino-lidz-2003} and others via RSA, rather than reporting new experiments.

Part I: Truth Conditions & Shared Types #

§1. Every-not (n=2): JumpOutcome, ScopeReading, scopeTruth
§2. Two-not (n=4): JumpOutcome4, NumeralReading, twoNotTruth
Scope entailment asymmetry, @cite{musolino-lidz-2003} data, and numeral semantics grounding via maxMeaning from Numeral.Semantics.

Part II: Every-Not RSA Model (§3, `EveryNot` namespace) #

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(w) = Binomial(n, b_suc).

QUDs (paper (3)) #

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}

Compositional Grounding #

Truth conditions grounded in every_sem (Quantifier.lean), ScopeConfig/ScopeDerivation (Scope.lean).

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

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

QUD manipulation (Figure 2, center panel): favoring none? < how-many? < all? yields monotonically increasing endorsement (paper: 0.38, 0.48, 0.63).

Developmental Continuity (§3.3) #

Same model architecture explains child and adult behavior. Children's isomorphic (surface-scope) preference follows from low b_suc priors.

Part III: Two-Not RSA Model (§4, `TwoNot` namespace) #

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

Central Claim (§4.2) #

Under exact semantics, surface scope pinpoints w=2 as the unique true world → high S2 endorsement (> 1/2). Under at-least semantics, surface scope is true at {w0,w1,w2} → low S2 endorsement (< 1/2). This predicts that adults endorse "two horses didn't jump" more readily in 2-of-4 contexts under exact numeral semantics.

inductive Phenomena.Quantification.Studies.ScontrasPearl2021.JumpOutcome :

How many horses jumped (out of 2).

Instances For

instance Phenomena.Quantification.Studies.ScontrasPearl2021.instDecidableEqJumpOutcome :

DecidableEq JumpOutcome

Equations

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

def Phenomena.Quantification.Studies.ScontrasPearl2021.instBEqJumpOutcome.beq :

JumpOutcome → JumpOutcome → Bool

Equations

Phenomena.Quantification.Studies.ScontrasPearl2021.instBEqJumpOutcome.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

instance Phenomena.Quantification.Studies.ScontrasPearl2021.instBEqJumpOutcome :

BEq JumpOutcome

Equations

Phenomena.Quantification.Studies.ScontrasPearl2021.instBEqJumpOutcome = { beq := Phenomena.Quantification.Studies.ScontrasPearl2021.instBEqJumpOutcome.beq }

instance Phenomena.Quantification.Studies.ScontrasPearl2021.instReprJumpOutcome :

Repr JumpOutcome

Equations

Phenomena.Quantification.Studies.ScontrasPearl2021.instReprJumpOutcome = { reprPrec := Phenomena.Quantification.Studies.ScontrasPearl2021.instReprJumpOutcome.repr }

def Phenomena.Quantification.Studies.ScontrasPearl2021.instReprJumpOutcome.repr :

JumpOutcome → ℕ → Std.Format

Equations

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

Instances For

def Phenomena.Quantification.Studies.ScontrasPearl2021.instInhabitedJumpOutcome.default :

Equations

Phenomena.Quantification.Studies.ScontrasPearl2021.instInhabitedJumpOutcome.default = Phenomena.Quantification.Studies.ScontrasPearl2021.JumpOutcome.zero

Instances For

instance Phenomena.Quantification.Studies.ScontrasPearl2021.instInhabitedJumpOutcome :

Inhabited JumpOutcome

Equations

Phenomena.Quantification.Studies.ScontrasPearl2021.instInhabitedJumpOutcome = { default := Phenomena.Quantification.Studies.ScontrasPearl2021.instInhabitedJumpOutcome.default }

instance Phenomena.Quantification.Studies.ScontrasPearl2021.instFintypeJumpOutcome :

Fintype JumpOutcome

Equations

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

inductive Phenomena.Quantification.Studies.ScontrasPearl2021.ScopeReading :

Scope configuration for "every...not".

surface : ScopeReading
inverse : ScopeReading

Instances For

instance Phenomena.Quantification.Studies.ScontrasPearl2021.instDecidableEqScopeReading :

DecidableEq ScopeReading

Equations

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

instance Phenomena.Quantification.Studies.ScontrasPearl2021.instBEqScopeReading :

BEq ScopeReading

Equations

Phenomena.Quantification.Studies.ScontrasPearl2021.instBEqScopeReading = { beq := Phenomena.Quantification.Studies.ScontrasPearl2021.instBEqScopeReading.beq }

def Phenomena.Quantification.Studies.ScontrasPearl2021.instBEqScopeReading.beq :

ScopeReading → ScopeReading → Bool

Equations

Phenomena.Quantification.Studies.ScontrasPearl2021.instBEqScopeReading.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

instance Phenomena.Quantification.Studies.ScontrasPearl2021.instReprScopeReading :

Repr ScopeReading

Equations

Phenomena.Quantification.Studies.ScontrasPearl2021.instReprScopeReading = { reprPrec := Phenomena.Quantification.Studies.ScontrasPearl2021.instReprScopeReading.repr }

def Phenomena.Quantification.Studies.ScontrasPearl2021.instReprScopeReading.repr :

ScopeReading → ℕ → Std.Format

Equations

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

Instances For

instance Phenomena.Quantification.Studies.ScontrasPearl2021.instInhabitedScopeReading :

Inhabited ScopeReading

Equations

Phenomena.Quantification.Studies.ScontrasPearl2021.instInhabitedScopeReading = { default := Phenomena.Quantification.Studies.ScontrasPearl2021.instInhabitedScopeReading.default }

def Phenomena.Quantification.Studies.ScontrasPearl2021.instInhabitedScopeReading.default :

Equations

Phenomena.Quantification.Studies.ScontrasPearl2021.instInhabitedScopeReading.default = Phenomena.Quantification.Studies.ScontrasPearl2021.ScopeReading.surface

Instances For

instance Phenomena.Quantification.Studies.ScontrasPearl2021.instFintypeScopeReading :

Fintype ScopeReading

Equations

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

def Phenomena.Quantification.Studies.ScontrasPearl2021.scopeTruth :

ScopeReading → JumpOutcome → Bool

Truth conditions for "Every horse didn't jump" under each scope reading.

Equations

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

Instances For

theorem Phenomena.Quantification.Studies.ScontrasPearl2021.surface_scope_truth :

scopeTruth ScopeReading.surface JumpOutcome.zero = true ∧ scopeTruth ScopeReading.surface JumpOutcome.one = false ∧ scopeTruth ScopeReading.surface JumpOutcome.two = false

Scope truth table correctness.

theorem Phenomena.Quantification.Studies.ScontrasPearl2021.inverse_scope_truth :

scopeTruth ScopeReading.inverse JumpOutcome.zero = true ∧ scopeTruth ScopeReading.inverse JumpOutcome.one = true ∧ scopeTruth ScopeReading.inverse JumpOutcome.two = false

inductive Phenomena.Quantification.Studies.ScontrasPearl2021.JumpOutcome4 :

How many horses jumped (out of 4).

Instances For

instance Phenomena.Quantification.Studies.ScontrasPearl2021.instDecidableEqJumpOutcome4 :

DecidableEq JumpOutcome4

Equations

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

def Phenomena.Quantification.Studies.ScontrasPearl2021.instBEqJumpOutcome4.beq :

JumpOutcome4 → JumpOutcome4 → Bool

Equations

Phenomena.Quantification.Studies.ScontrasPearl2021.instBEqJumpOutcome4.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

instance Phenomena.Quantification.Studies.ScontrasPearl2021.instBEqJumpOutcome4 :

BEq JumpOutcome4

Equations

Phenomena.Quantification.Studies.ScontrasPearl2021.instBEqJumpOutcome4 = { beq := Phenomena.Quantification.Studies.ScontrasPearl2021.instBEqJumpOutcome4.beq }

instance Phenomena.Quantification.Studies.ScontrasPearl2021.instReprJumpOutcome4 :

Repr JumpOutcome4

Equations

Phenomena.Quantification.Studies.ScontrasPearl2021.instReprJumpOutcome4 = { reprPrec := Phenomena.Quantification.Studies.ScontrasPearl2021.instReprJumpOutcome4.repr }

def Phenomena.Quantification.Studies.ScontrasPearl2021.instReprJumpOutcome4.repr :

JumpOutcome4 → ℕ → Std.Format

Equations

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

Instances For

instance Phenomena.Quantification.Studies.ScontrasPearl2021.instInhabitedJumpOutcome4 :

Inhabited JumpOutcome4

Equations

Phenomena.Quantification.Studies.ScontrasPearl2021.instInhabitedJumpOutcome4 = { default := Phenomena.Quantification.Studies.ScontrasPearl2021.instInhabitedJumpOutcome4.default }

def Phenomena.Quantification.Studies.ScontrasPearl2021.instInhabitedJumpOutcome4.default :

Equations

Phenomena.Quantification.Studies.ScontrasPearl2021.instInhabitedJumpOutcome4.default = Phenomena.Quantification.Studies.ScontrasPearl2021.JumpOutcome4.w0

Instances For

instance Phenomena.Quantification.Studies.ScontrasPearl2021.instFintypeJumpOutcome4 :

Fintype JumpOutcome4

Equations

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

def Phenomena.Quantification.Studies.ScontrasPearl2021.JumpOutcome4.toNat :

JumpOutcome4 → ℕ

Convert JumpOutcome4 to natural number.

Equations

Instances For

inductive Phenomena.Quantification.Studies.ScontrasPearl2021.NumeralReading :

Numeral reading: does "two" mean exactly 2 or at least 2?

exact : NumeralReading
atLeast : NumeralReading

Instances For

instance Phenomena.Quantification.Studies.ScontrasPearl2021.instDecidableEqNumeralReading :

DecidableEq NumeralReading

Equations

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

instance Phenomena.Quantification.Studies.ScontrasPearl2021.instBEqNumeralReading :

BEq NumeralReading

Equations

Phenomena.Quantification.Studies.ScontrasPearl2021.instBEqNumeralReading = { beq := Phenomena.Quantification.Studies.ScontrasPearl2021.instBEqNumeralReading.beq }

def Phenomena.Quantification.Studies.ScontrasPearl2021.instBEqNumeralReading.beq :

NumeralReading → NumeralReading → Bool

Equations

Phenomena.Quantification.Studies.ScontrasPearl2021.instBEqNumeralReading.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

def Phenomena.Quantification.Studies.ScontrasPearl2021.instReprNumeralReading.repr :

NumeralReading → ℕ → Std.Format

Equations

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

Instances For

instance Phenomena.Quantification.Studies.ScontrasPearl2021.instReprNumeralReading :

Repr NumeralReading

Equations

Phenomena.Quantification.Studies.ScontrasPearl2021.instReprNumeralReading = { reprPrec := Phenomena.Quantification.Studies.ScontrasPearl2021.instReprNumeralReading.repr }

instance Phenomena.Quantification.Studies.ScontrasPearl2021.instInhabitedNumeralReading :

Inhabited NumeralReading

Equations

Phenomena.Quantification.Studies.ScontrasPearl2021.instInhabitedNumeralReading = { default := Phenomena.Quantification.Studies.ScontrasPearl2021.instInhabitedNumeralReading.default }

def Phenomena.Quantification.Studies.ScontrasPearl2021.instInhabitedNumeralReading.default :

Equations

Phenomena.Quantification.Studies.ScontrasPearl2021.instInhabitedNumeralReading.default = Phenomena.Quantification.Studies.ScontrasPearl2021.NumeralReading.exact

Instances For

instance Phenomena.Quantification.Studies.ScontrasPearl2021.instFintypeNumeralReading :

Fintype NumeralReading

Equations

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

def Phenomena.Quantification.Studies.ScontrasPearl2021.twoNotTruth :

NumeralReading → ScopeReading → JumpOutcome4 → Bool

Truth conditions for "two horses didn't jump" with n=4 horses (paper (6)).

Parameterized by numeral reading and scope configuration.

Surface scope (two > not): "There are two horses that didn't jump"

Exact: exactly 2 didn't jump → exactly 2 jumped → w=2
At-least: at least 2 didn't jump → at most 2 jumped → w ∈ {0,1,2}

Inverse scope (not > two): "It's not the case that two horses jumped"

Exact: ¬(exactly 2 jumped) → w ≠ 2 → w ∈ {0,1,3,4}
At-least: ¬(at least 2 jumped) → fewer than 2 jumped → w ∈ {0,1}

Equations

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

Instances For

The two numeral theories diverge in the 2-of-4 context (n=4). Surface scope: exact → {w2}, at-least → {w0,w1,w2} Inverse scope: exact → {w0,w1,w3,w4}, at-least → {w0,w1}

theorem Phenomena.Quantification.Studies.ScontrasPearl2021.universal_surface_entails_inverse (w : JumpOutcome) :

scopeTruth ScopeReading.surface w = true → scopeTruth ScopeReading.inverse w = true

For universals, surface scope (∀>¬: none jumped) ENTAILS inverse scope (¬>∀: not all jumped). If no horse jumped, then trivially not every horse jumped. This means no truth-value judgment context can diagnose the isomorphism effect for universals: whenever surface is true, inverse is automatically true too.

theorem Phenomena.Quantification.Studies.ScontrasPearl2021.universal_inverse_not_entails_surface :

∃ (w : JumpOutcome), scopeTruth ScopeReading.inverse w = true ∧ scopeTruth ScopeReading.surface w = false

The entailment is strict: inverse does NOT entail surface. At w=1 (one horse jumped), inverse scope is true (not all jumped) but surface scope is false (not none jumped).

theorem Phenomena.Quantification.Studies.ScontrasPearl2021.numeral_surface_not_entails_inverse :

∃ (w : JumpOutcome4), twoNotTruth NumeralReading.exact ScopeReading.surface w = true ∧ twoNotTruth NumeralReading.exact ScopeReading.inverse w = false

For exact numerals, surface scope does NOT entail inverse scope. At w=2 (exactly 2 jumped out of 4), surface is true (exactly 2 didn't) but inverse is false (it IS the case that exactly 2 jumped). This independence is what makes numerals diagnostic for the isomorphism effect.

theorem Phenomena.Quantification.Studies.ScontrasPearl2021.numeral_inverse_not_entails_surface :

∃ (w : JumpOutcome4), twoNotTruth NumeralReading.exact ScopeReading.inverse w = true ∧ twoNotTruth NumeralReading.exact ScopeReading.surface w = false

Inverse scope also does not entail surface for exact numerals. At w=0 (none jumped), inverse is true (¬(exactly 2 jumped)) but surface is false (not exactly 2 didn't jump, since all 4 didn't).

Connects S&P's twoNotTruth truth conditions to linglib's numeral semantics infrastructure (maxMeaning in Numeral.Semantics).

The truth conditions in the data file are grounded in maxMeaning:

Exact surface: "exactly 2 didn't jump" = maxMeaning.eq 2 (4 - w)
Exact inverse: "¬(exactly 2 jumped)" = !(maxMeaning.eq 2 w)
At-least surface: "≥2 didn't jump" = maxMeaning.ge 2 (4 - w)
At-least inverse: "¬(≥2 jumped)" = !(maxMeaning.ge 2 w)

Convergent evidence for exact semantics from @cite{kennedy-2015} (de-Fregean semantics where bare numerals mean =n) and @cite{musolino-2004} (acquisition data — children reject "two" at w=3).

theorem Phenomena.Quantification.Studies.ScontrasPearl2021.twoNotExact_surface_matches_maxMeaning (w : JumpOutcome4) :

twoNotTruth NumeralReading.exact ScopeReading.surface w = Semantics.Lexical.Numeral.maxMeaning Semantics.Lexical.Numeral.OrderingRel.eq 2 (4 - w.toNat)

Exact surface: "exactly two didn't jump" (out of 4) ↔ exactly two jumped. Matches maxMeaning.eq 2 applied to the complement count (4 - w).

theorem Phenomena.Quantification.Studies.ScontrasPearl2021.twoNotExact_inverse_matches_maxMeaning (w : JumpOutcome4) :

twoNotTruth NumeralReading.exact ScopeReading.inverse w = !Semantics.Lexical.Numeral.maxMeaning Semantics.Lexical.Numeral.OrderingRel.eq 2 w.toNat

Exact inverse: "¬(exactly two jumped)" ↔ !(maxMeaning.eq 2 w).

theorem Phenomena.Quantification.Studies.ScontrasPearl2021.twoNotAtLeast_surface_matches_maxMeaning (w : JumpOutcome4) :

twoNotTruth NumeralReading.atLeast ScopeReading.surface w = Semantics.Lexical.Numeral.maxMeaning Semantics.Lexical.Numeral.OrderingRel.ge 2 (4 - w.toNat)

At-least surface: "at least two didn't jump" ↔ at most two jumped. Matches maxMeaning.ge 2 applied to the complement count.

theorem Phenomena.Quantification.Studies.ScontrasPearl2021.twoNotAtLeast_inverse_matches_maxMeaning (w : JumpOutcome4) :

twoNotTruth NumeralReading.atLeast ScopeReading.inverse w = !Semantics.Lexical.Numeral.maxMeaning Semantics.Lexical.Numeral.OrderingRel.ge 2 w.toNat

At-least inverse: "¬(at least two jumped)" ↔ !(maxMeaning.ge 2 w).

theorem Phenomena.Quantification.Studies.ScontrasPearl2021.exact_collapses_negation_scope :

Implicature.negatedMeaning Semantics.Lexical.Numeral.Exact Semantics.Lexical.Numeral.BareNumeral.three Implicature.NegationScope.internal 4 = Implicature.negatedMeaning Semantics.Lexical.Numeral.Exact Semantics.Lexical.Numeral.BareNumeral.three Implicature.NegationScope.external 4

The negation-scope asymmetry collapses under exact semantics: internal and external negation of "three" give the same result.

theorem Phenomena.Quantification.Studies.ScontrasPearl2021.lowerBound_preserves_negation_scope :

Implicature.negatedMeaning Semantics.Lexical.Numeral.LowerBound Semantics.Lexical.Numeral.BareNumeral.three Implicature.NegationScope.internal 4 ≠ Implicature.negatedMeaning Semantics.Lexical.Numeral.LowerBound Semantics.Lexical.Numeral.BareNumeral.three Implicature.NegationScope.external 4

Lower-bound semantics preserves the negation-scope distinction.

theorem Phenomena.Quantification.Studies.ScontrasPearl2021.typeshift_resolves_tension :

Semantics.Lexical.Numeral.typeLower (Semantics.Lexical.Numeral.maxMeaning Semantics.Lexical.Numeral.OrderingRel.eq) 4 2 2 = Semantics.Lexical.Numeral.maxMeaning Semantics.Lexical.Numeral.OrderingRel.ge 2 2

@cite{kennedy-2015}'s resolution: exact meaning is basic, lower-bound is derived via type-shift. Both meanings are grammatically available.

inductive Phenomena.Quantification.Studies.ScontrasPearl2021.EveryNot.Utt :

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

null : Utt
everyNot : Utt

Instances For

instance Phenomena.Quantification.Studies.ScontrasPearl2021.EveryNot.instDecidableEqUtt :

DecidableEq Utt

Equations

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

instance Phenomena.Quantification.Studies.ScontrasPearl2021.EveryNot.instBEqUtt :

Equations

Phenomena.Quantification.Studies.ScontrasPearl2021.EveryNot.instBEqUtt = { beq := Phenomena.Quantification.Studies.ScontrasPearl2021.EveryNot.instBEqUtt.beq }

def Phenomena.Quantification.Studies.ScontrasPearl2021.EveryNot.instBEqUtt.beq :

Utt → Utt → Bool

Equations

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

Instances For

instance Phenomena.Quantification.Studies.ScontrasPearl2021.EveryNot.instReprUtt :

Equations

Phenomena.Quantification.Studies.ScontrasPearl2021.EveryNot.instReprUtt = { reprPrec := Phenomena.Quantification.Studies.ScontrasPearl2021.EveryNot.instReprUtt.repr }

def Phenomena.Quantification.Studies.ScontrasPearl2021.EveryNot.instReprUtt.repr :

Utt → ℕ → Std.Format

Equations

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

Instances For

def Phenomena.Quantification.Studies.ScontrasPearl2021.EveryNot.instInhabitedUtt.default :

Equations

Phenomena.Quantification.Studies.ScontrasPearl2021.EveryNot.instInhabitedUtt.default = Phenomena.Quantification.Studies.ScontrasPearl2021.EveryNot.Utt.null

Instances For

instance Phenomena.Quantification.Studies.ScontrasPearl2021.EveryNot.instInhabitedUtt :

Equations

Phenomena.Quantification.Studies.ScontrasPearl2021.EveryNot.instInhabitedUtt = { default := Phenomena.Quantification.Studies.ScontrasPearl2021.EveryNot.instInhabitedUtt.default }

instance Phenomena.Quantification.Studies.ScontrasPearl2021.EveryNot.instFintypeUtt :

Equations

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

inductive Phenomena.Quantification.Studies.ScontrasPearl2021.EveryNot.QUD :

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

howMany : QUD
all_ : QUD
none_ : QUD

Instances For

instance Phenomena.Quantification.Studies.ScontrasPearl2021.EveryNot.instDecidableEqQUD :

DecidableEq QUD

Equations

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

instance Phenomena.Quantification.Studies.ScontrasPearl2021.EveryNot.instBEqQUD :

Equations

Phenomena.Quantification.Studies.ScontrasPearl2021.EveryNot.instBEqQUD = { beq := Phenomena.Quantification.Studies.ScontrasPearl2021.EveryNot.instBEqQUD.beq }

def Phenomena.Quantification.Studies.ScontrasPearl2021.EveryNot.instBEqQUD.beq :

QUD → QUD → Bool

Equations

Phenomena.Quantification.Studies.ScontrasPearl2021.EveryNot.instBEqQUD.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

def Phenomena.Quantification.Studies.ScontrasPearl2021.EveryNot.instReprQUD.repr :

QUD → ℕ → Std.Format

Equations

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

Instances For

instance Phenomena.Quantification.Studies.ScontrasPearl2021.EveryNot.instReprQUD :

Equations

Phenomena.Quantification.Studies.ScontrasPearl2021.EveryNot.instReprQUD = { reprPrec := Phenomena.Quantification.Studies.ScontrasPearl2021.EveryNot.instReprQUD.repr }

def Phenomena.Quantification.Studies.ScontrasPearl2021.EveryNot.instInhabitedQUD.default :

Equations

Phenomena.Quantification.Studies.ScontrasPearl2021.EveryNot.instInhabitedQUD.default = Phenomena.Quantification.Studies.ScontrasPearl2021.EveryNot.QUD.howMany

Instances For

instance Phenomena.Quantification.Studies.ScontrasPearl2021.EveryNot.instInhabitedQUD :

Equations

Phenomena.Quantification.Studies.ScontrasPearl2021.EveryNot.instInhabitedQUD = { default := Phenomena.Quantification.Studies.ScontrasPearl2021.EveryNot.instInhabitedQUD.default }

instance Phenomena.Quantification.Studies.ScontrasPearl2021.EveryNot.instFintypeQUD :

Equations

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

inductive Phenomena.Quantification.Studies.ScontrasPearl2021.EveryNot.Latent :

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

Instances For

instance Phenomena.Quantification.Studies.ScontrasPearl2021.EveryNot.instDecidableEqLatent :

DecidableEq Latent

Equations

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

instance Phenomena.Quantification.Studies.ScontrasPearl2021.EveryNot.instBEqLatent :

Equations

Phenomena.Quantification.Studies.ScontrasPearl2021.EveryNot.instBEqLatent = { beq := Phenomena.Quantification.Studies.ScontrasPearl2021.EveryNot.instBEqLatent.beq }

def Phenomena.Quantification.Studies.ScontrasPearl2021.EveryNot.instBEqLatent.beq :

Latent → Latent → Bool

Equations

Phenomena.Quantification.Studies.ScontrasPearl2021.EveryNot.instBEqLatent.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

instance Phenomena.Quantification.Studies.ScontrasPearl2021.EveryNot.instReprLatent :

Equations

Phenomena.Quantification.Studies.ScontrasPearl2021.EveryNot.instReprLatent = { reprPrec := Phenomena.Quantification.Studies.ScontrasPearl2021.EveryNot.instReprLatent.repr }

def Phenomena.Quantification.Studies.ScontrasPearl2021.EveryNot.instReprLatent.repr :

Latent → ℕ → Std.Format

Equations

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

Instances For

instance Phenomena.Quantification.Studies.ScontrasPearl2021.EveryNot.instInhabitedLatent :

Inhabited Latent

Equations

Phenomena.Quantification.Studies.ScontrasPearl2021.EveryNot.instInhabitedLatent = { default := Phenomena.Quantification.Studies.ScontrasPearl2021.EveryNot.instInhabitedLatent.default }

def Phenomena.Quantification.Studies.ScontrasPearl2021.EveryNot.instInhabitedLatent.default :

Equations

Phenomena.Quantification.Studies.ScontrasPearl2021.EveryNot.instInhabitedLatent.default = Phenomena.Quantification.Studies.ScontrasPearl2021.EveryNot.Latent.surfHowMany

Instances For

instance Phenomena.Quantification.Studies.ScontrasPearl2021.EveryNot.instFintypeLatent :

Equations

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

def Phenomena.Quantification.Studies.ScontrasPearl2021.EveryNot.Latent.scope :

Latent → ScopeReading

Extract scope reading from latent variable.

Equations

Instances For

def Phenomena.Quantification.Studies.ScontrasPearl2021.EveryNot.Latent.qud :

Extract QUD from latent variable.

Equations

Instances For

def Phenomena.Quantification.Studies.ScontrasPearl2021.EveryNot.uttMeaning :

ScopeReading → Utt → JumpOutcome → Bool

RSA meaning derived from scopeTruth. Null utterance is always true (uninformative baseline).

Equations

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

Instances For

Truth table verification against the paper's utterance semantics (2).

inductive Phenomena.Quantification.Studies.ScontrasPearl2021.EveryNot.Horse :

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

h1 : Horse
h2 : Horse

Instances For

instance Phenomena.Quantification.Studies.ScontrasPearl2021.EveryNot.instDecidableEqHorse :

DecidableEq Horse

Equations

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

def Phenomena.Quantification.Studies.ScontrasPearl2021.EveryNot.jumpIn :

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.ScontrasPearl2021.EveryNot.jumpIn Phenomena.Quantification.Studies.ScontrasPearl2021.JumpOutcome.zero x✝ = false
Phenomena.Quantification.Studies.ScontrasPearl2021.EveryNot.jumpIn Phenomena.Quantification.Studies.ScontrasPearl2021.JumpOutcome.two x✝ = true

Instances For

@[reducible, inline]

abbrev Phenomena.Quantification.Studies.ScontrasPearl2021.EveryNot.horseModel :

Semantics.Montague.Model

Horse model as a Montague Model.

Equations

Phenomena.Quantification.Studies.ScontrasPearl2021.EveryNot.horseModel = { Entity := Phenomena.Quantification.Studies.ScontrasPearl2021.EveryNot.Horse, decEq := inferInstance }

Instances For

instance Phenomena.Quantification.Studies.ScontrasPearl2021.EveryNot.instFintypeEntityHorseModel :

Fintype horseModel.Entity

Equations

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

def Phenomena.Quantification.Studies.ScontrasPearl2021.EveryNot.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.ScontrasPearl2021.EveryNot.horse_sem x✝ = true

Instances For

def Phenomena.Quantification.Studies.ScontrasPearl2021.EveryNot.jumpIn_sem (w : JumpOutcome) :

horseModel.interpTy (Semantics.Montague.Ty.e ⇒ Semantics.Montague.Ty.t)

Scope predicate: did entity h jump in world w?

Equations

Phenomena.Quantification.Studies.ScontrasPearl2021.EveryNot.jumpIn_sem w h = Phenomena.Quantification.Studies.ScontrasPearl2021.EveryNot.jumpIn w h

Instances For

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

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

Equations

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

Instances For

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

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

Equations

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

Instances For

theorem Phenomena.Quantification.Studies.ScontrasPearl2021.EveryNot.surface_from_every_sem (w : JumpOutcome) :

scopeTruth 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.ScontrasPearl2021.EveryNot.inverse_from_every_sem (w : JumpOutcome) :

scopeTruth 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.ScontrasPearl2021.EveryNot.scopeConfigToReading :

Semantics.Scope.ScopeConfig → ScopeReading

Map Montague ScopeConfig to data file's ScopeReading.

Equations

Instances For

def Phenomena.Quantification.Studies.ScontrasPearl2021.EveryNot.readingToScopeConfig :

ScopeReading → Semantics.Scope.ScopeConfig

Map data file's ScopeReading to Montague ScopeConfig.

Equations

Instances For

def Phenomena.Quantification.Studies.ScontrasPearl2021.EveryNot.everyHorseDidntJump (w : 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.

Instances For

theorem Phenomena.Quantification.Studies.ScontrasPearl2021.EveryNot.scopeDerivation_matches_scopeTruth (s : Semantics.Scope.ScopeConfig) (w : JumpOutcome) :

(everyHorseDidntJump w).meaningAt s = scopeTruth (scopeConfigToReading s) w

The ScopeDerivation's meaningAt matches scopeTruth for both readings.

theorem Phenomena.Quantification.Studies.ScontrasPearl2021.EveryNot.rsa_meaning_from_scope_derivation (lat : Latent) (w : 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.ScontrasPearl2021.EveryNot.every_not_scope_entailment :

Semantics.Scope.classifyScopeEntailment [JumpOutcome.zero , JumpOutcome.one , JumpOutcome.two ] (scopeTruth ScopeReading.surface) (scopeTruth 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.ScontrasPearl2021.EveryNot.qudAnswer :

QUD → JumpOutcome → Fin 3

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

Equations

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

Instances For

def Phenomena.Quantification.Studies.ScontrasPearl2021.EveryNot.qudProjectInline (q : QUD) (f : JumpOutcome → ℝ) (w : 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.

Instances For

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

0 ≤ qudProjectInline q f w

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

RSA.RSAConfig Utt 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.

Instances For

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.ScontrasPearl2021.EveryNot.baselineCfg :

RSA.RSAConfig Utt 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.

Instances For

@[reducible, inline]

noncomputable abbrev Phenomena.Quantification.Studies.ScontrasPearl2021.EveryNot.defaultCfg :

RSA.RSAConfig Utt 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.

Instances For

@[reducible, inline]

noncomputable abbrev Phenomena.Quantification.Studies.ScontrasPearl2021.EveryNot.highBaseCfg :

RSA.RSAConfig Utt 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.

Instances For

@[reducible, inline]

noncomputable abbrev Phenomena.Quantification.Studies.ScontrasPearl2021.EveryNot.supportiveCfg :

RSA.RSAConfig Utt JumpOutcome

Supportive context: b_suc = 0.9 + all?-biased QUD (1:18:1 ≈ 0.05:0.9:0.05). Models S&P's supportive-context prediction (§3.3, Figure 3), motivated by @cite{gualmini-etal-2008}'s finding that QUD manipulation increases endorsement. When both pragmatic factors are supportive, scope access has negligible impact on endorsement (paper: 0.91 at P(inv)=0.1 vs 0.91 at P(inv)=0.9).

Equations

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

Instances For

@[reducible, inline]

noncomputable abbrev Phenomena.Quantification.Studies.ScontrasPearl2021.EveryNot.surfaceOnlyCfg :

RSA.RSAConfig Utt 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.

Instances For

QUD manipulation: favored QUD gets P = 0.9, others get P = 0.05. Default world prior (b_suc = 0.5) and default scope prior (uniform). Paper: "we see an increase in utterance endorsement from the none? (0.38) to how-many? (0.48) to all? (0.63) QUD."

@[reducible, inline]

noncomputable abbrev Phenomena.Quantification.Studies.ScontrasPearl2021.EveryNot.noneBiasedCfg :

RSA.RSAConfig Utt JumpOutcome

None?-biased QUD: P(none?) ≈ 0.9, P(howMany?) = P(all?) ≈ 0.05. Figure 2, center panel, leftmost bar (S2 ≈ 0.38).

Equations

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

Instances For

@[reducible, inline]

noncomputable abbrev Phenomena.Quantification.Studies.ScontrasPearl2021.EveryNot.howManyBiasedCfg :

RSA.RSAConfig Utt JumpOutcome

How-many?-biased QUD: P(howMany?) ≈ 0.9, P(all?) = P(none?) ≈ 0.05. Figure 2, center panel, middle bar (S2 ≈ 0.48).

Equations

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

Instances For

@[reducible, inline]

noncomputable abbrev Phenomena.Quantification.Studies.ScontrasPearl2021.EveryNot.allBiasedCfg :

RSA.RSAConfig Utt JumpOutcome

All?-biased QUD: P(all?) ≈ 0.9, P(howMany?) = P(none?) ≈ 0.05. Figure 2, center panel, rightmost bar (S2 ≈ 0.63).

Equations

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

Instances For

S2 endorsement 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.ScontrasPearl2021.EveryNot.baseline_L1_w0_gt_w1 :

baselineCfg.L1 Utt.everyNot JumpOutcome.zero > baselineCfg.L1 Utt.everyNot 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.ScontrasPearl2021.EveryNot.baseline_L1_w1_gt_w2 :

baselineCfg.L1 Utt.everyNot JumpOutcome.one > baselineCfg.L1 Utt.everyNot JumpOutcome.two

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

theorem Phenomena.Quantification.Studies.ScontrasPearl2021.EveryNot.ambiguity_boosts_partial :

baselineCfg.L1 Utt.everyNot JumpOutcome.one > surfaceOnlyCfg.L1 Utt.everyNot 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.ScontrasPearl2021.EveryNot.baseline_S2_w0_gt_w1 :

baselineCfg.S2 JumpOutcome.zero Utt.everyNot > baselineCfg.S2 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.ScontrasPearl2021.EveryNot.baseline_S2_w1_gt_w2 :

baselineCfg.S2 JumpOutcome.one Utt.everyNot > baselineCfg.S2 JumpOutcome.two Utt.everyNot

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

theorem Phenomena.Quantification.Studies.ScontrasPearl2021.EveryNot.highBase_S2_w0_gt_w1 :

highBaseCfg.S2 JumpOutcome.zero Utt.everyNot > highBaseCfg.S2 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.ScontrasPearl2021.EveryNot.highBase_S2_w1_gt_w2 :

highBaseCfg.S2 JumpOutcome.one Utt.everyNot > highBaseCfg.S2 JumpOutcome.two Utt.everyNot

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

theorem Phenomena.Quantification.Studies.ScontrasPearl2021.EveryNot.default_S2_w0_gt_w1 :

defaultCfg.S2 JumpOutcome.zero Utt.everyNot > defaultCfg.S2 JumpOutcome.one Utt.everyNot

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

theorem Phenomena.Quantification.Studies.ScontrasPearl2021.EveryNot.default_S2_w1_gt_w2 :

defaultCfg.S2 JumpOutcome.one Utt.everyNot > defaultCfg.S2 JumpOutcome.two Utt.everyNot

theorem Phenomena.Quantification.Studies.ScontrasPearl2021.EveryNot.supportive_S2_w0_gt_w1 :

supportiveCfg.S2 JumpOutcome.zero Utt.everyNot > supportiveCfg.S2 JumpOutcome.one Utt.everyNot

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

theorem Phenomena.Quantification.Studies.ScontrasPearl2021.EveryNot.supportive_S2_w1_gt_w2 :

supportiveCfg.S2 JumpOutcome.one Utt.everyNot > supportiveCfg.S2 JumpOutcome.two Utt.everyNot

theorem Phenomena.Quantification.Studies.ScontrasPearl2021.EveryNot.qud_howMany_gt_none :

howManyBiasedCfg.S2 JumpOutcome.one Utt.everyNot > noneBiasedCfg.S2 JumpOutcome.one Utt.everyNot

QUD manipulation: how-many?-biased > none?-biased (Figure 2, center panel). Favoring the identity QUD yields higher endorsement than favoring the "did none succeed?" QUD, because how-many? makes the ambiguous utterance more informative at w=1 (partial success).

theorem Phenomena.Quantification.Studies.ScontrasPearl2021.EveryNot.qud_all_gt_howMany :

allBiasedCfg.S2 JumpOutcome.one Utt.everyNot > howManyBiasedCfg.S2 JumpOutcome.one Utt.everyNot

QUD manipulation: all?-biased > how-many?-biased (Figure 2, center panel). Favoring the "did all succeed?" QUD yields the highest endorsement because both scope interpretations fully resolve all? at w=1 (the answer is "no" under either reading).

inductive Phenomena.Quantification.Studies.ScontrasPearl2021.TwoNot.Utt :

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

null : Utt
twoNot : Utt

Instances For

instance Phenomena.Quantification.Studies.ScontrasPearl2021.TwoNot.instDecidableEqUtt :

DecidableEq Utt

Equations

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

instance Phenomena.Quantification.Studies.ScontrasPearl2021.TwoNot.instBEqUtt :

Equations

Phenomena.Quantification.Studies.ScontrasPearl2021.TwoNot.instBEqUtt = { beq := Phenomena.Quantification.Studies.ScontrasPearl2021.TwoNot.instBEqUtt.beq }

def Phenomena.Quantification.Studies.ScontrasPearl2021.TwoNot.instBEqUtt.beq :

Utt → Utt → Bool

Equations

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

Instances For

def Phenomena.Quantification.Studies.ScontrasPearl2021.TwoNot.instReprUtt.repr :

Utt → ℕ → Std.Format

Equations

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

Instances For

instance Phenomena.Quantification.Studies.ScontrasPearl2021.TwoNot.instReprUtt :

Equations

Phenomena.Quantification.Studies.ScontrasPearl2021.TwoNot.instReprUtt = { reprPrec := Phenomena.Quantification.Studies.ScontrasPearl2021.TwoNot.instReprUtt.repr }

def Phenomena.Quantification.Studies.ScontrasPearl2021.TwoNot.instInhabitedUtt.default :

Equations

Phenomena.Quantification.Studies.ScontrasPearl2021.TwoNot.instInhabitedUtt.default = Phenomena.Quantification.Studies.ScontrasPearl2021.TwoNot.Utt.null

Instances For

instance Phenomena.Quantification.Studies.ScontrasPearl2021.TwoNot.instInhabitedUtt :

Equations

Phenomena.Quantification.Studies.ScontrasPearl2021.TwoNot.instInhabitedUtt = { default := Phenomena.Quantification.Studies.ScontrasPearl2021.TwoNot.instInhabitedUtt.default }

instance Phenomena.Quantification.Studies.ScontrasPearl2021.TwoNot.instFintypeUtt :

Equations

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

inductive Phenomena.Quantification.Studies.ScontrasPearl2021.TwoNot.QUD5 :

QUDs for the two-not model (paper (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.ScontrasPearl2021.TwoNot.instDecidableEqQUD5 :

DecidableEq QUD5

Equations

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

instance Phenomena.Quantification.Studies.ScontrasPearl2021.TwoNot.instBEqQUD5 :

Equations

Phenomena.Quantification.Studies.ScontrasPearl2021.TwoNot.instBEqQUD5 = { beq := Phenomena.Quantification.Studies.ScontrasPearl2021.TwoNot.instBEqQUD5.beq }

def Phenomena.Quantification.Studies.ScontrasPearl2021.TwoNot.instBEqQUD5.beq :

QUD5 → QUD5 → Bool

Equations

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

Instances For

instance Phenomena.Quantification.Studies.ScontrasPearl2021.TwoNot.instReprQUD5 :

Equations

Phenomena.Quantification.Studies.ScontrasPearl2021.TwoNot.instReprQUD5 = { reprPrec := Phenomena.Quantification.Studies.ScontrasPearl2021.TwoNot.instReprQUD5.repr }

def Phenomena.Quantification.Studies.ScontrasPearl2021.TwoNot.instReprQUD5.repr :

QUD5 → ℕ → Std.Format

Equations

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

Instances For

def Phenomena.Quantification.Studies.ScontrasPearl2021.TwoNot.instInhabitedQUD5.default :

Equations

Phenomena.Quantification.Studies.ScontrasPearl2021.TwoNot.instInhabitedQUD5.default = Phenomena.Quantification.Studies.ScontrasPearl2021.TwoNot.QUD5.howMany

Instances For

instance Phenomena.Quantification.Studies.ScontrasPearl2021.TwoNot.instInhabitedQUD5 :

Equations

Phenomena.Quantification.Studies.ScontrasPearl2021.TwoNot.instInhabitedQUD5 = { default := Phenomena.Quantification.Studies.ScontrasPearl2021.TwoNot.instInhabitedQUD5.default }

instance Phenomena.Quantification.Studies.ScontrasPearl2021.TwoNot.instFintypeQUD5 :

Equations

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

inductive Phenomena.Quantification.Studies.ScontrasPearl2021.TwoNot.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.ScontrasPearl2021.TwoNot.instDecidableEqLatent10 :

DecidableEq Latent10

Equations

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

def Phenomena.Quantification.Studies.ScontrasPearl2021.TwoNot.instBEqLatent10.beq :

Latent10 → Latent10 → Bool

Equations

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

Instances For

instance Phenomena.Quantification.Studies.ScontrasPearl2021.TwoNot.instBEqLatent10 :

Equations

Phenomena.Quantification.Studies.ScontrasPearl2021.TwoNot.instBEqLatent10 = { beq := Phenomena.Quantification.Studies.ScontrasPearl2021.TwoNot.instBEqLatent10.beq }

def Phenomena.Quantification.Studies.ScontrasPearl2021.TwoNot.instReprLatent10.repr :

Latent10 → ℕ → Std.Format

Equations

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

Instances For

instance Phenomena.Quantification.Studies.ScontrasPearl2021.TwoNot.instReprLatent10 :

Equations

Phenomena.Quantification.Studies.ScontrasPearl2021.TwoNot.instReprLatent10 = { reprPrec := Phenomena.Quantification.Studies.ScontrasPearl2021.TwoNot.instReprLatent10.repr }

def Phenomena.Quantification.Studies.ScontrasPearl2021.TwoNot.instInhabitedLatent10.default :

Equations

Phenomena.Quantification.Studies.ScontrasPearl2021.TwoNot.instInhabitedLatent10.default = Phenomena.Quantification.Studies.ScontrasPearl2021.TwoNot.Latent10.surfHowMany

Instances For

instance Phenomena.Quantification.Studies.ScontrasPearl2021.TwoNot.instInhabitedLatent10 :

Inhabited Latent10

Equations

Phenomena.Quantification.Studies.ScontrasPearl2021.TwoNot.instInhabitedLatent10 = { default := Phenomena.Quantification.Studies.ScontrasPearl2021.TwoNot.instInhabitedLatent10.default }

instance Phenomena.Quantification.Studies.ScontrasPearl2021.TwoNot.instFintypeLatent10 :

Fintype Latent10

Equations

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

def Phenomena.Quantification.Studies.ScontrasPearl2021.TwoNot.Latent10.scope :

Latent10 → ScopeReading

Extract scope reading from latent variable.

Equations

Instances For

def Phenomena.Quantification.Studies.ScontrasPearl2021.TwoNot.Latent10.qud :

Latent10 → QUD5

Extract QUD from latent variable.

Equations

Instances For

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

ScopeReading → Utt → 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.ScontrasPearl2021.TwoNot.uttMeaning nr x✝¹ Phenomena.Quantification.Studies.ScontrasPearl2021.TwoNot.Utt.null x✝ = true

Instances For

theorem Phenomena.Quantification.Studies.ScontrasPearl2021.TwoNot.exact_truth_table :

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

Exact semantics truth table (paper (6), exact reading).

theorem Phenomena.Quantification.Studies.ScontrasPearl2021.TwoNot.atLeast_truth_table :

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

At-least semantics truth table (paper (6), at-least reading).

inductive Phenomena.Quantification.Studies.ScontrasPearl2021.TwoNot.Horse4 :

4-horse domain for grounding two-not truth conditions in numeral quantifier semantics.

h1 : Horse4
h2 : Horse4
h3 : Horse4
h4 : Horse4

Instances For

instance Phenomena.Quantification.Studies.ScontrasPearl2021.TwoNot.instDecidableEqHorse4 :

DecidableEq Horse4

Equations

Phenomena.Quantification.Studies.ScontrasPearl2021.TwoNot.instDecidableEqHorse4 x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Phenomena.Quantification.Studies.ScontrasPearl2021.TwoNot.instFintypeHorse4 :

Equations

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

def Phenomena.Quantification.Studies.ScontrasPearl2021.TwoNot.jumpIn4 :

JumpOutcome4 → Horse4 → Bool

Jump predicate for each world state (out of 4 horses). In partial worlds, the first k horses jumped.

Equations

Instances For

@[reducible, inline]

abbrev Phenomena.Quantification.Studies.ScontrasPearl2021.TwoNot.horseModel4 :

Semantics.Montague.Model

Horse4 model as a Montague Model.

Equations

Phenomena.Quantification.Studies.ScontrasPearl2021.TwoNot.horseModel4 = { Entity := Phenomena.Quantification.Studies.ScontrasPearl2021.TwoNot.Horse4, decEq := inferInstance }

Instances For

instance Phenomena.Quantification.Studies.ScontrasPearl2021.TwoNot.instFintypeEntityHorseModel4 :

Fintype horseModel4.Entity

Equations

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

def Phenomena.Quantification.Studies.ScontrasPearl2021.TwoNot.horse4_sem :

horseModel4.interpTy (Semantics.Montague.Ty.e ⇒ Semantics.Montague.Ty.t)

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

Equations

Phenomena.Quantification.Studies.ScontrasPearl2021.TwoNot.horse4_sem x✝ = true

Instances For

def Phenomena.Quantification.Studies.ScontrasPearl2021.TwoNot.jumpIn4_sem (w : JumpOutcome4) :

horseModel4.interpTy (Semantics.Montague.Ty.e ⇒ Semantics.Montague.Ty.t)

Jump predicate as Montague semantic value.

Equations

Phenomena.Quantification.Studies.ScontrasPearl2021.TwoNot.jumpIn4_sem w h = Phenomena.Quantification.Studies.ScontrasPearl2021.TwoNot.jumpIn4 w h

Instances For

def Phenomena.Quantification.Studies.ScontrasPearl2021.TwoNot.twoNotExact_surface (w : JumpOutcome4) :

Exact surface scope: ⟦exactly 2⟧(horse)(λx.¬jump(x))(w). "There are exactly two horses that didn't jump."

Equations

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

Instances For

def Phenomena.Quantification.Studies.ScontrasPearl2021.TwoNot.twoNotExact_inverse (w : JumpOutcome4) :

Exact inverse scope: ¬⟦exactly 2⟧(horse)(jump)(w). "It's not the case that exactly two horses jumped."

Equations

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

Instances For

theorem Phenomena.Quantification.Studies.ScontrasPearl2021.TwoNot.exact_surface_from_exactly_n_sem (w : JumpOutcome4) :

twoNotTruth NumeralReading.exact ScopeReading.surface w = twoNotExact_surface w

Exact surface grounding: twoNotTruth .exact .surface derives from compositional ⟦exactly 2⟧(horse)(λx.¬jump(x)), not stipulation.

theorem Phenomena.Quantification.Studies.ScontrasPearl2021.TwoNot.exact_inverse_from_exactly_n_sem (w : JumpOutcome4) :

twoNotTruth NumeralReading.exact ScopeReading.inverse w = twoNotExact_inverse w

Exact inverse grounding: twoNotTruth .exact .inverse derives from negating the compositional ⟦exactly 2⟧(horse)(jump).

def Phenomena.Quantification.Studies.ScontrasPearl2021.TwoNot.twoNotAtLeast_surface (w : JumpOutcome4) :

At-least surface scope: ⟦at least 2⟧(horse)(λx.¬jump(x))(w). "There are at least two horses that didn't jump."

Equations

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

Instances For

def Phenomena.Quantification.Studies.ScontrasPearl2021.TwoNot.twoNotAtLeast_inverse (w : JumpOutcome4) :

At-least inverse scope: ¬⟦at least 2⟧(horse)(jump)(w). "It's not the case that at least two horses jumped."

Equations

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

Instances For

theorem Phenomena.Quantification.Studies.ScontrasPearl2021.TwoNot.atLeast_surface_from_at_least_n_sem (w : JumpOutcome4) :

twoNotTruth NumeralReading.atLeast ScopeReading.surface w = twoNotAtLeast_surface w

At-least surface grounding: twoNotTruth .atLeast .surface derives from compositional ⟦at least 2⟧(horse)(λx.¬jump(x)).

theorem Phenomena.Quantification.Studies.ScontrasPearl2021.TwoNot.atLeast_inverse_from_at_least_n_sem (w : JumpOutcome4) :

twoNotTruth NumeralReading.atLeast ScopeReading.inverse w = twoNotAtLeast_inverse w

At-least inverse grounding: twoNotTruth .atLeast .inverse derives from negating the compositional ⟦at least 2⟧(horse)(jump).

theorem Phenomena.Quantification.Studies.ScontrasPearl2021.TwoNot.rsa_meaning_grounded (nr : NumeralReading) (s : ScopeReading) (w : JumpOutcome4) :

uttMeaning nr s Utt.twoNot w = match nr, s with | NumeralReading.exact, ScopeReading.surface => twoNotExact_surface w | NumeralReading.exact, ScopeReading.inverse => twoNotExact_inverse w | NumeralReading.atLeast, ScopeReading.surface => twoNotAtLeast_surface w | NumeralReading.atLeast, ScopeReading.inverse => twoNotAtLeast_inverse w

RSA meaning is grounded in compositional semantics: the meaning function used by the two-not RSA config matches the GQT numeral quantifiers.

theorem Phenomena.Quantification.Studies.ScontrasPearl2021.TwoNot.maxMeaning_agrees_gqt_exact_surface (w : JumpOutcome4) :

Semantics.Lexical.Numeral.maxMeaning Semantics.Lexical.Numeral.OrderingRel.eq 2 (4 - w.toNat) = twoNotExact_surface w

The two grounding layers agree: maxMeaning .eq (count-based) and exactly_n_sem (GQT compositional) produce the same truth values. Chains twoNotExact_surface_matches_maxMeaning with exact_surface_from_exactly_n_sem by transitivity.

theorem Phenomena.Quantification.Studies.ScontrasPearl2021.TwoNot.maxMeaning_agrees_gqt_exact_inverse (w : JumpOutcome4) :

(!decide (Semantics.Lexical.Numeral.maxMeaning Semantics.Lexical.Numeral.OrderingRel.eq 2 w.toNat = twoNotExact_inverse w)) = true

theorem Phenomena.Quantification.Studies.ScontrasPearl2021.TwoNot.maxMeaning_agrees_gqt_atLeast_surface (w : JumpOutcome4) :

Semantics.Lexical.Numeral.maxMeaning Semantics.Lexical.Numeral.OrderingRel.ge 2 (4 - w.toNat) = twoNotAtLeast_surface w

theorem Phenomena.Quantification.Studies.ScontrasPearl2021.TwoNot.maxMeaning_agrees_gqt_atLeast_inverse (w : JumpOutcome4) :

(!decide (Semantics.Lexical.Numeral.maxMeaning Semantics.Lexical.Numeral.OrderingRel.ge 2 w.toNat = twoNotAtLeast_inverse w)) = true

def Phenomena.Quantification.Studies.ScontrasPearl2021.TwoNot.readingToScopeConfig :

ScopeReading → Semantics.Scope.ScopeConfig

Map data file's ScopeReading to Montague ScopeConfig.

Equations

Instances For

def Phenomena.Quantification.Studies.ScontrasPearl2021.TwoNot.twoHorsesDidntJump_exact (w : JumpOutcome4) :

Semantics.Scope.ScopeDerivation horseModel4 Semantics.Montague.Ty.t

"Two horses didn't jump" as a ScopeDerivation under exact semantics: a single syntactic form with multiple semantic values indexed by scope.

Equations

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

Instances For

def Phenomena.Quantification.Studies.ScontrasPearl2021.TwoNot.twoHorsesDidntJump_atLeast (w : JumpOutcome4) :

Semantics.Scope.ScopeDerivation horseModel4 Semantics.Montague.Ty.t

"Two horses didn't jump" as a ScopeDerivation under at-least semantics.

Equations

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

Instances For

The exact two-not scope pair has INDEPENDENT readings: neither entails the other. This independence makes exact numerals diagnostic for the isomorphism effect — unlike universals, which have nested readings.

At-least two-not has NESTED readings: inverse (true at {w0,w1}) entails surface (true at {w0,w1,w2}). Like universals, at-least numerals are non-diagnostic for the isomorphism effect.

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

QUD projection for the 5-world domain (extends every-not QUDs; paper (7)). Explicit case analysis, kernel-reducible.

Equations

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

Instances For

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

0 ≤ qudProject q f w

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

RSA.RSAConfig Utt 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.ScontrasPearl2021.TwoNot.exactBaselineCfg :

RSA.RSAConfig Utt 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.ScontrasPearl2021.TwoNot.atleastBaselineCfg :

RSA.RSAConfig Utt 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

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.

The `rsa_predict` tactic handles the S2 computation via reflection,
building L0→S1→L1→S2 layers and comparing exact rational bounds.

theorem Phenomena.Quantification.Studies.ScontrasPearl2021.TwoNot.exact_baseline_endorsement_high :

exactBaselineCfg.S2 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.ScontrasPearl2021.TwoNot.atleast_baseline_endorsement_low :

1 / 2 > atleastBaselineCfg.S2 JumpOutcome4.w2 Utt.twoNot

Under at-least semantics with baseline parameters, S2 endorsement at w=2 is below 1/2 (Figure 7 left, red bar ≈ 0.1). Surface scope is true at {w0,w1,w2}, diluting informativity.

theorem Phenomena.Quantification.Studies.ScontrasPearl2021.TwoNot.exact_vs_atleast_endorsement :

exactBaselineCfg.S2 JumpOutcome4.w2 Utt.twoNot > atleastBaselineCfg.S2 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.ScontrasPearl2021.TwoNot.exact_surface_singleton :

(List.filter (uttMeaning NumeralReading.exact ScopeReading.surface Utt.twoNot) [JumpOutcome4.w0 , JumpOutcome4.w1 , JumpOutcome4.w2 , JumpOutcome4.w3 , 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.ScontrasPearl2021.TwoNot.exact_inverse_quad :

(List.filter (uttMeaning NumeralReading.exact ScopeReading.inverse Utt.twoNot) [JumpOutcome4.w0 , JumpOutcome4.w1 , JumpOutcome4.w2 , JumpOutcome4.w3 , 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.ScontrasPearl2021.TwoNot.atLeast_inverse_double :

(List.filter (uttMeaning NumeralReading.atLeast ScopeReading.inverse Utt.twoNot) [JumpOutcome4.w0 , JumpOutcome4.w1 , JumpOutcome4.w2 , JumpOutcome4.w3 , 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.

The paper's key argument: the SAME "baseline" parameters that produce low 1-of-2 endorsement also produce high 2-of-4 endorsement — but only under exact numeral semantics.

The models have different world types (JumpOutcome vs JumpOutcome4),
so we state this as two separate bounds that together establish the
1-of-2 vs 2-of-4 asymmetry:

- Every-not baseline: S2(everyNot|w=1) < 1/2 (low)
- Two-not exact baseline: S2(twoNot|w=2) > 1/2 (high)
- Two-not at-least baseline: S2(twoNot|w=2) < 1/2 (low)

The first two use "baseline" parameters (b_suc=0.1, P(inv)=0.1).
The asymmetry between the second and third is the argument for exact
semantics: changing only the numeral reading flips the prediction.

theorem Phenomena.Quantification.Studies.ScontrasPearl2021.everyNot_baseline_endorsement_low :

1 / 2 > EveryNot.baselineCfg.S2 JumpOutcome.one EveryNot.Utt.everyNot

Every-not baseline endorsement at w=1 is below 1/2. This is the low-endorsement end of the 1-of-2 vs 2-of-4 asymmetry. Uses the same b_suc=0.1 parameter that the TwoNot baseline uses.

Cross-model summary (proved above): - everyNot_baseline_endorsement_low: S2(everyNot|w=1) < 1/2 - TwoNot.exact_baseline_endorsement_high: S2(twoNot|w=2) > 1/2 - TwoNot.atleast_baseline_endorsement_low: S2(twoNot|w=2) < 1/2

Same parameters, different domain size, same model architecture.
The exact/at-least split is the only difference between high and low
endorsement in the 2-of-4 context.