Karttunen 1971: Implicative Verbs [Kar71]

Implicative Verbs. Language 47(2): 340–358.

Core Contribution

Complement-taking predicates that take infinitival complements divide into implicative and non-implicative classes based on complement entailment:

• Implicative (manage, remember, bother): "managed to VP" → VP; "didn't manage to VP" → ¬VP. Two-way entailment.
• Non-implicative (hope, want, intend): no complement entailment.
• Negative implicatives (fail, forget): entail ¬complement.
• Sufficient-only (force, cause): affirmative → complement, but negation ↛ ¬complement.
• Necessary-only (be able, possible): negation → ¬complement, but affirmative ↛ complement.

Historical Context

Karttunen's 2×2 classification (necessary × sufficient) was the original descriptive taxonomy. The modern consensus ([Nad23a]) derives the entailment patterns from causal structure rather than from presuppositional schemas. The theory layer (Causation/Implicative.lean) implements the modern causal analysis; this study file preserves Karttunen's original classification. The bridges to the modern types live with the papers that draw them: Studies/Nadathur2023.lean (classification conversion) and Studies/NadathurLauer2020.lean (entailment cells vs causal mechanism).

Key differences from the modern analysis:

• Karttunen treats the entailment as arising from a presupposition that v(S) is a nec/suf condition for S. Nadathur derives it from causal sufficiency in a structural equation model.
• Karttunen's classification ignores aspect. Nadathur shows that be able is aspect-governed (perfective triggers entailment, imperfective doesn't).
• Karttunen groups force/cause/make together (ex. 56) as having the same entailment pattern (sufficient-only). Nadathur & Lauer show they have the same entailment pattern but different truth conditions: make/force assert causal sufficiency, while cause asserts causal necessity. This difference surfaces in overdetermination scenarios.

Karttunen's schemas: - (37) nec + suf: PRESUP v(S) is nec+suf for S. PROP v(S). - (41) nec + suf (neg): same but for ¬S. - (54) nec only: PRESUP v(S) is nec for S. PROP v(S). - (59) suf only: PRESUP v(S) is suf for S. PROP v(S). - neither: no complement entailment.

structure Karttunen1971.KarttunenClass : Type

Karttunen's descriptive classification of complement-entailing predicates as a 2×2: necessary × sufficient × polarity.

This is the historical taxonomy from the 1971 paper. The modern causal analysis uses ImplicativeClass (which adds aspectGoverned) and Causative (which distinguishes causal mechanisms).

• isSufficient : Bool

  v(S) is sufficient for S: affirmative entails complement.

• isNecessary : Bool

  v(S) is necessary for S: negation entails ¬complement.

• polarity : Features.Implicative

  Positive (manage: entails S) vs negative (fail: entails ¬S).

def Karttunen1971.instDecidableEqKarttunenClass.decEq (x✝ x✝¹ : KarttunenClass) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance Karttunen1971.instDecidableEqKarttunenClass : DecidableEq KarttunenClass

Equations

• Karttunen1971.instDecidableEqKarttunenClass = Karttunen1971.instDecidableEqKarttunenClass.decEq

def Karttunen1971.instReprKarttunenClass.repr : KarttunenClass → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Karttunen1971.instReprKarttunenClass : Repr KarttunenClass

Equations

• Karttunen1971.instReprKarttunenClass = { reprPrec := Karttunen1971.instReprKarttunenClass.repr }

def Karttunen1971.KarttunenClass.manage : KarttunenClass

Equations

• Karttunen1971.KarttunenClass.manage = { isSufficient := true, isNecessary := true, polarity := Features.Implicative.positive }

def Karttunen1971.KarttunenClass.fail : KarttunenClass

Equations

• Karttunen1971.KarttunenClass.fail = { isSufficient := true, isNecessary := true, polarity := Features.Implicative.negative }

def Karttunen1971.KarttunenClass.force : KarttunenClass

Sufficient only: "forced X to VP" → VP; "didn't force" ↛ ¬VP.

Equations

• Karttunen1971.KarttunenClass.force = { isSufficient := true, isNecessary := false, polarity := Features.Implicative.positive }

def Karttunen1971.KarttunenClass.prevent : KarttunenClass

Sufficient only, negative: "prevented X from VP-ing" → ¬VP.

Equations

• Karttunen1971.KarttunenClass.prevent = { isSufficient := true, isNecessary := false, polarity := Features.Implicative.negative }

def Karttunen1971.KarttunenClass.beAble : KarttunenClass

Necessary only: "wasn't able to VP" → ¬VP; "was able" ↛ VP.

Equations

• Karttunen1971.KarttunenClass.beAble = { isSufficient := false, isNecessary := true, polarity := Features.Implicative.positive }

def Karttunen1971.KarttunenClass.hope : KarttunenClass

Neither: hope, want, intend.

Equations

• Karttunen1971.KarttunenClass.hope = { isSufficient := false, isNecessary := false, polarity := Features.Implicative.positive }

def Karttunen1971.KarttunenClass.isTwoWay (k : KarttunenClass) : Bool

Equations

• k.isTwoWay = (k.isNecessary && k.isSufficient)

def Karttunen1971.KarttunenClass.hasEntailment (k : KarttunenClass) : Bool

Equations

• k.hasEntailment = (k.isNecessary || k.isSufficient)

theorem Karttunen1971.manage_isTwoWay : KarttunenClass.manage.isTwoWay = true

theorem Karttunen1971.fail_isTwoWay : KarttunenClass.fail.isTwoWay = true

theorem Karttunen1971.force_not_twoWay : KarttunenClass.force.isTwoWay = false

theorem Karttunen1971.beAble_not_twoWay : KarttunenClass.beAble.isTwoWay = false

theorem Karttunen1971.hope_no_entailment : KarttunenClass.hope.hasEntailment = false

theorem Karttunen1971.manage_fail_same_profile : KarttunenClass.manage.isNecessary = KarttunenClass.fail.isNecessary ∧ KarttunenClass.manage.isSufficient = KarttunenClass.fail.isSufficient ∧ KarttunenClass.manage.polarity ≠ KarttunenClass.fail.polarity

manage and fail differ only in polarity.

theorem Karttunen1971.force_prevent_same_profile : KarttunenClass.force.isNecessary = KarttunenClass.prevent.isNecessary ∧ KarttunenClass.force.isSufficient = KarttunenClass.prevent.isSufficient ∧ KarttunenClass.force.polarity ≠ KarttunenClass.prevent.polarity

force and prevent differ only in polarity.

Verify that Fragment verb entries carry the correct annotations, matching Karttunen's inventory (ex. 2, p.341).

theorem Karttunen1971.manage_positive_implicative : English.Predicates.Verbal.manage.implicative = some Features.Implicative.positive

theorem Karttunen1971.remember_positive_implicative : English.Predicates.Verbal.remember.implicative = some Features.Implicative.positive

theorem Karttunen1971.dare_positive_implicative : English.Predicates.Verbal.dare.implicative = some Features.Implicative.positive

theorem Karttunen1971.bother_positive_implicative : English.Predicates.Verbal.bother.implicative = some Features.Implicative.positive

theorem Karttunen1971.venture_positive_implicative : English.Predicates.Verbal.venture.implicative = some Features.Implicative.positive

theorem Karttunen1971.condescend_positive_implicative : English.Predicates.Verbal.condescend.implicative = some Features.Implicative.positive

theorem Karttunen1971.happen_positive_implicative : English.Predicates.Verbal.happen.implicative = some Features.Implicative.positive

theorem Karttunen1971.fail_negative_implicative : English.Predicates.Verbal.fail.implicative = some Features.Implicative.negative

theorem Karttunen1971.forget_negative_implicative : English.Predicates.Verbal.forget.implicative = some Features.Implicative.negative

theorem Karttunen1971.neglect_negative_implicative : English.Predicates.Verbal.neglect.implicative = some Features.Implicative.negative

theorem Karttunen1971.hope_not_implicative : English.Predicates.Verbal.hope.implicative = none

theorem Karttunen1971.want_not_implicative : English.Predicates.Verbal.want.implicative = none

theorem Karttunen1971.try_not_implicative : English.Predicates.Verbal.try_.implicative = none

theorem Karttunen1971.believe_not_implicative : English.Predicates.Verbal.believe.implicative = none

theorem Karttunen1971.manage_entails : English.Predicates.Verbal.manage.entailsComplement = some true

theorem Karttunen1971.fail_entails_not : English.Predicates.Verbal.fail.entailsComplement = some false

theorem Karttunen1971.hope_no_complement_entailment : English.Predicates.Verbal.hope.entailsComplement = none

theorem Karttunen1971.happen_is_raising : English.Predicates.Verbal.happen.controlType = ControlType.raising

happen is a raising verb, not subject-control. "It happened to rain" is grammatical — the matrix subject receives no theta role from happen. Karttunen (§9) describes happen's presupposition as chance-dependence, but does not discuss its syntactic control type.

theorem Karttunen1971.dare_presup_and_implicative : English.Predicates.Verbal.dare.presupType = some PresupTriggerType.prerequisiteSoft ∧ English.Predicates.Verbal.dare.implicative = some Features.Implicative.positive

dare and bother have both presupposition (occasion verbs) AND implicative entailment: "John dared to speak" presupposes risk AND entails "John spoke." These are compatible per Karttunen §9.

theorem Karttunen1971.bother_presup_and_implicative : English.Predicates.Verbal.bother.presupType = some PresupTriggerType.prerequisiteSoft ∧ English.Predicates.Verbal.bother.implicative = some Features.Implicative.positive

The key diagnostic: factives preserve complement presupposition under negation; implicatives reverse the complement entailment.

"John didn't realize he had no money" — still presupposes "he had no money."
"John didn't manage to solve it" — entails "he didn't solve it." 

theorem Karttunen1971.know_factive_not_implicative : English.Predicates.Verbal.know.presupType = some PresupTriggerType.softTrigger ∧ English.Predicates.Verbal.know.implicative = none

theorem Karttunen1971.manage_implicative_not_factive : English.Predicates.Verbal.manage.implicative = some Features.Implicative.positive ∧ English.Predicates.Verbal.manage.presupType = some PresupTriggerType.prerequisiteSoft

theorem Karttunen1971.hope_neither : English.Predicates.Verbal.hope.presupType = none ∧ English.Predicates.Verbal.hope.implicative = none

theorem Karttunen1971.force_has_causative : English.Predicates.Verbal.force.causative = some Features.Causative.force

theorem Karttunen1971.force_asserts_sufficiency : Features.Causative.force.assertsSufficiency = true

theorem Karttunen1971.force_no_necessity : Features.Causative.force.assertsNecessity = false

The grounding chain: KarttunenClass → Implicative → causal semantics → complement entailment.

For sufficient-positive classes, the chain is:
`KarttunenClass.manage.polarity` = `.positive`
→ `Implicative.positive.toSemantics` = `manageSem`
→ `manage_entails_complement`: manageSem sc → complement true

These theorems derive the entailment from the classification,
not just re-export the theory-layer theorem. 

sufficient_positive_class_entails / sufficient_negative_class_entails / manage_class_entails / fail_class_entails — these grounded KarttunenClass.polarity.toSemantics chain theorems were over the legacy ImplicativeScenario/normalDevelopment substrate; deleted in Phase D-H. The polymorphic V2 analog is direct: for any BoolSEM V and a positive (resp. negative) KarttunenClass, Implicative.toSemantics M .positive bg p xP c xC IS Implicative.manageSem M bg p xP c xC IS SEM.causallySufficient M bg p xP c xC (rfl-chain).

Double negation cancellation is a signature property of implicative verbs. Karttunen's examples:

- (13) "John didn't remember not to lock his door" → "John locked his door."
- (40a) "John didn't forget to lock his door" → (40d) "John locked his door."

The current causal semantics models the *positive* direction
(manageSem → complement true) and the *negative* direction
(failSem → complement false) separately. Full double negation
— where matrix negation and complement negation interact to yield
a positive entailment — would require compositional negation over
the causal model, which is not yet formalized.

What we CAN verify: the two directions (positive entailment, negative
entailment) are separately grounded, and two-way KarttunenClasses
predict both directions. 

theorem Karttunen1971.two_way_has_both_directions (k : KarttunenClass) (hTwoWay : k.isTwoWay = true) : k.isSufficient = true ∧ k.isNecessary = true

Two-way classes predict entailment in BOTH directions: the positive polarity grounds the affirmative direction, the negative polarity grounds the negation direction.

theorem Karttunen1971.all_cells_populated : KarttunenClass.manage.isTwoWay = true ∧ KarttunenClass.force.isTwoWay = false ∧ KarttunenClass.beAble.isTwoWay = false ∧ KarttunenClass.hope.hasEntailment = false

All four cells of the 2×2 are populated by Fragment entries.

theorem Karttunen1971.beAble_not_lexical_implicative : English.Predicates.Copular.beAble.implicative = none

be able is NOT a lexical implicative — it has no implicative. The actuality entailment is aspect-governed ([Nad23a]): perfective "was able to VP" → VP; imperfective "was able to VP" ↛ VP. Karttunen (§11) notes these verbs are ambiguous between implicative and non-implicative readings.

theorem Karttunen1971.beAble_infinitival_subject_control : English.Predicates.Copular.beAble.complementType = ComplementType.infinitival ∧ English.Predicates.Copular.beAble.controlType = ControlType.subjectControl

be able takes infinitival complement with subject control. "He was able to leave" — the subject has the ability (theta role).

Tension with Noonan's Reality Status

[noonan-2007] classifies achievement CTPs (*manage*, *fail*) as
IRREALIS because they take infinitival complements. But Karttunen shows
these verbs ENTAIL complement truth — semantically realis. Complement
*form* (irrealis) and complement *entailment* (realis) diverge for
implicative verbs.