Projection Mechanisms: Compositional Filtering vs. RSA BToM

@cite{scontras-tonhauser-2025} @cite{heim-1983}

Compares two theories of presupposition projection:

1. Compositional filtering: Presuppositions project through connectives via local context computation. The filtering presupposition of "if A then B_p" is "A → p" (the antecedent filters the consequent's presupposition).

2. RSA BToM: Projection is a pragmatic inference. The listener (L1) inverts the speaker's generative model to infer which propositions the speaker takes for granted. No lexical presupposition encoding is required.

The Key Empirical Argument

@cite{scontras-tonhauser-2025} argue that projection arises from pragmatic reasoning about the speaker's private assumptions, not from lexical encoding of presuppositions. Their BToM model predicts that even non-factive "think" — which has NO presupposition to filter — should exhibit projection effects, because L1 can still infer what the speaker takes for granted. This is predicted by RSA BToM but NOT by compositional filtering (which predicts trivial presupposition for non-presuppositional items).

What This Comparison Formalizes

1. For factive "know": both theories predict conditional presupposition, but for different reasons (filtering: "A → C"; BToM: pragmatic inference)
2. For non-factive "think": only BToM predicts conditional presupposition effects; filtering predicts nothing (trivial presupposition)
3. BToM strictly subsumes filtering for projection predictions in conditional environments

def Comparisons.ProjectionMechanisms.factivePresup {W : Type u_1} (c : W → Bool) : Core.Presupposition.PrProp W

A factive verb "know" has a presupposition: C must be true.

Equations

• Comparisons.ProjectionMechanisms.factivePresup c = { presup := c, assertion := fun (x : W) => true }

def Comparisons.ProjectionMechanisms.nonFactivePresup {W : Type u_1} : Core.Presupposition.PrProp W

A non-factive verb "think" has NO presupposition.

Equations

• Comparisons.ProjectionMechanisms.nonFactivePresup = { presup := fun (x : W) => true, assertion := fun (x : W) => true }

def Comparisons.ProjectionMechanisms.filteringPrediction_know {W : Type u_1} (a c : W → Bool) : Core.Presupposition.PrProp 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

• Comparisons.ProjectionMechanisms.filteringPrediction_know a c = (Core.Presupposition.PrProp.ofBProp a).impFilter (Comparisons.ProjectionMechanisms.factivePresup c)

def Comparisons.ProjectionMechanisms.filteringPrediction_think {W : Type u_1} (a : W → Bool) : Core.Presupposition.PrProp W

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

Equations

• Comparisons.ProjectionMechanisms.filteringPrediction_think a = (Core.Presupposition.PrProp.ofBProp a).impFilter Comparisons.ProjectionMechanisms.nonFactivePresup

theorem Comparisons.ProjectionMechanisms.filtering_know_nontrivial {W : Type u_1} (a c : W → Bool) (h : ∃ (w : W), a w = true ∧ c w = false) : ∃ (w : W), (filteringPrediction_know a c).presup w = false

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 Comparisons.ProjectionMechanisms.filtering_think_trivial {W : Type u_1} (a : W → Bool) (w : W) : (filteringPrediction_think a).presup w = true

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 Comparisons.ProjectionMechanisms.BToMPrediction : 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 Comparisons.ProjectionMechanisms.btomPrediction : BToMPrediction

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

Equations

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

def Comparisons.ProjectionMechanisms.filteringPrediction : BToMPrediction

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

Equations

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

theorem Comparisons.ProjectionMechanisms.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 Comparisons.ProjectionMechanisms.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 @cite{scontras-tonhauser-2025} 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 Comparisons.ProjectionMechanisms.filtering_is_limiting_case {W : Type u_1} (a c : W → Bool) : (∀ (w : W), a w = true → c w = true) → ∀ (w : W), (filteringPrediction_know a c).presup w = true

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.