Causative Interpretation (force-dynamic dispatch)

[NL20] [Tal88] [Wol03]

Maps Causative verb classifications to their compositional semantics under the force-dynamic view ([Tal88], [Wol03]), which collapses enable/force/make into a single sufficiency predicate (causallySufficient) distinguished post-hoc by isCoercive/isPermissive.

Causative	Mechanism	English verbs	N&L property (derived)
cause	Counterfactual dependence	cause	necessity
make	Direct sufficient guarantee	make, have, get	sufficiency
force	Coercive (overcome resistance)	force	sufficiency + coercion
enable	Barrier removal (permissive)	let, enable	sufficiency
prevent	Barrier addition (blocking)	prevent	preventSem

Theoretical commitment

This file commits to the force-dynamic mapping. The competing causal-model-theoretic view ([SBH09]) distinguishes enable from make/cause structurally: enable asserts B := A ∧ X (accessory variable required), while cause asserts B := A. Under that view, the present Causative.toSemantics mis-classifies enable. The Sloman alternative dispatch — and a divergence theorem witnessing the disagreement on enable — lives in Studies/SlomanBarbeyHotaling2009.lean.

This is intentional. linglib does not pretend a single canonical mapping exists; both dispatches coexist as named functions and the disagreement is theorem-provable.

Methods on Features.Causative that depend on heavy semantic machinery (Causation.SEM, CausalGraph, the Necessity/ Sufficiency/Prevention modules) live here rather than in Features/Causation.lean, which is kept import-free per the "Features/ stays lightweight" convention. The namespace Features.Causative block below is the standard mathlib pattern for distributing methods on a type across files based on import weight.

def Features.Causative.selectionMode : Causative → Causation.CCSelection.CCSelectionMode

The CC-selection mode associated with each variant.

• .cause selects any necessary condition → memberOfSufficientSet
• .make/.force/.enable select the completing condition → completionOfSufficientSet
• .prevent selects the condition that blocks the effect → completionOfSufficientSet (the preventer completes the blocking set)

Equations

• Features.Causative.cause.selectionMode = Causation.CCSelection.CCSelectionMode.memberOfSufficientSet
• Features.Causative.make.selectionMode = Causation.CCSelection.CCSelectionMode.completionOfSufficientSet
• Features.Causative.force.selectionMode = Causation.CCSelection.CCSelectionMode.completionOfSufficientSet
• Features.Causative.enable.selectionMode = Causation.CCSelection.CCSelectionMode.completionOfSufficientSet
• Features.Causative.prevent.selectionMode = Causation.CCSelection.CCSelectionMode.completionOfSufficientSet

noncomputable def Features.Causative.toSemantics {V : Type u_1} {α : V → Type u_2} [Fintype V] [DecidableEq V] [Causation.DecidableValuation α] [(v : V) → Fintype (α v)] (M : Causation.SEM V α) [M.graph.IsDAG] [M.IsDeterministic] : Causative → Causation.Valuation α → (c : V) → α c → (e : V) → α e → Prop

Force-dynamic dispatch: map a causative classification to its V2 polymorphic semantic function.

Equations

• Features.Causative.toSemantics M Features.Causative.cause = Causation.Necessity.causeSem M
• Features.Causative.toSemantics M Features.Causative.make = Causation.Sufficiency.makeSem M
• Features.Causative.toSemantics M Features.Causative.force = Causation.Sufficiency.makeSem M
• Features.Causative.toSemantics M Features.Causative.enable = Causation.Sufficiency.makeSem M
• Features.Causative.toSemantics M Features.Causative.prevent = Causation.Prevention.preventSem M

theorem Causation.Interpretation.make_force_distinguished_by_coercion : Features.Causative.make.isCoercive = false ∧ Features.Causative.force.isCoercive = true

make and force are distinguished by coercion despite sharing truth conditions.

theorem Causation.Interpretation.make_enable_distinguished_by_permissivity : Features.Causative.make.isPermissive = false ∧ Features.Causative.enable.isPermissive = true

make and enable are distinguished by permissivity despite sharing truth conditions.

Causative encodes force-dynamic mechanisms; CCSelectionMode ([BBS25]) encodes which element of a causal model the construction can select as "the cause." These are orthogonal but connected: each variant has a canonical selection mode.

theorem Causation.Interpretation.sufficiency_selects_completion (b : Features.Causative) (h : b.assertsSufficiency = true) : b.selectionMode = CCSelection.CCSelectionMode.completionOfSufficientSet

Sufficiency variants have completion selection mode.

theorem Causation.Interpretation.necessity_selects_member : Features.Causative.cause.selectionMode = CCSelection.CCSelectionMode.memberOfSufficientSet

Necessity variant has member selection mode.