Implicative Verbs ([Nad23b])

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 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 Causation.Implicative.instDecidableEqPrerequisite : DecidableEq Prerequisite

Equations

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

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

Equations

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

@[implicit_reducible]

instance Causation.Implicative.instReprPrerequisite : Repr Prerequisite

Equations

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

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

Is the prerequisite lexically specific or underspecified?

Equations

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

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

V2 manage-sem ([Nad23b] Definition 10a with the Definition 10 preamble, over the strict T_D development): prerequisite-as-xP is causally sufficient for complement-as-xC — the background entails neither fact, and augmenting it with the prerequisite causally entails the complement. Polymorphic over value types.

Equations

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

@[implicit_reducible]

noncomputable instance Causation.Implicative.instDecidableManageSem {V : Type u_1} {α : V → Type u_2} [Fintype V] [DecidableEq V] [DecidableValuation α] (M : SEM V α) [M.graph.IsDAG] [M.IsDeterministic] (background : Valuation α) (prerequisite : V) (xP : α prerequisite) (complement : V) (xC : α complement) : Decidable (manageSem M background prerequisite xP complement xC)

Equations

• Causation.Implicative.instDecidableManageSem M background prerequisite xP complement xC = Classical.dec (Causation.Implicative.manageSem M background prerequisite xP complement xC)

@[reducible, inline]

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

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

TODO: this is denial of the sufficiency presupposition, which is what the Dreyfus infelicity judgments test, but it is NOT Proposal 32's semantics for negative implicative assertions (assert ¬A(x) with both presuppositions intact); the Features.Implicative.toSemantics .negative dispatch below inherits the same caveat.

Equations

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

@[reducible, inline]

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

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

Equations

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

[Nad23b] (pp. 316–317) takes Facts A–C as the class-level data any account of implicatives must derive. On the prerequisite account they fall out of the presupposition + assertion split of Proposal 32, for an arbitrary deterministic SEM:

• Fact B, positive half (complement_of_positive_assertion): asserting the prerequisite realizes the complement — the sufficiency presupposition's entailment clause.
• Fact B, negative half (no_complement_of_negative_assertion): given the necessity presupposition, the negative assertion leaves no consistent completion realizing the complement.
• Fact C (complement_iff_prerequisite): in a felicitous two-way context the prerequisite is sufficient and necessary — a consistent completion realizes the complement exactly when it realizes the prerequisite.

Fact A (the existence of a potential obstacle, blocking the entailment from complement to implicative claim) is carried by the presuppositional preamble itself (SEM.causallyNecessary.precondition).

theorem Causation.Implicative.complement_of_positive_assertion {V : Type u_1} {α : V → Type u_2} [Fintype V] [DecidableEq V] [DecidableValuation α] (M : SEM V α) [M.graph.IsDAG] [M.IsDeterministic] {background : Valuation α} {p : V} {xP : α p} {c : V} {xC : α c} (h : manageSem M background p xP c xC) : M.causallyEntails (background.extend p xP) c xC

Fact B, positive half: a positive two-way implicative claim entails its complement — the background updated with the asserted prerequisite causally entails the complement.

theorem Causation.Implicative.no_complement_of_negative_assertion {V : Type u_1} {α : V → Type u_2} [Fintype V] [DecidableEq V] [DecidableValuation α] [(v : V) → Fintype (α v)] (M : SEM V α) [M.graph.IsDAG] [M.IsDeterministic] {background : Valuation α} {p : V} {xP xP' : α p} {c : V} {xC : α c} (hexo : M.graph.parents p = ∅) (hp : background.get p = none) (hne : xP' ≠ xP) (hnec : necessityPresup M background p xP c xC) (s' : Valuation α) : M.IsExogenousSettlement (background.extend p xP') s' → s'.get c = none → ¬M.causallyEntails s' c xC

Fact B, negative half: given the necessity presupposition, a negative implicative claim (asserting the prerequisite took a value other than xP) leaves no consistent completion realizing the complement: by no-alternative, every consistent path to the complement runs through the prerequisite value the assertion denies.

theorem Causation.Implicative.complement_iff_prerequisite {V : Type u_1} {α : V → Type u_2} [Fintype V] [DecidableEq V] [DecidableValuation α] [(v : V) → Fintype (α v)] (M : SEM V α) [M.graph.IsDAG] [M.IsDeterministic] {background : Valuation α} {p : V} {xP : α p} {c : V} {xC : α c} (hexo : M.graph.parents p = ∅) (hp : background.get p = none) (hsuf : manageSem M background p xP c xC) (hnec : necessityPresup M background p xP c xC) (s' : Valuation α) : M.IsExogenousSettlement background s' → s'.get c = none → (M.causallyEntails s' c xC ↔ M.causallyEntails s' p xP)

Fact C: in a felicitous two-way context (both presuppositions in force), a consistent completion of the background realizes the complement exactly when it realizes the prerequisite. The forward direction is no-alternative; the converse composes the sufficiency clause with causallyEntails_mono (determinations cannot be undone).

theorem Causation.Implicative.twoWay_entailment_profile {V : Type u_1} {α : V → Type u_2} [Fintype V] [DecidableEq V] [DecidableValuation α] [(v : V) → Fintype (α v)] (M : SEM V α) [M.graph.IsDAG] [M.IsDeterministic] {background : Valuation α} {p : V} {xP : α p} {c : V} {xC : α c} (hexo : M.graph.parents p = ∅) (hp : background.get p = none) (hsuf : manageSem M background p xP c xC) (hnec : necessityPresup M background p xP c xC) : M.causallyEntails (background.extend p xP) c xC ∧ ∀ (xP' : α p), xP' ≠ xP → ∀ (s' : Valuation α), M.IsExogenousSettlement (background.extend p xP') s' → s'.get c = none → ¬M.causallyEntails s' c xC

The two-way entailment profile — [Kar71]'s defining criterion for the manage class — follows from the prerequisite account: in a context satisfying both presuppositions, the positive assertion entails the complement (Fact B, positive) and any negative assertion precludes it in every consistent completion (Fact B, negative). This is the derivation [Nad23b] advertises for Facts A–C at the class level.

inductive Causation.Implicative.Directionality : Type

Directionality of complement entailment ([Nad23b]).

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

• oneWay : Directionality
• twoWay : Directionality

@[implicit_reducible]

instance Causation.Implicative.instDecidableEqDirectionality : DecidableEq Directionality

Equations

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

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

Equations

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

@[implicit_reducible]

instance Causation.Implicative.instReprDirectionality : Repr Directionality

Equations

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

structure Causation.Implicative.ImplicativeClass : Type

The full lexical signature of an implicative verb ([Nad23b]).

• 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)

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

Equations

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

@[implicit_reducible]

instance Causation.Implicative.instDecidableEqImplicativeClass : DecidableEq ImplicativeClass

Equations

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

@[implicit_reducible]

instance Causation.Implicative.instReprImplicativeClass : Repr ImplicativeClass

Equations

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

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

Equations

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

def Causation.Implicative.ImplicativeClass.manage : ImplicativeClass

Equations

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

def Causation.Implicative.ImplicativeClass.fail : ImplicativeClass

Equations

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

def Causation.Implicative.ImplicativeClass.dare : ImplicativeClass

Equations

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

def Causation.Implicative.ImplicativeClass.bother : ImplicativeClass

Equations

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

def Causation.Implicative.ImplicativeClass.jaksaa : ImplicativeClass

Equations

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

def Causation.Implicative.ImplicativeClass.ability : ImplicativeClass

Equations

• Causation.Implicative.ImplicativeClass.ability = { polarity := Features.Implicative.positive, directionality := Causation.Implicative.Directionality.oneWay, aspectGoverned := true }

def Causation.Implicative.ImplicativeClass.enough : ImplicativeClass

Equations

• Causation.Implicative.ImplicativeClass.enough = { polarity := Features.Implicative.positive, directionality := Causation.Implicative.Directionality.oneWay, aspectGoverned := true }

def Causation.Implicative.ImplicativeClass.too : ImplicativeClass

Equations

• Causation.Implicative.ImplicativeClass.too = { polarity := Features.Implicative.negative, directionality := Causation.Implicative.Directionality.oneWay, aspectGoverned := true }

def Causation.Implicative.ImplicativeClass.hesitate : ImplicativeClass

Equations

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

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

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

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

theorem 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 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 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 Causation.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] [Causation.DecidableValuation α] (M : Causation.SEM V α) [M.graph.IsDAG] [M.IsDeterministic] : Implicative → Causation.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 = Causation.Implicative.manageSem M
• Features.Implicative.toSemantics M Features.Implicative.negative = Causation.Implicative.failSem M