Linglib.Theories.Pragmatics.RSA.Implementations.BellerGerstenberg2025

This is a simplified representation. In the full paper, these aspects are computed from structural causal models via counterfactual simulation. Here we treat them as primitive Boolean features to focus on the RSA pragmatic reasoning over expression choice.

See Core.StructuralEquationModel and NadathurLauer2020 for full causal machinery.

whether : Bool
Whether-causation: was cause necessary? (but-for test)
how : Bool
How-causation: did cause affect how outcome occurred?
sufficient : Bool
Sufficient-causation: was cause sufficient?

Instances For

source

def RSA.BellerGerstenberg2025.instDecidableEqCausalWorld.decEq (x✝ x✝¹ : CausalWorld) :

Decidable (x✝ = x✝¹)

Equations

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

Instances For

source

instance RSA.BellerGerstenberg2025.instDecidableEqCausalWorld :

DecidableEq CausalWorld

Equations

RSA.BellerGerstenberg2025.instDecidableEqCausalWorld = RSA.BellerGerstenberg2025.instDecidableEqCausalWorld.decEq

source

def RSA.BellerGerstenberg2025.instBEqCausalWorld.beq :

CausalWorld → CausalWorld → Bool

Equations

RSA.BellerGerstenberg2025.instBEqCausalWorld.beq { whether := a, how := a_1, sufficient := a_2 } { whether := b, how := b_1, sufficient := b_2 } = (a == b && (a_1 == b_1 && a_2 == b_2))
RSA.BellerGerstenberg2025.instBEqCausalWorld.beq x✝¹ x✝ = false

Instances For

source

instance RSA.BellerGerstenberg2025.instBEqCausalWorld :

BEq CausalWorld

Equations

RSA.BellerGerstenberg2025.instBEqCausalWorld = { beq := RSA.BellerGerstenberg2025.instBEqCausalWorld.beq }

source

instance RSA.BellerGerstenberg2025.instReprCausalWorld :

Repr CausalWorld

Equations

RSA.BellerGerstenberg2025.instReprCausalWorld = { reprPrec := RSA.BellerGerstenberg2025.instReprCausalWorld.repr }

source

def RSA.BellerGerstenberg2025.instReprCausalWorld.repr :

CausalWorld → ℕ → Std.Format

Equations

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

Instances For

source

instance RSA.BellerGerstenberg2025.instInhabitedCausalWorld :

Inhabited CausalWorld

Equations

RSA.BellerGerstenberg2025.instInhabitedCausalWorld = { default := RSA.BellerGerstenberg2025.instInhabitedCausalWorld.default }

source

def RSA.BellerGerstenberg2025.instInhabitedCausalWorld.default :

CausalWorld

Equations

RSA.BellerGerstenberg2025.instInhabitedCausalWorld.default = { whether := default, how := default, sufficient := default }

Instances For

source

instance RSA.BellerGerstenberg2025.instToStringCausalWorld :

ToString CausalWorld

Equations

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

source

def RSA.BellerGerstenberg2025.allCausalWorlds :

List CausalWorld

All 8 possible causal worlds (2³ combinations of W, H, S)

Equations

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

Instances For

source

instance RSA.BellerGerstenberg2025.instFintypeCausalWorld :

Fintype CausalWorld

Equations

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

source

instance RSA.BellerGerstenberg2025.instNonemptyCausalWorld :

Nonempty CausalWorld

source

def RSA.BellerGerstenberg2025.expressionMeaning (cw : CausalWorld) :

CausalExpression → Bool

Semantics of causal expressions in terms of causal aspects.

From @cite{beller-gerstenberg-2025}:

affected: W ∨ H ∨ S (any causal involvement)
enabled: W ∨ S (necessity or sufficiency, but not just how)
caused: H ∧ (W ∨ S) (process + counterfactual dependence)
made_no_difference: ¬W ∧ ¬H ∧ ¬S (no causal involvement)

Equations

Instances For

source

noncomputable def RSA.BellerGerstenberg2025.cfg :

RSAConfig CausalExpression CausalWorld

RSAConfig for causal expression choice.

Meaning: Boolean expression semantics (1 if expression applies, 0 otherwise). World prior: uniform over causal worlds. S1 score: belief-based (rpow): score = L0(w|u)^α.

Equations

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

Instances For

source

theorem RSA.BellerGerstenberg2025.caused_implies_enabled (cw : CausalWorld) :

expressionMeaning cw CausalExpression.caused = true → expressionMeaning cw CausalExpression.enabled = true

"caused" implies "enabled": if H ∧ (W ∨ S) then W ∨ S.

This captures the scalar relationship: "caused" is stronger than "enabled".

source

theorem RSA.BellerGerstenberg2025.enabled_implies_affected (cw : CausalWorld) :

expressionMeaning cw CausalExpression.enabled = true → expressionMeaning cw CausalExpression.affected = true

"enabled" implies "affected": if W ∨ S then W ∨ H ∨ S.

This captures the scalar relationship: "enabled" is stronger than "affected".

source

theorem RSA.BellerGerstenberg2025.caused_implies_affected (cw : CausalWorld) :

expressionMeaning cw CausalExpression.caused = true → expressionMeaning cw CausalExpression.affected = true

Full scalar chain: caused → enabled → affected.

source

theorem RSA.BellerGerstenberg2025.madeNoDifference_iff_not_affected (cw : CausalWorld) :

expressionMeaning cw CausalExpression.madeNoDifference = true ↔ (!expressionMeaning cw CausalExpression.affected) = true

"madeNoDifference" is the negation of "affected".

source

def RSA.BellerGerstenberg2025.world_W_only :

CausalWorld

World where cause was only necessary (W only)

Equations

RSA.BellerGerstenberg2025.world_W_only = { whether := true, how := false, sufficient := false }

Instances For

source

def RSA.BellerGerstenberg2025.world_S_only :

CausalWorld

World where cause was only sufficient (S only)

Equations

RSA.BellerGerstenberg2025.world_S_only = { whether := false, how := false, sufficient := true }

Instances For

source

def RSA.BellerGerstenberg2025.world_H_only :

CausalWorld

World where cause affected how (H only)

Equations

RSA.BellerGerstenberg2025.world_H_only = { whether := false, how := true, sufficient := false }

Instances For

source

def RSA.BellerGerstenberg2025.world_full :

CausalWorld

World with full causation (W, H, S all true)

Equations

RSA.BellerGerstenberg2025.world_full = { whether := true, how := true, sufficient := true }

Instances For

source

def RSA.BellerGerstenberg2025.world_none :

CausalWorld

World with no causal involvement

Equations

RSA.BellerGerstenberg2025.world_none = { whether := false, how := false, sufficient := false }

Instances For

source

def RSA.BellerGerstenberg2025.world_caused :

CausalWorld

World where "caused" applies (H and W)

Equations

RSA.BellerGerstenberg2025.world_caused = { whether := true, how := true, sufficient := false }

Instances For

source

theorem RSA.BellerGerstenberg2025.W_only_enabled_not_caused :

expressionMeaning world_W_only CausalExpression.enabled = true ∧ expressionMeaning world_W_only CausalExpression.caused = false

In W-only world, "enabled" is true but "caused" is false

source

theorem RSA.BellerGerstenberg2025.H_only_affected_only :

expressionMeaning world_H_only CausalExpression.affected = true ∧ expressionMeaning world_H_only CausalExpression.enabled = false ∧ expressionMeaning world_H_only CausalExpression.caused = false

In H-only world, neither "caused" nor "enabled" applies

source

In full world, all positive expressions apply

source

In none world, only madeNoDifference applies

source

theorem RSA.BellerGerstenberg2025.s1_full_prefers_caused :

cfg.S1 () world_full CausalExpression.caused > cfg.S1 () world_full CausalExpression.enabled

In full causation world, S1 prefers "caused" (most informative).

source

theorem RSA.BellerGerstenberg2025.l1_caused_infers_how :

cfg.L1 CausalExpression.caused world_caused > cfg.L1 CausalExpression.caused world_W_only

L1 hearing "caused" infers H is likely true.

How RSA Derives Causal Expression Pragmatics #

Literal Semantics (L0) #

"caused" → true in worlds with H ∧ (W ∨ S)
"enabled" → true in worlds with W ∨ S
"affected" → true in worlds with W ∨ H ∨ S

Pragmatic Speaker (S1) #

In world_full (W, H, S all true): prefers "caused" (most informative)
In world_W_only: "enabled" is more informative than "affected"
In world_H_only: only "affected" applies

Pragmatic Listener (L1) #

Hearing "caused": infers H is likely true
Hearing "enabled" (not "caused"): infers H is likely false
Hearing "affected" (not "enabled"): infers W and S both likely false

This captures the scalar implicature pattern: stronger expressions implicate the presence of stronger causal aspects.

Bridge to Structural Causal Models #

Beller & Gerstenberg's W, H, S dimensions can be COMPUTED from structural causal models, grounding the primitive Boolean features in the counterfactual reasoning machinery of Core.StructuralEquationModel.

B&G dimension	Structural definition
W (whether)	`causallyNecessary` — would effect still occur without cause?
H (how)	`hasDirectLaw` — does a causal law directly connect cause to effect?
S (sufficient)	`causallySufficient` — does adding cause guarantee effect?

This bridge reveals why certain causal scenarios yield specific expression choices: the structural properties of the causal model determine the W-H-S world, which determines literal semantics, which RSA pragmatics then sharpens.

source

def RSA.BellerGerstenberg2025.causalWorldFromModel (dyn : Core.StructuralEquationModel.CausalDynamics) (bg : Core.StructuralEquationModel.Situation) (cause effect : Core.StructuralEquationModel.Variable) :

CausalWorld

Compute a CausalWorld from a structural causal model.

Grounds B&G's W-H-S Booleans in Core.StructuralEquationModel: W = necessity, H = direct law, S = sufficiency.

Equations

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

Instances For

source

theorem RSA.BellerGerstenberg2025.solo_cause_world :

causalWorldFromModel RSA.BellerGerstenberg2025.soloModel✝ Core.StructuralEquationModel.Situation.empty RSA.BellerGerstenberg2025.mA✝ RSA.BellerGerstenberg2025.mC✝ = { whether := true, how := true, sufficient := true }

Solo cause → full causation world (W=true, H=true, S=true).

When there's one direct cause and no alternatives, all three causal dimensions are active.

source

theorem RSA.BellerGerstenberg2025.overdetermination_world :

causalWorldFromModel RSA.BellerGerstenberg2025.overdetModel✝ RSA.BellerGerstenberg2025.overdetBg✝ RSA.BellerGerstenberg2025.mA✝ RSA.BellerGerstenberg2025.mC✝ = { whether := false, how := true, sufficient := true }

Overdetermination → W=false, H=true, S=true.

The cause is sufficient (S) and directly connected (H), but NOT necessary (W=false) because the alternative cause in the background would produce the effect anyway.

source

theorem RSA.BellerGerstenberg2025.chain_world :

causalWorldFromModel RSA.BellerGerstenberg2025.chainModel✝ Core.StructuralEquationModel.Situation.empty RSA.BellerGerstenberg2025.mA✝ RSA.BellerGerstenberg2025.mC✝ = { whether := true, how := false, sufficient := true }

Causal chain → W=true, H=false, S=true.

The initial cause is sufficient (S) and necessary (W), but NOT directly connected (H=false) — it operates through an intermediate. This is @cite{levin-2019}'s "intervening causer" scenario.

Expression predictions from structural models #

The structural bridge makes testable predictions: given a causal model, we can compute both the W-H-S world AND the appropriate causal expression.

source

theorem RSA.BellerGerstenberg2025.solo_cause_expression_caused :

expressionMeaning (causalWorldFromModel RSA.BellerGerstenberg2025.soloModel✝ Core.StructuralEquationModel.Situation.empty RSA.BellerGerstenberg2025.mA✝ RSA.BellerGerstenberg2025.mC✝) CausalExpression.caused = true

Solo cause: "caused" is literally true.

With W, H, S all true, the strongest expression applies.

source

theorem RSA.BellerGerstenberg2025.chain_not_caused :

expressionMeaning (causalWorldFromModel RSA.BellerGerstenberg2025.chainModel✝ Core.StructuralEquationModel.Situation.empty RSA.BellerGerstenberg2025.mA✝ RSA.BellerGerstenberg2025.mC✝) CausalExpression.caused = false

Chain causation: "caused" is NOT literally true.

Despite sufficiency and necessity, the lack of direct connection (H=false) means "caused" doesn't apply. B&G predict speakers will use "enabled" instead — capturing @cite{levin-2019}'s intuition that indirect causation is expressed differently.

source

theorem RSA.BellerGerstenberg2025.chain_still_enabled :

Chain causation: "enabled" still applies.

W ∨ S = true ∨ true = true, so "enabled" is literally true. This is the weaker expression appropriate for indirect causation.

source

theorem RSA.BellerGerstenberg2025.overdetermination_caused :

expressionMeaning (causalWorldFromModel RSA.BellerGerstenberg2025.overdetModel✝ RSA.BellerGerstenberg2025.overdetBg✝ RSA.BellerGerstenberg2025.mA✝ RSA.BellerGerstenberg2025.mC✝) CausalExpression.caused = true

Overdetermination: "caused" is literally true.

H ∧ (W ∨ S) = true ∧ (false ∨ true) = true. The cause is directly connected (H) and sufficient (S), so "caused" applies even without necessity (W=false).

source

Bridge between B&G's "caused" and N&L's make/cause distinction.

In the overdetermination scenario, makeSem holds (a IS sufficient) but causeSem fails (a is NOT necessary). Meanwhile B&G's "caused" applies (because H is true). This shows B&G's expression semantics and N&L's verb semantics make orthogonal predictions:

N&L: You can say "A made C happen" (sufficient) but NOT "A caused C" (not necessary)
B&G: Speakers would use "caused" (H ∧ S = true)

The divergence reflects different questions: N&L model verb choice (make vs cause), B&G model expression choice (caused vs enabled).