[ST25]: projection without lexical presupposition

An RSA model of know under negation (SuB 29, pp. 1431–1448): the pragmatic listener jointly infers the world state and the speaker's private assumptions (eq. 7), the speaker scores QUD-projected informativity (eq. 6, α = 10, fn. 12), and the literal listener answers the QUD within the assumption set (eq. 5). Projection of the complement C emerges with no lexically-specified constraint on the common ground. Domain: 6 utterances × 4 worlds (BEL × C) × 15 belief states × 2 QUDs; literal semantics from Semantics.Attitudes.Factivity (know = factivePos, think = nonFactivePos).

Main results

• bel_qud_marginal_eq_prior_high / _low: under the BEL? QUD the world C-marginal equals the prior for every utterance — S1 depends on the world only through its BEL-cell, so projection is invisible there.
• prediction_2b: higher prior ⇒ stronger projection (C? QUD), the effect [DT21] documents across 20 predicates (Exp 1: β = 0.16, p < .001).
• prediction_2c: BEL? QUD ⇒ stronger projection than C? QUD (Exp 2: β = 0.14, p < .001).
• c_qud_thinkNeg_higher: under C?, negated know is evidence against C.
• model_predicts_effects: the model directions match the regressions.

Implementation notes

α = 10 is a natural power, so the chain is exact ℚ≥0: the speaker is RSA.Score.s1 over the QUD-aggregated literal listener with degenerate cells falling back to cPos (one declaration covering both faces), the listener is PMF.ofScores, and every prediction is one kernel-verified event-mass comparison.

Utterance cost (§3.1: complex = 2 × simple) is omitted: exp(−αC) is transcendental, and the omission reverses prediction (2a)'s world-marginal direction (the paper derives know > think with cost, Figure 7a); predictions (2b) and (2c) are robust to it. Prior parameters follow §3.1: P(C) ∈ {2/3, 1/3}, P(BEL | C) = 1/2, uniform over the 15 assumption sets.

TODO

Model the cost term (log-rational costs keep ℚ exactness) and derive prediction (2a)'s world-marginal direction. Prove the structural equivalence with [QGL16] (fn. 10: "private assumptions" vs "common ground" is interpretive, not computational) — see the matching TODO in QingGoodmanLassiter2016.lean.

Worlds and utterances

inductive ScontrasTonhauser2025.WorldState : Type

World state: (BEL, C) where BEL = Cole believes C, C = complement is true. Flat inductive for tactic enumerability.

• w11 : WorldState
• w10 : WorldState
• w01 : WorldState
• w00 : WorldState

@[implicit_reducible]

instance ScontrasTonhauser2025.instDecidableEqWorldState : DecidableEq WorldState

Equations

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

@[implicit_reducible]

instance ScontrasTonhauser2025.instReprWorldState : Repr WorldState

Equations

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

def ScontrasTonhauser2025.instReprWorldState.repr : WorldState → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance ScontrasTonhauser2025.instInhabitedWorldState : Inhabited WorldState

Equations

• ScontrasTonhauser2025.instInhabitedWorldState = { default := ScontrasTonhauser2025.instInhabitedWorldState.default }

@[implicit_reducible]

instance ScontrasTonhauser2025.instFintypeWorldState : Fintype WorldState

Equations

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

def ScontrasTonhauser2025.WorldState.bel : WorldState → Bool

Equations

• ScontrasTonhauser2025.WorldState.w11.bel = true
• ScontrasTonhauser2025.WorldState.w10.bel = true
• ScontrasTonhauser2025.WorldState.w01.bel = false
• ScontrasTonhauser2025.WorldState.w00.bel = false

def ScontrasTonhauser2025.WorldState.c : WorldState → Bool

Equations

• ScontrasTonhauser2025.WorldState.w11.c = true
• ScontrasTonhauser2025.WorldState.w01.c = true
• ScontrasTonhauser2025.WorldState.w10.c = false
• ScontrasTonhauser2025.WorldState.w00.c = false

@[implicit_reducible]

instance ScontrasTonhauser2025.instHasComplementWorldState : Semantics.Attitudes.Factivity.HasComplement WorldState

Equations

• ScontrasTonhauser2025.instHasComplementWorldState = { c := ScontrasTonhauser2025.WorldState.c }

@[implicit_reducible]

instance ScontrasTonhauser2025.instHasBeliefWorldState : Semantics.Attitudes.Factivity.HasBelief WorldState

Equations

• ScontrasTonhauser2025.instHasBeliefWorldState = { bel := ScontrasTonhauser2025.WorldState.bel }

inductive ScontrasTonhauser2025.Utterance : Type

Attitude verb utterances about Cole's mental state, plus bare complement assertions.

• knowPos : Utterance
• knowNeg : Utterance
• thinkPos : Utterance
• thinkNeg : Utterance
• cPos : Utterance
• cNeg : Utterance

@[implicit_reducible]

instance ScontrasTonhauser2025.instDecidableEqUtterance : DecidableEq Utterance

Equations

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

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

Equations

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

@[implicit_reducible]

instance ScontrasTonhauser2025.instReprUtterance : Repr Utterance

Equations

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

@[implicit_reducible]

instance ScontrasTonhauser2025.instInhabitedUtterance : Inhabited Utterance

Equations

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

@[implicit_reducible]

instance ScontrasTonhauser2025.instFintypeUtterance : Fintype Utterance

Equations

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

Literal truth conditions (from Factivity)

def ScontrasTonhauser2025.literalMeaning : Utterance → WorldState → Bool

Literal truth conditions derived from factive/non-factive semantics.

"know" is factive: factivePos = BEL ∧ C "think" is non-factive: nonFactivePos = BEL "C" / "not C" are direct assertions about the complement.

Equations

• ScontrasTonhauser2025.literalMeaning ScontrasTonhauser2025.Utterance.knowPos = Semantics.Attitudes.Factivity.factivePos
• ScontrasTonhauser2025.literalMeaning ScontrasTonhauser2025.Utterance.knowNeg = Semantics.Attitudes.Factivity.factiveNeg
• ScontrasTonhauser2025.literalMeaning ScontrasTonhauser2025.Utterance.thinkPos = Semantics.Attitudes.Factivity.nonFactivePos
• ScontrasTonhauser2025.literalMeaning ScontrasTonhauser2025.Utterance.thinkNeg = Semantics.Attitudes.Factivity.nonFactiveNeg
• ScontrasTonhauser2025.literalMeaning ScontrasTonhauser2025.Utterance.cPos = Semantics.Attitudes.Factivity.HasComplement.c
• ScontrasTonhauser2025.literalMeaning ScontrasTonhauser2025.Utterance.cNeg = fun (w : ScontrasTonhauser2025.WorldState) => !Semantics.Attitudes.Factivity.HasComplement.c w

Speaker belief states (the 15 non-empty subsets of W)

inductive ScontrasTonhauser2025.BeliefState : Type

Speaker's private assumptions: all 15 non-empty subsets of W. Section 3 follows [QGL16]: A ranges over all non-empty subsets of the world space.

• onlyW11 : BeliefState
• onlyW10 : BeliefState
• onlyW01 : BeliefState
• onlyW00 : BeliefState
• belTrue : BeliefState
• belFalse : BeliefState
• cTrue : BeliefState
• cFalse : BeliefState
• diagonal : BeliefState
• antiDiagonal : BeliefState
• notW11 : BeliefState
• notW10 : BeliefState
• notW01 : BeliefState
• notW00 : BeliefState
• all : BeliefState

@[implicit_reducible]

instance ScontrasTonhauser2025.instDecidableEqBeliefState : DecidableEq BeliefState

Equations

• ScontrasTonhauser2025.instDecidableEqBeliefState x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def ScontrasTonhauser2025.instReprBeliefState.repr : BeliefState → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance ScontrasTonhauser2025.instReprBeliefState : Repr BeliefState

Equations

• ScontrasTonhauser2025.instReprBeliefState = { reprPrec := ScontrasTonhauser2025.instReprBeliefState.repr }

@[implicit_reducible]

instance ScontrasTonhauser2025.instInhabitedBeliefState : Inhabited BeliefState

Equations

• ScontrasTonhauser2025.instInhabitedBeliefState = { default := ScontrasTonhauser2025.instInhabitedBeliefState.default }

@[implicit_reducible]

instance ScontrasTonhauser2025.instFintypeBeliefState : Fintype BeliefState

Equations

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

def ScontrasTonhauser2025.speakerCredenceBool : BeliefState → WorldState → Bool

Membership in belief state. Boolean operations on WorldState fields reduce cleanly under kernel evaluation.

Equations

• ScontrasTonhauser2025.speakerCredenceBool ScontrasTonhauser2025.BeliefState.all x✝ = true
• ScontrasTonhauser2025.speakerCredenceBool ScontrasTonhauser2025.BeliefState.onlyW11 x✝ = (x✝.bel && x✝.c)
• ScontrasTonhauser2025.speakerCredenceBool ScontrasTonhauser2025.BeliefState.onlyW10 x✝ = (x✝.bel && !x✝.c)
• ScontrasTonhauser2025.speakerCredenceBool ScontrasTonhauser2025.BeliefState.onlyW01 x✝ = (!x✝.bel && x✝.c)
• ScontrasTonhauser2025.speakerCredenceBool ScontrasTonhauser2025.BeliefState.onlyW00 x✝ = (!x✝.bel && !x✝.c)
• ScontrasTonhauser2025.speakerCredenceBool ScontrasTonhauser2025.BeliefState.belTrue x✝ = x✝.bel
• ScontrasTonhauser2025.speakerCredenceBool ScontrasTonhauser2025.BeliefState.belFalse x✝ = !x✝.bel
• ScontrasTonhauser2025.speakerCredenceBool ScontrasTonhauser2025.BeliefState.cTrue x✝ = x✝.c
• ScontrasTonhauser2025.speakerCredenceBool ScontrasTonhauser2025.BeliefState.cFalse x✝ = !x✝.c
• ScontrasTonhauser2025.speakerCredenceBool ScontrasTonhauser2025.BeliefState.diagonal x✝ = (x✝.bel && x✝.c || !x✝.bel && !x✝.c)
• ScontrasTonhauser2025.speakerCredenceBool ScontrasTonhauser2025.BeliefState.antiDiagonal x✝ = (!x✝.bel && x✝.c || x✝.bel && !x✝.c)
• ScontrasTonhauser2025.speakerCredenceBool ScontrasTonhauser2025.BeliefState.notW11 x✝ = !(x✝.bel && x✝.c)
• ScontrasTonhauser2025.speakerCredenceBool ScontrasTonhauser2025.BeliefState.notW10 x✝ = !(x✝.bel && !x✝.c)
• ScontrasTonhauser2025.speakerCredenceBool ScontrasTonhauser2025.BeliefState.notW01 x✝ = !(!x✝.bel && x✝.c)
• ScontrasTonhauser2025.speakerCredenceBool ScontrasTonhauser2025.BeliefState.notW00 x✝ = !(!x✝.bel && !x✝.c)

def ScontrasTonhauser2025.assumesC : BeliefState → Bool

Whether C is true in all worlds of the belief state.

Equations

• ScontrasTonhauser2025.assumesC ScontrasTonhauser2025.BeliefState.onlyW11 = true
• ScontrasTonhauser2025.assumesC ScontrasTonhauser2025.BeliefState.onlyW01 = true
• ScontrasTonhauser2025.assumesC ScontrasTonhauser2025.BeliefState.cTrue = true
• ScontrasTonhauser2025.assumesC x✝ = false

Priors

def ScontrasTonhauser2025.worldPrior (pC : ℚ≥0) : WorldState → ℚ≥0

World prior parameterized by P(C). P(BEL, C) = P(BEL | C) · P(C), with P(BEL | C) = 1/2.

Equations

• ScontrasTonhauser2025.worldPrior pC ScontrasTonhauser2025.WorldState.w11 = pC / 2
• ScontrasTonhauser2025.worldPrior pC ScontrasTonhauser2025.WorldState.w01 = pC / 2
• ScontrasTonhauser2025.worldPrior pC ScontrasTonhauser2025.WorldState.w10 = (1 - pC) / 2
• ScontrasTonhauser2025.worldPrior pC ScontrasTonhauser2025.WorldState.w00 = (1 - pC) / 2

theorem ScontrasTonhauser2025.worldPrior_sum {pC : ℚ≥0} (h1 : pC ≤ 1) : worldPrior pC WorldState.w11 + worldPrior pC WorldState.w10 + worldPrior pC WorldState.w01 + worldPrior pC WorldState.w00 = 1

World prior sums to 1 whenever P(C) is a probability.

The score chain

def ScontrasTonhauser2025.l0Score (pC : ℚ≥0) (bs : BeliefState) (u : Utterance) : WorldState → ℚ≥0

Literal listener within the assumption set (eq. 5): prior conditioned on worlds where u is true, empty extensions normalizing to zero rows.

Equations

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

def ScontrasTonhauser2025.qAgg (qud : Semantics.Attitudes.Factivity.QUD) (pC : ℚ≥0) (bs : BeliefState) (u : Utterance) : WorldState → ℚ≥0

QUD aggregation of the literal listener (eq. 5).

Equations

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

def ScontrasTonhauser2025.s1Post (qud : Semantics.Attitudes.Factivity.QUD) (pC : ℚ≥0) (bs : BeliefState) : WorldState → Utterance → ℚ≥0

Speaker (eq. 6 at α = 10, zero cost): RSA.Score.s1 over the QUD-aggregated literal listener; degenerate cells fall back to cPos — one declaration covering both faces.

Equations

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

def ScontrasTonhauser2025.worldScore (qud : Semantics.Attitudes.Factivity.QUD) (pC : ℚ≥0) (u : Utterance) (w : WorldState) : ℚ≥0

Listener world score (eq. 7; uniform assumption prior).

Equations

• ScontrasTonhauser2025.worldScore qud pC u w = ScontrasTonhauser2025.worldPrior pC w * ∑ bs : ScontrasTonhauser2025.BeliefState, ScontrasTonhauser2025.s1Post qud pC bs w u

noncomputable def ScontrasTonhauser2025.l1World (qud : Semantics.Attitudes.Factivity.QUD) (pC : ℚ≥0) (u : Utterance) : PMF WorldState

Pragmatic listener over worlds (eq. 7).

Equations

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

noncomputable def ScontrasTonhauser2025.l1CEvent (qud : Semantics.Attitudes.Factivity.QUD) (pC : ℚ≥0) (u : Utterance) : ENNReal

The listener's C-marginal.

Equations

• ScontrasTonhauser2025.l1CEvent qud pC u = ∑' (w : ScontrasTonhauser2025.WorldState), if w.c = true then (ScontrasTonhauser2025.l1World qud pC u) w else 0

Listener predictions

theorem ScontrasTonhauser2025.bel_qud_marginal_eq_prior_high (u : Utterance) : l1CEvent Semantics.Attitudes.Factivity.QUD.bel (2 / 3) u = ↑↑(2 / 3)

Under the BEL? QUD the C-marginal equals the prior, for every utterance: S1 depends on the world only through its BEL-cell, so the C-dimension washes out of the world posterior. Projection is invisible at the world marginal.

theorem ScontrasTonhauser2025.bel_qud_marginal_eq_prior_low (u : Utterance) : l1CEvent Semantics.Attitudes.Factivity.QUD.bel (1 / 3) u = ↑↑(1 / 3)

The low-prior analogue of bel_qud_marginal_eq_prior_high.

theorem ScontrasTonhauser2025.c_qud_thinkNeg_higher : l1CEvent Semantics.Attitudes.Factivity.QUD.c (2 / 3) Utterance.knowNeg < l1CEvent Semantics.Attitudes.Factivity.QUD.c (2 / 3) Utterance.thinkNeg

Under the C? QUD, knowNeg is evidence against C — ¬(BEL∧C) is compatible with C-false worlds — so thinkNeg preserves P(C) better.

Prediction 2a: utterance effect (know > think)

The paper derives 2a with utterance cost (Figure 7a); the cost-free model does not — under BEL? both marginals sit at the prior, and under C? the direction reverses (c_qud_thinkNeg_higher). Fn. 11's A-marginal measure (P(A ⊧ C | u)) may capture the effect without cost; see the module TODO.

theorem ScontrasTonhauser2025.prediction_2b : l1CEvent Semantics.Attitudes.Factivity.QUD.c (1 / 3) Utterance.knowNeg < l1CEvent Semantics.Attitudes.Factivity.QUD.c (2 / 3) Utterance.knowNeg

Prediction 2b (prior effect): higher prior increases projection.

theorem ScontrasTonhauser2025.prediction_2c : l1CEvent Semantics.Attitudes.Factivity.QUD.c (2 / 3) Utterance.knowNeg < l1CEvent Semantics.Attitudes.Factivity.QUD.bel (2 / 3) Utterance.knowNeg

Prediction 2c (QUD effect): under BEL? the C-marginal stays at the prior (bel_qud_marginal_eq_prior_high), while under C? the literal semantics of "doesn't know C" lowers it.

Structural properties

theorem ScontrasTonhauser2025.know_entails_c (w : WorldState) : literalMeaning Utterance.knowPos w = true → w.c = true

"know" entails C (from factivePos_entails_c).

theorem ScontrasTonhauser2025.think_not_entails_c : ∃ (w : WorldState), literalMeaning Utterance.thinkPos w = true ∧ w.c = false

"think" does NOT entail C.

theorem ScontrasTonhauser2025.know_entails_bel (w : WorldState) : literalMeaning Utterance.knowPos w = true → w.bel = true

"know" entails BEL (from factivePos_entails_bel).

theorem ScontrasTonhauser2025.know_entails_think (w : WorldState) : literalMeaning Utterance.knowPos w = true → literalMeaning Utterance.thinkPos w = true

Know entails think (factivity is strictly stronger than belief).

theorem ScontrasTonhauser2025.knowNeg_semantics : literalMeaning Utterance.knowNeg WorldState.w11 = false ∧ literalMeaning Utterance.knowNeg WorldState.w10 = true ∧ literalMeaning Utterance.knowNeg WorldState.w01 = true ∧ literalMeaning Utterance.knowNeg WorldState.w00 = true

knowNeg (= ¬(BEL∧C)) is true at all worlds except w11.

theorem ScontrasTonhauser2025.thinkNeg_semantics : literalMeaning Utterance.thinkNeg WorldState.w11 = false ∧ literalMeaning Utterance.thinkNeg WorldState.w10 = false ∧ literalMeaning Utterance.thinkNeg WorldState.w01 = true ∧ literalMeaning Utterance.thinkNeg WorldState.w00 = true

thinkNeg (= ¬BEL) is true only at worlds where Cole doesn't believe.

theorem ScontrasTonhauser2025.knowNeg_weaker_than_thinkNeg : {w : WorldState | literalMeaning Utterance.knowNeg w = true}.card > {w : WorldState | literalMeaning Utterance.thinkNeg w = true}.card

knowNeg is compatible with strictly more worlds than thinkNeg (3 vs 2), making it the weaker (less informative) negation.

theorem ScontrasTonhauser2025.assumesC_matches_generic (bs : BeliefState) : assumesC bs = Semantics.Attitudes.Factivity.assumesComplement (speakerCredenceBool bs) [WorldState.w11, WorldState.w10, WorldState.w01, WorldState.w00]

The pattern-matched assumesC agrees with the generic assumesComplement from Factivity.

theorem ScontrasTonhauser2025.three_of_fifteen_assume_c : {bs : BeliefState | assumesC bs = true}.card = 3

Exactly 3 of 15 belief states assume C: onlyW11, onlyW01, cTrue.

Experimental data

structure ScontrasTonhauser2025.UtteranceEffect : Type

Effect size from a linear mixed-effects model. p values are upper bounds (paper reports "< .001").

• β : ℚ
• se : ℚ
• t : ℚ
• p : ℚ

def ScontrasTonhauser2025.instReprUtteranceEffect.repr : UtteranceEffect → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance ScontrasTonhauser2025.instReprUtteranceEffect : Repr UtteranceEffect

Equations

• ScontrasTonhauser2025.instReprUtteranceEffect = { reprPrec := ScontrasTonhauser2025.instReprUtteranceEffect.repr }

def ScontrasTonhauser2025.exp1_utteranceEffect : UtteranceEffect

Exp 1: Utterance effect (know > think).

Equations

• ScontrasTonhauser2025.exp1_utteranceEffect = { β := 0.35, se := 3e-2, t := 12.2, p := 1e-3 }

def ScontrasTonhauser2025.exp1_priorEffect : UtteranceEffect

Exp 1: Prior effect (higher > lower).

Equations

• ScontrasTonhauser2025.exp1_priorEffect = { β := 0.16, se := 3e-2, t := 5.5, p := 1e-3 }

def ScontrasTonhauser2025.exp1_qudEffect : UtteranceEffect

Exp 1: QUD effect (NOT significant — manipulation too weak).

Equations

• ScontrasTonhauser2025.exp1_qudEffect = { β := 9e-3, se := 3e-2, t := 0.3, p := 0.75 }

def ScontrasTonhauser2025.exp2_utteranceEffect : UtteranceEffect

Exp 2: Utterance effect (know > think).

Equations

• ScontrasTonhauser2025.exp2_utteranceEffect = { β := 0.34, se := 4e-2, t := 8.8, p := 1e-3 }

def ScontrasTonhauser2025.exp2_qudEffect : UtteranceEffect

Exp 2: QUD effect (significant with stronger manipulation).

Equations

• ScontrasTonhauser2025.exp2_qudEffect = { β := 0.14, se := 4e-2, t := 3.6, p := 1e-3 }

inductive ScontrasTonhauser2025.Hypothesis : Type

• utterance : Hypothesis
• prior : Hypothesis
• qud : Hypothesis

@[implicit_reducible]

instance ScontrasTonhauser2025.instDecidableEqHypothesis : DecidableEq Hypothesis

Equations

• ScontrasTonhauser2025.instDecidableEqHypothesis x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance ScontrasTonhauser2025.instReprHypothesis : Repr Hypothesis

Equations

• ScontrasTonhauser2025.instReprHypothesis = { reprPrec := ScontrasTonhauser2025.instReprHypothesis.repr }

def ScontrasTonhauser2025.instReprHypothesis.repr : Hypothesis → ℕ → Std.Format

Equations

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

def ScontrasTonhauser2025.supported : Hypothesis → Bool × Bool

Which experiments support each hypothesis. Exp 1: (2a) yes, (2b) yes, (2c) no (QUD not significant). Exp 2: (2a) yes, (2b) not tested, (2c) yes.

Equations

• ScontrasTonhauser2025.supported ScontrasTonhauser2025.Hypothesis.utterance = (true, true)
• ScontrasTonhauser2025.supported ScontrasTonhauser2025.Hypothesis.prior = (true, false)
• ScontrasTonhauser2025.supported ScontrasTonhauser2025.Hypothesis.qud = (false, true)

def ScontrasTonhauser2025.directionCorrect : Hypothesis → Bool

Equations

• ScontrasTonhauser2025.directionCorrect ScontrasTonhauser2025.Hypothesis.utterance = decide (ScontrasTonhauser2025.exp1_utteranceEffect.β > 0)
• ScontrasTonhauser2025.directionCorrect ScontrasTonhauser2025.Hypothesis.prior = decide (ScontrasTonhauser2025.exp1_priorEffect.β > 0)
• ScontrasTonhauser2025.directionCorrect ScontrasTonhauser2025.Hypothesis.qud = decide (ScontrasTonhauser2025.exp2_qudEffect.β > 0)

BToM bridge

def ScontrasTonhauser2025.beliefStateCategory : Core.LatentCategory

Classification of BeliefState in BToM terms.

Equations

• ScontrasTonhauser2025.beliefStateCategory = Core.LatentCategory.mental

def ScontrasTonhauser2025.qudCategory : Core.LatentCategory

Classification of QUD in BToM terms.

Equations

• ScontrasTonhauser2025.qudCategory = Core.LatentCategory.shared

def ScontrasTonhauser2025.assumesCIndicator : BeliefState → ℚ

Characteristic function: does the speaker assume C?

Equations

• ScontrasTonhauser2025.assumesCIndicator bs = if ScontrasTonhauser2025.assumesC bs = true then 1 else 0

theorem ScontrasTonhauser2025.assumesCIndicator_pos (bs : BeliefState) (h : assumesC bs = true) : assumesCIndicator bs = 1

Belief states that assume C have indicator 1.

theorem ScontrasTonhauser2025.assumesCIndicator_neg (bs : BeliefState) (h : assumesC bs = false) : assumesCIndicator bs = 0

Belief states that don't assume C have indicator 0.

theorem ScontrasTonhauser2025.assumesCIndicator_classification : assumesCIndicator BeliefState.onlyW11 = 1 ∧ assumesCIndicator BeliefState.onlyW01 = 1 ∧ assumesCIndicator BeliefState.cTrue = 1 ∧ assumesCIndicator BeliefState.onlyW10 = 0 ∧ assumesCIndicator BeliefState.onlyW00 = 0 ∧ assumesCIndicator BeliefState.belTrue = 0 ∧ assumesCIndicator BeliefState.belFalse = 0 ∧ assumesCIndicator BeliefState.cFalse = 0 ∧ assumesCIndicator BeliefState.diagonal = 0 ∧ assumesCIndicator BeliefState.antiDiagonal = 0 ∧ assumesCIndicator BeliefState.notW11 = 0 ∧ assumesCIndicator BeliefState.notW10 = 0 ∧ assumesCIndicator BeliefState.notW01 = 0 ∧ assumesCIndicator BeliefState.notW00 = 0 ∧ assumesCIndicator BeliefState.all = 0

The three C-entailing belief states have indicator 1; the remaining twelve have indicator 0.

Model–data connection

theorem ScontrasTonhauser2025.model_predicts_effects : l1CEvent Semantics.Attitudes.Factivity.QUD.c (2 / 3) Utterance.knowNeg > l1CEvent Semantics.Attitudes.Factivity.QUD.c (1 / 3) Utterance.knowNeg ∧ l1CEvent Semantics.Attitudes.Factivity.QUD.bel (2 / 3) Utterance.knowNeg > l1CEvent Semantics.Attitudes.Factivity.QUD.c (2 / 3) Utterance.knowNeg ∧ directionCorrect Hypothesis.prior = true ∧ directionCorrect Hypothesis.qud = true

Predictions (2b) and (2c) match experimental effect directions. Prediction (2a) requires cost; see the commentary above.

Connection to [DT21]

theorem ScontrasTonhauser2025.prior_effect_consistent_with_dt2021 : exp1_priorEffect.β > 0

The prior effect found by S&T 2025 (β = 0.16 > 0) replicates the positive prior effect of [DT21] (β = 0.14 categorical, β = 0.28 individual): higher prior probability of the complement content leads to stronger projection. [DT21] makes this structural — any prior-sensitive (monotone) account predicts the modulation (DegenTonhauser2021.sensitive_predicts_modulation) — and the RSA model's prediction_2b provides the same explanation here.

Compositional filtering vs BToM

Compares the BToM model against compositional filtering ([Hei83]): presuppositions project through connectives via local context computation; the filtering presupposition of "if A then B_p" is "A → p".

The key empirical argument: the BToM model predicts that even non-factive "think" — which has NO presupposition to filter — exhibits projection effects, because L1 can still infer what the speaker takes for granted. Compositional filtering predicts a trivial presupposition for non-presuppositional items.

def ScontrasTonhauser2025.filteringPrediction_know {W : Type u_1} (a c : W → Prop) : Semantics.Presupposition.PartialProp W

The filtering prediction for "if A then know-C": the presupposition of the consequent (= C) is filtered by the antecedent. Result: conditional presupposes "A → C".

Equations

• ScontrasTonhauser2025.filteringPrediction_know a c = (Semantics.Presupposition.PartialProp.ofProp a).impFilter (Semantics.Presupposition.PartialProp.condAssert c fun (x : W) => True)

def ScontrasTonhauser2025.filteringPrediction_think {W : Type u_1} (a : W → Prop) : Semantics.Presupposition.PartialProp W

The filtering prediction for "if A then think-C": "think" has no presupposition, so filtering produces a trivial result.

Equations

• ScontrasTonhauser2025.filteringPrediction_think a = (Semantics.Presupposition.PartialProp.ofProp a).impFilter Semantics.Presupposition.PartialProp.top

theorem ScontrasTonhauser2025.filtering_know_nontrivial {W : Type u_1} (a c : W → Prop) (h : ∃ (w : W), a w ∧ ¬c w) : ∃ (w : W), ¬(filteringPrediction_know a c).presup w

Filtering predicts non-trivial presupposition for "know": The presupposition of "if A then know-C" is ¬A ∨ C (= A → C), which is NOT tautological.

theorem ScontrasTonhauser2025.filtering_think_trivial {W : Type u_1} (a : W → Prop) (w : W) : (filteringPrediction_think a).presup w

Filtering predicts TRIVIAL presupposition for "think": The presupposition of "if A then think-C" is always true, regardless of A, because "think" contributes no presupposition.

structure ScontrasTonhauser2025.ProjectionPrediction : Type

BToM predicts projection effects for ANY verb in conditional environments, because projection arises from pragmatic reasoning about the speaker's private assumptions, not from lexical presupposition.

The key mechanism: when A and C are related (correlated in the prior), the listener infers that a speaker who utters "if A, X Vs C" likely takes C for granted — regardless of whether V is factive.

• factive_projects : Bool

  Whether projection is predicted for factive verbs in conditionals.

• nonFactive_projects : Bool

  Whether projection is predicted for non-factive verbs in conditionals.

• relatedness_modulates : Bool

  Whether relatedness modulates projection strength.

def ScontrasTonhauser2025.btomPrediction : ProjectionPrediction

BToM predictions: both factive and non-factive show conditional presupposition, modulated by relatedness.

Equations

• ScontrasTonhauser2025.btomPrediction = { factive_projects := true, nonFactive_projects := true, relatedness_modulates := true }

def ScontrasTonhauser2025.filteringPrediction : ProjectionPrediction

Filtering predictions: only factive shows conditional presupposition, with no role for relatedness (it's purely structural).

Equations

• ScontrasTonhauser2025.filteringPrediction = { factive_projects := true, nonFactive_projects := false, relatedness_modulates := false }

theorem ScontrasTonhauser2025.btom_subsumes_filtering : btomPrediction.factive_projects = filteringPrediction.factive_projects ∧ btomPrediction.nonFactive_projects = true ∧ filteringPrediction.nonFactive_projects = false ∧ btomPrediction.relatedness_modulates = true ∧ filteringPrediction.relatedness_modulates = false

Strict subsumption: BToM predicts everything filtering predicts (factive conditional presupposition) plus more (non-factive conditional presupposition, relatedness modulation).

theorem ScontrasTonhauser2025.critical_divergence_at_nonfactive : filteringPrediction.nonFactive_projects ≠ btomPrediction.nonFactive_projects

The critical divergence: For non-factive "think" in conditionals, filtering predicts trivial presupposition (no projection), while BToM predicts non-trivial projection modulated by relatedness.

This is the [ST25] argument: if projection were due to compositional filtering alone, non-presuppositional items like "think" should show no effect. But BToM predicts projection effects even for "think", because L1 infers the speaker's private assumptions regardless of the verb's factivity status.

theorem ScontrasTonhauser2025.filtering_is_limiting_case {W : Type u_1} (a c : W → Prop) (h_entails : ∀ (w : W), a w → c w) (w : W) : (filteringPrediction_know a c).presup w

Filtering is a special case: When relatedness is maximal (A entails C), BToM's projection prediction converges to the filtering prediction. Filtering captures the structural component; BToM adds the probabilistic modulation.