Implicative Verb Semantics

@cite{nadathur-2024} @cite{karttunen-1971} @cite{nadathur-lauer-2020}

Causal Semantics for Implicative Verbs. Journal of Semantics 40: 311–358.

Core Insight: The Prerequisite Account (Proposal 32)

Implicative verbs (manage, dare, fail) have complement entailments derived from causal structure. The prerequisite account (Proposal 32) decomposes implicative meaning into three components:

• (32i) Presuppose: ∃ prerequisite A(x) causally necessary for P(x)
• (32ii) Assert: x did A — the subject satisfied the prerequisite
• (32iii) Presuppose (two-way only): A(x) is the only unresolved causally necessary condition, hence causally sufficient for P(x)

One-way implicatives (jaksaa 'have the strength', pystyä 'be able') have only (32i)–(32ii), not (32iii). The missing positive entailment arises as a defeasible antiperfection implicature via circumscription.

Causal Grounding

manageSem (causal sufficiency of the prerequisite for the complement) is derived from the prerequisite account: when both the necessity presupposition (32i) and sufficiency presupposition (32iii) hold, and the assertion (32ii) establishes that A(x) is true, complement truth follows as a causal consequence. The entailment is not stipulated but emerges from the causal model.

Lexically-Specified Prerequisites

Specific implicatives lexicalize which prerequisite matters:

• dare/uskaltaa → courage
• bother/viitsiä → engagement/effort
• malttaa → patience
• hennoa → hard-heartedness
• jaksaa → strength
• manage/onnistua → underspecified (contextual enrichment)

inductive Nadathur2024.Implicative.Prerequisite : Type

Lexically-specified prerequisite types for implicative verbs.

The chief dimension of semantic variation between implicative verbs lies in what they lexicalize about the nature of the prerequisite — the sort of activity needed to overcome the potential obstacle.

Specific verbs (dare, bother) name their prerequisites; bleached verbs (manage, onnistua) leave the prerequisite underspecified.

• courage : Prerequisite
• engagement : Prerequisite
• patience : Prerequisite
• hardHeartedness : Prerequisite
• strength : Prerequisite
• fitness : Prerequisite
• time : Prerequisite
• shamelessness : Prerequisite
• unspecified : Prerequisite

instance Nadathur2024.Implicative.instDecidableEqPrerequisite : DecidableEq Prerequisite

Equations

• Nadathur2024.Implicative.instDecidableEqPrerequisite x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Nadathur2024.Implicative.instReprPrerequisite : Repr Prerequisite

Equations

• Nadathur2024.Implicative.instReprPrerequisite = { reprPrec := Nadathur2024.Implicative.instReprPrerequisite.repr }

def Nadathur2024.Implicative.instReprPrerequisite.repr : Prerequisite → ℕ → Std.Format

Equations

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

instance Nadathur2024.Implicative.instBEqPrerequisite : BEq Prerequisite

Equations

• Nadathur2024.Implicative.instBEqPrerequisite = { beq := Nadathur2024.Implicative.instBEqPrerequisite.beq }

def Nadathur2024.Implicative.instBEqPrerequisite.beq : Prerequisite → Prerequisite → Bool

Equations

• Nadathur2024.Implicative.instBEqPrerequisite.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Nadathur2024.Implicative.Prerequisite.isSpecific : Prerequisite → Bool

Is the prerequisite lexically specific (names a particular condition) or underspecified (contextual enrichment)?

Equations

• Nadathur2024.Implicative.Prerequisite.unspecified.isSpecific = false
• x✝.isSpecific = true

structure Nadathur2024.Implicative.ImplicativeScenario : Type

A scenario for implicative verbs: a causal model linking a prerequisite action to a complement outcome.

The prerequisite variable represents A(x) — the causally-relevant condition whose satisfaction (or non-satisfaction) determines the complement outcome via the causal dynamics. For dare, A(x) = "x was daring/courageous"; for manage, A(x) is underspecified.

• dynamics : Core.StructuralEquationModel.CausalDynamics

  The causal dynamics (structural equations)

• prerequisite : Core.StructuralEquationModel.Variable

  The prerequisite variable A(x) — the condition whose satisfaction is asserted by the implicative verb (@cite{nadathur-2024} Proposal 32ii)

• complement : Core.StructuralEquationModel.Variable

  The complement variable P(x) — the VP outcome

• background : Core.StructuralEquationModel.Situation

  The background situation c

def Nadathur2024.Implicative.manageSem (sc : ImplicativeScenario) : Bool

Semantics of "manage": the prerequisite was causally sufficient for the complement outcome.

This is the derived prediction of Proposal 32 for two-way implicatives: when A(x) is presupposed to be both causally necessary (32i) and causally sufficient (32iii) for P(x), and A(x) holds (32ii), then P(x) follows as a causal consequence of A(x) + the background situation.

The old label "action" has been renamed to "prerequisite" to match @cite{nadathur-2024}'s terminology.

Equations

• Nadathur2024.Implicative.manageSem sc = Core.StructuralEquationModel.causallySufficient sc.dynamics sc.background sc.prerequisite sc.complement

def Nadathur2024.Implicative.failSem (sc : ImplicativeScenario) : Bool

Semantics of "fail": the complement did NOT develop.

"Kim failed to swim across" entails "Kim did not swim across." Dual of manageSem: failSem sc = !manageSem sc.

Equations

• Nadathur2024.Implicative.failSem sc = !Nadathur2024.Implicative.manageSem sc

theorem Nadathur2024.Implicative.manage_entails_complement (sc : ImplicativeScenario) (h : manageSem sc = true) : (Core.StructuralEquationModel.normalDevelopment sc.dynamics (sc.background.extend sc.prerequisite true)).hasValue sc.complement true = true

Central grounding theorem: if manageSem holds, the complement is true after normal development.

This grounds VerbEntry.implicativeBuilder := some.positive for manage: the entailment is not stipulated but follows from causal sufficiency.

theorem Nadathur2024.Implicative.fail_entails_not_complement (sc : ImplicativeScenario) (h : failSem sc = true) : (Core.StructuralEquationModel.normalDevelopment sc.dynamics (sc.background.extend sc.prerequisite true)).hasValue sc.complement true = false

If failSem holds, the complement is false after normal development.

theorem Nadathur2024.Implicative.implicative_not_aspect_governed (sc : ImplicativeScenario) (h : manageSem sc = true) : (Core.StructuralEquationModel.normalDevelopment sc.dynamics (sc.background.extend sc.prerequisite true)).hasValue sc.complement true = true

Implicative entailment is NOT aspect-governed: the entailment holds with no aspect parameter in the semantics. This contrasts with ability modals (see Modal/Ability.lean) where aspect determines whether the complement is entailed.

structure Nadathur2024.Implicative.PrerequisiteAccount : Type

Proposal 32: The prerequisite account of implicative semantics.

For a two-way implicative I, agent x, predicate P, background c:

• (32i) Presupposes: ∃ prerequisite A(x) causally necessary for P(x)
• (32ii) Asserts: x did A (A(x) holds)
• (32iii) Presupposes: A(x) is causally sufficient for P(x) in c

One-way verbs have only (32i) and (32ii); (32iii) is absent, so the positive entailment is merely an antiperfection implicature.

The prerequisiteType field identifies which lexical prerequisite the verb encodes; hasSufficiencyPresup distinguishes one-way from two-way verbs.

• dynamics : Core.StructuralEquationModel.CausalDynamics

  The causal dynamics governing the scenario

• background : Core.StructuralEquationModel.Situation

  Background situation c

• prereqVar : Core.StructuralEquationModel.Variable

  The prerequisite variable A(x)

• complementVar : Core.StructuralEquationModel.Variable

  The complement variable P(x)

• prerequisiteType : Prerequisite

  What kind of prerequisite A is (courage, patience, etc.)

• hasSufficiencyPresup : Bool

  (32iii): Does this verb presuppose causal sufficiency? true for two-way implicatives (manage, dare); false for one-way implicatives (jaksaa, pystyä).

def Nadathur2024.Implicative.PrerequisiteAccount.necessityPresup (pa : PrerequisiteAccount) : Bool

(32i): The necessity presupposition holds — A(x) is causally necessary for P(x) relative to the background.

Equations

• pa.necessityPresup = Core.StructuralEquationModel.causallyNecessary pa.dynamics pa.background pa.prereqVar pa.complementVar

def Nadathur2024.Implicative.PrerequisiteAccount.sufficiencyPresup (pa : PrerequisiteAccount) : Bool

(32iii): Check whether A(x) is causally sufficient for P(x) in the model. This is a computed property of the dynamics/background, distinct from hasSufficiencyPresup (a lexical property of the verb). For well-formed accounts, sufficiencyPresup = hasSufficiencyPresup.

Equations

• pa.sufficiencyPresup = Core.StructuralEquationModel.causallySufficient pa.dynamics pa.background pa.prereqVar pa.complementVar

def Nadathur2024.Implicative.PrerequisiteAccount.assertion (pa : PrerequisiteAccount) (w : Core.StructuralEquationModel.Situation) : Bool

(32ii): The assertion — A(x) holds in the evaluation world.

Equations

• pa.assertion w = w.hasValue pa.prereqVar true

def Nadathur2024.Implicative.PrerequisiteAccount.toScenario (pa : PrerequisiteAccount) : ImplicativeScenario

Convert a prerequisite account to the ImplicativeScenario used by manageSem/failSem. Shows that the scenario-level semantics is derived from the prerequisite account, not primitive.

Equations

• pa.toScenario = { dynamics := pa.dynamics, prerequisite := pa.prereqVar, complement := pa.complementVar, background := pa.background }

theorem Nadathur2024.Implicative.prerequisite_derives_manageSem (pa : PrerequisiteAccount) (hSuf : pa.sufficiencyPresup = true) : manageSem pa.toScenario = true

For two-way implicatives: if the necessity presupposition (32i), sufficiency presupposition (32iii), and assertion (32ii) all hold, then manageSem holds — complement truth follows.

This derives the complement entailment from the prerequisite account rather than stipulating it.

inductive Nadathur2024.Implicative.Directionality : Type

Directionality of complement entailment (@cite{nadathur-2024} §6.3).

• oneWay: complement entailment under only one matrix polarity. For polarity-preserving verbs (jaksaa), negation entails ¬VP but affirmation only implicates VP (via antiperfection). For polarity-reversing verbs (hesitate), negation entails VP but affirmation doesn't entail ¬VP.
• twoWay: complement entailment under both polarities ("manage to VP" → VP; "not manage to VP" → ¬VP).

@cite{nadathur-2024} derives this from causal structure: two-way = both necessity and sufficiency presupposed (32i + 32iii); one-way = only necessity presupposed (32i).

• oneWay : Directionality
• twoWay : Directionality

instance Nadathur2024.Implicative.instDecidableEqDirectionality : DecidableEq Directionality

Equations

• Nadathur2024.Implicative.instDecidableEqDirectionality x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Nadathur2024.Implicative.instReprDirectionality.repr : Directionality → ℕ → Std.Format

Equations

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

instance Nadathur2024.Implicative.instReprDirectionality : Repr Directionality

Equations

• Nadathur2024.Implicative.instReprDirectionality = { reprPrec := Nadathur2024.Implicative.instReprDirectionality.repr }

def Nadathur2024.Implicative.instBEqDirectionality.beq : Directionality → Directionality → Bool

Equations

• Nadathur2024.Implicative.instBEqDirectionality.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Nadathur2024.Implicative.instBEqDirectionality : BEq Directionality

Equations

• Nadathur2024.Implicative.instBEqDirectionality = { beq := Nadathur2024.Implicative.instBEqDirectionality.beq }

def Nadathur2024.Implicative.PrerequisiteAccount.directionality (pa : PrerequisiteAccount) : Directionality

The directionality of a prerequisite account is determined by whether causal sufficiency is presupposed (32iii). Two-way verbs presuppose sufficiency; one-way verbs do not.

Equations

• pa.directionality = if pa.hasSufficiencyPresup = true then Nadathur2024.Implicative.Directionality.twoWay else Nadathur2024.Implicative.Directionality.oneWay

theorem Nadathur2024.Implicative.manage_swim_holds : manageSem Nadathur2024.Implicative.manageScenario✝ = true

Concrete verification: manageSem holds for the swim scenario.

theorem Nadathur2024.Implicative.manage_swim_complement_true : (Core.StructuralEquationModel.normalDevelopment Nadathur2024.Implicative.manageScenario✝.dynamics (Nadathur2024.Implicative.manageScenario✝¹.background.extend Nadathur2024.Implicative.manageScenario✝².prerequisite true)).hasValue Nadathur2024.Implicative.manageScenario✝³.complement true = true

Concrete verification: the complement (swimming across) is true.

theorem Nadathur2024.Implicative.fail_swim_false_when_sufficient : failSem Nadathur2024.Implicative.manageScenario✝ = false

The fail scenario: same dynamics, but testing failSem. If the dynamics DO fire (prerequisite sufficient for complement), failSem is false.

theorem Nadathur2024.Implicative.fail_no_law_holds : failSem Nadathur2024.Implicative.failScenario✝ = true

When there's no causal connection, failSem holds (complement doesn't develop).

inductive Nadathur2024.Implicative.ImplicativeBuilder : Type

Builder enum for implicative verbs, following the CausativeBuilder pattern.

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

Note: ImplicativeBuilder and CausativeBuilder 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 : ImplicativeBuilder
• negative : ImplicativeBuilder

instance Nadathur2024.Implicative.instDecidableEqImplicativeBuilder : DecidableEq ImplicativeBuilder

Equations

• Nadathur2024.Implicative.instDecidableEqImplicativeBuilder x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Nadathur2024.Implicative.instReprImplicativeBuilder : Repr ImplicativeBuilder

Equations

• Nadathur2024.Implicative.instReprImplicativeBuilder = { reprPrec := Nadathur2024.Implicative.instReprImplicativeBuilder.repr }

def Nadathur2024.Implicative.instReprImplicativeBuilder.repr : ImplicativeBuilder → ℕ → Std.Format

Equations

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

def Nadathur2024.Implicative.instBEqImplicativeBuilder.beq : ImplicativeBuilder → ImplicativeBuilder → Bool

Equations

• Nadathur2024.Implicative.instBEqImplicativeBuilder.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Nadathur2024.Implicative.instBEqImplicativeBuilder : BEq ImplicativeBuilder

Equations

• Nadathur2024.Implicative.instBEqImplicativeBuilder = { beq := Nadathur2024.Implicative.instBEqImplicativeBuilder.beq }

def Nadathur2024.Implicative.ImplicativeBuilder.entailsComplement : ImplicativeBuilder → Bool

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

Equations

• Nadathur2024.Implicative.ImplicativeBuilder.positive.entailsComplement = true
• Nadathur2024.Implicative.ImplicativeBuilder.negative.entailsComplement = false

def Nadathur2024.Implicative.ImplicativeBuilder.toSemantics : ImplicativeBuilder → ImplicativeScenario → Bool

Map to the compositional semantics (manageSem or failSem).

Equations

• Nadathur2024.Implicative.ImplicativeBuilder.positive.toSemantics = Nadathur2024.Implicative.manageSem
• Nadathur2024.Implicative.ImplicativeBuilder.negative.toSemantics = Nadathur2024.Implicative.failSem

theorem Nadathur2024.Implicative.positive_entails_complement (sc : ImplicativeScenario) (h : ImplicativeBuilder.positive.toSemantics sc = true) : (Core.StructuralEquationModel.normalDevelopment sc.dynamics (sc.background.extend sc.prerequisite true)).hasValue sc.complement true = true

Positive builder entails complement: if manageSem holds, complement is true.

theorem Nadathur2024.Implicative.negative_entails_not_complement (sc : ImplicativeScenario) (h : ImplicativeBuilder.negative.toSemantics sc = true) : (Core.StructuralEquationModel.normalDevelopment sc.dynamics (sc.background.extend sc.prerequisite true)).hasValue sc.complement true = false

Negative builder entails NOT complement: if failSem holds, complement is false.

theorem Nadathur2024.Implicative.entailsComplement_positive : ImplicativeBuilder.positive.entailsComplement = true

entailsComplement matches semantic behavior: positive ↔ manageSem, negative ↔ failSem.

theorem Nadathur2024.Implicative.entailsComplement_negative : ImplicativeBuilder.negative.entailsComplement = false

structure Nadathur2024.Implicative.ImplicativeClass : Type

Full classification of complement-entailing verbs.

The four parameters:

• polarity: positive (manage → complement true) vs negative (fail → complement false)
• directionality: one-way vs two-way complement entailment
• aspectGoverned: whether aspect modulates the entailment (true for ability modals & enough/too; false for lexical implicatives)
• prerequisite: what kind of causal prerequisite the verb lexicalizes (@cite{nadathur-2024} §5.2)

• polarity : ImplicativeBuilder

  Positive (manage, force) or negative (fail, prevent) polarity

• directionality : Directionality

  One-way (ability) or two-way (manage) entailment

• aspectGoverned : Bool

  Does aspect govern the actuality inference?

• prerequisite : Option Prerequisite

  Lexically-specified prerequisite type (if any)

instance Nadathur2024.Implicative.instDecidableEqImplicativeClass : DecidableEq ImplicativeClass

Equations

• Nadathur2024.Implicative.instDecidableEqImplicativeClass = Nadathur2024.Implicative.instDecidableEqImplicativeClass.decEq

def Nadathur2024.Implicative.instDecidableEqImplicativeClass.decEq (x✝ x✝¹ : ImplicativeClass) : Decidable (x✝ = x✝¹)

Equations

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

instance Nadathur2024.Implicative.instReprImplicativeClass : Repr ImplicativeClass

Equations

• Nadathur2024.Implicative.instReprImplicativeClass = { reprPrec := Nadathur2024.Implicative.instReprImplicativeClass.repr }

def Nadathur2024.Implicative.instReprImplicativeClass.repr : ImplicativeClass → ℕ → Std.Format

Equations

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

instance Nadathur2024.Implicative.instBEqImplicativeClass : BEq ImplicativeClass

Equations

• Nadathur2024.Implicative.instBEqImplicativeClass = { beq := Nadathur2024.Implicative.instBEqImplicativeClass.beq }

def Nadathur2024.Implicative.instBEqImplicativeClass.beq : ImplicativeClass → ImplicativeClass → Bool

Equations

• One or more equations did not get rendered due to their size.
• Nadathur2024.Implicative.instBEqImplicativeClass.beq x✝¹ x✝ = false

def Nadathur2024.Implicative.ImplicativeClass.manage : ImplicativeClass

manage: two-way positive, not aspect-governed, unspecified prerequisite. "managed to VP" → VP; "didn't manage to VP" → ¬VP.

Equations

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

def Nadathur2024.Implicative.ImplicativeClass.fail : ImplicativeClass

fail: two-way negative, not aspect-governed, unspecified prerequisite.

Equations

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

def Nadathur2024.Implicative.ImplicativeClass.dare : ImplicativeClass

dare/uskaltaa: two-way positive, prerequisite = courage.

Equations

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

def Nadathur2024.Implicative.ImplicativeClass.bother : ImplicativeClass

bother/viitsiä: two-way positive, prerequisite = engagement.

Equations

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

def Nadathur2024.Implicative.ImplicativeClass.jaksaa : ImplicativeClass

jaksaa 'have the strength': one-way positive, prerequisite = strength. Positive assertion ↛ complement; only negative entails.

Equations

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

def Nadathur2024.Implicative.ImplicativeClass.ability : ImplicativeClass

be able: one-way positive, aspect-governed.

Equations

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

def Nadathur2024.Implicative.ImplicativeClass.enough : ImplicativeClass

enough to VP: one-way positive, aspect-governed.

Equations

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

def Nadathur2024.Implicative.ImplicativeClass.too : ImplicativeClass

too Adj to VP: one-way negative, aspect-governed.

Equations

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

def Nadathur2024.Implicative.ImplicativeClass.hesitate : ImplicativeClass

hesitate/epäröidä: polarity-reversing one-way. "hesitated to VP" ↛ ¬VP; "didn't hesitate to VP" → VP. (@cite{nadathur-2024} §6.4)

Equations

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

theorem Nadathur2024.Implicative.manage_fail_polarity : ImplicativeClass.manage.directionality = ImplicativeClass.fail.directionality ∧ ImplicativeClass.manage.aspectGoverned = ImplicativeClass.fail.aspectGoverned ∧ ImplicativeClass.manage.polarity ≠ ImplicativeClass.fail.polarity

Manage and fail differ only in polarity.

theorem Nadathur2024.Implicative.ability_vs_manage : ImplicativeClass.ability.aspectGoverned = true ∧ ImplicativeClass.manage.aspectGoverned = false ∧ ImplicativeClass.ability.directionality = Directionality.oneWay ∧ ImplicativeClass.manage.directionality = Directionality.twoWay

Ability and manage differ: ability is aspect-governed and one-way.

theorem Nadathur2024.Implicative.enough_too_polarity : ImplicativeClass.enough.aspectGoverned = ImplicativeClass.too.aspectGoverned ∧ ImplicativeClass.enough.directionality = ImplicativeClass.too.directionality ∧ ImplicativeClass.enough.polarity ≠ ImplicativeClass.too.polarity

Enough and too share aspect-governance but differ in polarity.

theorem Nadathur2024.Implicative.dare_vs_manage_prerequisite : ImplicativeClass.dare.polarity = ImplicativeClass.manage.polarity ∧ ImplicativeClass.dare.directionality = ImplicativeClass.manage.directionality ∧ ImplicativeClass.dare.prerequisite ≠ ImplicativeClass.manage.prerequisite

Dare and manage share polarity and directionality but differ in prerequisite.

theorem Nadathur2024.Implicative.jaksaa_vs_dare_directionality : ImplicativeClass.jaksaa.directionality = Directionality.oneWay ∧ ImplicativeClass.dare.directionality = Directionality.twoWay ∧ ImplicativeClass.jaksaa.prerequisite.isSome = true ∧ ImplicativeClass.dare.prerequisite.isSome = true

Jaksaa (one-way) vs uskaltaa/dare (two-way): same prerequisite specificity, different directionality — derived from whether sufficiency is presupposed.

theorem Nadathur2024.Implicative.specific_vs_bleached : (ImplicativeClass.dare.prerequisite.bind fun (x : Prerequisite) => some x.isSpecific) = some true ∧ (ImplicativeClass.manage.prerequisite.bind fun (x : Prerequisite) => some x.isSpecific) = some false

Specific implicatives have specific prerequisites; bleached ones don't.

def Nadathur2024.Implicative.PrerequisiteAccount.toImplicativeClass (pa : PrerequisiteAccount) (polarity : ImplicativeBuilder) : ImplicativeClass

Derive the full ImplicativeClass from a PrerequisiteAccount.

Polarity (positive/negative) must be supplied externally — it is a lexical choice orthogonal to causal structure. The prerequisite account determines directionality and prerequisite type; lexical implicatives are never aspect-governed.

Equations

• pa.toImplicativeClass polarity = { polarity := polarity, directionality := pa.directionality, aspectGoverned := false, prerequisite := some pa.prerequisiteType }