The Three Measures (§2.2-2.4)

All three are defined within structural causal models. In the general case they are continuous ∈ [0,1] (or ℕ for ALT). Our deterministic CausalDynamics yields the boundary cases.

structure CaoWhiteLassiter2025.CausalMeasures : Type

The three causal measures that jointly predict causative verb acceptability.

• suf: Probability of sufficiency. Continuous [0,1]. In the deterministic limit, collapses to causallySufficient.
• int: Degree of intention. Continuous [0,1]. How much the causer intended the outcome relative to alternatives.
• alt: Number of alternative actions available to the causee. ℕ. Fewer alternatives → stronger causal influence.

• suf : ℚ
• int : ℚ
• alt : ℕ

instance CaoWhiteLassiter2025.instReprCausalMeasures : Repr CausalMeasures

Equations

• CaoWhiteLassiter2025.instReprCausalMeasures = { reprPrec := CaoWhiteLassiter2025.instReprCausalMeasures.repr }

def CaoWhiteLassiter2025.instReprCausalMeasures.repr : CausalMeasures → ℕ → Std.Format

Equations

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

def CaoWhiteLassiter2025.instDecidableEqCausalMeasures.decEq (x✝ x✝¹ : CausalMeasures) : Decidable (x✝ = x✝¹)

Equations

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

instance CaoWhiteLassiter2025.instDecidableEqCausalMeasures : DecidableEq CausalMeasures

Equations

• CaoWhiteLassiter2025.instDecidableEqCausalMeasures = CaoWhiteLassiter2025.instDecidableEqCausalMeasures.decEq

def CaoWhiteLassiter2025.instBEqCausalMeasures.beq : CausalMeasures → CausalMeasures → Bool

Equations

• CaoWhiteLassiter2025.instBEqCausalMeasures.beq { suf := a, int := a_1, alt := a_2 } { suf := b, int := b_1, alt := b_2 } = (a == b && (a_1 == b_1 && a_2 == b_2))
• CaoWhiteLassiter2025.instBEqCausalMeasures.beq x✝¹ x✝ = false

instance CaoWhiteLassiter2025.instBEqCausalMeasures : BEq CausalMeasures

Equations

• CaoWhiteLassiter2025.instBEqCausalMeasures = { beq := CaoWhiteLassiter2025.instBEqCausalMeasures.beq }

Deterministic SUF

When the causal model is deterministic (as in CausalDynamics), SUF collapses to a binary value matching causallySufficient.

def CaoWhiteLassiter2025.deterministicSuf (dyn : Core.StructuralEquationModel.CausalDynamics) (background : Core.StructuralEquationModel.Situation) (cause effect : Core.StructuralEquationModel.Variable) : ℚ

Compute SUF from a deterministic causal model.

In a deterministic model, SUF is either 0 or 1:

• 1 when the cause guarantees the effect (= causallySufficient)
• 0 otherwise

Equations

• CaoWhiteLassiter2025.deterministicSuf dyn background cause effect = if Core.StructuralEquationModel.causallySufficient dyn background cause effect = true then 1 else 0

theorem CaoWhiteLassiter2025.deterministicSuf_iff_sufficient (dyn : Core.StructuralEquationModel.CausalDynamics) (bg : Core.StructuralEquationModel.Situation) (c e : Core.StructuralEquationModel.Variable) : deterministicSuf dyn bg c e = 1 ↔ Core.StructuralEquationModel.causallySufficient dyn bg c e = true

Deterministic SUF = 1 iff binary causallySufficient holds.

This is the grounding theorem connecting Cao et al.'s probabilistic SUF to Nadathur & Lauer's structural sufficiency.

theorem CaoWhiteLassiter2025.deterministicSuf_zero_iff_not_sufficient (dyn : Core.StructuralEquationModel.CausalDynamics) (bg : Core.StructuralEquationModel.Situation) (c e : Core.StructuralEquationModel.Variable) : deterministicSuf dyn bg c e = 0 ↔ Core.StructuralEquationModel.causallySufficient dyn bg c e = false

Deterministic SUF = 0 iff binary causallySufficient fails.

ALT → ActionType Bridge

Cao et al.'s continuous ALT measure generalizes the binary Volitional/NonVolitional distinction in CoerciveImplication.

def CaoWhiteLassiter2025.altToActionType (alt : ℕ) : NadathurLauer2020.CoerciveImplication.ActionType

Map ALT count to the categorical ActionType from CoerciveImplication.

• ALT = 0: causee had no choice → NonVolitional (forced action)
• ALT > 0: causee could have done otherwise → Volitional

This connects Cao et al.'s graded ALT to Nadathur & Lauer's binary volitionality, used in the coercive implication analysis.

Equations

• CaoWhiteLassiter2025.altToActionType alt = if alt > 0 then NadathurLauer2020.CoerciveImplication.ActionType.Volitional else NadathurLauer2020.CoerciveImplication.ActionType.NonVolitional

theorem CaoWhiteLassiter2025.alt_zero_nonvolitional : altToActionType 0 = NadathurLauer2020.CoerciveImplication.ActionType.NonVolitional

theorem CaoWhiteLassiter2025.alt_positive_volitional (n : ℕ) (h : n > 0) : altToActionType n = NadathurLauer2020.CoerciveImplication.ActionType.Volitional

Interaction Profiles (Table 1)

The core empirical finding: each verb has a unique set of reliable interaction terms among SUF, INT, and ALT.

inductive CaoWhiteLassiter2025.InteractionTerm : Type

Two-way and three-way interaction terms from the regression model.

These correspond to the product terms in the Bayesian regression (Model I, Table 2). An interaction is "reliable" when its 95% credible interval excludes 0.

• sufInt : InteractionTerm
• sufAlt : InteractionTerm
• intAlt : InteractionTerm
• sufIntAlt : InteractionTerm

instance CaoWhiteLassiter2025.instDecidableEqInteractionTerm : DecidableEq InteractionTerm

Equations

• CaoWhiteLassiter2025.instDecidableEqInteractionTerm x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance CaoWhiteLassiter2025.instReprInteractionTerm : Repr InteractionTerm

Equations

• CaoWhiteLassiter2025.instReprInteractionTerm = { reprPrec := CaoWhiteLassiter2025.instReprInteractionTerm.repr }

def CaoWhiteLassiter2025.instReprInteractionTerm.repr : InteractionTerm → ℕ → Std.Format

Equations

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

def CaoWhiteLassiter2025.instBEqInteractionTerm.beq : InteractionTerm → InteractionTerm → Bool

Equations

• CaoWhiteLassiter2025.instBEqInteractionTerm.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance CaoWhiteLassiter2025.instBEqInteractionTerm : BEq InteractionTerm

Equations

• CaoWhiteLassiter2025.instBEqInteractionTerm = { beq := CaoWhiteLassiter2025.instBEqInteractionTerm.beq }

structure CaoWhiteLassiter2025.InteractionProfile : Type

A verb's interaction profile: which interaction terms reliably predict its acceptability.

Each verb has a unique combination, supporting the claim that causative verb semantics is multidimensional.

• verb : String
• reliablePositive : List InteractionTerm
• reliableNegative : List InteractionTerm

def CaoWhiteLassiter2025.instReprInteractionProfile.repr : InteractionProfile → ℕ → Std.Format

Equations

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

instance CaoWhiteLassiter2025.instReprInteractionProfile : Repr InteractionProfile

Equations

• CaoWhiteLassiter2025.instReprInteractionProfile = { reprPrec := CaoWhiteLassiter2025.instReprInteractionProfile.repr }

def CaoWhiteLassiter2025.causeProfile : InteractionProfile

caused: SUF×ALT (+), INT×ALT (+), SUF×INT×ALT (-). No reliable SUF×INT interaction.

Equations

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

def CaoWhiteLassiter2025.makeProfile : InteractionProfile

made: SUF×INT (+), SUF×ALT (+), INT×ALT (+), SUF×INT×ALT (-). Uniquely has the SUF×INT interaction.

Equations

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

def CaoWhiteLassiter2025.forceProfile : InteractionProfile

forced: SUF×ALT (+), INT×ALT (+), SUF×INT×ALT (-). Same shape as caused but with different main effect intercepts.

Equations

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

theorem CaoWhiteLassiter2025.make_has_unique_sufInt : makeProfile.reliablePositive.contains InteractionTerm.sufInt = true ∧ causeProfile.reliablePositive.contains InteractionTerm.sufInt = false ∧ forceProfile.reliablePositive.contains InteractionTerm.sufInt = false ∧ causeProfile.reliableNegative.contains InteractionTerm.sufInt = false ∧ forceProfile.reliableNegative.contains InteractionTerm.sufInt = false

make uniquely has a reliable SUF×INT interaction.

This is the key finding distinguishing make from both cause and force. It means make's acceptability is sensitive to the joint contribution of sufficiency and intention in a way the other verbs are not.

theorem CaoWhiteLassiter2025.shared_interactions : causeProfile.reliablePositive.contains InteractionTerm.sufAlt = true ∧ makeProfile.reliablePositive.contains InteractionTerm.sufAlt = true ∧ forceProfile.reliablePositive.contains InteractionTerm.sufAlt = true ∧ causeProfile.reliablePositive.contains InteractionTerm.intAlt = true ∧ makeProfile.reliablePositive.contains InteractionTerm.intAlt = true ∧ forceProfile.reliablePositive.contains InteractionTerm.intAlt = true

All three verbs share the SUF×ALT and INT×ALT interactions. This reflects the common causal core.

Bridge to CausativeBuilder

The force-dynamic builder (@cite{wolff-2003} / @cite{talmy-1988}) provides a finer categorization than sufficiency/necessity alone. The graded model reveals that verbs with different builders (e.g., .make and .force) can still differ in their full semantics even when they share the same N&L truth conditions.

theorem CaoWhiteLassiter2025.make_force_both_assert_sufficiency_different_profiles : NadathurLauer2020.Builder.CausativeBuilder.make.assertsSufficiency = true ∧ NadathurLauer2020.Builder.CausativeBuilder.force.assertsSufficiency = true ∧ makeProfile.reliablePositive ≠ forceProfile.reliablePositive

make and force now have different CausativeBuilders (.make vs .force) but both assert sufficiency, and have different interaction profiles.

This demonstrates that the graded model provides information beyond even the fine-grained force-dynamic builder: make has a SUF×INT sensitivity that force lacks.

theorem CaoWhiteLassiter2025.graded_subsumes_binary (dyn : Core.StructuralEquationModel.CausalDynamics) (bg : Core.StructuralEquationModel.Situation) (c e : Core.StructuralEquationModel.Variable) : deterministicSuf dyn bg c e = 1 → NadathurLauer2020.Builder.CausativeBuilder.make.toSemantics dyn bg c e = true

The graded model subsumes the binary model.

In the deterministic limit (SUF ∈ {0,1}, no probabilistic INT), the graded verb selection reduces to the binary sufficiency/necessity distinction of CausativeBuilder.

Main Effects (Model I, Table 2)

The regression coefficients for the main effects, showing the direction and relative magnitude of each measure's contribution.

structure CaoWhiteLassiter2025.MainEffects : Type

Main effect coefficients from Model I (Table 2).

All three main effects are reliable (95% CI excludes 0):

• SUFresidALT: +1.19 (more sufficiency → more acceptable)
• INT: +0.54 (more intention → more acceptable)
• ALT: -0.82 (more alternatives → less acceptable)

Note the sign of ALT: more alternatives for the causee means weaker causal influence, hence lower acceptability for all verbs.

• sufResidAlt : ℚ
• int : ℚ
• alt : ℚ

instance CaoWhiteLassiter2025.instReprMainEffects : Repr MainEffects

Equations

• CaoWhiteLassiter2025.instReprMainEffects = { reprPrec := CaoWhiteLassiter2025.instReprMainEffects.repr }

def CaoWhiteLassiter2025.instReprMainEffects.repr : MainEffects → ℕ → Std.Format

Equations

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

def CaoWhiteLassiter2025.modelIMainEffects : MainEffects

Equations

• CaoWhiteLassiter2025.modelIMainEffects = { sufResidAlt := 119 / 100, int := 54 / 100, alt := -82 / 100 }

theorem CaoWhiteLassiter2025.suf_largest_main_effect : modelIMainEffects.sufResidAlt > modelIMainEffects.int ∧ modelIMainEffects.sufResidAlt > -modelIMainEffects.alt

SUF has the largest main effect, consistent with Nadathur & Lauer's emphasis on sufficiency as the core semantic content.

theorem CaoWhiteLassiter2025.alt_negative_effect : modelIMainEffects.alt < 0

ALT is negative: more alternatives → less acceptable. This is expected since fewer alternatives = stronger causal influence.