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 (makeSem); the three remain distinct lexical classifications.

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 `Causative` #

Methods on Causative that depend on heavy semantic machinery (Causation.SEM, CausalGraph, the Necessity/ Sufficiency/Prevention modules) live here rather than in Semantics/Causation/VerbClass.lean, which is kept import-free.

source

def 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

Instances For

source

noncomputable def 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

Instances For

source

theorem Causative.AssertsSufficiency.toSemantics_eq {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] {b : Causative} (h : b.AssertsSufficiency) :

toSemantics M b = Causation.Sufficiency.makeSem M

Sufficiency-asserting variants share makeSem truth conditions: the AssertsSufficiency classification tracks the force-dynamic dispatch.

Derivation theorems (substrate-independent) #

Bridge to CC-Selection #

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.

source