Nadathur 2024: Causal Semantics for Implicative Verbs

@cite{nadathur-2024}

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

Summary

Derives the inferential profile of implicative verbs from causal structure (structural equation models, @cite{pearl-2000}; @cite{schulz-2011}). Builds on @cite{baglini-francez-2016}'s causal analysis of manage but extends to the full implicative class: lexically-specific two-way verbs (dare, bother), one-way verbs (jaksaa, pystyä), and polarity- reversing verbs (fail, hesitate).

Core Contribution: Proposal 32

The prerequisite account decomposes implicative meaning into:

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

One-way implicatives lack (32iii); their positive implicature arises via circumscription/antiperfection.

Dreyfus Scenario (§6.1.1, Figure 3)

Eight-vertex SCM illustrating how causal structure determines implicative felicity:

• INT: Dreyfus intends to spy
• NRV: Dreyfus has the nerve
• SEC: Dreyfus collects secrets (= INT)
• MSG: Dreyfus sends a radio message (= INT ∧ NRV)
• LST: A German is listening on the correct frequency
• BRK: The message is garbled
• COM: Dreyfus establishes communication (= MSG ∧ LST ∧ ¬BRK)
• SPY: Dreyfus spies for the Germans (= SEC ∧ COM)

Background: INT = true, SEC = true, BRK = false. NRV/LST undetermined. The question is whether NRV (the unresolved prerequisite) is sufficient for the various effects.

The legacy CausalDynamics-based Dreyfus model + Karttunen/Finnish classification machinery were deleted in Phase D-H. Necessity-side claims (manage_send_msg_felicitous etc.) require V2's polymorphic causallyNecessary over multi-parent mechanisms with negative preconditions; deferred until the supersituation enumeration handles multi-parent disjunctive cases.

inductive Nadathur2024.V : Type

Dreyfus scenario vertices (@cite{nadathur-2024} §6.1.1, Figure 3).

• INT : V
• NRV : V
• LST : V
• BRK : V
• SEC : V
• MSG : V
• COM : V
• SPY : V

@[implicit_reducible]

instance Nadathur2024.instDecidableEqV : DecidableEq V

Equations

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

@[implicit_reducible]

instance Nadathur2024.instFintypeV : Fintype V

Equations

• Nadathur2024.instFintypeV = { elems := { val := ↑Nadathur2024.V.enumList, nodup := Nadathur2024.V.enumList_nodup }, complete := Nadathur2024.instFintypeV._proof_1 }

@[implicit_reducible]

instance Nadathur2024.instReprV : Repr V

Equations

• Nadathur2024.instReprV = { reprPrec := Nadathur2024.instReprV.repr }

def Nadathur2024.instReprV.repr : V → ℕ → Std.Format

Equations

• Nadathur2024.instReprV.repr Nadathur2024.V.INT prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Nadathur2024.V.INT")).group prec✝
• Nadathur2024.instReprV.repr Nadathur2024.V.NRV prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Nadathur2024.V.NRV")).group prec✝
• Nadathur2024.instReprV.repr Nadathur2024.V.LST prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Nadathur2024.V.LST")).group prec✝
• Nadathur2024.instReprV.repr Nadathur2024.V.BRK prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Nadathur2024.V.BRK")).group prec✝
• Nadathur2024.instReprV.repr Nadathur2024.V.SEC prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Nadathur2024.V.SEC")).group prec✝
• Nadathur2024.instReprV.repr Nadathur2024.V.MSG prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Nadathur2024.V.MSG")).group prec✝
• Nadathur2024.instReprV.repr Nadathur2024.V.COM prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Nadathur2024.V.COM")).group prec✝
• Nadathur2024.instReprV.repr Nadathur2024.V.SPY prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Nadathur2024.V.SPY")).group prec✝

def Nadathur2024.varList : List V

Equations

• Nadathur2024.varList = [Nadathur2024.V.INT, Nadathur2024.V.NRV, Nadathur2024.V.LST, Nadathur2024.V.BRK, Nadathur2024.V.SEC, Nadathur2024.V.MSG, Nadathur2024.V.COM, Nadathur2024.V.SPY]

def Nadathur2024.graph : Core.Causal.CausalGraph V

Graph: SEC←{INT}, MSG←{INT,NRV}, COM←{MSG,LST,BRK}, SPY←{SEC,COM}.

Equations

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

noncomputable def Nadathur2024.dreyfusSEM : Core.Causal.BoolSEM V

Dreyfus SEM with the negative ¬BRK precondition encoded directly in the COM mechanism — first-class on V2's Boolean substrate.

Equations

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

@[implicit_reducible]

noncomputable instance Nadathur2024.instIsDeterministicVBoolDreyfusSEM : Core.Causal.SEM.IsDeterministic dreyfusSEM

Equations

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

def Nadathur2024.dreyfusBg : Core.Causal.Valuation fun (x : V) => Bool

Background: Dreyfus intends, has collected secrets, channel intact.

Equations

• Nadathur2024.dreyfusBg = ((Core.Causal.Valuation.empty.extend Nadathur2024.V.INT true).extend Nadathur2024.V.SEC true).extend Nadathur2024.V.BRK false

theorem Nadathur2024.nrv_sufficient_for_msg : (Core.Causal.SEM.developDetOn dreyfusSEM varList 1 (dreyfusBg.extend V.NRV true)).hasValue V.MSG true

(34a) dare felicitous for MSG: NRV is sufficient for MSG. With INT already true and BRK irrelevant for MSG, adding NRV=true yields MSG=true.

theorem Nadathur2024.nrv_not_sufficient_for_com : ¬(Core.Causal.SEM.developDetOn dreyfusSEM varList 2 (dreyfusBg.extend V.NRV true)).hasValue V.COM true

(34c) dare INFELICITOUS for COM: NRV is NOT sufficient for COM. Even with NRV=true, COM also requires LST=true (which is undetermined in dreyfusBg), so COM does not develop to true.

theorem Nadathur2024.nrv_not_sufficient_for_spy : ¬(Core.Causal.SEM.developDetOn dreyfusSEM varList 3 (dreyfusBg.extend V.NRV true)).hasValue V.SPY true

(34d) dare INFELICITOUS for SPY: NRV is NOT sufficient for SPY (SPY depends on COM, which requires LST).