Documentation

Linglib.Phenomena.Presupposition.Studies.ScontrasTonhauser2025

@cite{scontras-tonhauser-2025} #

Projection emerges from RSA over speaker's private assumptions, not lexical presupposition. L1 jointly infers world state and speaker's belief state.

The Model (Section 3) #

L0 (eq. 5): L0(Q(w)|u,A,Q) ∝ Σ_{w'∈A∩⟦u⟧, Q(w')=Q(w)} P(w')
S1 (eq. 6): S1(u|w,A,Q) ∝ exp(α(log L0(Q(w)|u,A,Q) − C(u)))
L1 (eq. 7): L1(w,A|u,Q) ∝ S1(u|w,A,Q) · P(w) · P(A)

Domain: 6 utterances × 4 worlds × 15 belief states × 2 QUDs. α = 10.

Section 3 Parameters (fn. 12) #

Belief states A: all 15 non-empty subsets of W (following @cite{qing-goodman-lassiter-2016})
Prior over A: uniform
α = 10
P(C): 2/3 (higher) or 1/3 (lower); P(BEL|C) = 1/2

Cost (complex = 2×simple) is omitted: exp(−αC) with α = 10 introduces irrational numbers incompatible with ℚ arithmetic. Cost omission affects S1's normalization even for same-cost comparisons, reversing the direction of prediction (2a); the full model with cost predicts know > think (Figure 7a). Predictions (2b) and (2c) are robust to cost omission.

Factive Semantics #

Literal truth conditions derive from Semantics.Attitudes.Factivity: know = factivePos (BEL ∧ C), think = nonFactivePos (BEL).

Key Structural Insight #

Under QUD=BEL?, L1's world-marginal P(C|u) = P(C) for all utterances — a mathematical identity. S1 scores depend on w only through w.bel, so the complement dimension washes out in the marginal. Prediction 2b (prior effect) therefore comes from the C? QUD condition; prediction 2c (QUD effect) compares the uninformative BEL? marginal against the C? marginal.

BToM Connection #

This is a BToM model: L1 inverts S1's generative model to jointly infer the speaker's belief state and the world state.

Experimental Results #

Exp 1 confirms (2a) utterance effect (β = 0.35, p < .001) and (2b) prior effect (β = 0.16, p < .001). The QUD manipulation was not significant (β = 0.009, p = .75). Exp 2 confirms (2a) utterance effect (β = 0.34, p < .001) and (2c) QUD effect (β = 0.14, p < .001) with a stronger QUD manipulation. Exp 2 did not manipulate prior probability.

Connection to @cite{degen-tonhauser-2021} #

The prior effect (prediction 2b) replicates the core finding of @cite{degen-tonhauser-2021}: higher prior probability of complement content leads to stronger projection. D&T 2021 demonstrate this across 20 predicates with β = 0.14 (categorical) / β = 0.28 (individual-level). S&T 2025's RSA model provides the theoretical explanation: L1's Bayesian inference naturally incorporates prior beliefs, so higher priors yield higher posteriors.

inductive Phenomena.Presupposition.Studies.ScontrasTonhauser2025.WorldState :

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

Instances For

instance Phenomena.Presupposition.Studies.ScontrasTonhauser2025.instDecidableEqWorldState :

DecidableEq WorldState

Equations

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

instance Phenomena.Presupposition.Studies.ScontrasTonhauser2025.instReprWorldState :

Repr WorldState

Equations

Phenomena.Presupposition.Studies.ScontrasTonhauser2025.instReprWorldState = { reprPrec := Phenomena.Presupposition.Studies.ScontrasTonhauser2025.instReprWorldState.repr }

def Phenomena.Presupposition.Studies.ScontrasTonhauser2025.instReprWorldState.repr :

WorldState → ℕ → Std.Format

Equations

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

Instances For

instance Phenomena.Presupposition.Studies.ScontrasTonhauser2025.instBEqWorldState :

Equations

Phenomena.Presupposition.Studies.ScontrasTonhauser2025.instBEqWorldState = { beq := Phenomena.Presupposition.Studies.ScontrasTonhauser2025.instBEqWorldState.beq }

def Phenomena.Presupposition.Studies.ScontrasTonhauser2025.instBEqWorldState.beq :

WorldState → WorldState → Bool

Equations

Phenomena.Presupposition.Studies.ScontrasTonhauser2025.instBEqWorldState.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

instance Phenomena.Presupposition.Studies.ScontrasTonhauser2025.instInhabitedWorldState :

Inhabited WorldState

Equations

Phenomena.Presupposition.Studies.ScontrasTonhauser2025.instInhabitedWorldState = { default := Phenomena.Presupposition.Studies.ScontrasTonhauser2025.instInhabitedWorldState.default }

def Phenomena.Presupposition.Studies.ScontrasTonhauser2025.instInhabitedWorldState.default :

Equations

Phenomena.Presupposition.Studies.ScontrasTonhauser2025.instInhabitedWorldState.default = Phenomena.Presupposition.Studies.ScontrasTonhauser2025.WorldState.w11

Instances For

instance Phenomena.Presupposition.Studies.ScontrasTonhauser2025.instFintypeWorldState :

Fintype WorldState

Equations

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

instance Phenomena.Presupposition.Studies.ScontrasTonhauser2025.instHasComplementWorldState :

Semantics.Attitudes.Factivity.HasComplement WorldState

Equations

Phenomena.Presupposition.Studies.ScontrasTonhauser2025.instHasComplementWorldState = { c := Phenomena.Presupposition.Studies.ScontrasTonhauser2025.WorldState.c }

instance Phenomena.Presupposition.Studies.ScontrasTonhauser2025.instHasBeliefWorldState :

Semantics.Attitudes.Factivity.HasBelief WorldState

Equations

Phenomena.Presupposition.Studies.ScontrasTonhauser2025.instHasBeliefWorldState = { bel := Phenomena.Presupposition.Studies.ScontrasTonhauser2025.WorldState.bel }

inductive Phenomena.Presupposition.Studies.ScontrasTonhauser2025.Utterance :

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

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

Instances For

instance Phenomena.Presupposition.Studies.ScontrasTonhauser2025.instDecidableEqUtterance :

DecidableEq Utterance

Equations

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

instance Phenomena.Presupposition.Studies.ScontrasTonhauser2025.instReprUtterance :

Equations

Phenomena.Presupposition.Studies.ScontrasTonhauser2025.instReprUtterance = { reprPrec := Phenomena.Presupposition.Studies.ScontrasTonhauser2025.instReprUtterance.repr }

def Phenomena.Presupposition.Studies.ScontrasTonhauser2025.instReprUtterance.repr :

Utterance → ℕ → Std.Format

Equations

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

Instances For

instance Phenomena.Presupposition.Studies.ScontrasTonhauser2025.instBEqUtterance :

Equations

Phenomena.Presupposition.Studies.ScontrasTonhauser2025.instBEqUtterance = { beq := Phenomena.Presupposition.Studies.ScontrasTonhauser2025.instBEqUtterance.beq }

def Phenomena.Presupposition.Studies.ScontrasTonhauser2025.instBEqUtterance.beq :

Utterance → Utterance → Bool

Equations

Phenomena.Presupposition.Studies.ScontrasTonhauser2025.instBEqUtterance.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

def Phenomena.Presupposition.Studies.ScontrasTonhauser2025.instInhabitedUtterance.default :

Equations

Phenomena.Presupposition.Studies.ScontrasTonhauser2025.instInhabitedUtterance.default = Phenomena.Presupposition.Studies.ScontrasTonhauser2025.Utterance.knowPos

Instances For

instance Phenomena.Presupposition.Studies.ScontrasTonhauser2025.instInhabitedUtterance :

Inhabited Utterance

Equations

Phenomena.Presupposition.Studies.ScontrasTonhauser2025.instInhabitedUtterance = { default := Phenomena.Presupposition.Studies.ScontrasTonhauser2025.instInhabitedUtterance.default }

instance Phenomena.Presupposition.Studies.ScontrasTonhauser2025.instFintypeUtterance :

Fintype Utterance

Equations

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

def Phenomena.Presupposition.Studies.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

Instances For

inductive Phenomena.Presupposition.Studies.ScontrasTonhauser2025.BeliefState :

Speaker's private assumptions: all 15 non-empty subsets of W. Section 3 follows @cite{qing-goodman-lassiter-2016}: 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

Instances For

instance Phenomena.Presupposition.Studies.ScontrasTonhauser2025.instDecidableEqBeliefState :

DecidableEq BeliefState

Equations

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

def Phenomena.Presupposition.Studies.ScontrasTonhauser2025.instReprBeliefState.repr :

BeliefState → ℕ → Std.Format

Equations

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

Instances For

instance Phenomena.Presupposition.Studies.ScontrasTonhauser2025.instReprBeliefState :

Repr BeliefState

Equations

Phenomena.Presupposition.Studies.ScontrasTonhauser2025.instReprBeliefState = { reprPrec := Phenomena.Presupposition.Studies.ScontrasTonhauser2025.instReprBeliefState.repr }

instance Phenomena.Presupposition.Studies.ScontrasTonhauser2025.instBEqBeliefState :

BEq BeliefState

Equations

Phenomena.Presupposition.Studies.ScontrasTonhauser2025.instBEqBeliefState = { beq := Phenomena.Presupposition.Studies.ScontrasTonhauser2025.instBEqBeliefState.beq }

def Phenomena.Presupposition.Studies.ScontrasTonhauser2025.instBEqBeliefState.beq :

BeliefState → BeliefState → Bool

Equations

Phenomena.Presupposition.Studies.ScontrasTonhauser2025.instBEqBeliefState.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

def Phenomena.Presupposition.Studies.ScontrasTonhauser2025.instInhabitedBeliefState.default :

Equations

Phenomena.Presupposition.Studies.ScontrasTonhauser2025.instInhabitedBeliefState.default = Phenomena.Presupposition.Studies.ScontrasTonhauser2025.BeliefState.onlyW11

Instances For

instance Phenomena.Presupposition.Studies.ScontrasTonhauser2025.instInhabitedBeliefState :

Inhabited BeliefState

Equations

Phenomena.Presupposition.Studies.ScontrasTonhauser2025.instInhabitedBeliefState = { default := Phenomena.Presupposition.Studies.ScontrasTonhauser2025.instInhabitedBeliefState.default }

instance Phenomena.Presupposition.Studies.ScontrasTonhauser2025.instFintypeBeliefState :

Fintype BeliefState

Equations

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

def Phenomena.Presupposition.Studies.ScontrasTonhauser2025.speakerCredenceBool :

BeliefState → WorldState → Bool

Membership in belief state. Boolean operations on WorldState fields reduce cleanly for rsa_predict.

Equations

Instances For

def Phenomena.Presupposition.Studies.ScontrasTonhauser2025.assumesC :

BeliefState → Bool

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

Equations

Instances For

def Phenomena.Presupposition.Studies.ScontrasTonhauser2025.qudAggregate (qud : Semantics.Attitudes.Factivity.QUD) (f : WorldState → ℝ) (w : WorldState) :

QUD aggregation: sums L0 probabilities over the QUD equivalence class of w. Named qudAggregate to distinguish from Factivity.qudProject (the equivalence relation, not the aggregation).

BEL? QUD: partitions by BEL → sums over same-BEL worlds
C? QUD: partitions by C → sums over same-C worlds

Equations

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

Instances For

theorem Phenomena.Presupposition.Studies.ScontrasTonhauser2025.qudAggregate_nonneg {qud : Semantics.Attitudes.Factivity.QUD} {f : WorldState → ℝ} {w : WorldState} (hf : ∀ (w : WorldState), 0 ≤ f w) :

0 ≤ qudAggregate qud f w

def Phenomena.Presupposition.Studies.ScontrasTonhauser2025.worldPriorQ (pC : ℚ) :

WorldState → ℚ

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

Equations

Instances For

theorem Phenomena.Presupposition.Studies.ScontrasTonhauser2025.worldPriorQ_nonneg (pC : ℚ) (h0 : 0 ≤ pC) (h1 : pC ≤ 1) (w : WorldState) :

0 ≤ worldPriorQ pC w

theorem Phenomena.Presupposition.Studies.ScontrasTonhauser2025.worldPriorQ_sum (pC : ℚ) :

worldPriorQ pC WorldState.w11 + worldPriorQ pC WorldState.w10 + worldPriorQ pC WorldState.w01 + worldPriorQ pC WorldState.w00 = 1

World prior sums to 1 for any P(C).

noncomputable def Phenomena.Presupposition.Studies.ScontrasTonhauser2025.cfg (qud : Semantics.Attitudes.Factivity.QUD) (pC : ℚ) (hpC : 0 ≤ pC) (hpC1 : pC ≤ 1) :

RSA.RSAConfig Utterance WorldState

RSA model for Section 3: uniform prior over all 15 belief states, QUD-projected rpow scoring, α = 10.

Equations

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

Instances For

@[reducible, inline]

noncomputable abbrev Phenomena.Presupposition.Studies.ScontrasTonhauser2025.cfgBelHigh :

RSA.RSAConfig Utterance WorldState

QUD=BEL?, P(C)=2/3.

Equations

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

Instances For

@[reducible, inline]

noncomputable abbrev Phenomena.Presupposition.Studies.ScontrasTonhauser2025.cfgBelLow :

RSA.RSAConfig Utterance WorldState

QUD=BEL?, P(C)=1/3.

Equations

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

Instances For

@[reducible, inline]

noncomputable abbrev Phenomena.Presupposition.Studies.ScontrasTonhauser2025.cfgCHigh :

RSA.RSAConfig Utterance WorldState

QUD=C?, P(C)=2/3.

Equations

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

Instances For

@[reducible, inline]

noncomputable abbrev Phenomena.Presupposition.Studies.ScontrasTonhauser2025.cfgCLow :

RSA.RSAConfig Utterance WorldState

QUD=C?, P(C)=1/3.

Equations

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

Instances For

theorem Phenomena.Presupposition.Studies.ScontrasTonhauser2025.bel_qud_marginal_eq_prior_high (u : Utterance) :

(cfgBelHigh.L1_marginal u fun (x : WorldState) => x.c) = 2 / 3

Under BEL? QUD, L1's world-marginal for C equals the prior P(C) for every utterance. S1 scores depend on w only through w.bel, so the complement dimension washes out in the marginal:

L1_marginal(C|u, BEL?) = Σ_{w:C(w)} P(w)·f(u,w.bel) / Σ_w P(w)·f(u,w.bel) = (pC/2)·(f₁+f₀) / ((1/2)·(f₁+f₀)) = pC.

theorem Phenomena.Presupposition.Studies.ScontrasTonhauser2025.bel_qud_marginal_eq_prior_low (u : Utterance) :

(cfgBelLow.L1_marginal u fun (x : WorldState) => x.c) = 1 / 3

Same identity for the low-prior configuration: P(C|u, BEL?) = P(C) = 1/3.

theorem Phenomena.Presupposition.Studies.ScontrasTonhauser2025.c_qud_thinkNeg_higher :

(cfgCHigh.L1_marginal Utterance.thinkNeg fun (x : WorldState) => x.c) > cfgCHigh.L1_marginal Utterance.knowNeg fun (x : WorldState) => x.c

Under C? QUD, knowNeg is evidence AGAINST C: ¬(BEL∧C) is literally compatible with C-false worlds, so an informative speaker uses knowNeg more often when C is false. Thus thinkNeg preserves P(C) better.

Prediction 2a: Utterance Effect (know > think) #

The paper predicts stronger projection for factive know than non-factive think (Figure 7a). The full Section 3 model — including utterance cost (complex = 2×simple) — produces this direction via the world-marginal. Our cost-free model does not:

BEL? QUD: both utterances yield P(C|u) = P(C) (the identity above)
C? QUD: the direction is reversed (c_qud_thinkNeg_higher)

The reversal is due to cost omission, which changes S1's normalization. With cost, simple utterances (cPos, cNeg) dominate S1's softmax via exp(−α·C_simple) ≫ exp(−α·C_complex), altering which (world, belief state) combinations favor knowNeg vs thinkNeg in L1's posterior.

The paper also notes (fn. 11) that projection can be measured via the A-marginal P(A ⊧ C | u) — the probability that the speaker's inferred belief state entails C. This measure may capture the utterance effect even without cost, since the mechanism works through belief state inference rather than world-marginal.

theorem Phenomena.Presupposition.Studies.ScontrasTonhauser2025.prediction_2b :

(cfgCHigh.L1_marginal Utterance.knowNeg fun (x : WorldState) => x.c) > cfgCLow.L1_marginal Utterance.knowNeg fun (x : WorldState) => x.c

Prediction 2b (prior effect): higher prior increases projection. Under C? QUD, L1 assigns higher probability to C with P(C) = 2/3 than with P(C) = 1/3.

theorem Phenomena.Presupposition.Studies.ScontrasTonhauser2025.prediction_2c :

(cfgBelHigh.L1_marginal Utterance.knowNeg fun (x : WorldState) => x.c) > cfgCHigh.L1_marginal Utterance.knowNeg fun (x : WorldState) => x.c

Prediction 2c (QUD effect): BEL? QUD increases projection over C? QUD. Under BEL? QUD, C is not at-issue and L1_marginal(C) = P(C) = 2/3. Under C? QUD, the literal semantics of "doesn't know C" (= ¬(BEL∧C)) lowers P(C) from the prior, so BEL? > C?.

theorem Phenomena.Presupposition.Studies.ScontrasTonhauser2025.know_entails_c (w : WorldState) :

literalMeaning Utterance.knowPos w = true → w.c = true

"know" entails C (from factivePos_entails_c).

theorem Phenomena.Presupposition.Studies.ScontrasTonhauser2025.think_not_entails_c :

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

"think" does NOT entail C.

theorem Phenomena.Presupposition.Studies.ScontrasTonhauser2025.know_entails_bel (w : WorldState) :

literalMeaning Utterance.knowPos w = true → w.bel = true

"know" entails BEL (from factivePos_entails_bel).

theorem Phenomena.Presupposition.Studies.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).

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

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

theorem Phenomena.Presupposition.Studies.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 Phenomena.Presupposition.Studies.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 Phenomena.Presupposition.Studies.ScontrasTonhauser2025.three_of_fifteen_assume_c :

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

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

structure Phenomena.Presupposition.Studies.ScontrasTonhauser2025.UtteranceEffect :

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

β : Float
se : Float
t : Float
p : Float

Instances For

def Phenomena.Presupposition.Studies.ScontrasTonhauser2025.instReprUtteranceEffect.repr :

UtteranceEffect → ℕ → Std.Format

Equations

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

Instances For

instance Phenomena.Presupposition.Studies.ScontrasTonhauser2025.instReprUtteranceEffect :

Repr UtteranceEffect

Equations

Phenomena.Presupposition.Studies.ScontrasTonhauser2025.instReprUtteranceEffect = { reprPrec := Phenomena.Presupposition.Studies.ScontrasTonhauser2025.instReprUtteranceEffect.repr }

def Phenomena.Presupposition.Studies.ScontrasTonhauser2025.exp1_utteranceEffect :

UtteranceEffect

Exp 1: Utterance effect (know > think).

Equations

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

Instances For

def Phenomena.Presupposition.Studies.ScontrasTonhauser2025.exp1_priorEffect :

UtteranceEffect

Exp 1: Prior effect (higher > lower).

Equations

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

Instances For

def Phenomena.Presupposition.Studies.ScontrasTonhauser2025.exp1_qudEffect :

UtteranceEffect

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

Equations

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

Instances For

def Phenomena.Presupposition.Studies.ScontrasTonhauser2025.exp2_utteranceEffect :

UtteranceEffect

Exp 2: Utterance effect (know > think).

Equations

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

Instances For

def Phenomena.Presupposition.Studies.ScontrasTonhauser2025.exp2_qudEffect :

UtteranceEffect

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

Equations

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

Instances For

inductive Phenomena.Presupposition.Studies.ScontrasTonhauser2025.Hypothesis :

utterance : Hypothesis
prior : Hypothesis
qud : Hypothesis

Instances For

instance Phenomena.Presupposition.Studies.ScontrasTonhauser2025.instDecidableEqHypothesis :

DecidableEq Hypothesis

Equations

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

def Phenomena.Presupposition.Studies.ScontrasTonhauser2025.instReprHypothesis.repr :

Hypothesis → ℕ → Std.Format

Equations

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

Instances For

instance Phenomena.Presupposition.Studies.ScontrasTonhauser2025.instReprHypothesis :

Repr Hypothesis

Equations

Phenomena.Presupposition.Studies.ScontrasTonhauser2025.instReprHypothesis = { reprPrec := Phenomena.Presupposition.Studies.ScontrasTonhauser2025.instReprHypothesis.repr }

def Phenomena.Presupposition.Studies.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

Instances For

def Phenomena.Presupposition.Studies.ScontrasTonhauser2025.directionCorrect :

Hypothesis → Bool

Equations

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

Instances For

def Phenomena.Presupposition.Studies.ScontrasTonhauser2025.beliefStateCategory :

Core.BToM.LatentCategory

Classification of BeliefState in BToM terms.

Equations

Phenomena.Presupposition.Studies.ScontrasTonhauser2025.beliefStateCategory = Core.BToM.LatentCategory.mental

Instances For

def Phenomena.Presupposition.Studies.ScontrasTonhauser2025.qudCategory :

Core.BToM.LatentCategory

Classification of QUD in BToM terms.

Equations

Phenomena.Presupposition.Studies.ScontrasTonhauser2025.qudCategory = Core.BToM.LatentCategory.shared

Instances For

def Phenomena.Presupposition.Studies.ScontrasTonhauser2025.assumesCIndicator :

BeliefState → ℚ

Characteristic function: does the speaker assume C?

Equations

Phenomena.Presupposition.Studies.ScontrasTonhauser2025.assumesCIndicator bs = if Phenomena.Presupposition.Studies.ScontrasTonhauser2025.assumesC bs = true then 1 else 0

Instances For

theorem Phenomena.Presupposition.Studies.ScontrasTonhauser2025.assumesCIndicator_pos (bs : BeliefState) (h : assumesC bs = true) :

assumesCIndicator bs = 1

Belief states that assume C have indicator 1.

theorem Phenomena.Presupposition.Studies.ScontrasTonhauser2025.assumesCIndicator_neg (bs : BeliefState) (h : assumesC bs = false) :

assumesCIndicator bs = 0

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

theorem Phenomena.Presupposition.Studies.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.

theorem Phenomena.Presupposition.Studies.ScontrasTonhauser2025.model_predicts_effects :

((cfgCHigh.L1_marginal Utterance.knowNeg fun (x : WorldState) => x.c) > cfgCLow.L1_marginal Utterance.knowNeg fun (x : WorldState) => x.c) ∧ ((cfgBelHigh.L1_marginal Utterance.knowNeg fun (x : WorldState) => x.c) > cfgCHigh.L1_marginal Utterance.knowNeg fun (x : WorldState) => x.c) ∧ directionCorrect Hypothesis.prior = true ∧ directionCorrect Hypothesis.qud = true

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

theorem Phenomena.Presupposition.Studies.ScontrasTonhauser2025.prior_effect_consistent_with_dt2021 :

exp1_priorEffect.β > 0 ∧ (DegenTonhauser2021.exp1_priorEffect DegenTonhauser2021.PriorLevel.categorical).β > 0 ∧ (DegenTonhauser2021.exp1_priorEffect DegenTonhauser2021.PriorLevel.individualLevel).β > 0

The prior effect found by S&T 2025 (β = 0.16) replicates the prior effect found by @cite{degen-tonhauser-2021} (β = 0.14 categorical, β = 0.28 individual). Both find that higher prior probability of the complement content leads to stronger projection. The RSA model's prediction_2b provides the theoretical explanation for this empirical finding.