Beller and Gerstenberg (2025): Causation, Meaning, and Communication

Beller and Gerstenberg model causal language by counterfactual simulation. A causal knowledge module computes three aspects of causation, namely whether-causation (counterfactual necessity), how-causation (a difference to the fine-grained outcome) and sufficient-causation (whether-causation with the alternative causes removed). A semantics module defines "affected", "enabled", "caused" and "made no difference" as logical combinations of the aspects, and a pragmatics module chooses among the true expressions by informativity, as a rational speech act speaker and listener after Frank and Goodman.

Main results

• caused_implies_enabled, enabled_implies_affected: the expressions are ordered by specificity, the hierarchy behind the scale causalScale.
• speaker_prefers_caused, speaker_prefers_enabled: the speaker prefers the most informative true expression at every positive rationality.
• listener_enabled_implicature: hearing "enabled", the pragmatic listener favours the scenario where "caused" is false.
• launch_ofModel: Michottean launching, as a two-variable structural model, has the aspect profile of the first sample scenario.

Implementation notes

• The speaker is the paper's first-level pragmatic speaker over Boolean aspects. The fitted model uses a second-level speaker over graded aspects from noisy simulations, with fitted noise, softening and optimality parameters.
• listener_affected_prefers_howOnly is the model's prediction for "affected", which the listener experiment did not bear out.

References

• [BG25]
• [GGLT21]
• [FG12]
• [HP05]

Expressions and aspects

inductive BellerGerstenberg2025.CausalExpression : Type

The four causal expressions offered to participants.

• caused : CausalExpression
• enabled : CausalExpression
• affected : CausalExpression
• madeNoDifference : CausalExpression

@[instance_reducible]

instance BellerGerstenberg2025.instDecidableEqCausalExpression : DecidableEq CausalExpression

Equations

• BellerGerstenberg2025.instDecidableEqCausalExpression x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance BellerGerstenberg2025.instReprCausalExpression : Repr CausalExpression

Equations

• BellerGerstenberg2025.instReprCausalExpression = { reprPrec := BellerGerstenberg2025.instReprCausalExpression.repr }

def BellerGerstenberg2025.instReprCausalExpression.repr : CausalExpression → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance BellerGerstenberg2025.instInhabitedCausalExpression : Inhabited CausalExpression

Equations

• BellerGerstenberg2025.instInhabitedCausalExpression = { default := BellerGerstenberg2025.instInhabitedCausalExpression.default }

@[instance_reducible]

instance BellerGerstenberg2025.instFintypeCausalExpression : Fintype CausalExpression

Equations

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

instance BellerGerstenberg2025.instNonemptyCausalExpression : Nonempty CausalExpression

@[instance_reducible]

instance BellerGerstenberg2025.instMeasurableSpaceCausalExpression : MeasurableSpace CausalExpression

Equations

• BellerGerstenberg2025.instMeasurableSpaceCausalExpression = ⊤

instance BellerGerstenberg2025.instDiscreteMeasurableSpaceCausalExpression : DiscreteMeasurableSpace CausalExpression

structure BellerGerstenberg2025.CausalWorld : Type

An aspect profile records whether-causation W (1), how-causation H (2) and sufficient-causation S (3), at Boolean values.

• whether : Bool
• how : Bool
• sufficient : Bool

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

Equations

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

@[instance_reducible]

instance BellerGerstenberg2025.instDecidableEqCausalWorld : DecidableEq CausalWorld

Equations

• BellerGerstenberg2025.instDecidableEqCausalWorld = BellerGerstenberg2025.instDecidableEqCausalWorld.decEq

@[instance_reducible]

instance BellerGerstenberg2025.instReprCausalWorld : Repr CausalWorld

Equations

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

def BellerGerstenberg2025.instReprCausalWorld.repr : CausalWorld → ℕ → Std.Format

Equations

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

Semantics

def BellerGerstenberg2025.expressionMeaning (cw : CausalWorld) : CausalExpression → Prop

The Boolean core of the semantics is affected = W ∨ H ∨ S (4), enabled = W ∨ S (5), caused = H ∧ (W ∨ S) (6) without the softened movement and uniqueness conjuncts, and made no difference = ¬W ∧ ¬H ∧ ¬S (7) with a hard negation.

Equations

• BellerGerstenberg2025.expressionMeaning cw BellerGerstenberg2025.CausalExpression.affected = (cw.whether = true ∨ cw.how = true ∨ cw.sufficient = true)
• BellerGerstenberg2025.expressionMeaning cw BellerGerstenberg2025.CausalExpression.enabled = (cw.whether = true ∨ cw.sufficient = true)
• BellerGerstenberg2025.expressionMeaning cw BellerGerstenberg2025.CausalExpression.caused = (cw.how = true ∧ (cw.whether = true ∨ cw.sufficient = true))
• BellerGerstenberg2025.expressionMeaning cw BellerGerstenberg2025.CausalExpression.madeNoDifference = (¬cw.whether = true ∧ ¬cw.how = true ∧ ¬cw.sufficient = true)

@[instance_reducible]

instance BellerGerstenberg2025.instDecidableExpressionMeaning (cw : CausalWorld) (u : CausalExpression) : Decidable (expressionMeaning cw u)

Equations

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

theorem BellerGerstenberg2025.caused_implies_enabled (cw : CausalWorld) : expressionMeaning cw CausalExpression.caused → expressionMeaning cw CausalExpression.enabled

theorem BellerGerstenberg2025.enabled_implies_affected (cw : CausalWorld) : expressionMeaning cw CausalExpression.enabled → expressionMeaning cw CausalExpression.affected

theorem BellerGerstenberg2025.caused_implies_affected (cw : CausalWorld) : expressionMeaning cw CausalExpression.caused → expressionMeaning cw CausalExpression.affected

theorem BellerGerstenberg2025.madeNoDifference_iff_not_affected (cw : CausalWorld) : expressionMeaning cw CausalExpression.madeNoDifference ↔ ¬expressionMeaning cw CausalExpression.affected

"Made no difference" is the negation of "affected".

def BellerGerstenberg2025.gradedMeaning (cw : CausalWorld) (ν : ℚ) : CausalExpression → ℚ

The graded semantics softens the negation of how-causation in "made no difference", which a how-cause that is neither a whether- nor a sufficient-cause satisfies to degree ν (7).

Equations

• One or more equations did not get rendered due to their size.
• BellerGerstenberg2025.gradedMeaning cw ν BellerGerstenberg2025.CausalExpression.affected = if (cw.whether || cw.how || cw.sufficient) = true then 1 else 0
• BellerGerstenberg2025.gradedMeaning cw ν BellerGerstenberg2025.CausalExpression.enabled = if (cw.whether || cw.sufficient) = true then 1 else 0
• BellerGerstenberg2025.gradedMeaning cw ν BellerGerstenberg2025.CausalExpression.caused = if (cw.how && (cw.whether || cw.sufficient)) = true then 1 else 0

theorem BellerGerstenberg2025.gradedMeaning_zero (cw : CausalWorld) (u : CausalExpression) : gradedMeaning cw 0 u = if expressionMeaning cw u then 1 else 0

Without softening, the graded semantics is the indicator of the Boolean core.

The sample scenarios

inductive BellerGerstenberg2025.Scenario : Type

The paper's four sample scenarios are Michottean launching, double prevention, a how-cause pushing a ball already headed for the gate, and no interaction.

• s1 : Scenario
• s2 : Scenario
• s3 : Scenario
• s4 : Scenario

@[instance_reducible]

instance BellerGerstenberg2025.instDecidableEqScenario : DecidableEq Scenario

Equations

• BellerGerstenberg2025.instDecidableEqScenario x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def BellerGerstenberg2025.instReprScenario.repr : Scenario → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance BellerGerstenberg2025.instReprScenario : Repr Scenario

Equations

• BellerGerstenberg2025.instReprScenario = { reprPrec := BellerGerstenberg2025.instReprScenario.repr }

@[instance_reducible]

instance BellerGerstenberg2025.instFintypeScenario : Fintype Scenario

Equations

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

instance BellerGerstenberg2025.instNonemptyScenario : Nonempty Scenario

@[instance_reducible]

instance BellerGerstenberg2025.instMeasurableSpaceScenario : MeasurableSpace Scenario

Equations

• BellerGerstenberg2025.instMeasurableSpaceScenario = ⊤

instance BellerGerstenberg2025.instDiscreteMeasurableSpaceScenario : DiscreteMeasurableSpace Scenario

def BellerGerstenberg2025.Scenario.aspects : Scenario → CausalWorld

The aspect values of the sample scenarios (Table 1a).

Equations

• BellerGerstenberg2025.Scenario.s1.aspects = { whether := true, how := true, sufficient := true }
• BellerGerstenberg2025.Scenario.s2.aspects = { whether := true, how := false, sufficient := true }
• BellerGerstenberg2025.Scenario.s3.aspects = { whether := false, how := true, sufficient := false }
• BellerGerstenberg2025.Scenario.s4.aspects = { whether := false, how := false, sufficient := false }

def BellerGerstenberg2025.sem (u : CausalExpression) : Finset Scenario

Each expression's extension over the sample scenarios under the Boolean core.

Equations

• BellerGerstenberg2025.sem u = {s : BellerGerstenberg2025.Scenario | BellerGerstenberg2025.expressionMeaning s.aspects u}

The pragmatics module

@[reducible, inline]

noncomputable abbrev BellerGerstenberg2025.literal : ProbabilityTheory.Kernel CausalExpression Scenario

The literal listener is uniform on the scenarios an expression is true of.

Equations

• BellerGerstenberg2025.literal = RSA.listener (ProbabilityTheory.uniformOn Set.univ) (RSA.truthful fun (u : BellerGerstenberg2025.CausalExpression) => ↑(BellerGerstenberg2025.sem u))

@[reducible, inline]

noncomputable abbrev BellerGerstenberg2025.speaker (α : ℝ) : ProbabilityTheory.Kernel Scenario CausalExpression

The first-level speaker knows the scenario and addresses the literal listener at rationality α.

Equations

• BellerGerstenberg2025.speaker α = RSA.speaker α 0 (⇑BellerGerstenberg2025.literal) MeasureTheory.Measure.dirac

@[reducible, inline]

noncomputable abbrev BellerGerstenberg2025.listener (α : ℝ) : ProbabilityTheory.Kernel CausalExpression Scenario

The pragmatic listener inverts the speaker at a uniform prior over the scenarios.

Equations

• BellerGerstenberg2025.listener α = RSA.listener (ProbabilityTheory.uniformOn Set.univ) ⇑(BellerGerstenberg2025.speaker α)

theorem BellerGerstenberg2025.literal_enabled : (literal CausalExpression.enabled) {Scenario.s1} = 2⁻¹ ∧ (literal CausalExpression.enabled) {Scenario.s3} = 0

Hearing "enabled", the literal listener finds the two enabling scenarios equally likely (Table 1c).

theorem BellerGerstenberg2025.speaker_s1 : ((speaker 1) Scenario.s1).real {CausalExpression.caused} = 6 / 11 ∧ ((speaker 1) Scenario.s1).real {CausalExpression.enabled} = 3 / 11 ∧ ((speaker 1) Scenario.s1).real {CausalExpression.affected} = 2 / 11

At Michottean launching the first-level speaker says "caused" with probability 6/11, "enabled" with 3/11 and "affected" with 2/11 (Table 1d).

theorem BellerGerstenberg2025.speaker_s2 : ((speaker 1) Scenario.s2).real {CausalExpression.enabled} = 3 / 5 ∧ ((speaker 1) Scenario.s2).real {CausalExpression.affected} = 2 / 5 ∧ ((speaker 1) Scenario.s2).real {CausalExpression.caused} = 0

At double prevention the first-level speaker says "enabled" with probability 3/5 and "affected" with 2/5, and never "caused" (Table 1d).

Informativity and implicature

theorem BellerGerstenberg2025.speaker_prefers_caused {α : ℝ} (hα : 0 < α) : ((speaker α) Scenario.s1).real {CausalExpression.enabled} < ((speaker α) Scenario.s1).real {CausalExpression.caused} ∧ ((speaker α) Scenario.s1).real {CausalExpression.affected} < ((speaker α) Scenario.s1).real {CausalExpression.enabled}

At Michottean launching the speaker prefers "caused" to "enabled" and "enabled" to "affected", at every positive rationality.

theorem BellerGerstenberg2025.speaker_prefers_enabled {α : ℝ} (hα : 0 < α) : ((speaker α) Scenario.s2).real {CausalExpression.affected} < ((speaker α) Scenario.s2).real {CausalExpression.enabled}

At double prevention, where "caused" is false, the speaker prefers "enabled" to "affected" at every positive rationality.

theorem BellerGerstenberg2025.listener_caused_identifies {α : ℝ} (hα : 0 < α) : ((listener α) CausalExpression.caused).real {Scenario.s2} < ((listener α) CausalExpression.caused).real {Scenario.s1}

Hearing "caused", the pragmatic listener favours Michottean launching over double prevention, where the expression is false.

theorem BellerGerstenberg2025.listener_enabled_implicature {α : ℝ} (hα : 0 < α) : ((listener α) CausalExpression.enabled).real {Scenario.s1} < ((listener α) CausalExpression.enabled).real {Scenario.s2}

Hearing "enabled", the pragmatic listener favours double prevention over Michottean launching, where the speaker would have said "caused". This is the scalar implicature.

theorem BellerGerstenberg2025.listener_affected_prefers_howOnly {α : ℝ} (hα : 0 < α) : ((listener α) CausalExpression.affected).real {Scenario.s1} < ((listener α) CausalExpression.affected).real {Scenario.s3}

Hearing "affected", the pragmatic listener favours the how-cause-only scenario, where no stronger expression is true, over Michottean launching. The listener experiment found the opposite preference for the analogous pair, the case the paper singles out as the model's failure.

theorem BellerGerstenberg2025.listener_noDifference_identifies {α : ℝ} (hα : 0 < α) : ((listener α) CausalExpression.madeNoDifference).real {Scenario.s3} < ((listener α) CausalExpression.madeNoDifference).real {Scenario.s4}

Hearing "made no difference", the pragmatic listener favours the no-interaction scenario over the how-cause-only one.

The Horn scale

def BellerGerstenberg2025.causalScale : Fin 3 → CausalExpression

The scale ⟨affected, enabled, caused⟩, weakest to strongest.

Equations

• BellerGerstenberg2025.causalScale = ![BellerGerstenberg2025.CausalExpression.affected, BellerGerstenberg2025.CausalExpression.enabled, BellerGerstenberg2025.CausalExpression.caused]

theorem BellerGerstenberg2025.causalScale_strictAnti : StrictAnti fun (i : Fin 3) => {cw : CausalWorld | expressionMeaning cw (causalScale i)}

The scale is a Horn scale. Its meanings are strictly antitone in scale position, each member entailing the weaker ones and not conversely, the specificity hierarchy caused_implies_enabled and enabled_implies_affected.

Aspects from a structural model

inductive BellerGerstenberg2025.Var : Type

The variables of a two-event structural model are the candidate cause and the outcome.

• cause : Var
• effect : Var

@[instance_reducible]

instance BellerGerstenberg2025.instDecidableEqVar : DecidableEq Var

Equations

• BellerGerstenberg2025.instDecidableEqVar x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance BellerGerstenberg2025.instFintypeVar : Fintype Var

Equations

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

@[instance_reducible]

instance BellerGerstenberg2025.instReprVar : Repr Var

Equations

• BellerGerstenberg2025.instReprVar = { reprPrec := BellerGerstenberg2025.instReprVar.repr }

def BellerGerstenberg2025.instReprVar.repr : Var → ℕ → Std.Format

Equations

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

def BellerGerstenberg2025.launchEdges : Finset (Var × Var)

The outcome depends on the candidate cause alone.

Equations

• BellerGerstenberg2025.launchEdges = {(BellerGerstenberg2025.Var.cause, BellerGerstenberg2025.Var.effect)}

structure BellerGerstenberg2025.LaunchContext : Type

The context settles whether the candidate cause occurs.

• cause : Bool

def BellerGerstenberg2025.launch : CausalModel LaunchContext Var fun (x : Var) => Bool

In Michottean launching the outcome takes the candidate cause's value.

Equations

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

@[instance_reducible]

instance BellerGerstenberg2025.instDecidableRelVarAdjGraphLaunchContextBoolLaunch : DecidableRel launch.graph.Adj

Equations

• BellerGerstenberg2025.instDecidableRelVarAdjGraphLaunchContextBoolLaunch w v = BellerGerstenberg2025.instDecidableRelVarAdjGraphLaunchContextBoolLaunch._aux_1 w v

instance BellerGerstenberg2025.instIsAcyclicLaunchContextVarBoolLaunch : launch.IsAcyclic

noncomputable def BellerGerstenberg2025.CausalWorld.ofModel {U : Type u_1} {V : Type u_2} [Fintype V] [DecidableEq V] (M : CausalModel U V fun (x : V) => Bool) [M.IsAcyclic] [DecidableRel M.graph.Adj] (removed : V → Flat Bool) (u : U) (cause effect : V) : CausalWorld

The aspect profile of cause → effect in the context u of a deterministic model. W is whether-causation (1), that had the cause been absent the effect would not have been present. H is a direct law, and S is sufficient-causation (3), whether-causation under the intervention removed that takes the alternative causes away.

Equations

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

theorem BellerGerstenberg2025.launch_ofModel : CausalWorld.ofModel launch ⊥ { cause := true } Var.cause Var.effect = Scenario.s1.aspects

Michottean launching, in the context where the cause occurs, computes the profile of the first scenario, since with no alternative causes to remove sufficient-causation is whether-causation.