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

@[implicit_reducible]

instance QingGoodmanLassiter2016.instDecidableEqWorldState :

DecidableEq WorldState

Equations

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

def QingGoodmanLassiter2016.instReprWorldState.repr :

WorldState → ℕ → Std.Format

Equations

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

Instances For

@[implicit_reducible]

instance QingGoodmanLassiter2016.instReprWorldState :

Repr WorldState

Equations

QingGoodmanLassiter2016.instReprWorldState = { reprPrec := QingGoodmanLassiter2016.instReprWorldState.repr }

def QingGoodmanLassiter2016.instInhabitedWorldState.default :

Equations

QingGoodmanLassiter2016.instInhabitedWorldState.default = QingGoodmanLassiter2016.WorldState.wTT

Instances For

@[implicit_reducible]

instance QingGoodmanLassiter2016.instInhabitedWorldState :

Inhabited WorldState

Equations

QingGoodmanLassiter2016.instInhabitedWorldState = { default := QingGoodmanLassiter2016.instInhabitedWorldState.default }

@[implicit_reducible]

instance QingGoodmanLassiter2016.instFintypeWorldState :

Fintype WorldState

Equations

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

def QingGoodmanLassiter2016.WorldState.past :

WorldState → Bool

Equations

QingGoodmanLassiter2016.WorldState.wTT.past = true
QingGoodmanLassiter2016.WorldState.wTF.past = true
QingGoodmanLassiter2016.WorldState.wFT.past = false
QingGoodmanLassiter2016.WorldState.wFF.past = false

Instances For

def QingGoodmanLassiter2016.WorldState.now :

WorldState → Bool

Equations

QingGoodmanLassiter2016.WorldState.wTT.now = true
QingGoodmanLassiter2016.WorldState.wFT.now = true
QingGoodmanLassiter2016.WorldState.wTF.now = false
QingGoodmanLassiter2016.WorldState.wFF.now = false

Instances For

inductive 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

@[implicit_reducible]

instance QingGoodmanLassiter2016.instDecidableEqUtterance :

DecidableEq Utterance

Equations

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

def QingGoodmanLassiter2016.instReprUtterance.repr :

Utterance → ℕ → Std.Format

Equations

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

Instances For

@[implicit_reducible]

instance QingGoodmanLassiter2016.instReprUtterance :

Equations

QingGoodmanLassiter2016.instReprUtterance = { reprPrec := QingGoodmanLassiter2016.instReprUtterance.repr }

@[implicit_reducible]

instance QingGoodmanLassiter2016.instInhabitedUtterance :

Inhabited Utterance

Equations

QingGoodmanLassiter2016.instInhabitedUtterance = { default := QingGoodmanLassiter2016.instInhabitedUtterance.default }

def QingGoodmanLassiter2016.instInhabitedUtterance.default :

Equations

QingGoodmanLassiter2016.instInhabitedUtterance.default = QingGoodmanLassiter2016.Utterance.smokes

Instances For

@[implicit_reducible]

instance QingGoodmanLassiter2016.instFintypeUtterance :

Fintype Utterance

Equations

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

def 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.Aspect.ChangeOfState.

Equations

QingGoodmanLassiter2016.literalMeaning QingGoodmanLassiter2016.Utterance.smokes x✝ = x✝.now
QingGoodmanLassiter2016.literalMeaning QingGoodmanLassiter2016.Utterance.doesntSmoke x✝ = !x✝.now
QingGoodmanLassiter2016.literalMeaning QingGoodmanLassiter2016.Utterance.smoked x✝ = x✝.past
QingGoodmanLassiter2016.literalMeaning QingGoodmanLassiter2016.Utterance.didntSmoke x✝ = !x✝.past
QingGoodmanLassiter2016.literalMeaning QingGoodmanLassiter2016.Utterance.alwaysSmoked x✝ = (x✝.past && x✝.now)
QingGoodmanLassiter2016.literalMeaning QingGoodmanLassiter2016.Utterance.notAlwaysSmoked x✝ = !(x✝.past && x✝.now)
QingGoodmanLassiter2016.literalMeaning QingGoodmanLassiter2016.Utterance.stoppedSmoking x✝ = (x✝.past && !x✝.now)
QingGoodmanLassiter2016.literalMeaning QingGoodmanLassiter2016.Utterance.notStoppedSmoking x✝ = !(x✝.past && !x✝.now)
QingGoodmanLassiter2016.literalMeaning QingGoodmanLassiter2016.Utterance.startedSmoking x✝ = (!x✝.past && x✝.now)
QingGoodmanLassiter2016.literalMeaning QingGoodmanLassiter2016.Utterance.notStartedSmoking x✝ = !(!x✝.past && x✝.now)
QingGoodmanLassiter2016.literalMeaning QingGoodmanLassiter2016.Utterance.neverSmoked x✝ = (!x✝.past && !x✝.now)
QingGoodmanLassiter2016.literalMeaning QingGoodmanLassiter2016.Utterance.notNeverSmoked x✝ = !(!x✝.past && !x✝.now)
QingGoodmanLassiter2016.literalMeaning QingGoodmanLassiter2016.Utterance.silence x✝ = true

Instances For

theorem QingGoodmanLassiter2016.stopped_matches_cessation (w : WorldState) :

literalMeaning Utterance.stoppedSmoking w = true ↔ Features.ChangeOfState.priorStatePresup Features.ChangeOfState.CoSType.cessation (fun (w : WorldState) => w.past = true) w ∧ Features.ChangeOfState.resultStateAssertion Features.ChangeOfState.CoSType.cessation (fun (w : WorldState) => w.now = true) 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 QingGoodmanLassiter2016.started_matches_inception (w : WorldState) :

literalMeaning Utterance.startedSmoking w = true ↔ Features.ChangeOfState.priorStatePresup Features.ChangeOfState.CoSType.inception (fun (w : WorldState) => w.past = true) w ∧ Features.ChangeOfState.resultStateAssertion Features.ChangeOfState.CoSType.inception (fun (w : WorldState) => w.now = true) w

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

theorem QingGoodmanLassiter2016.always_matches_continuation (w : WorldState) :

literalMeaning Utterance.alwaysSmoked w = true ↔ Features.ChangeOfState.priorStatePresup Features.ChangeOfState.CoSType.continuation (fun (w : WorldState) => w.past = true) w ∧ Features.ChangeOfState.resultStateAssertion Features.ChangeOfState.CoSType.continuation (fun (w : WorldState) => w.now = true) w

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

inductive 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

@[implicit_reducible]

instance QingGoodmanLassiter2016.instDecidableEqContextSet :

DecidableEq ContextSet

Equations

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

@[implicit_reducible]

instance QingGoodmanLassiter2016.instReprContextSet :

Repr ContextSet

Equations

QingGoodmanLassiter2016.instReprContextSet = { reprPrec := QingGoodmanLassiter2016.instReprContextSet.repr }

def QingGoodmanLassiter2016.instReprContextSet.repr :

ContextSet → ℕ → Std.Format

Equations

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

Instances For

@[implicit_reducible]

instance QingGoodmanLassiter2016.instInhabitedContextSet :

Inhabited ContextSet

Equations

QingGoodmanLassiter2016.instInhabitedContextSet = { default := QingGoodmanLassiter2016.instInhabitedContextSet.default }

def QingGoodmanLassiter2016.instInhabitedContextSet.default :

Equations

QingGoodmanLassiter2016.instInhabitedContextSet.default = QingGoodmanLassiter2016.ContextSet.pastTrue

Instances For

@[implicit_reducible]

instance QingGoodmanLassiter2016.instFintypeContextSet :

Fintype ContextSet

Equations

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

def QingGoodmanLassiter2016.compatibleBool :

ContextSet → WorldState → Bool

World-context compatibility: w ∈ C.

Equations

QingGoodmanLassiter2016.compatibleBool QingGoodmanLassiter2016.ContextSet.pastTrue x✝ = x✝.past
QingGoodmanLassiter2016.compatibleBool QingGoodmanLassiter2016.ContextSet.pastFalse x✝ = !x✝.past
QingGoodmanLassiter2016.compatibleBool QingGoodmanLassiter2016.ContextSet.nowTrue x✝ = x✝.now
QingGoodmanLassiter2016.compatibleBool QingGoodmanLassiter2016.ContextSet.nowFalse x✝ = !x✝.now
QingGoodmanLassiter2016.compatibleBool QingGoodmanLassiter2016.ContextSet.pastTrueNowTrue x✝ = (x✝.past && x✝.now)
QingGoodmanLassiter2016.compatibleBool QingGoodmanLassiter2016.ContextSet.pastTrueNowFalse x✝ = (x✝.past && !x✝.now)
QingGoodmanLassiter2016.compatibleBool QingGoodmanLassiter2016.ContextSet.pastFalseNowTrue x✝ = (!x✝.past && x✝.now)
QingGoodmanLassiter2016.compatibleBool QingGoodmanLassiter2016.ContextSet.pastFalseNowFalse x✝ = (!x✝.past && !x✝.now)
QingGoodmanLassiter2016.compatibleBool QingGoodmanLassiter2016.ContextSet.universe x✝ = true

Instances For

inductive QingGoodmanLassiter2016.QUD :

Questions under discussion.

now : QUD
max : QUD
past : QUD

Instances For

@[implicit_reducible]

instance QingGoodmanLassiter2016.instDecidableEqQUD :

DecidableEq QUD

Equations

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

@[implicit_reducible]

instance QingGoodmanLassiter2016.instReprQUD :

Repr QUD

Equations

QingGoodmanLassiter2016.instReprQUD = { reprPrec := QingGoodmanLassiter2016.instReprQUD.repr }

def QingGoodmanLassiter2016.instReprQUD.repr :

QUD → ℕ → Std.Format

Equations

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

Instances For

@[implicit_reducible]

instance QingGoodmanLassiter2016.instInhabitedQUD :

Inhabited QUD

Equations

QingGoodmanLassiter2016.instInhabitedQUD = { default := QingGoodmanLassiter2016.instInhabitedQUD.default }

def QingGoodmanLassiter2016.instInhabitedQUD.default :

Equations

QingGoodmanLassiter2016.instInhabitedQUD.default = QingGoodmanLassiter2016.QUD.now

Instances For

@[implicit_reducible]

instance QingGoodmanLassiter2016.instFintypeQUD :

Fintype QUD

Equations

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

def 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

Instances For

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

0 ≤ qudAggregate qud f w

def 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 QingGoodmanLassiter2016.utterancePrior_nonneg (u : Utterance) :

0 ≤ utterancePrior u

def 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 QingGoodmanLassiter2016.contextPrior_pos (cs : ContextSet) :

0 < contextPrior cs

noncomputable def 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 QingGoodmanLassiter2016.cfgNow :

RSA.RSAConfig Utterance WorldState

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

Equations

QingGoodmanLassiter2016.cfgNow = QingGoodmanLassiter2016.cfg QingGoodmanLassiter2016.QUD.now

Instances For

@[reducible, inline]

noncomputable abbrev QingGoodmanLassiter2016.cfgMax :

RSA.RSAConfig Utterance WorldState

Comparison model: CG prior + QUD_max.

Equations

QingGoodmanLassiter2016.cfgMax = QingGoodmanLassiter2016.cfg QingGoodmanLassiter2016.QUD.max

Instances For

@[reducible, inline]

noncomputable abbrev QingGoodmanLassiter2016.cfgPast :

RSA.RSAConfig Utterance WorldState

Comparison model: CG prior + QUD_past.

Equations

QingGoodmanLassiter2016.cfgPast = QingGoodmanLassiter2016.cfg 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 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 QingGoodmanLassiter2016.qud_answer_now_true :

(cfgNow.L1_marginal Utterance.notStoppedSmoking fun (w : WorldState) => w.now = true) > cfgNow.L1_marginal Utterance.notStoppedSmoking fun (w : WorldState) => w.now = false

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 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 QingGoodmanLassiter2016.projection_under_qud_max :

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

Projection under QUD_max: wTT > wFT.

theorem 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 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 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 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 QingGoodmanLassiter2016.stopped_qud_answer :

(cfgNow.L1_marginal Utterance.stoppedSmoking fun (w : WorldState) => w.now = false) > cfgNow.L1_marginal Utterance.stoppedSmoking fun (w : WorldState) => w.now = true

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

theorem QingGoodmanLassiter2016.notStopped_compatible_worlds :

literalMeaning Utterance.notStoppedSmoking WorldState.wTT = true ∧ literalMeaning Utterance.notStoppedSmoking WorldState.wTF = false ∧ literalMeaning Utterance.notStoppedSmoking WorldState.wFT = true ∧ literalMeaning Utterance.notStoppedSmoking WorldState.wFF = true

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

theorem QingGoodmanLassiter2016.stopped_world :

literalMeaning Utterance.stoppedSmoking WorldState.wTT = false ∧ literalMeaning Utterance.stoppedSmoking WorldState.wTF = true ∧ literalMeaning Utterance.stoppedSmoking WorldState.wFT = false ∧ literalMeaning Utterance.stoppedSmoking WorldState.wFF = false

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

theorem QingGoodmanLassiter2016.alwaysSmoked_world :

literalMeaning Utterance.alwaysSmoked WorldState.wTT = true ∧ literalMeaning Utterance.alwaysSmoked WorldState.wTF = false ∧ literalMeaning Utterance.alwaysSmoked WorldState.wFT = false ∧ literalMeaning Utterance.alwaysSmoked WorldState.wFF = false

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

theorem QingGoodmanLassiter2016.neverSmoked_world :

literalMeaning Utterance.neverSmoked WorldState.wTT = false ∧ literalMeaning Utterance.neverSmoked WorldState.wTF = false ∧ literalMeaning Utterance.neverSmoked WorldState.wFT = false ∧ literalMeaning Utterance.neverSmoked WorldState.wFF = true

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

def QingGoodmanLassiter2016.entailsPast :

ContextSet → Bool

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

Equations

Instances For

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