[QGL16]: an RSA model of projective content

The listener jointly infers the world state and the context set the speaker assumed (CogSci 2016, pp. 1110–1115). Under the right QUD this derives presupposition projection with no special semantic mechanism: L0 answers the QUD within the context set (eq. 5), S1 scores QUD-projected informativity (eq. 6, α = 6), and L1 inverts jointly over worlds and context sets (eq. 7). Domain: 13 utterances × 4 worlds × 9 context sets.

Main results

• qud_now_wTT_eq_wFT: under QUD_now the world marginal cannot show projection — the now-cell aggregation is definitionally symmetric.
• context_projection: the paper's headline — after "didn't stop smoking", L1 infers a +past context set over −past (and over universe, context_projection_over_universe, despite its higher prior).
• projection_under_qud_max / qud_max_incomplete_projection: under the identity QUD projection is visible at the world level but incomplete (wTT = wFF, Figure 1c).
• qud_answer_now_true / stopped_qud_answer: L1 recovers the QUD answer.

Implementation notes

α = 6 is a natural power, so the chain is exact ℚ≥0: the speaker is RSA.Score.s1 over the QUD-aggregated literal listener (dead cells fall back to silence — one fallback declaration covers both faces), listeners are PMF.ofScores of the prior-weighted speaker mass, and each prediction closes by the ofScores comparison family with one kernel certificate.

The paper uses 15 context sets with 5% noise; we model the 9 derivable from past/now observations — the omitted 6 carry only the noise prior (≥ 18× lower) and do not affect the qualitative predictions.

TODO

Prove the structural equivalence with [ST25] (factives; latent = "private assumptions", their fn. 10: the difference from QGL's "common ground" is interpretive, not computational) and [War22] (genus-species) — all three compute L1(w, C | u, Q) ∝ S1(u | w, C, Q) · P(w) · P(C) over different domains. Blocked on ScontrasTonhauser2025.lean reaching the PMF face.

World states

inductive QingGoodmanLassiter2016.WorldState : Type

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

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

@[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.

@[implicit_reducible]

instance QingGoodmanLassiter2016.instReprWorldState : Repr WorldState

Equations

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

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

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

Utterances (Table 1, negations, silence)

inductive QingGoodmanLassiter2016.Assertion : Type

Content utterances about John's smoking habits: 6 positive utterances from Table 1 and their 6 negations.

• smokes : Assertion
• doesntSmoke : Assertion
• smoked : Assertion
• didntSmoke : Assertion
• always : Assertion
• notAlways : Assertion
• stopped : Assertion
• notStopped : Assertion
• started : Assertion
• notStarted : Assertion
• never : Assertion
• notNever : Assertion

@[implicit_reducible]

instance QingGoodmanLassiter2016.instDecidableEqAssertion : DecidableEq Assertion

Equations

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

@[implicit_reducible]

instance QingGoodmanLassiter2016.instReprAssertion : Repr Assertion

Equations

• QingGoodmanLassiter2016.instReprAssertion = { reprPrec := QingGoodmanLassiter2016.instReprAssertion.repr }

def QingGoodmanLassiter2016.instReprAssertion.repr : Assertion → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance QingGoodmanLassiter2016.instInhabitedAssertion : Inhabited Assertion

Equations

• QingGoodmanLassiter2016.instInhabitedAssertion = { default := QingGoodmanLassiter2016.instInhabitedAssertion.default }

@[implicit_reducible]

instance QingGoodmanLassiter2016.instFintypeAssertion : Fintype Assertion

Equations

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

@[reducible, inline]

abbrev QingGoodmanLassiter2016.Utterance : Type

Utterances with the null alternative: none is silence, some a a content assertion from Table 1.

Equations

• QingGoodmanLassiter2016.Utterance = RSA.WithSilence QingGoodmanLassiter2016.Assertion

Literal semantics

def QingGoodmanLassiter2016.assertionMeaning : Assertion → WorldState → Bool

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

The change-of-state utterances evaluate the corresponding Features.ChangeOfState.CoSType at the world's temporal projections — presupposition and assertion by construction (Features.ChangeOfState.CoSType.eval_iff), not by bridge theorem.

Equations

• QingGoodmanLassiter2016.assertionMeaning QingGoodmanLassiter2016.Assertion.smokes x✝ = x✝.now
• QingGoodmanLassiter2016.assertionMeaning QingGoodmanLassiter2016.Assertion.doesntSmoke x✝ = !x✝.now
• QingGoodmanLassiter2016.assertionMeaning QingGoodmanLassiter2016.Assertion.smoked x✝ = x✝.past
• QingGoodmanLassiter2016.assertionMeaning QingGoodmanLassiter2016.Assertion.didntSmoke x✝ = !x✝.past
• QingGoodmanLassiter2016.assertionMeaning QingGoodmanLassiter2016.Assertion.always x✝ = Features.ChangeOfState.CoSType.continuation.eval x✝.past x✝.now
• QingGoodmanLassiter2016.assertionMeaning QingGoodmanLassiter2016.Assertion.notAlways x✝ = !Features.ChangeOfState.CoSType.continuation.eval x✝.past x✝.now
• QingGoodmanLassiter2016.assertionMeaning QingGoodmanLassiter2016.Assertion.stopped x✝ = Features.ChangeOfState.CoSType.cessation.eval x✝.past x✝.now
• QingGoodmanLassiter2016.assertionMeaning QingGoodmanLassiter2016.Assertion.notStopped x✝ = !Features.ChangeOfState.CoSType.cessation.eval x✝.past x✝.now
• QingGoodmanLassiter2016.assertionMeaning QingGoodmanLassiter2016.Assertion.started x✝ = Features.ChangeOfState.CoSType.inception.eval x✝.past x✝.now
• QingGoodmanLassiter2016.assertionMeaning QingGoodmanLassiter2016.Assertion.notStarted x✝ = !Features.ChangeOfState.CoSType.inception.eval x✝.past x✝.now
• QingGoodmanLassiter2016.assertionMeaning QingGoodmanLassiter2016.Assertion.never x✝ = (!x✝.past && !x✝.now)
• QingGoodmanLassiter2016.assertionMeaning QingGoodmanLassiter2016.Assertion.notNever x✝ = !(!x✝.past && !x✝.now)

def QingGoodmanLassiter2016.literalMeaning : Utterance → WorldState → Bool

Literal truth conditions lifted to Utterance: silence is universally true (RSA.liftMeaning).

Equations

• QingGoodmanLassiter2016.literalMeaning = RSA.liftMeaning QingGoodmanLassiter2016.assertionMeaning

Context sets

inductive QingGoodmanLassiter2016.ContextSet : Type

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

@[implicit_reducible]

instance QingGoodmanLassiter2016.instDecidableEqContextSet : DecidableEq ContextSet

Equations

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

def QingGoodmanLassiter2016.instReprContextSet.repr : ContextSet → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance QingGoodmanLassiter2016.instReprContextSet : Repr ContextSet

Equations

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

@[implicit_reducible]

instance QingGoodmanLassiter2016.instInhabitedContextSet : Inhabited ContextSet

Equations

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

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

QUD

inductive QingGoodmanLassiter2016.QUD : Type

Questions under discussion.

• now : QUD
• max : QUD
• past : QUD

@[implicit_reducible]

instance QingGoodmanLassiter2016.instDecidableEqQUD : DecidableEq QUD

Equations

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

def QingGoodmanLassiter2016.instReprQUD.repr : QUD → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance QingGoodmanLassiter2016.instReprQUD : Repr QUD

Equations

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

@[implicit_reducible]

instance QingGoodmanLassiter2016.instInhabitedQUD : Inhabited QUD

Equations

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

@[implicit_reducible]

instance QingGoodmanLassiter2016.instFintypeQUD : Fintype QUD

Equations

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

Priors

def QingGoodmanLassiter2016.utterancePrior : Utterance → ℚ≥0

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

• QingGoodmanLassiter2016.utterancePrior (some QingGoodmanLassiter2016.Assertion.smokes) = 1 / 2
• QingGoodmanLassiter2016.utterancePrior (some QingGoodmanLassiter2016.Assertion.doesntSmoke) = 1 / 2
• QingGoodmanLassiter2016.utterancePrior (some QingGoodmanLassiter2016.Assertion.smoked) = 1 / 2
• QingGoodmanLassiter2016.utterancePrior (some QingGoodmanLassiter2016.Assertion.didntSmoke) = 1 / 2
• QingGoodmanLassiter2016.utterancePrior (some QingGoodmanLassiter2016.Assertion.always) = 1 / 4
• QingGoodmanLassiter2016.utterancePrior (some QingGoodmanLassiter2016.Assertion.notAlways) = 1 / 4
• QingGoodmanLassiter2016.utterancePrior (some QingGoodmanLassiter2016.Assertion.stopped) = 1 / 4
• QingGoodmanLassiter2016.utterancePrior (some QingGoodmanLassiter2016.Assertion.notStopped) = 1 / 4
• QingGoodmanLassiter2016.utterancePrior (some QingGoodmanLassiter2016.Assertion.started) = 1 / 4
• QingGoodmanLassiter2016.utterancePrior (some QingGoodmanLassiter2016.Assertion.notStarted) = 1 / 4
• QingGoodmanLassiter2016.utterancePrior (some QingGoodmanLassiter2016.Assertion.never) = 1 / 4
• QingGoodmanLassiter2016.utterancePrior (some QingGoodmanLassiter2016.Assertion.notNever) = 1 / 4
• QingGoodmanLassiter2016.utterancePrior none = 1

def QingGoodmanLassiter2016.contextPrior : ContextSet → ℚ≥0

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

• QingGoodmanLassiter2016.contextPrior QingGoodmanLassiter2016.ContextSet.universe = 9
• QingGoodmanLassiter2016.contextPrior QingGoodmanLassiter2016.ContextSet.pastTrue = 6
• QingGoodmanLassiter2016.contextPrior QingGoodmanLassiter2016.ContextSet.pastFalse = 6
• QingGoodmanLassiter2016.contextPrior QingGoodmanLassiter2016.ContextSet.nowTrue = 6
• QingGoodmanLassiter2016.contextPrior QingGoodmanLassiter2016.ContextSet.nowFalse = 6
• QingGoodmanLassiter2016.contextPrior QingGoodmanLassiter2016.ContextSet.pastTrueNowTrue = 4
• QingGoodmanLassiter2016.contextPrior QingGoodmanLassiter2016.ContextSet.pastTrueNowFalse = 4
• QingGoodmanLassiter2016.contextPrior QingGoodmanLassiter2016.ContextSet.pastFalseNowTrue = 4
• QingGoodmanLassiter2016.contextPrior QingGoodmanLassiter2016.ContextSet.pastFalseNowFalse = 4

The score chain

def QingGoodmanLassiter2016.l0Score (cs : ContextSet) (u : Utterance) : WorldState → ℚ≥0

Literal listener within the context set (eq. 5; the uniform world prior cancels, and empty extensions normalize to the zero row).

Equations

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

def QingGoodmanLassiter2016.qAgg (qud : QUD) (cs : ContextSet) (u : Utterance) : WorldState → ℚ≥0

QUD aggregation of the literal listener (eq. 5): sum over the QUD cell.

Equations

• One or more equations did not get rendered due to their size.
• QingGoodmanLassiter2016.qAgg QingGoodmanLassiter2016.QUD.max cs u QingGoodmanLassiter2016.WorldState.wTT = QingGoodmanLassiter2016.l0Score cs u QingGoodmanLassiter2016.WorldState.wTT
• QingGoodmanLassiter2016.qAgg QingGoodmanLassiter2016.QUD.max cs u QingGoodmanLassiter2016.WorldState.wTF = QingGoodmanLassiter2016.l0Score cs u QingGoodmanLassiter2016.WorldState.wTF
• QingGoodmanLassiter2016.qAgg QingGoodmanLassiter2016.QUD.max cs u QingGoodmanLassiter2016.WorldState.wFT = QingGoodmanLassiter2016.l0Score cs u QingGoodmanLassiter2016.WorldState.wFT
• QingGoodmanLassiter2016.qAgg QingGoodmanLassiter2016.QUD.max cs u QingGoodmanLassiter2016.WorldState.wFF = QingGoodmanLassiter2016.l0Score cs u QingGoodmanLassiter2016.WorldState.wFF

def QingGoodmanLassiter2016.s1Post (qud : QUD) (cs : ContextSet) : WorldState → Utterance → ℚ≥0

Speaker (eq. 6 at α = 6): RSA.Score.s1 over the QUD-aggregated literal listener with the utterance prior as multiplicative cost; dead cells fall back to silence.

Equations

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

def QingGoodmanLassiter2016.worldScore (qud : QUD) (u : Utterance) (w : WorldState) : ℚ≥0

Listener world score (eq. 7, world side): context-prior-weighted speaker mass.

Equations

• QingGoodmanLassiter2016.worldScore qud u w = ∑ cs : QingGoodmanLassiter2016.ContextSet, QingGoodmanLassiter2016.contextPrior cs * QingGoodmanLassiter2016.s1Post qud cs w u

def QingGoodmanLassiter2016.ctxScore (qud : QUD) (u : Utterance) (cs : ContextSet) : ℚ≥0

Listener context score (eq. 7, context side).

Equations

• QingGoodmanLassiter2016.ctxScore qud u cs = QingGoodmanLassiter2016.contextPrior cs * ∑ w : QingGoodmanLassiter2016.WorldState, QingGoodmanLassiter2016.s1Post qud cs w u

noncomputable def QingGoodmanLassiter2016.l1World (qud : QUD) (u : Utterance) : PMF WorldState

World-side pragmatic listener (eq. 7).

Equations

• QingGoodmanLassiter2016.l1World qud u = PMF.ofScores PMF.Fallback.uniform (QingGoodmanLassiter2016.worldScore qud u)

noncomputable def QingGoodmanLassiter2016.l1Ctx (qud : QUD) (u : Utterance) : PMF ContextSet

Context-side pragmatic listener (eq. 7).

Equations

• QingGoodmanLassiter2016.l1Ctx qud u = PMF.ofScores PMF.Fallback.uniform (QingGoodmanLassiter2016.ctxScore qud u)

noncomputable def QingGoodmanLassiter2016.l1WorldEvent (qud : QUD) (u : Utterance) (P : WorldState → Bool) : ENNReal

Event marginal of the world-side listener.

Equations

• QingGoodmanLassiter2016.l1WorldEvent qud u P = ∑' (w : QingGoodmanLassiter2016.WorldState), if P w = true then (QingGoodmanLassiter2016.l1World qud u) w else 0

Listener predictions

QUD_now symmetry

theorem QingGoodmanLassiter2016.qud_now_wTT_eq_wFT : (l1World QUD.now (some Assertion.notStopped)) WorldState.wTT = (l1World QUD.now (some Assertion.notStopped)) WorldState.wFT

Under QUD_now, wTT and wFT are indistinguishable: qAggQ .now is definitionally symmetric in the now-cell, so projection must be measured on the context-set side (l1Ctx), not the world marginal.

QUD answer

theorem QingGoodmanLassiter2016.qud_answer_now_true : (l1WorldEvent QUD.now (some Assertion.notStopped) fun (w : WorldState) => !w.now) < l1WorldEvent QUD.now (some Assertion.notStopped) fun (x : WorldState) => x.now

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

World elimination

"Didn't stop smoking" is literally false at wTF, concentrating L1 on wTT.

theorem QingGoodmanLassiter2016.wTT_gt_wTF : (l1World QUD.now (some Assertion.notStopped)) WorldState.wTF < (l1World QUD.now (some Assertion.notStopped)) WorldState.wTT

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

Projection under QUD_max (Figure 1c)

The identity QUD breaks the QUD_now degeneracy — under +past, "didn't stop" narrows to exactly wTT — but projection stays incomplete: wTT = wFF, so the past marginals still coincide.

theorem QingGoodmanLassiter2016.projection_under_qud_max : (l1World QUD.max (some Assertion.notStopped)) WorldState.wFT < (l1World QUD.max (some Assertion.notStopped)) WorldState.wTT

Projection under QUD_max: wTT > wFT.

theorem QingGoodmanLassiter2016.qud_max_incomplete_projection : (l1World QUD.max (some Assertion.notStopped)) WorldState.wTT = (l1World QUD.max (some Assertion.notStopped)) WorldState.wFF

Incomplete projection under QUD_max: wTT = wFF (Figure 1c). The involution (past, now) ↦ (¬now, ¬past) fixes ⟦didn't stop⟧ and permutes the context sets prior-preservingly, so world marginals cannot fully register the presupposition.

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

Under +past, "didn't stop" narrows L0 to wTT (aggregate 1, 1⁶ = 1); under −past it spreads ((1/2)⁶ = 1/64). S1 rewards informativity, so L1 infers the speaker assumed a +past common ground — projection as context-set inference, with (wTT, +past) the joint mode (Figure 3).

theorem QingGoodmanLassiter2016.context_projection : (l1Ctx QUD.now (some Assertion.notStopped)) ContextSet.pastFalse < (l1Ctx QUD.now (some Assertion.notStopped)) ContextSet.pastTrue

The headline: L1 infers a +past context set over −past.

theorem QingGoodmanLassiter2016.context_projection_over_universe : (l1Ctx QUD.now (some Assertion.notStopped)) ContextSet.universe < (l1Ctx QUD.now (some Assertion.notStopped)) ContextSet.pastTrue

+past beats universe despite the prior (6 vs 9): "didn't stop" narrows to wTT under +past (1⁶ = 1) but spreads over three worlds under universe ((1/4)⁶).

theorem QingGoodmanLassiter2016.now_context_dispreferred : (l1Ctx QUD.now (some Assertion.notStopped)) ContextSet.nowFalse < (l1Ctx QUD.now (some Assertion.notStopped)) ContextSet.pastTrue

−now contexts are dispreferred (p. 1114): −now already entails the QUD answer, so "didn't stop smoking" adds nothing there.

"Stopped smoking"

theorem QingGoodmanLassiter2016.stopped_qud_answer : (l1WorldEvent QUD.now (some Assertion.stopped) fun (x : WorldState) => x.now) < l1WorldEvent QUD.now (some Assertion.stopped) fun (w : WorldState) => !w.now

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

Structural properties

theorem QingGoodmanLassiter2016.notStopped_compatible_worlds (w : WorldState) : literalMeaning (some Assertion.notStopped) w = true ↔ w ≠ WorldState.wTF

"didn't stop smoking" excludes exactly the stopping world.

theorem QingGoodmanLassiter2016.notStopped_informative_in_pastTrue (w : WorldState) : (compatibleBool ContextSet.pastTrue w && literalMeaning (some Assertion.notStopped) w) = true ↔ w = WorldState.wTT

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

theorem QingGoodmanLassiter2016.stopped_world (w : WorldState) : literalMeaning (some Assertion.stopped) w = true ↔ w = WorldState.wTF

"stopped smoking" denotes exactly the stopping world (T,F).

theorem QingGoodmanLassiter2016.alwaysSmoked_world (w : WorldState) : literalMeaning (some Assertion.always) w = true ↔ w = WorldState.wTT

"always smoked" denotes exactly (T,T).

theorem QingGoodmanLassiter2016.neverSmoked_world (w : WorldState) : literalMeaning (some Assertion.never) w = true ↔ w = WorldState.wFF

"never smoked" denotes exactly (F,F).

def QingGoodmanLassiter2016.entailsPast : ContextSet → Bool

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

Equations

• QingGoodmanLassiter2016.entailsPast QingGoodmanLassiter2016.ContextSet.pastTrue = true
• QingGoodmanLassiter2016.entailsPast QingGoodmanLassiter2016.ContextSet.pastTrueNowTrue = true
• QingGoodmanLassiter2016.entailsPast QingGoodmanLassiter2016.ContextSet.pastTrueNowFalse = true
• QingGoodmanLassiter2016.entailsPast x✝ = false

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

3 of 9 context sets entail past=T.