Implicative Verbs (@cite{nadathur-2024})

Causal-prerequisite semantics for implicative verbs. Implicatives (manage, fail, dare, bother, jaksaa, hesitate, ...) all share a prerequisite-account schema (Proposal 32):

• (32i) Presuppose: ∃ prerequisite A(x) causally necessary for P(x)
• (32ii) Assert: x did A
• (32iii) Presuppose (two-way only): A(x) causally sufficient for P(x)

Lexical variation

The chief dimension of variation is the type of prerequisite:

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

V2 substrate

Polymorphic V2 forms over SEM V α. The legacy ImplicativeScenario struct + manageSem/failSem over CausalDynamics, PrerequisiteAccount, ConcreteExample (swim/manage), the ComplementEntailing.CausalFrame abstraction (with abilityFrame/ viewpoint-aspect bridges), and Implicative.toSemantics over scenarios were deleted in Phase D-H. The polymorphic V2 versions (manageSem, failSem, necessityPresup, Implicative.toSemantics dispatch) are promoted to canonical here.

inductive Semantics.Causation.Implicative.Prerequisite : Type

Lexically-specified prerequisite types for implicative verbs.

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

@[implicit_reducible]

instance Semantics.Causation.Implicative.instDecidableEqPrerequisite : DecidableEq Prerequisite

Equations

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

@[implicit_reducible]

instance Semantics.Causation.Implicative.instReprPrerequisite : Repr Prerequisite

Equations

• Semantics.Causation.Implicative.instReprPrerequisite = { reprPrec := Semantics.Causation.Implicative.instReprPrerequisite.repr }

def Semantics.Causation.Implicative.instReprPrerequisite.repr : Prerequisite → ℕ → Std.Format

Equations

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

def Semantics.Causation.Implicative.Prerequisite.isSpecific : Prerequisite → Bool

Is the prerequisite lexically specific or underspecified?

Equations

• Semantics.Causation.Implicative.Prerequisite.unspecified.isSpecific = false
• x✝.isSpecific = true

@[reducible, inline]

abbrev Semantics.Causation.Implicative.manageSem {V : Type u_1} {α : V → Type u_2} [Fintype V] [DecidableEq V] [Core.Causal.DecidableValuation α] (M : Core.Causal.SEM V α) [M.graph.IsDAG] [M.IsDeterministic] (background : Core.Causal.Valuation α) (prerequisite : V) (xP : α prerequisite) (complement : V) (xC : α complement) : Prop

V2 manage-sem: prerequisite-as-xP is causally sufficient for complement-as-xC. Polymorphic over value types.

Equations

• Semantics.Causation.Implicative.manageSem M background prerequisite xP complement xC = M.causallySufficient background prerequisite xP complement xC

@[reducible, inline]

abbrev Semantics.Causation.Implicative.failSem {V : Type u_1} {α : V → Type u_2} [Fintype V] [DecidableEq V] [Core.Causal.DecidableValuation α] (M : Core.Causal.SEM V α) [M.graph.IsDAG] [M.IsDeterministic] (background : Core.Causal.Valuation α) (prerequisite : V) (xP : α prerequisite) (complement : V) (xC : α complement) : Prop

V2 fail-sem: prerequisite-as-xP is NOT causally sufficient for complement-as-xC.

Equations

• Semantics.Causation.Implicative.failSem M background prerequisite xP complement xC = ¬Semantics.Causation.Implicative.manageSem M background prerequisite xP complement xC

@[reducible, inline]

abbrev Semantics.Causation.Implicative.necessityPresup {V : Type u_1} {α : V → Type u_2} [Fintype V] [DecidableEq V] [Core.Causal.DecidableValuation α] [(v : V) → Fintype (α v)] (M : Core.Causal.SEM V α) [M.graph.IsDAG] [M.IsDeterministic] (background : Core.Causal.Valuation α) (prerequisite : V) (xP : α prerequisite) (complement : V) (xC : α complement) : Prop

V2 necessity presupposition: prerequisite-as-xP is causally necessary (Nadathur 2024 Def 10b) for complement-as-xC.

Equations

• Semantics.Causation.Implicative.necessityPresup M background prerequisite xP complement xC = M.causallyNecessary background prerequisite xP complement xC

inductive Semantics.Causation.Implicative.Directionality : Type

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

• oneWay: complement entailment under only one matrix polarity.
• twoWay: complement entailment under both polarities.

• oneWay : Directionality
• twoWay : Directionality

@[implicit_reducible]

instance Semantics.Causation.Implicative.instDecidableEqDirectionality : DecidableEq Directionality

Equations

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

@[implicit_reducible]

instance Semantics.Causation.Implicative.instReprDirectionality : Repr Directionality

Equations

• Semantics.Causation.Implicative.instReprDirectionality = { reprPrec := Semantics.Causation.Implicative.instReprDirectionality.repr }

def Semantics.Causation.Implicative.instReprDirectionality.repr : Directionality → ℕ → Std.Format

Equations

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

structure Semantics.Causation.Implicative.ImplicativeClass : Type

The full lexical signature of an implicative verb (@cite{nadathur-2024}).

• polarity : Features.Implicative

  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)

@[implicit_reducible]

instance Semantics.Causation.Implicative.instDecidableEqImplicativeClass : DecidableEq ImplicativeClass

Equations

• Semantics.Causation.Implicative.instDecidableEqImplicativeClass = Semantics.Causation.Implicative.instDecidableEqImplicativeClass.decEq

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

Equations

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

def Semantics.Causation.Implicative.instReprImplicativeClass.repr : ImplicativeClass → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Semantics.Causation.Implicative.instReprImplicativeClass : Repr ImplicativeClass

Equations

• Semantics.Causation.Implicative.instReprImplicativeClass = { reprPrec := Semantics.Causation.Implicative.instReprImplicativeClass.repr }

def Semantics.Causation.Implicative.ImplicativeClass.manage : ImplicativeClass

Equations

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

def Semantics.Causation.Implicative.ImplicativeClass.fail : ImplicativeClass

Equations

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

def Semantics.Causation.Implicative.ImplicativeClass.dare : ImplicativeClass

Equations

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

def Semantics.Causation.Implicative.ImplicativeClass.bother : ImplicativeClass

Equations

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

def Semantics.Causation.Implicative.ImplicativeClass.jaksaa : ImplicativeClass

Equations

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

def Semantics.Causation.Implicative.ImplicativeClass.ability : ImplicativeClass

Equations

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

def Semantics.Causation.Implicative.ImplicativeClass.enough : ImplicativeClass

Equations

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

def Semantics.Causation.Implicative.ImplicativeClass.too : ImplicativeClass

Equations

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

def Semantics.Causation.Implicative.ImplicativeClass.hesitate : ImplicativeClass

Equations

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

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

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

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

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

theorem Semantics.Causation.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

theorem Semantics.Causation.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

Lives here rather than in Features/Causation.lean because the dispatch needs Core.Causal.SEM + the Implicative.manageSem/failSem machinery defined above; Features/Causation.lean is kept import-free. Standard mathlib pattern: methods on a type may live in a sibling file via namespace TypeName block when import weight matters.

noncomputable def Features.Implicative.toSemantics {V : Type u_1} {α : V → Type u_2} [Fintype V] [DecidableEq V] [Core.Causal.DecidableValuation α] (M : Core.Causal.SEM V α) [M.graph.IsDAG] [M.IsDeterministic] : Implicative → Core.Causal.Valuation α → (p : V) → α p → (c : V) → α c → Prop

V2 dispatch: map an Implicative polarity to its V2 polymorphic semantic function.

Equations

• Features.Implicative.toSemantics M Features.Implicative.positive = Semantics.Causation.Implicative.manageSem M
• Features.Implicative.toSemantics M Features.Implicative.negative = Semantics.Causation.Implicative.failSem M