@cite{qing-goodman-lassiter-2016} @cite{qing-goodman-lassiter-2016} @cite{scontras-tonhauser-2025} @cite{warstadt-2022}

RSA Projective Content Model. The original formulation of the joint-inference-over-(world, context) model for presupposition projection. @cite{scontras-tonhauser-2025} and @cite{warstadt-2022} are mathematically equivalent instances applied to different domains.

The Model

L1 jointly infers the world state and the context set C (what's in the common ground). Projection emerges because:

1. "John didn't stop smoking" is under-informative in the full universe
2. But it's informative if the listener assumes the speaker has taken "John smoked in the past" for granted (i.e., +past in C)
3. L1 infers that C = +past best explains the utterance

Domain: Change-of-State Verbs

Utterances about John's smoking habit:

• "John stopped smoking" / "John didn't stop smoking"
• "John started smoking" / "John didn't start smoking"
• "John smokes" / "John doesn't smoke" (baselines)

Context sets:

• +past: John smoked in the past is in CG
• -past: John didn't smoke is in CG
• +now: John smokes now is in CG
• -now: John doesn't smoke now is in CG
• U: No constraints (full universe)

Predictions

1. "John didn't stop smoking" -> P(+past in C | utterance) > prior (presupposition projects through negation)

2. QUD sensitivity: projection is stronger when QUD = now? (non-at-issue content projects more)

structure RSA.QingEtAl2016.WorldState : Type

World state: John's smoking status at two time points.

Following Qing et al., a world is a pair (past, now) where:

• past: John smoked in the past
• now: John smokes now

• past : Bool
• now : Bool

def RSA.QingEtAl2016.instDecidableEqWorldState.decEq (x✝ x✝¹ : WorldState) : Decidable (x✝ = x✝¹)

Equations

• RSA.QingEtAl2016.instDecidableEqWorldState.decEq { past := a, now := a_1 } { past := b, now := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

instance RSA.QingEtAl2016.instDecidableEqWorldState : DecidableEq WorldState

Equations

• RSA.QingEtAl2016.instDecidableEqWorldState = RSA.QingEtAl2016.instDecidableEqWorldState.decEq

instance RSA.QingEtAl2016.instReprWorldState : Repr WorldState

Equations

• RSA.QingEtAl2016.instReprWorldState = { reprPrec := RSA.QingEtAl2016.instReprWorldState.repr }

def RSA.QingEtAl2016.instReprWorldState.repr : WorldState → ℕ → Std.Format

Equations

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

instance RSA.QingEtAl2016.instBEqWorldState : BEq WorldState

Equations

• RSA.QingEtAl2016.instBEqWorldState = { beq := RSA.QingEtAl2016.instBEqWorldState.beq }

def RSA.QingEtAl2016.instBEqWorldState.beq : WorldState → WorldState → Bool

Equations

• RSA.QingEtAl2016.instBEqWorldState.beq { past := a, now := a_1 } { past := b, now := b_1 } = (a == b && a_1 == b_1)
• RSA.QingEtAl2016.instBEqWorldState.beq x✝¹ x✝ = false

def RSA.QingEtAl2016.instInhabitedWorldState.default : WorldState

Equations

• RSA.QingEtAl2016.instInhabitedWorldState.default = { past := default, now := default }

instance RSA.QingEtAl2016.instInhabitedWorldState : Inhabited WorldState

Equations

• RSA.QingEtAl2016.instInhabitedWorldState = { default := RSA.QingEtAl2016.instInhabitedWorldState.default }

def RSA.QingEtAl2016.allWorlds : List WorldState

All four world states

Equations

• RSA.QingEtAl2016.allWorlds = [{ past := true, now := true }, { past := true, now := false }, { past := false, now := true }, { past := false, now := false }]

inductive RSA.QingEtAl2016.ContextSet : Type

Context set: which facts are established in the common ground.

Following Qing et al., we model context sets as constraints on worlds. A context set C is the set of worlds compatible with what's taken for granted.

We use named context sets rather than arbitrary subsets for tractability.

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

instance RSA.QingEtAl2016.instDecidableEqContextSet : DecidableEq ContextSet

Equations

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

instance RSA.QingEtAl2016.instReprContextSet : Repr ContextSet

Equations

• RSA.QingEtAl2016.instReprContextSet = { reprPrec := RSA.QingEtAl2016.instReprContextSet.repr }

def RSA.QingEtAl2016.instReprContextSet.repr : ContextSet → ℕ → Std.Format

Equations

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

def RSA.QingEtAl2016.instBEqContextSet.beq : ContextSet → ContextSet → Bool

Equations

• RSA.QingEtAl2016.instBEqContextSet.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance RSA.QingEtAl2016.instBEqContextSet : BEq ContextSet

Equations

• RSA.QingEtAl2016.instBEqContextSet = { beq := RSA.QingEtAl2016.instBEqContextSet.beq }

def RSA.QingEtAl2016.instInhabitedContextSet.default : ContextSet

Equations

• RSA.QingEtAl2016.instInhabitedContextSet.default = RSA.QingEtAl2016.ContextSet.pastTrue

instance RSA.QingEtAl2016.instInhabitedContextSet : Inhabited ContextSet

Equations

• RSA.QingEtAl2016.instInhabitedContextSet = { default := RSA.QingEtAl2016.instInhabitedContextSet.default }

def RSA.QingEtAl2016.allContextSets : List ContextSet

All context sets

Equations

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

def RSA.QingEtAl2016.compatibleBool (c : ContextSet) (w : WorldState) : Bool

World-context compatibility: Is world w compatible with context set C?

This constraint function plays the same role as speakerCredence in S&T and contextCredence in Warstadt.

Equations

• RSA.QingEtAl2016.compatibleBool RSA.QingEtAl2016.ContextSet.pastTrue w = w.past
• RSA.QingEtAl2016.compatibleBool RSA.QingEtAl2016.ContextSet.pastFalse w = !w.past
• RSA.QingEtAl2016.compatibleBool RSA.QingEtAl2016.ContextSet.nowTrue w = w.now
• RSA.QingEtAl2016.compatibleBool RSA.QingEtAl2016.ContextSet.nowFalse w = !w.now
• RSA.QingEtAl2016.compatibleBool RSA.QingEtAl2016.ContextSet.pastTrueNowTrue w = (w.past && w.now)
• RSA.QingEtAl2016.compatibleBool RSA.QingEtAl2016.ContextSet.pastTrueNowFalse w = (w.past && !w.now)
• RSA.QingEtAl2016.compatibleBool RSA.QingEtAl2016.ContextSet.pastFalseNowTrue w = (!w.past && w.now)
• RSA.QingEtAl2016.compatibleBool RSA.QingEtAl2016.ContextSet.pastFalseNowFalse w = (!w.past && !w.now)
• RSA.QingEtAl2016.compatibleBool RSA.QingEtAl2016.ContextSet.universe w = true

inductive RSA.QingEtAl2016.Utterance : Type

Utterances about John's smoking, following Qing et al.'s example.

• stoppedSmoking : Utterance
• notStoppedSmoking : Utterance
• startedSmoking : Utterance
• notStartedSmoking : Utterance
• smokes : Utterance
• doesntSmoke : Utterance
• smoked : Utterance
• didntSmoke : Utterance
• silence : Utterance

instance RSA.QingEtAl2016.instDecidableEqUtterance : DecidableEq Utterance

Equations

• RSA.QingEtAl2016.instDecidableEqUtterance x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance RSA.QingEtAl2016.instReprUtterance : Repr Utterance

Equations

• RSA.QingEtAl2016.instReprUtterance = { reprPrec := RSA.QingEtAl2016.instReprUtterance.repr }

def RSA.QingEtAl2016.instReprUtterance.repr : Utterance → ℕ → Std.Format

Equations

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

def RSA.QingEtAl2016.instBEqUtterance.beq : Utterance → Utterance → Bool

Equations

• RSA.QingEtAl2016.instBEqUtterance.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance RSA.QingEtAl2016.instBEqUtterance : BEq Utterance

Equations

• RSA.QingEtAl2016.instBEqUtterance = { beq := RSA.QingEtAl2016.instBEqUtterance.beq }

instance RSA.QingEtAl2016.instInhabitedUtterance : Inhabited Utterance

Equations

• RSA.QingEtAl2016.instInhabitedUtterance = { default := RSA.QingEtAl2016.instInhabitedUtterance.default }

def RSA.QingEtAl2016.instInhabitedUtterance.default : Utterance

Equations

• RSA.QingEtAl2016.instInhabitedUtterance.default = RSA.QingEtAl2016.Utterance.stoppedSmoking

def RSA.QingEtAl2016.allUtterances : List Utterance

Equations

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

def RSA.QingEtAl2016.smokesNow (w : WorldState) : Bool

Activity predicate: "smokes" at the current time.

Equations

• RSA.QingEtAl2016.smokesNow w = w.now

def RSA.QingEtAl2016.smokedPast (w : WorldState) : Bool

Activity predicate: "smoked" in the past.

Equations

• RSA.QingEtAl2016.smokedPast w = w.past

def RSA.QingEtAl2016.literalMeaning : Utterance → WorldState → Bool

Literal semantics using compositional CoS machinery.

Note: CoS semantics in Montague are defined for (prior state, current state). We interpret:

• presup = constraint on w.past
• assertion = constraint on w.now

For "John stopped smoking":

• presup: w.past = true (John smoked)
• assertion: w.now = false (John doesn't smoke)

Equations

• RSA.QingEtAl2016.literalMeaning RSA.QingEtAl2016.Utterance.stoppedSmoking x✝ = (x✝.past && !x✝.now)
• RSA.QingEtAl2016.literalMeaning RSA.QingEtAl2016.Utterance.notStoppedSmoking x✝ = !(x✝.past && !x✝.now)
• RSA.QingEtAl2016.literalMeaning RSA.QingEtAl2016.Utterance.startedSmoking x✝ = (!x✝.past && x✝.now)
• RSA.QingEtAl2016.literalMeaning RSA.QingEtAl2016.Utterance.notStartedSmoking x✝ = !(!x✝.past && x✝.now)
• RSA.QingEtAl2016.literalMeaning RSA.QingEtAl2016.Utterance.smokes x✝ = x✝.now
• RSA.QingEtAl2016.literalMeaning RSA.QingEtAl2016.Utterance.doesntSmoke x✝ = !x✝.now
• RSA.QingEtAl2016.literalMeaning RSA.QingEtAl2016.Utterance.smoked x✝ = x✝.past
• RSA.QingEtAl2016.literalMeaning RSA.QingEtAl2016.Utterance.didntSmoke x✝ = !x✝.past
• RSA.QingEtAl2016.literalMeaning RSA.QingEtAl2016.Utterance.silence x✝ = true

theorem RSA.QingEtAl2016.stopped_follows_cos_pattern (w : WorldState) : literalMeaning Utterance.stoppedSmoking w = (w.past && !w.now)

Our semantics follow the CoS pattern: cessation presupposes prior state, asserts negation of current state.

Note: The Montague CoS module defines semantics over a single predicate P, while our worlds have separate past/now fields. The correspondence is:

• "stopped smoking" = prior state held (past=true), current state doesn't (now=false)
• This matches cessation: presup P, assert not-P

inductive RSA.QingEtAl2016.QUD : Type

Questions Under Discussion, following Qing et al.

• nowQ : QUD
• pastQ : QUD
• maxQ : QUD
• changeQ : QUD

instance RSA.QingEtAl2016.instDecidableEqQUD : DecidableEq QUD

Equations

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

instance RSA.QingEtAl2016.instReprQUD : Repr QUD

Equations

• RSA.QingEtAl2016.instReprQUD = { reprPrec := RSA.QingEtAl2016.instReprQUD.repr }

def RSA.QingEtAl2016.instReprQUD.repr : QUD → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• RSA.QingEtAl2016.instReprQUD.repr RSA.QingEtAl2016.QUD.nowQ prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "RSA.QingEtAl2016.QUD.nowQ")).group prec✝
• RSA.QingEtAl2016.instReprQUD.repr RSA.QingEtAl2016.QUD.maxQ prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "RSA.QingEtAl2016.QUD.maxQ")).group prec✝

instance RSA.QingEtAl2016.instBEqQUD : BEq QUD

Equations

• RSA.QingEtAl2016.instBEqQUD = { beq := RSA.QingEtAl2016.instBEqQUD.beq }

def RSA.QingEtAl2016.instBEqQUD.beq : QUD → QUD → Bool

Equations

• RSA.QingEtAl2016.instBEqQUD.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def RSA.QingEtAl2016.instInhabitedQUD.default : QUD

Equations

• RSA.QingEtAl2016.instInhabitedQUD.default = RSA.QingEtAl2016.QUD.nowQ

instance RSA.QingEtAl2016.instInhabitedQUD : Inhabited QUD

Equations

• RSA.QingEtAl2016.instInhabitedQUD = { default := RSA.QingEtAl2016.instInhabitedQUD.default }

def RSA.QingEtAl2016.allQUDs : List QUD

Equations

• RSA.QingEtAl2016.allQUDs = [RSA.QingEtAl2016.QUD.nowQ, RSA.QingEtAl2016.QUD.pastQ, RSA.QingEtAl2016.QUD.maxQ, RSA.QingEtAl2016.QUD.changeQ]

def RSA.QingEtAl2016.qudProject : QUD → WorldState → WorldState → Bool

QUD projection: two worlds are equivalent if they give the same QUD answer.

Equations

• RSA.QingEtAl2016.qudProject RSA.QingEtAl2016.QUD.nowQ x✝¹ x✝ = (x✝¹.now == x✝.now)
• RSA.QingEtAl2016.qudProject RSA.QingEtAl2016.QUD.pastQ x✝¹ x✝ = (x✝¹.past == x✝.past)
• RSA.QingEtAl2016.qudProject RSA.QingEtAl2016.QUD.maxQ x✝¹ x✝ = (x✝¹.past == x✝.past && x✝¹.now == x✝.now)
• RSA.QingEtAl2016.qudProject RSA.QingEtAl2016.QUD.changeQ x✝¹ x✝ = ((x✝¹.past != x✝¹.now) == (x✝.past != x✝.now))

def RSA.QingEtAl2016.worldPrior (_w : WorldState) : ℚ

World prior: uniform

Equations

• RSA.QingEtAl2016.worldPrior _w = 1 / 4

def RSA.QingEtAl2016.contextPrior : ContextSet → ℚ

Context set prior: Following Qing et al., context sets derived from "natural observations" about past/now smoking have higher prior.

Complex context sets (like "change") have lower prior.

Equations

• RSA.QingEtAl2016.contextPrior RSA.QingEtAl2016.ContextSet.pastTrue = 4
• RSA.QingEtAl2016.contextPrior RSA.QingEtAl2016.ContextSet.pastFalse = 4
• RSA.QingEtAl2016.contextPrior RSA.QingEtAl2016.ContextSet.nowTrue = 4
• RSA.QingEtAl2016.contextPrior RSA.QingEtAl2016.ContextSet.nowFalse = 4
• RSA.QingEtAl2016.contextPrior RSA.QingEtAl2016.ContextSet.pastTrueNowTrue = 2
• RSA.QingEtAl2016.contextPrior RSA.QingEtAl2016.ContextSet.pastTrueNowFalse = 2
• RSA.QingEtAl2016.contextPrior RSA.QingEtAl2016.ContextSet.pastFalseNowTrue = 2
• RSA.QingEtAl2016.contextPrior RSA.QingEtAl2016.ContextSet.pastFalseNowFalse = 2
• RSA.QingEtAl2016.contextPrior RSA.QingEtAl2016.ContextSet.universe = 1

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

This implementation demonstrates that @cite{qing-goodman-lassiter-2016} uses the same mathematical structure as S&T and Warstadt:

Component	@cite{qing-goodman-lassiter-2016}	@cite{scontras-tonhauser-2025}	@cite{warstadt-2022}
World	(past, now)	(BEL, C)	(hasDog, sick)
Latent var	ContextSet	BeliefState	Context
Constraint	compatibleBool	speakerCredenceBool	compatibleBool
Measure	projectionOfPast	projectionOfC	accommodationStrength

All three use the latent variable in the BeliefState slot. The differences are purely domain-specific.

The Unified Equation

All three implement:

L1(w, C | u, Q) proportional-to S1(u | w, C, Q) * P(w) * P(C)

Where:

• C is the latent "conversational state" variable
• S1 optimizes for L0(Q(w) | u, C, Q)
• L1 jointly infers (world, context)
• Projection = marginal P(C | u) for contexts entailing the presupposition