Features.Causation

@cite{talmy-1988} @cite{wolff-2003} @cite{karttunen-1971} @cite{nadathur-2024}

Per-verb-entry feature taxonomies for causal verb classifications: the Causative enum (force-dynamic mechanism) and the Implicative enum (Karttunen complement-entailment polarity).

Provenance

Bundled together (rather than 2 separate single-enum files) per the mathlib idiom of co-locating peer concepts. Moved from Core/Lexical/VerbClass.lean in the cleanup that dissolved Core/Lexical/.

Framework commitment

Both enums here encode specific theoretical commitments rather than neutral substrate:

• Causative (Causative): the 5-way cause/make/force/enable/prevent split is linglib's extension of the 3-way force-dynamic taxonomy of @cite{wolff-2003} (CAUSE / ENABLE / PREVENT). The substrate subdivides Wolff's CAUSE category into {cause, make, force} to carry the counterfactual-dependence (cause) vs direct-sufficient- guarantee (make) vs coercive-sufficiency (force) distinctions that @cite{talmy-1988} discusses but does not crystallize as named primitives. The assertsSufficiency/assertsNecessity/isCoercive/ isPermissive derivations match the @cite{nadathur-lauer-2020} sufficiency/necessity decomposition.

  Major non-force-dynamic frameworks for causation:

  • @cite{comrie-1989} typological scale (lexical / morphological / syntactic causatives, with implications for productivity).
  • Shibatani 1976 / Shibatani & Pardeshi 2002 directness typology (direct vs indirect causation correlating with morphological vs analytic encoding); not currently in references.bib.
  • @cite{pylkkanen-2008} Voice/Cause-head theory (where the cause head is a separately licensed functional element). None of these carve verbs into exactly the 5 cases here.

  See Theories/Semantics/Causation/Interpretation.lean for the force-dynamic mapping to truth conditions; alternative analyses live in sibling Theories files.

• Implicative (Implicative): the binary positive/negative split is the @cite{karttunen-1971} bipartition. Finer-grained alternatives: Karttunen 2012 / Nairn et al. 2006 9-way matrix (++/+-/-+/ --/+o/o+/-o/o-/oo) capturing both one-direction and two-direction implications, and update-semantics revisions that treat implicativity as projection through context rather than direct entailment. The substrate fixes 2 cases; richer frameworks need their own enum (planned slot: Theories/Semantics/Implicative/NairnCondoravdiKarttunen.lean).

UNVERIFIED: Shibatani 1976 / Shibatani & Pardeshi 2002 publication details and Karttunen 2012 / Nairn-Condoravdi-Karttunen 2006 9-way matrix details cited from memory; verify before adding to references.bib.

inductive Features.Causative : Type

How a causative verb's semantics is built from causal model infrastructure.

Names a force-dynamic mechanism, not a causal-model property. toSemantics (in Theories/Semantics/Causation/Interpretation.lean) maps each variant to its truth-condition function; properties like sufficiency/necessity are derived via theorems.

• cause: Counterfactual dependence — removing cause blocks effect.
• make: Direct sufficient guarantee — adding cause ensures effect.
• force: Coercive sufficiency — overcome resistance, no alternatives.
• enable: Permissive — remove barrier so effect can occur.
• prevent: Blocking — add barrier so effect cannot occur.

• cause : Causative

  Counterfactual dependence: removing cause → no effect. Semantic function: causeSem.

• make : Causative

  Direct sufficient guarantee: adding cause → effect. Semantic function: causallySufficient.

• force : Causative

  Coercive sufficiency: overcome resistance, no alternatives. Same truth conditions as make; distinguished by isCoercive.

• enable : Causative

  Permissive: remove barrier so effect can occur. Same truth conditions as make; distinguished by isPermissive.

• prevent : Causative

  Blocking: add barrier so effect cannot occur. Semantic function: preventSem (dual of causeSem).

@[implicit_reducible]

instance Features.instDecidableEqCausative : DecidableEq Causative

Equations

• Features.instDecidableEqCausative x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Features.instReprCausative.repr : Causative → Nat → Std.Format

Equations

• Features.instReprCausative.repr Features.Causative.cause prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Features.Causative.cause")).group prec✝
• Features.instReprCausative.repr Features.Causative.make prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Features.Causative.make")).group prec✝
• Features.instReprCausative.repr Features.Causative.force prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Features.Causative.force")).group prec✝
• Features.instReprCausative.repr Features.Causative.enable prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Features.Causative.enable")).group prec✝
• Features.instReprCausative.repr Features.Causative.prevent prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Features.Causative.prevent")).group prec✝

@[implicit_reducible]

instance Features.instReprCausative : Repr Causative

Equations

• Features.instReprCausative = { reprPrec := Features.instReprCausative.repr }

def Features.Causative.assertsSufficiency : Causative → Bool

Does this variant assert causal sufficiency (N&L Def 23)?

DERIVED: true for variants whose toSemantics maps to causallySufficient.

UNVERIFIED: Nadathur & Lauer Def 23 reference cited from memory.

Equations

• Features.Causative.make.assertsSufficiency = true
• Features.Causative.force.assertsSufficiency = true
• Features.Causative.enable.assertsSufficiency = true
• Features.Causative.cause.assertsSufficiency = false
• Features.Causative.prevent.assertsSufficiency = false

def Features.Causative.assertsNecessity : Causative → Bool

Does this variant assert causal necessity (N&L Def 24)?

DERIVED: true only for .cause, whose toSemantics maps to causeSem.

UNVERIFIED: Nadathur & Lauer Def 24 reference cited from memory.

Equations

• Features.Causative.cause.assertsNecessity = true
• x✝.assertsNecessity = false

def Features.Causative.isCoercive : Causative → Bool

Does this variant encode coercion (overcoming resistance)?

Force-dynamic property: .force encodes that the causer overcame the causee's resistance.

Equations

• Features.Causative.force.isCoercive = true
• x✝.isCoercive = false

def Features.Causative.isPermissive : Causative → Bool

Does this variant encode permissivity (barrier removal)?

Force-dynamic property: .enable encodes that the causer removed a barrier, allowing the effect to occur naturally.

Equations

• Features.Causative.enable.isPermissive = true
• x✝.isPermissive = false

inductive Features.Implicative : Type

Polarity for implicative verbs.

Positive implicatives (manage, remember) entail the complement on success. Negative implicatives (fail, forget) entail the complement does NOT hold on success.

Note: Implicative and Causative are structurally different (@cite{nadathur-2024}): causatives directly predicate causation (make/cause → sufficiency/necessity), while implicatives predicate a prerequisite whose causal relationship to the complement is only presupposed.

• positive : Implicative
• negative : Implicative

@[implicit_reducible]

instance Features.instDecidableEqImplicative : DecidableEq Implicative

Equations

• Features.instDecidableEqImplicative x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Features.instReprImplicative.repr : Implicative → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Features.instReprImplicative : Repr Implicative

Equations

• Features.instReprImplicative = { reprPrec := Features.instReprImplicative.repr }

def Features.Implicative.entailsComplement : Implicative → Bool

Whether the verb entails the complement (positive) or its negation (negative).

Equations

• Features.Implicative.positive.entailsComplement = true
• Features.Implicative.negative.entailsComplement = false