Documentation

Linglib.Phenomena.Presupposition.Studies.QingGoodmanLassiter2016

@cite{qing-goodman-lassiter-2016} #

A rational speech-act model of projective content. CogSci 2016, pp. 1110–1115.

The listener jointly infers the world state and the common ground (context set) the speaker assumed. Under the right QUD, this derives presupposition projection without any special semantic mechanism.

The Model #

L0 (eq. 5): L0(Q(w) | u, C, Q) ∝ Σ_{w'∈C∩⟦u⟧} δ_{Q(w)=Q(w')} · P(w')
S1 (eq. 6): S(u|w,C,Q) ∝ P(u) · L0(Q(w) | u, C, Q)^α
L1 (eq. 7): L(w,C | u, Q) ∝ P(w) · P(C) · S(u | w, C, Q)

Domain: 13 utterances × 4 worlds × 9 context sets. α = 6.

Key Insight: QUD Projection and Context Set Inference #

Under QUD_now ("Does John smoke now?"), S1 scores depend on now(w) only — worlds with the same now value are indistinguishable (§8.1). This means presupposition projection CANNOT be observed at the world marginal level. Instead, projection surfaces in the context set posterior (L1_latent): L1 infers the speaker assumed a context set entailing past=T (§8.5).

Under QUD_max (identity QUD), the past-now degeneracy breaks and projection is visible directly at the world level (§8.4).

Context Set Simplification #

The paper uses 15 non-empty context sets (all 2^4 - 1 subsets of 4 worlds) with 5% noise added to eq. (8) to ensure nonzero priors. We model only the 9 context sets derivable from observations about past/now, since the remaining 6 (e.g., change = {(T,F),(F,T)}) receive only the noise prior (≥18× lower) and do not affect qualitative predictions.

Connection to @cite{scontras-tonhauser-2025} and @cite{warstadt-2022} #

All three papers implement the same mathematical structure with different domains (change-of-state verbs, factives, genus-species). The latent variable is called "context set" here and "private assumptions" in S&T, but the computation is identical. See ScontrasTonhauser2025.lean for the factive domain.

inductive Phenomena.Presupposition.Studies.QingGoodmanLassiter2016.WorldState :

World state: (past, now) where past = John smoked, now = John smokes. Flat inductive for tactic enumerability.

wTT : WorldState
wTF : WorldState
wFT : WorldState
wFF : WorldState

Instances For

instance Phenomena.Presupposition.Studies.QingGoodmanLassiter2016.instDecidableEqWorldState :

DecidableEq WorldState

Equations

Phenomena.Presupposition.Studies.QingGoodmanLassiter2016.instDecidableEqWorldState x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.Presupposition.Studies.QingGoodmanLassiter2016.instReprWorldState.repr :

WorldState → ℕ → Std.Format

Equations

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

Instances For

instance Phenomena.Presupposition.Studies.QingGoodmanLassiter2016.instReprWorldState :

Repr WorldState

Equations

Phenomena.Presupposition.Studies.QingGoodmanLassiter2016.instReprWorldState = { reprPrec := Phenomena.Presupposition.Studies.QingGoodmanLassiter2016.instReprWorldState.repr }

def Phenomena.Presupposition.Studies.QingGoodmanLassiter2016.instBEqWorldState.beq :

WorldState → WorldState → Bool

Equations

Phenomena.Presupposition.Studies.QingGoodmanLassiter2016.instBEqWorldState.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

instance Phenomena.Presupposition.Studies.QingGoodmanLassiter2016.instBEqWorldState :

Equations

Phenomena.Presupposition.Studies.QingGoodmanLassiter2016.instBEqWorldState = { beq := Phenomena.Presupposition.Studies.QingGoodmanLassiter2016.instBEqWorldState.beq }

instance Phenomena.Presupposition.Studies.QingGoodmanLassiter2016.instInhabitedWorldState :

Inhabited WorldState

Equations

Phenomena.Presupposition.Studies.QingGoodmanLassiter2016.instInhabitedWorldState = { default := Phenomena.Presupposition.Studies.QingGoodmanLassiter2016.instInhabitedWorldState.default }

def Phenomena.Presupposition.Studies.QingGoodmanLassiter2016.instInhabitedWorldState.default :

Equations

Phenomena.Presupposition.Studies.QingGoodmanLassiter2016.instInhabitedWorldState.default = Phenomena.Presupposition.Studies.QingGoodmanLassiter2016.WorldState.wTT

Instances For

instance Phenomena.Presupposition.Studies.QingGoodmanLassiter2016.instFintypeWorldState :

Fintype WorldState

Equations

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

inductive Phenomena.Presupposition.Studies.QingGoodmanLassiter2016.Utterance :

Utterances about John's smoking habits. 6 positive utterances from Table 1, their 6 negations, and silence.

smokes : Utterance
doesntSmoke : Utterance
smoked : Utterance
didntSmoke : Utterance
alwaysSmoked : Utterance
notAlwaysSmoked : Utterance
stoppedSmoking : Utterance
notStoppedSmoking : Utterance
startedSmoking : Utterance
notStartedSmoking : Utterance
neverSmoked : Utterance
notNeverSmoked : Utterance
silence : Utterance

Instances For

instance Phenomena.Presupposition.Studies.QingGoodmanLassiter2016.instDecidableEqUtterance :

DecidableEq Utterance

Equations

Phenomena.Presupposition.Studies.QingGoodmanLassiter2016.instDecidableEqUtterance x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Phenomena.Presupposition.Studies.QingGoodmanLassiter2016.instReprUtterance :

Equations

Phenomena.Presupposition.Studies.QingGoodmanLassiter2016.instReprUtterance = { reprPrec := Phenomena.Presupposition.Studies.QingGoodmanLassiter2016.instReprUtterance.repr }

def Phenomena.Presupposition.Studies.QingGoodmanLassiter2016.instReprUtterance.repr :

Utterance → ℕ → Std.Format

Equations

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

Instances For

def Phenomena.Presupposition.Studies.QingGoodmanLassiter2016.instBEqUtterance.beq :

Utterance → Utterance → Bool

Equations

Phenomena.Presupposition.Studies.QingGoodmanLassiter2016.instBEqUtterance.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

instance Phenomena.Presupposition.Studies.QingGoodmanLassiter2016.instBEqUtterance :

Equations

Phenomena.Presupposition.Studies.QingGoodmanLassiter2016.instBEqUtterance = { beq := Phenomena.Presupposition.Studies.QingGoodmanLassiter2016.instBEqUtterance.beq }

def Phenomena.Presupposition.Studies.QingGoodmanLassiter2016.instInhabitedUtterance.default :

Equations

Phenomena.Presupposition.Studies.QingGoodmanLassiter2016.instInhabitedUtterance.default = Phenomena.Presupposition.Studies.QingGoodmanLassiter2016.Utterance.smokes

Instances For

instance Phenomena.Presupposition.Studies.QingGoodmanLassiter2016.instInhabitedUtterance :

Inhabited Utterance

Equations

Phenomena.Presupposition.Studies.QingGoodmanLassiter2016.instInhabitedUtterance = { default := Phenomena.Presupposition.Studies.QingGoodmanLassiter2016.instInhabitedUtterance.default }

instance Phenomena.Presupposition.Studies.QingGoodmanLassiter2016.instFintypeUtterance :

Fintype Utterance

Equations

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

def Phenomena.Presupposition.Studies.QingGoodmanLassiter2016.literalMeaning :

Utterance → WorldState → Bool

Literal truth conditions from Table 1. Negation of u is U - ⟦u⟧.

The change-of-state utterances (stopped, started, always smoked) encode presupposition + assertion as a conjunction over two temporal projections of the world state. See bridge theorems below connecting these to the CoS theory in Theories.Semantics.Lexical.Verb.ChangeOfState.Theory.

Equations

Instances For

theorem Phenomena.Presupposition.Studies.QingGoodmanLassiter2016.stopped_matches_cessation (w : WorldState) :

literalMeaning Utterance.stoppedSmoking w = (Semantics.Lexical.Verb.ChangeOfState.priorStatePresup Semantics.Lexical.Verb.ChangeOfState.CoSType.cessation (fun (x : WorldState) => x.past) w && Semantics.Lexical.Verb.ChangeOfState.resultStateAssertion Semantics.Lexical.Verb.ChangeOfState.CoSType.cessation (fun (x : WorldState) => x.now) w)

"Stopped smoking" = cessation presupposition (past=T) ∧ cessation assertion (now=F).

The CoS theory operates on a single predicate P, but the QGL world model separates prior state (past) from current state (now). We use ·.past for the presupposition and ·.now for the assertion.

theorem Phenomena.Presupposition.Studies.QingGoodmanLassiter2016.started_matches_inception (w : WorldState) :

literalMeaning Utterance.startedSmoking w = (Semantics.Lexical.Verb.ChangeOfState.priorStatePresup Semantics.Lexical.Verb.ChangeOfState.CoSType.inception (fun (x : WorldState) => x.past) w && Semantics.Lexical.Verb.ChangeOfState.resultStateAssertion Semantics.Lexical.Verb.ChangeOfState.CoSType.inception (fun (x : WorldState) => x.now) w)

"Started smoking" = inception presupposition (past=F) ∧ inception assertion (now=T).

theorem Phenomena.Presupposition.Studies.QingGoodmanLassiter2016.always_matches_continuation (w : WorldState) :

literalMeaning Utterance.alwaysSmoked w = (Semantics.Lexical.Verb.ChangeOfState.priorStatePresup Semantics.Lexical.Verb.ChangeOfState.CoSType.continuation (fun (x : WorldState) => x.past) w && Semantics.Lexical.Verb.ChangeOfState.resultStateAssertion Semantics.Lexical.Verb.ChangeOfState.CoSType.continuation (fun (x : WorldState) => x.now) w)

"Always smoked" = continuation presupposition (past=T) ∧ continuation assertion (now=T).

inductive Phenomena.Presupposition.Studies.QingGoodmanLassiter2016.ContextSet :

Context sets: subsets of worlds representing common ground. These are the 9 context sets derivable from observations about past and now (eq. 8). The paper's full model uses 15 non-empty subsets with 5% noise; the omitted 6 (e.g., change = {(T,F),(F,T)}) have negligible prior.

pastTrue : ContextSet
pastFalse : ContextSet
nowTrue : ContextSet
nowFalse : ContextSet
pastTrueNowTrue : ContextSet
pastTrueNowFalse : ContextSet
pastFalseNowTrue : ContextSet
pastFalseNowFalse : ContextSet
universe : ContextSet

Instances For

instance Phenomena.Presupposition.Studies.QingGoodmanLassiter2016.instDecidableEqContextSet :

DecidableEq ContextSet

Equations

Phenomena.Presupposition.Studies.QingGoodmanLassiter2016.instDecidableEqContextSet x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Phenomena.Presupposition.Studies.QingGoodmanLassiter2016.instReprContextSet :

Repr ContextSet

Equations

Phenomena.Presupposition.Studies.QingGoodmanLassiter2016.instReprContextSet = { reprPrec := Phenomena.Presupposition.Studies.QingGoodmanLassiter2016.instReprContextSet.repr }

def Phenomena.Presupposition.Studies.QingGoodmanLassiter2016.instReprContextSet.repr :

ContextSet → ℕ → Std.Format

Equations

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

Instances For

def Phenomena.Presupposition.Studies.QingGoodmanLassiter2016.instBEqContextSet.beq :

ContextSet → ContextSet → Bool

Equations

Phenomena.Presupposition.Studies.QingGoodmanLassiter2016.instBEqContextSet.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

instance Phenomena.Presupposition.Studies.QingGoodmanLassiter2016.instBEqContextSet :

Equations

Phenomena.Presupposition.Studies.QingGoodmanLassiter2016.instBEqContextSet = { beq := Phenomena.Presupposition.Studies.QingGoodmanLassiter2016.instBEqContextSet.beq }

def Phenomena.Presupposition.Studies.QingGoodmanLassiter2016.instInhabitedContextSet.default :

Equations

Phenomena.Presupposition.Studies.QingGoodmanLassiter2016.instInhabitedContextSet.default = Phenomena.Presupposition.Studies.QingGoodmanLassiter2016.ContextSet.pastTrue

Instances For

instance Phenomena.Presupposition.Studies.QingGoodmanLassiter2016.instInhabitedContextSet :

Inhabited ContextSet

Equations

Phenomena.Presupposition.Studies.QingGoodmanLassiter2016.instInhabitedContextSet = { default := Phenomena.Presupposition.Studies.QingGoodmanLassiter2016.instInhabitedContextSet.default }

instance Phenomena.Presupposition.Studies.QingGoodmanLassiter2016.instFintypeContextSet :

Fintype ContextSet

Equations

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

def Phenomena.Presupposition.Studies.QingGoodmanLassiter2016.compatibleBool :

ContextSet → WorldState → Bool

World-context compatibility: w ∈ C.

Equations

Instances For

inductive Phenomena.Presupposition.Studies.QingGoodmanLassiter2016.QUD :

Questions under discussion.

now : QUD
max : QUD
past : QUD

Instances For

instance Phenomena.Presupposition.Studies.QingGoodmanLassiter2016.instDecidableEqQUD :

DecidableEq QUD

Equations

Phenomena.Presupposition.Studies.QingGoodmanLassiter2016.instDecidableEqQUD x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.Presupposition.Studies.QingGoodmanLassiter2016.instReprQUD.repr :

QUD → ℕ → Std.Format

Equations

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

Instances For

instance Phenomena.Presupposition.Studies.QingGoodmanLassiter2016.instReprQUD :

Equations

Phenomena.Presupposition.Studies.QingGoodmanLassiter2016.instReprQUD = { reprPrec := Phenomena.Presupposition.Studies.QingGoodmanLassiter2016.instReprQUD.repr }

def Phenomena.Presupposition.Studies.QingGoodmanLassiter2016.instBEqQUD.beq :

QUD → QUD → Bool

Equations

Phenomena.Presupposition.Studies.QingGoodmanLassiter2016.instBEqQUD.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

instance Phenomena.Presupposition.Studies.QingGoodmanLassiter2016.instBEqQUD :

Equations

Phenomena.Presupposition.Studies.QingGoodmanLassiter2016.instBEqQUD = { beq := Phenomena.Presupposition.Studies.QingGoodmanLassiter2016.instBEqQUD.beq }

instance Phenomena.Presupposition.Studies.QingGoodmanLassiter2016.instInhabitedQUD :

Equations

Phenomena.Presupposition.Studies.QingGoodmanLassiter2016.instInhabitedQUD = { default := Phenomena.Presupposition.Studies.QingGoodmanLassiter2016.instInhabitedQUD.default }

def Phenomena.Presupposition.Studies.QingGoodmanLassiter2016.instInhabitedQUD.default :

Equations

Phenomena.Presupposition.Studies.QingGoodmanLassiter2016.instInhabitedQUD.default = Phenomena.Presupposition.Studies.QingGoodmanLassiter2016.QUD.now

Instances For

instance Phenomena.Presupposition.Studies.QingGoodmanLassiter2016.instFintypeQUD :

Equations

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

def Phenomena.Presupposition.Studies.QingGoodmanLassiter2016.qudAggregate (qud : QUD) (f : WorldState → ℝ) (w : WorldState) :

QUD aggregation: sums L0 probabilities over the QUD equivalence class.

now: sums over worlds with same now value
max: identity (no aggregation)
past: sums over worlds with same past value

Equations

One or more equations did not get rendered due to their size.
Phenomena.Presupposition.Studies.QingGoodmanLassiter2016.qudAggregate Phenomena.Presupposition.Studies.QingGoodmanLassiter2016.QUD.max f w = f w

Instances For

theorem Phenomena.Presupposition.Studies.QingGoodmanLassiter2016.qudAggregate_nonneg {qud : QUD} {f : WorldState → ℝ} {w : WorldState} (hf : ∀ (w : WorldState), 0 ≤ f w) :

0 ≤ qudAggregate qud f w

def Phenomena.Presupposition.Studies.QingGoodmanLassiter2016.utterancePrior :

Utterance → ℚ

Utterance prior (eq. 1): Pr(u) ∝ 2^{-#content-words(u)}. Negation and auxiliaries excluded from count.

2 content words: stopped/started/always/never smoking → 1/4
1 content word: smokes/smoked → 1/2
0 content words: silence → 1

Equations

Instances For

theorem Phenomena.Presupposition.Studies.QingGoodmanLassiter2016.utterancePrior_nonneg (u : Utterance) :

0 ≤ utterancePrior u

def Phenomena.Presupposition.Studies.QingGoodmanLassiter2016.contextPrior :

ContextSet → ℚ

Context set prior (eq. 8): Pr(C) ∝ Σ_{CG⊆Obs} P(CG) · δ_{C=∩CG}. Each observation enters CG independently with probability 0.4. P(CG) = 0.4^|CG| × 0.6^(4-|CG|).

0 observations (universe): 0.6^4 ∝ 9
1 observation (single): 0.4 × 0.6^3 ∝ 6
2 observations (pair): 0.4^2 × 0.6^2 ∝ 4

Equations

Instances For

theorem Phenomena.Presupposition.Studies.QingGoodmanLassiter2016.contextPrior_pos (cs : ContextSet) :

0 < contextPrior cs

noncomputable def Phenomena.Presupposition.Studies.QingGoodmanLassiter2016.cfg (qud : QUD) :

RSA.RSAConfig Utterance WorldState

RSA model parameterized by QUD. The paper's final model uses QUD_now with CG prior.

L0: meaning = compatibility ∧ literal truth (eq. 5)
S1: utterancePrior × rpow(qudAggregate(L0), α) (eq. 6)
L1: worldPrior × contextPrior × S1 (eq. 7)

Equations

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

Instances For

@[reducible, inline]

noncomputable abbrev Phenomena.Presupposition.Studies.QingGoodmanLassiter2016.cfgNow :

RSA.RSAConfig Utterance WorldState

Final model: CG prior + QUD_now (paper's main prediction).

Equations

Phenomena.Presupposition.Studies.QingGoodmanLassiter2016.cfgNow = Phenomena.Presupposition.Studies.QingGoodmanLassiter2016.cfg Phenomena.Presupposition.Studies.QingGoodmanLassiter2016.QUD.now

Instances For

@[reducible, inline]

noncomputable abbrev Phenomena.Presupposition.Studies.QingGoodmanLassiter2016.cfgMax :

RSA.RSAConfig Utterance WorldState

Comparison model: CG prior + QUD_max.

Equations

Phenomena.Presupposition.Studies.QingGoodmanLassiter2016.cfgMax = Phenomena.Presupposition.Studies.QingGoodmanLassiter2016.cfg Phenomena.Presupposition.Studies.QingGoodmanLassiter2016.QUD.max

Instances For

@[reducible, inline]

noncomputable abbrev Phenomena.Presupposition.Studies.QingGoodmanLassiter2016.cfgPast :

RSA.RSAConfig Utterance WorldState

Comparison model: CG prior + QUD_past.

Equations

Phenomena.Presupposition.Studies.QingGoodmanLassiter2016.cfgPast = Phenomena.Presupposition.Studies.QingGoodmanLassiter2016.cfg Phenomena.Presupposition.Studies.QingGoodmanLassiter2016.QUD.past

Instances For

§8.1 QUD_now symmetry #

Under QUD_now, qudAggregate maps wTT and wFT to the same value (both have now=T), so S1(cs, wTT, u) = S1(cs, wFT, u) for all cs. With uniform worldPrior and w-independent latentPrior, L1(wTT) = L1(wFT). This means presupposition projection cannot be measured by world marginal under QUD_now — the past dimension is invisible to L1.

theorem Phenomena.Presupposition.Studies.QingGoodmanLassiter2016.qud_now_wTT_eq_wFT :

cfgNow.L1 Utterance.notStoppedSmoking WorldState.wTT = cfgNow.L1 Utterance.notStoppedSmoking WorldState.wFT

QUD_now symmetry: wTT and wFT are indistinguishable.

This is the structural reason why projection under QUD_now must be measured via context set inference (L1_latent), not world marginal.

§8.2 QUD answer #

After hearing "didn't stop smoking" with QUD = "Does John smoke now?", L1 correctly infers the QUD answer: John smokes (now=T).

theorem Phenomena.Presupposition.Studies.QingGoodmanLassiter2016.qud_answer_now_true :

(cfgNow.L1_marginal Utterance.notStoppedSmoking fun (x : WorldState) => x.now) > cfgNow.L1_marginal Utterance.notStoppedSmoking fun (w : WorldState) => !w.now

QUD answer inference: L1 infers now=T from "didn't stop smoking".

§8.3 World elimination #

Within worlds sharing the same past value, now=T dominates now=F. "Didn't stop smoking" is literally false at wTF (past=T, now=F is exactly "stopped smoking"), concentrating L1 mass on wTT.

theorem Phenomena.Presupposition.Studies.QingGoodmanLassiter2016.wTT_gt_wTF :

cfgNow.L1 Utterance.notStoppedSmoking WorldState.wTT > cfgNow.L1 Utterance.notStoppedSmoking WorldState.wTF

Now=T dominates now=F among past=T worlds.

§8.4 Projection under QUD_max (Figure 1c) #

Under the identity QUD, the past-now degeneracy of §8.1 breaks: S1 scores depend on all world dimensions, so L1 can distinguish wTT from wFT. The key asymmetry: under +past context, "didn't stop" narrows to exactly wTT (maximally informative for the speaker), while under -past context it spreads over both wFT and wFF (less informative). This makes wTT more likely than wFT.

The paper observes that (T,T) = (F,F) under QUD_max (Figure 1c), so projection is incomplete — the past=T marginal still equals the past=F marginal. Full projection requires QUD_now + context set inference (§8.5).

theorem Phenomena.Presupposition.Studies.QingGoodmanLassiter2016.projection_under_qud_max :

cfgMax.L1 Utterance.notStoppedSmoking WorldState.wTT > cfgMax.L1 Utterance.notStoppedSmoking WorldState.wFT

Projection under QUD_max: wTT > wFT.

theorem Phenomena.Presupposition.Studies.QingGoodmanLassiter2016.qud_max_incomplete_projection :

cfgMax.L1 Utterance.notStoppedSmoking WorldState.wTT = cfgMax.L1 Utterance.notStoppedSmoking WorldState.wFF

Incomplete projection under QUD_max: wTT = wFF (Figure 1c).

Under the identity QUD, (T,T) and (F,F) receive equal L1 probability. This means the past=T marginal equals the past=F marginal — projection is NOT captured at the world level under QUD_max.

§8.5 Context set projection (the paper's main result, Figure 3) #

The paper's headline result: after hearing "didn't stop smoking" under QUD_now, L1 infers the speaker assumed a +past context set (common ground where John smoked). This is presupposition projection: the presupposed content (past=T) enters the listener's beliefs about the common ground, even though the utterance literally says nothing about the past.

The mechanism: under +past context, "didn't stop" narrows L0 to exactly wTT, giving qudAggregate = 1 and rpow(1, 6) = 1 (maximally informative). Under -past context, L0 spreads over wFT and wFF, giving qudAggregate = 1/2 and rpow(1/2, 6) = 1/64 (weakly informative). Since S1 rewards informativity, the speaker is much more likely to use "didn't stop" when the +past context holds, and L1 infers this.

Figure 3 shows that (T,T) with context set +past is the unique maximum of the joint distribution under CG prior + QUD_now.

theorem Phenomena.Presupposition.Studies.QingGoodmanLassiter2016.context_projection :

cfgNow.L1_latent Utterance.notStoppedSmoking ContextSet.pastTrue > cfgNow.L1_latent Utterance.notStoppedSmoking ContextSet.pastFalse

Context set projection: L1 infers +past context over -past context.

theorem Phenomena.Presupposition.Studies.QingGoodmanLassiter2016.context_projection_over_universe :

cfgNow.L1_latent Utterance.notStoppedSmoking ContextSet.pastTrue > cfgNow.L1_latent Utterance.notStoppedSmoking ContextSet.universe

+past beats uninformative universe despite lower prior (9 vs 6).

Under +past, "didn't stop" narrows to exactly wTT (rpow(1,6) = 1). Under universe, it spreads over 3 worlds (rpow(1/4,6) ≈ 0). The informativity gain overwhelms the prior advantage.

theorem Phenomena.Presupposition.Studies.QingGoodmanLassiter2016.now_context_dispreferred :

cfgNow.L1_latent Utterance.notStoppedSmoking ContextSet.pastTrue > cfgNow.L1_latent Utterance.notStoppedSmoking ContextSet.nowFalse

-now context is dispreferred (p. 1114): -now already entails the QUD answer (John doesn't smoke now), so the speaker would be maximally informative even saying nothing — "didn't stop smoking" adds no value. L1 therefore infers the speaker did NOT assume a -now context.

§8.6 "Stopped smoking" projects past=T via QUD answer #

"Stopped smoking" is true only at wTF (past=T, now=F). Under QUD_now, L1 infers the QUD answer is now=F.

theorem Phenomena.Presupposition.Studies.QingGoodmanLassiter2016.stopped_qud_answer :

(cfgNow.L1_marginal Utterance.stoppedSmoking fun (w : WorldState) => !w.now) > cfgNow.L1_marginal Utterance.stoppedSmoking fun (x : WorldState) => x.now

"Stopped smoking" → L1 infers now=F (the assertion).

"didn't stop smoking" is compatible with 3 of 4 worlds.

Under context set +past, "didn't stop" is maximally informative for QUD_now: it narrows to exactly (T,T).

"stopped smoking" narrows to exactly (T,F): past=T and now=F.

"always smoked" = {(T,T)}, maximally informative for (T,T).

"never smoked" = {(F,F)}, maximally informative for (F,F).

def Phenomena.Presupposition.Studies.QingGoodmanLassiter2016.entailsPast :

ContextSet → Bool

Context sets that entail past=T (used for measuring projection).

Equations

Instances For

theorem Phenomena.Presupposition.Studies.QingGoodmanLassiter2016.three_entail_past :

{cs : ContextSet | entailsPast cs = true}.card = 3

3 of 9 context sets entail past=T.

Mathematical Equivalence with @cite{scontras-tonhauser-2025} and @cite{warstadt-2022} #

All three papers implement the same RSA computation:

L1(w, C | u, Q) ∝ S1(u | w, C, Q) · P(w) · P(C)

Paper	Latent	Interpretation	Domain
@cite{qing-goodman-lassiter-2016}	Context set C	Common ground	CoS verbs
@cite{scontras-tonhauser-2025}	Assumptions A	Speaker beliefs	Factives
@cite{warstadt-2022}	Context set C	Common ground	Genus-species

The RSAConfig encoding is structurally identical: Latent = context/belief state, meaning filters by compatibility, s1Score uses QUD-projected rpow. See ScontrasTonhauser2025.lean for the factive domain implementation.

@cite{scontras-tonhauser-2025} fn. 10: "@cite{qing-goodman-lassiter-2016} call these subsets the 'common ground,' but we think 'private assumptions' better captures this component of the model."

The terminological difference is interpretive, not computational.