Nadathur 2023: Causal Semantics for Implicative Verbs

The Dreyfus scenario of [Nad23b] (§6.1.1, Figure 3; introduced in [Nad19] ch. 3 as "the modified Dreyfus scenario", adapted from [BF16]): an eight-vertex structural causal model discriminating where two-way dare is felicitous. The felicity theorems are stated through Causation.Implicative.manageSem / failSem — the substrate formalization of this paper's prerequisite account (Proposal 32) — so they instantiate the same sufficiency predicate the rest of the codebase attributes to implicative verbs.

Main declarations

• Nadathur2023.dreyfusSEM: the Dreyfus SCM (SEC = INT, MSG = INT ∧ NRV, COM = MSG ∧ LST ∧ ¬BRK, SPY = SEC ∧ COM), background INT = SEC = true with NRV, LST, BRK unresolved.
• dare_felicitous_for_msg: NRV (courage, dare's lexical prerequisite) is causally necessary and sufficient for MSG — (34a), via nrv_necessary_for_msg (Def 10b) and nrv_sufficient_for_msg.
• dare_infelicitous_for_com, dare_infelicitous_for_spy: NRV is not sufficient for COM / SPY ((34c), (34d)) — though it is necessary for both (nrv_necessary_for_com, nrv_necessary_for_spy), completing the paper's "necessary but not sufficient" verdicts.

Implementation notes

Theorems are stated over the strict T_D development (developDetVtx?, faithful to the paper's Definitions 4–5): the infelicity verdicts hold because COM and SPY stay unsettled while LST and BRK are unresolved — the paper's route. Concrete claims are discharged through the fuel bridge (causallyEntails_iff_fuel / causallyNecessary_iff_fuel) with the model's depth function as rank certificate, then decide.

TODO: the manage examples (35a–d) need set-valued prerequisites (the (35c) prerequisite is the conjunction NRV ∧ LST ∧ ¬BRK, [Nad23b] fn. 21); manageSem currently takes a single prerequisite vertex.

inductive Nadathur2023.V : Type

Dreyfus scenario vertices ([Nad23b] §6.1.1, Figure 3): INT (Dreyfus intends to spy), NRV (he has the nerve), LST (a German is listening on the correct frequency), BRK (the message is garbled), SEC (he collects secrets), MSG (he sends a radio message), COM (he establishes communication), SPY (he spies for the Germans).

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

@[implicit_reducible]

instance Nadathur2023.instDecidableEqV : DecidableEq V

Equations

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

@[implicit_reducible]

instance Nadathur2023.instFintypeV : Fintype V

Equations

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

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

Equations

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

@[implicit_reducible]

instance Nadathur2023.instReprV : Repr V

Equations

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

def Nadathur2023.graph : Causation.CausalGraph V

Causal graph: SEC←{INT}, MSG←{INT,NRV}, COM←{MSG,LST,BRK}, SPY←{SEC,COM}; INT, NRV, LST, BRK exogenous.

Equations

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

def Nadathur2023.depth : V → ℕ

Depth certificate (also the rank for the fuel bridge).

Equations

• Nadathur2023.depth Nadathur2023.V.INT = 0
• Nadathur2023.depth Nadathur2023.V.NRV = 0
• Nadathur2023.depth Nadathur2023.V.LST = 0
• Nadathur2023.depth Nadathur2023.V.BRK = 0
• Nadathur2023.depth Nadathur2023.V.SEC = 1
• Nadathur2023.depth Nadathur2023.V.MSG = 1
• Nadathur2023.depth Nadathur2023.V.COM = 2
• Nadathur2023.depth Nadathur2023.V.SPY = 3

instance Nadathur2023.instIsDAGVGraph : graph.IsDAG

noncomputable def Nadathur2023.dreyfusSEM : Causation.BoolSEM V

Dreyfus SEM, with the negative ¬BRK precondition encoded directly in the COM mechanism.

Equations

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

instance Nadathur2023.instIsDAGVGraphBoolDreyfusSEM : dreyfusSEM.graph.IsDAG

@[implicit_reducible]

instance Nadathur2023.instIsDeterministicVBoolDreyfusSEM : Causation.SEM.IsDeterministic dreyfusSEM

Equations

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

def Nadathur2023.dreyfusBg : Causation.Valuation fun (x : V) => Bool

Background: Dreyfus intends to spy and has already collected secrets (INT = SEC = 1); NRV, LST, BRK are unresolved.

Equations

• Nadathur2023.dreyfusBg = (Causation.Valuation.empty.extend Nadathur2023.V.INT true).extend Nadathur2023.V.SEC true

theorem Nadathur2023.dare_semantics_via_manageSem : Features.Implicative.toSemantics dreyfusSEM Causation.Implicative.ImplicativeClass.dare.polarity = Causation.Implicative.manageSem dreyfusSEM ∧ Causation.Implicative.ImplicativeClass.dare.prerequisite = some Causation.Implicative.Prerequisite.courage

dare dispatches to the sufficiency semantics the theorems below are stated through, and its lexical prerequisite is courage — instantiated in the Dreyfus scenario by the NRV vertex.

theorem Nadathur2023.nrv_sufficient_for_msg : Causation.Implicative.manageSem dreyfusSEM dreyfusBg V.NRV true V.MSG true

Sufficiency presupposition (32iii) for (34a): NRV is causally sufficient (Def 10a) for MSG — neither fact is entailed by the background, and adding NRV = 1 causally entails MSG = 1.

theorem Nadathur2023.nrv_necessary_for_msg : Causation.Implicative.necessityPresup dreyfusSEM dreyfusBg V.NRV true V.MSG true

Necessity presupposition (32i) for (34a): NRV is causally necessary (Def 10b) for MSG. Decided through the fuel bridge: the supersituation quantifiers range over the finite valuation space.

theorem Nadathur2023.dare_felicitous_for_msg : Causation.Implicative.necessityPresup dreyfusSEM dreyfusBg V.NRV true V.MSG true ∧ Causation.Implicative.manageSem dreyfusSEM dreyfusBg V.NRV true V.MSG true

(34a) Dreyfus dared to send a message to the Germans — felicitous: "NRV is the only undetermined condition for the truth of MSG: it is thus both causally necessary and sufficient for MSG" ([Nad23b] §6.1.1). Both presuppositions of two-way dare (Proposal 32 i, iii) are satisfied in context.

theorem Nadathur2023.dare_infelicitous_for_com : Causation.Implicative.failSem dreyfusSEM dreyfusBg V.NRV true V.COM true

(34c) ?/# Dreyfus dared to establish communication with the Germans — infelicitous: NRV is not causally sufficient for COM, which stays unsettled while LST and BRK are unresolved in the background.

theorem Nadathur2023.dare_infelicitous_for_spy : Causation.Implicative.failSem dreyfusSEM dreyfusBg V.NRV true V.SPY true

(34d) ?/# Dreyfus dared to spy for the Germans — infelicitous: NRV is not causally sufficient for SPY (its conditions LST, BRK, COM are all undetermined).

theorem Nadathur2023.nrv_necessary_for_com : Causation.Implicative.necessityPresup dreyfusSEM dreyfusBg V.NRV true V.COM true

(34c), necessity half: "⟨NRV,1⟩ is causally necessary but not sufficient for COM" — achievability settles the exogenous LST = 1, BRK = 0; every consistent path to COM = 1 runs through NRV = 1. Was unprovable under the eager-default dynamics (achievability could never resolve an exogenous unknown).

theorem Nadathur2023.nrv_necessary_for_spy : Causation.Implicative.necessityPresup dreyfusSEM dreyfusBg V.NRV true V.SPY true

(34d), necessity half: NRV is causally necessary but not sufficient for SPY ("BRK, LST, COM ∈ Anc(SPY) are all undetermined").

theorem Nadathur2023.nrv_necessary_not_sufficient_for_com_and_spy : (Causation.Implicative.necessityPresup dreyfusSEM dreyfusBg V.NRV true V.COM true ∧ Causation.Implicative.failSem dreyfusSEM dreyfusBg V.NRV true V.COM true) ∧ Causation.Implicative.necessityPresup dreyfusSEM dreyfusBg V.NRV true V.SPY true ∧ Causation.Implicative.failSem dreyfusSEM dreyfusBg V.NRV true V.SPY true

(34c)/(34d) complete profiles: NRV is causally necessary but not sufficient for COM and for SPY — the paper's exact §6.1.1 verdicts, as single statements.

theorem Nadathur2023.no_msg_without_nerve (s' : Causation.Valuation fun (x : V) => Bool) : Causation.SEM.IsExogenousSettlement dreyfusSEM (dreyfusBg.extend V.NRV false) s' → s'.get V.MSG = none → ¬Causation.SEM.causallyEntails dreyfusSEM s' V.MSG true

Fact B, negative half, at (34b): Dreyfus did not dare to send a message — no consistent completion of the negative-assertion context realizes MSG. Instantiates Implicative.no_complement_of_negative_assertion at the Dreyfus model.

theorem Nadathur2023.msg_iff_nerve (s' : Causation.Valuation fun (x : V) => Bool) : Causation.SEM.IsExogenousSettlement dreyfusSEM dreyfusBg s' → s'.get V.MSG = none → (Causation.SEM.causallyEntails dreyfusSEM s' V.MSG true ↔ Causation.SEM.causallyEntails dreyfusSEM s' V.NRV true)

Fact C at (34a): in the Dreyfus context, a consistent completion realizes MSG exactly when Dreyfus has the nerve — the prerequisite is sufficient and necessary, so the dare claim's truth value tracks NRV across all consistent resolutions.

[Nad23b] §2 motivates the prerequisite account from [Kar71]'s descriptive 2×2 taxonomy; the conversion lives here (the later paper draws the comparison). The two-way cell's defining entailment pattern is not stipulated but derived: Implicative.twoWay_entailment_profile produces both halves of Fact B from the sufficiency + necessity presuppositions, witnessed concretely at the Dreyfus model by Nadathur2023.dare_felicitous_for_msg together with Nadathur2023.no_msg_without_nerve.

def Karttunen1971.KarttunenClass.toImplicativeClass (k : KarttunenClass) : Causation.Implicative.ImplicativeClass

Convert KarttunenClass to ImplicativeClass ([Nad23b]). aspectGoverned is always false because Karttunen's 1971 analysis does not account for aspect — a limitation the modern analysis corrects.

Equations

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

theorem Karttunen1971.karttunen_manage_matches : KarttunenClass.manage.toImplicativeClass = Causation.Implicative.ImplicativeClass.manage

theorem Karttunen1971.karttunen_fail_matches : KarttunenClass.fail.toImplicativeClass = Causation.Implicative.ImplicativeClass.fail