Causative and implicative verb features

This file defines two classifications carried by verb lexical entries: Causative, the force-dynamic mechanism a causative verb lexicalizes, and Implicative, the polarity of an implicative verb's complement entailment.

References

• Lauri Karttunen, Implicative Verbs
• Prerna Nadathur and Sven Lauer, Causal Necessity, Causal Sufficiency, and the Implications of Causative Verbs
• Leonard Talmy, Force dynamics in language and cognition
• Phillip Wolff, Direct causation in the linguistic coding and individuation of causal events

Force-dynamic causatives

inductive Causative : Type

Force-dynamic classification of causative verbs by the causal mechanism the verb lexicalizes. Causative.toSemantics (in Semantics/Causation/Interpretation.lean) maps each variant to its truth conditions.

• cause : Causative

  Counterfactual dependence: removing the cause blocks the effect (cause).

• make : Causative

  Direct sufficient guarantee: adding the cause ensures the effect (make).

• force : Causative

  Coercive sufficiency: the causer overcomes the causee's resistance (force).

• enable : Causative

  Permissive: the causer removes a barrier so the effect can occur (let).

• prevent : Causative

  Blocking: the causer adds a barrier so the effect cannot occur (prevent).

@[instance_reducible]

instance instDecidableEqCausative : DecidableEq Causative

Equations

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

@[instance_reducible]

instance instReprCausative : Repr Causative

Equations

• instReprCausative = { reprPrec := instReprCausative.repr }

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

Equations

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

def Causative.AssertsSufficiency (b : Causative) : Prop

The variant asserts causal sufficiency: make, force, and enable share sufficiency truth conditions (AssertsSufficiency.toSemantics_eq).

Equations

• b.AssertsSufficiency = (b = Causative.make ∨ b = Causative.force ∨ b = Causative.enable)

@[instance_reducible]

instance Causative.instDecidablePredAssertsSufficiency : DecidablePred AssertsSufficiency

Equations

• b.instDecidablePredAssertsSufficiency = id inferInstance

Implicative polarity

inductive Implicative : Type

Polarity for implicative verbs: positive implicatives entail their complement, negative implicatives entail its negation.

• positive : Implicative

  The verb entails its complement (manage, remember).

• negative : Implicative

  The verb entails the negation of its complement (fail, forget).

@[instance_reducible]

instance instDecidableEqImplicative : DecidableEq Implicative

Equations

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

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

Equations

• instReprImplicative.repr Implicative.positive prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Implicative.positive")).group prec✝
• instReprImplicative.repr Implicative.negative prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Implicative.negative")).group prec✝

@[instance_reducible]

instance instReprImplicative : Repr Implicative

Equations

• instReprImplicative = { reprPrec := instReprImplicative.repr }