Qing, Goodman, and Lassiter (2016): A Rational Speech-Act Model of Projective Content

Qing, Goodman and Lassiter derive the projective content of change-of-state verbs under negation from a listener who jointly infers the world and the context set the speaker took for granted. The worlds record whether John smoked and whether he smokes. Within a context set the literal listener answers the question under discussion (L0), the speaker is informative about the answer (speaker), and the pragmatic listener inverts the speaker over pairs of a world and a context set (listener).

Main results

• standard_uniform: the standard model puts the three worlds compatible with John did not stop smoking on a par at every rationality.
• uniform_tie, uniform_change_lt: with every context set equally likely and the maximal question, the world in which John still smokes, with the context set that he smoked, ties with the world in which he never smoked, with the context set that he does not smoke, and the changed world trails.
• now_settled_lt, now_change_lt, now_universe_lt: asked whether John smokes now, the listener prefers the world in which he still smokes with the context set that he smoked to a context set that already settles the question, to the change context set, and, at every rationality of at least one, to the universe.
• now_cg_mode: the paper's common-ground prior is one instance.

Implementation notes

• The utterance prior enters the speaker as the cost -log Pr(u) / α, since the paper multiplies by the prior outside the rationality.
• The pair prior puts the actual world in the context set, as the paper's figures do.
• Speaker shares are evaluated cell by cell from tables of the literal listener's counts, certified by decide.
• The common-ground prior carries the paper's observation probability of 0.4 and 5% noise, scaled to naturals. The theorems quantify over any prior meeting the ordering hypotheses it satisfies.

TODO

• The world marginals of the paper's first figure and the questions of its fourth are not formalized.

References

• [QGL16]
• [FG12]
• [Sta74]

Worlds, utterances, and questions

inductive QingGoodmanLassiter2016.World : Type

A world records whether John smoked in the past and whether he smokes now.

• TT : World
• TF : World
• FT : World
• FF : World

@[instance_reducible]

instance QingGoodmanLassiter2016.instDecidableEqWorld : DecidableEq World

Equations

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

@[instance_reducible]

instance QingGoodmanLassiter2016.instFintypeWorld : Fintype World

Equations

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

@[instance_reducible]

instance QingGoodmanLassiter2016.instReprWorld : Repr World

Equations

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

def QingGoodmanLassiter2016.instReprWorld.repr : World → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance QingGoodmanLassiter2016.instInhabitedWorld : Inhabited World

Equations

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

@[instance_reducible]

instance QingGoodmanLassiter2016.instMeasurableSpaceWorld : MeasurableSpace World

Equations

• QingGoodmanLassiter2016.instMeasurableSpaceWorld = ⊤

instance QingGoodmanLassiter2016.instDiscreteMeasurableSpaceWorld : DiscreteMeasurableSpace World

instance QingGoodmanLassiter2016.instMeasurableSingletonClassWorld : MeasurableSingletonClass World

def QingGoodmanLassiter2016.World.past : World → Bool

John smoked in the past.

Equations

• QingGoodmanLassiter2016.World.TT.past = true
• QingGoodmanLassiter2016.World.TF.past = true
• QingGoodmanLassiter2016.World.FT.past = false
• QingGoodmanLassiter2016.World.FF.past = false

def QingGoodmanLassiter2016.World.now : World → Bool

John smokes now.

Equations

• QingGoodmanLassiter2016.World.TT.now = true
• QingGoodmanLassiter2016.World.FT.now = true
• QingGoodmanLassiter2016.World.TF.now = false
• QingGoodmanLassiter2016.World.FF.now = false

inductive QingGoodmanLassiter2016.Positive : Type

The six positive utterances of Table 1.

• smokes : Positive
• smoked : Positive
• always : Positive
• stopped : Positive
• started : Positive
• never : Positive

@[instance_reducible]

instance QingGoodmanLassiter2016.instDecidableEqPositive : DecidableEq Positive

Equations

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

@[instance_reducible]

instance QingGoodmanLassiter2016.instFintypePositive : Fintype Positive

Equations

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

@[instance_reducible]

instance QingGoodmanLassiter2016.instReprPositive : Repr Positive

Equations

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

def QingGoodmanLassiter2016.instReprPositive.repr : Positive → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance QingGoodmanLassiter2016.instInhabitedPositive : Inhabited Positive

Equations

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

def QingGoodmanLassiter2016.Positive.ext : Positive → Set World

The denotation of a positive utterance, the change-of-state verbs evaluated at the world's two times.

Equations

• QingGoodmanLassiter2016.Positive.smokes.ext = {w : QingGoodmanLassiter2016.World | w.now = true}
• QingGoodmanLassiter2016.Positive.smoked.ext = {w : QingGoodmanLassiter2016.World | w.past = true}
• QingGoodmanLassiter2016.Positive.always.ext = {w : QingGoodmanLassiter2016.World | Aspect.Phasal.continuation.Transition (w.past = true) (w.now = true)}
• QingGoodmanLassiter2016.Positive.stopped.ext = {w : QingGoodmanLassiter2016.World | Aspect.Phasal.cessation.Transition (w.past = true) (w.now = true)}
• QingGoodmanLassiter2016.Positive.started.ext = {w : QingGoodmanLassiter2016.World | Aspect.Phasal.inception.Transition (w.past = true) (w.now = true)}
• QingGoodmanLassiter2016.Positive.never.ext = {w : QingGoodmanLassiter2016.World | ¬w.past = true ∧ ¬w.now = true}

@[instance_reducible]

instance QingGoodmanLassiter2016.instDecidablePredWorldMemSetExt (p : Positive) : DecidablePred fun (x : World) => x ∈ p.ext

Equations

• One or more equations did not get rendered due to their size.
• QingGoodmanLassiter2016.instDecidablePredWorldMemSetExt QingGoodmanLassiter2016.Positive.smokes x✝ = QingGoodmanLassiter2016.instDecidablePredWorldMemSetExt._aux_1 x✝
• QingGoodmanLassiter2016.instDecidablePredWorldMemSetExt QingGoodmanLassiter2016.Positive.smoked x✝ = QingGoodmanLassiter2016.instDecidablePredWorldMemSetExt._aux_3 x✝
• QingGoodmanLassiter2016.instDecidablePredWorldMemSetExt QingGoodmanLassiter2016.Positive.never x✝ = { decide := decide ¬x✝.past = true && decide ¬x✝.now = true, reflects_decide := ⋯ }

inductive QingGoodmanLassiter2016.Utterance : Type

An utterance is silence or a positive utterance, affirmed or negated.

• silence : Utterance
• say (p : Positive) (negated : Bool) : Utterance

@[instance_reducible]

instance QingGoodmanLassiter2016.instDecidableEqUtterance : DecidableEq Utterance

Equations

• QingGoodmanLassiter2016.instDecidableEqUtterance = QingGoodmanLassiter2016.instDecidableEqUtterance.decEq

def QingGoodmanLassiter2016.instDecidableEqUtterance.decEq (x✝ x✝¹ : Utterance) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• QingGoodmanLassiter2016.instDecidableEqUtterance.decEq QingGoodmanLassiter2016.Utterance.silence QingGoodmanLassiter2016.Utterance.silence = isTrue ⋯
• QingGoodmanLassiter2016.instDecidableEqUtterance.decEq QingGoodmanLassiter2016.Utterance.silence (QingGoodmanLassiter2016.Utterance.say p negated) = isFalse ⋯
• QingGoodmanLassiter2016.instDecidableEqUtterance.decEq (QingGoodmanLassiter2016.Utterance.say p negated) QingGoodmanLassiter2016.Utterance.silence = isFalse ⋯

@[instance_reducible]

instance QingGoodmanLassiter2016.instFintypeUtterance : Fintype Utterance

Equations

• QingGoodmanLassiter2016.instFintypeUtterance = Fintype.ofEquiv (Unit ⊕ (_ : QingGoodmanLassiter2016.Positive) × Bool) QingGoodmanLassiter2016.Utterance.proxyTypeEquiv

def QingGoodmanLassiter2016.instReprUtterance.repr : Utterance → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance QingGoodmanLassiter2016.instReprUtterance : Repr Utterance

Equations

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

@[instance_reducible]

instance QingGoodmanLassiter2016.instInhabitedUtterance : Inhabited Utterance

Equations

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

@[instance_reducible]

instance QingGoodmanLassiter2016.instMeasurableSpaceUtterance : MeasurableSpace Utterance

Equations

• QingGoodmanLassiter2016.instMeasurableSpaceUtterance = ⊤

instance QingGoodmanLassiter2016.instDiscreteMeasurableSpaceUtterance : DiscreteMeasurableSpace Utterance

instance QingGoodmanLassiter2016.instMeasurableSingletonClassUtterance : MeasurableSingletonClass Utterance

def QingGoodmanLassiter2016.Utterance.sem : Utterance → Set World

Silence is true everywhere, and a negation denotes the complement.

Equations

• QingGoodmanLassiter2016.Utterance.silence.sem = Set.univ
• (QingGoodmanLassiter2016.Utterance.say p false).sem = p.ext
• (QingGoodmanLassiter2016.Utterance.say p true).sem = p.extᶜ

@[instance_reducible]

instance QingGoodmanLassiter2016.instDecidablePredWorldMemSetSem (u : Utterance) : DecidablePred fun (x : World) => x ∈ u.sem

Equations

• QingGoodmanLassiter2016.instDecidablePredWorldMemSetSem QingGoodmanLassiter2016.Utterance.silence x✝ = { decide := true, reflects_decide := ⋯ }
• QingGoodmanLassiter2016.instDecidablePredWorldMemSetSem (QingGoodmanLassiter2016.Utterance.say p false) x✝ = QingGoodmanLassiter2016.instDecidablePredWorldMemSetSem._aux_2 p x✝
• QingGoodmanLassiter2016.instDecidablePredWorldMemSetSem (QingGoodmanLassiter2016.Utterance.say p true) x✝ = { decide := !decide (x✝ ∈ p.ext), reflects_decide := ⋯ }

@[reducible, inline]

abbrev QingGoodmanLassiter2016.notStopped : Utterance

John did not stop smoking.

Equations

• QingGoodmanLassiter2016.notStopped = QingGoodmanLassiter2016.Utterance.say QingGoodmanLassiter2016.Positive.stopped true

noncomputable def QingGoodmanLassiter2016.Utterance.prior : Utterance → ENNReal

The utterance prior (1) halves with each content word, negation and auxiliaries being free.

Equations

• QingGoodmanLassiter2016.Utterance.silence.prior = 1
• (QingGoodmanLassiter2016.Utterance.say QingGoodmanLassiter2016.Positive.smokes negated).prior = 1 / 2
• (QingGoodmanLassiter2016.Utterance.say QingGoodmanLassiter2016.Positive.smoked negated).prior = 1 / 2
• (QingGoodmanLassiter2016.Utterance.say p negated).prior = 1 / 4

inductive QingGoodmanLassiter2016.QUD : Type

The question under discussion asks which world it is, or whether John smokes now.

• max : QUD
• now : QUD

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

@[instance_reducible]

instance QingGoodmanLassiter2016.instReprQUD : Repr QUD

Equations

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

def QingGoodmanLassiter2016.QUD.cell : QUD → World → Finset World

The cell of a world under a question.

Equations

• QingGoodmanLassiter2016.QUD.max.cell x✝ = {x✝}
• QingGoodmanLassiter2016.QUD.now.cell x✝ = {x : QingGoodmanLassiter2016.World | x.now = x✝.now}

theorem QingGoodmanLassiter2016.QUD.cell_preimage (q : QUD) (w : World) : q.cell ⁻¹' {q.cell w} = ↑(q.cell w)

Context sets

def QingGoodmanLassiter2016.pastT : Finset World

The context set that John smoked.

Equations

• QingGoodmanLassiter2016.pastT = {QingGoodmanLassiter2016.World.TT, QingGoodmanLassiter2016.World.TF}

def QingGoodmanLassiter2016.nowF : Finset World

The context set that John does not smoke.

Equations

• QingGoodmanLassiter2016.nowF = {QingGoodmanLassiter2016.World.TF, QingGoodmanLassiter2016.World.FF}

def QingGoodmanLassiter2016.nowT : Finset World

The context set that John smokes.

Equations

• QingGoodmanLassiter2016.nowT = {QingGoodmanLassiter2016.World.TT, QingGoodmanLassiter2016.World.FT}

def QingGoodmanLassiter2016.change : Finset World

The context set that John's habit changed, one way or the other.

Equations

• QingGoodmanLassiter2016.change = {QingGoodmanLassiter2016.World.TF, QingGoodmanLassiter2016.World.FT}

The literal listener within a context set (5)

noncomputable def QingGoodmanLassiter2016.L0 (C : Finset World) (q : QUD) : ProbabilityTheory.Kernel Utterance (Finset World)

The literal listener within a context set under a question samples a world of the context set at which the utterance is true and returns the question's answer there.

Equations

• QingGoodmanLassiter2016.L0 C q = (RSA.listener (MeasureTheory.Measure.count.restrict ↑C) (RSA.truthful fun (u : QingGoodmanLassiter2016.Utterance) => u.sem)).map q.cell

instance QingGoodmanLassiter2016.instIsFiniteKernelUtteranceFinsetWorldL0 (C : Finset World) (q : QUD) : ProbabilityTheory.IsFiniteKernel (L0 C q)

def QingGoodmanLassiter2016.l0 (C : Finset World) (q : QUD) (u : Utterance) (w : World) : ℕ × ℕ

The literal listener counts the worlds of the context set where the utterance is true and the question's answer is the world's, over those where the utterance is true.

Equations

• QingGoodmanLassiter2016.l0 C q u w = ({x ∈ {x ∈ C | x ∈ u.sem} | x ∈ q.cell w}.card, {x ∈ C | x ∈ u.sem}.card)

theorem QingGoodmanLassiter2016.L0_apply (C : Finset World) (q : QUD) (u : Utterance) (w : World) : ((L0 C q) u) {q.cell w} = ↑(l0 C q u w).1 / ↑(l0 C q u w).2

theorem QingGoodmanLassiter2016.prior_ne_zero (u : Utterance) : u.prior ≠ 0

theorem QingGoodmanLassiter2016.prior_ne_top (u : Utterance) : u.prior ≠ ⊤

noncomputable def QingGoodmanLassiter2016.cost (α : ℝ) (u : Utterance) : ℝ

An utterance costs -log Pr(u) / α at rationality α, since (3) weighs the speaker's choice by the utterance prior outside the rationality.

Equations

• QingGoodmanLassiter2016.cost α u = -Real.log u.prior.toReal / α

theorem QingGoodmanLassiter2016.exp_neg_cost {α : ℝ} (hα : α ≠ 0) (u : Utterance) : Real.exp (-(α * cost α u)) = u.prior.toReal

Speaker and listeners (6), (7)

noncomputable def QingGoodmanLassiter2016.speaker (q : QUD) (C : Finset World) (α : ℝ) (w : World) : MeasureTheory.Measure Utterance

The speaker within a context set (6) knows the answer to the question at her world and is informative about the literal listener's belief about it, weighted by the utterance prior.

Equations

• QingGoodmanLassiter2016.speaker q C α w = (RSA.speaker α (QingGoodmanLassiter2016.cost α) (⇑(QingGoodmanLassiter2016.L0 C q)) MeasureTheory.Measure.dirac) (q.cell w)

instance QingGoodmanLassiter2016.instIsFiniteMeasureUtteranceSpeaker (q : QUD) (C : Finset World) (α : ℝ) (w : World) : MeasureTheory.IsFiniteMeasure (speaker q C α w)

noncomputable def QingGoodmanLassiter2016.ctxPrior (π : Finset World → ℕ) : MeasureTheory.Measure (Finset World)

The prior over context sets determined by a weighting.

Equations

• QingGoodmanLassiter2016.ctxPrior π = MeasureTheory.Measure.count.withDensity fun (C : Finset QingGoodmanLassiter2016.World) => ↑(π C)

theorem QingGoodmanLassiter2016.ctxPrior_singleton (π : Finset World → ℕ) (C : Finset World) : (ctxPrior π) {C} = ↑(π C)

instance QingGoodmanLassiter2016.instIsFiniteMeasureFinsetWorldCtxPrior (π : Finset World → ℕ) : MeasureTheory.IsFiniteMeasure (ctxPrior π)

noncomputable def QingGoodmanLassiter2016.pairPrior (π : Finset World → ℕ) : MeasureTheory.Measure (World × Finset World)

The pair prior weighs a world with a context set containing it by the context prior; the paper's uniform world prior cancels.

Equations

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

@[simp]

theorem QingGoodmanLassiter2016.pairPrior_singleton (π : Finset World → ℕ) (w : World) (C : Finset World) : (pairPrior π) {(w, C)} = if w ∈ C then ↑(π C) else 0

instance QingGoodmanLassiter2016.instIsFiniteMeasureProdWorldFinsetPairPrior (π : Finset World → ℕ) : MeasureTheory.IsFiniteMeasure (pairPrior π)

noncomputable def QingGoodmanLassiter2016.listener (q : QUD) (π : Finset World → ℕ) (α : ℝ) : ProbabilityTheory.Kernel Utterance (World × Finset World)

The joint listener (7) inverts the speaker within each context set against the pair prior.

Equations

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

def QingGoodmanLassiter2016.cgWeight (C : Finset World) : ℕ

The common-ground prior (8) takes the paper's observation probability 0.4 and 5% noise, scaled by 14700, over the universe, the four single observations, the four pairs, and the six context sets no observations derive.

Equations

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

Evaluating a cell

noncomputable def QingGoodmanLassiter2016.share (q : QUD) (C : Finset World) (w : World) (α : ℝ) : ℝ

The share of did not stop smoking at a cell, on reals.

Equations

• QingGoodmanLassiter2016.share q C w α = (QingGoodmanLassiter2016.speaker q C α w).real {QingGoodmanLassiter2016.notStopped}

Listener comparisons

The standard model (Figure 1a)

noncomputable def QingGoodmanLassiter2016.standard (α : ℝ) : ProbabilityTheory.Kernel Utterance World

The standard listener is the pragmatic listener over the universe with a uniform world prior, the first column of Table 2.

Equations

• QingGoodmanLassiter2016.standard α = RSA.listener (ProbabilityTheory.uniformOn Set.univ) (QingGoodmanLassiter2016.speaker QingGoodmanLassiter2016.QUD.max Finset.univ α)

theorem QingGoodmanLassiter2016.standard_uniform {α : ℝ} (hα : 0 < α) : ((standard α) notStopped) {World.TT} = ((standard α) notStopped) {World.FT} ∧ ((standard α) notStopped) {World.FT} = ((standard α) notStopped) {World.FF}

The standard model puts the three worlds compatible with did not stop smoking on a par at every rationality, since the utterance is equally under-informative at each, so nothing projects.

Context sets under the maximal question (Figures 1b, 2a)

theorem QingGoodmanLassiter2016.uniform_tie {α : ℝ} (hα : 0 < α) : ((listener QUD.max (fun (x : Finset World) => 1) α) notStopped) {(World.TT, pastT)} = ((listener QUD.max (fun (x : Finset World) => 1) α) notStopped) {(World.FF, nowF)}

With every context set equally likely, the world in which John still smokes taken with the context set that he smoked ties with the world in which he never smoked taken with the context set that he does not smoke, since did not stop smoking identifies the world within either.

theorem QingGoodmanLassiter2016.uniform_change_lt {α : ℝ} (hα : 0 < α) : ((listener QUD.max (fun (x : Finset World) => 1) α) notStopped).real {(World.FT, change)} < ((listener QUD.max (fun (x : Finset World) => 1) α) notStopped).real {(World.TT, pastT)}

The changed world with the change context set trails, since did not stop smoking identifies it there too, but against more informative competitors.

The question whether John smokes now (Figures 1d, 3)

theorem QingGoodmanLassiter2016.now_settled_lt (π : Finset World → ℕ) (hπ : π pastT ≠ 0) (hF : π nowF ≤ π pastT) (hT : π nowT ≤ π pastT) {α : ℝ} (hα : 0 < α) : ((listener QUD.now π α) notStopped).real {(World.FF, nowF)} < ((listener QUD.now π α) notStopped).real {(World.TT, pastT)} ∧ ((listener QUD.now π α) notStopped).real {(World.TT, nowT)} < ((listener QUD.now π α) notStopped).real {(World.TT, pastT)}

A context set that already settles the question, that he does not smoke or that he does, has made silence maximally informative and cannot explain the utterance. Either loses to the world in which he still smokes with the context set that he smoked, under any prior weighting that context set at least as much.

theorem QingGoodmanLassiter2016.now_change_lt (π : Finset World → ℕ) (hπ : π pastT ≠ 0) (h : π change ≤ π pastT) {α : ℝ} (hα : 0 < α) : ((listener QUD.now π α) notStopped).real {(World.FT, change)} < ((listener QUD.now π α) notStopped).real {(World.TT, pastT)}

The change context set is dispreferred under any prior weighting it at most as much as the context set that John smoked, which the common-ground prior does by design.

theorem QingGoodmanLassiter2016.now_universe_lt (π : Finset World → ℕ) (hπ : π pastT ≠ 0) (h : 2 * π Finset.univ ≤ 3 * π pastT) {α : ℝ} (hα : 1 ≤ α) : ((listener QUD.now π α) notStopped).real {(World.TT, Finset.univ)} < ((listener QUD.now π α) notStopped).real {(World.TT, pastT)}

The universe is outrun at every rationality of at least one under any prior weighting it under three halves of the context set that John smoked, since there the utterance leaves a third of the answer open.

theorem QingGoodmanLassiter2016.cgWeight_facts : cgWeight pastT ≠ 0 ∧ cgWeight nowF ≤ cgWeight pastT ∧ cgWeight nowT ≤ cgWeight pastT ∧ cgWeight change ≤ cgWeight pastT ∧ 2 * cgWeight Finset.univ ≤ 3 * cgWeight pastT

The common-ground prior (8) meets the hypotheses, since the observed context sets outweigh change and the universe weighs under three halves of a single observation.

theorem QingGoodmanLassiter2016.now_cg_mode {α : ℝ} (hα : 1 ≤ α) : ((listener QUD.now cgWeight α) notStopped).real {(World.FF, nowF)} < ((listener QUD.now cgWeight α) notStopped).real {(World.TT, pastT)} ∧ ((listener QUD.now cgWeight α) notStopped).real {(World.TT, nowT)} < ((listener QUD.now cgWeight α) notStopped).real {(World.TT, pastT)} ∧ ((listener QUD.now cgWeight α) notStopped).real {(World.FT, change)} < ((listener QUD.now cgWeight α) notStopped).real {(World.TT, pastT)} ∧ ((listener QUD.now cgWeight α) notStopped).real {(World.TT, Finset.univ)} < ((listener QUD.now cgWeight α) notStopped).real {(World.TT, pastT)}

Under the common-ground prior and the question whether John smokes now, the world in which he still smokes with the context set that he smoked beats every competitor the paper discusses at every rationality of at least one. Projection is context-set inference (Figure 3).