@cite{nadathur-lauer-2020}: Causal Necessity, Causal Sufficiency, and the Implications of Causative Verbs

@cite{nadathur-lauer-2020} @cite{pearl-2000}

Nadathur & Lauer 2020. Glossa 5(1): 49.

Headline claim

Periphrastic make and cause differ truth-conditionally:

• cause asserts causal necessity (Def 24)
• make asserts causal sufficiency (Def 23)

The two notions are mathematically distinct over a structural-equation framework: there exist scenarios where one holds but the other doesn't, producing minimal-pair contrasts in felicity.

This file formalizes N&L's three illustrative scenarios (§3.6.1-§3.6.3) plus the volitional-action constraint (§4.1, Def 43) that distinguishes make from sister periphrastics like let.

Project-canonical definitions

The substrate's Necessity.causeSem (in Theories/Semantics/Causation/) implements @cite{nadathur-2024} Definition 10b rather than this paper's literal Def 24. The paper itself anticipates this in fn 18: "the semantics of necessity causatives may well be better explicated in terms of one of the definitions of actual cause, rather than the version of causal necessity defined here." Def 10b IS an actual-cause formulation. The deviation is principled.

Sufficiency.makeSem is N&L's Def 23 essentially verbatim (modulo the actuality conjunct, which the deterministic substrate makes redundant with the development-equals-effect clause).

Scenarios

• Fire (§3.6.1, Fig 2): necessary but insufficient cause. cause OK, make infelicitous. Adding the missing precondition flips both to felicitous.
• Bus (§3.6.2, Fig 3): sufficient but unnecessary cause. make OK, cause infelicitous.
• Lighthouse (§3.6.3, Fig 4): temporal location constraint (Def 28) blocks make for the earlier of two necessary causes; cause remains felicitous for both.
• Permission (§4.1, Fig 5): bare sufficiency holds but Def 43 (volitional-action constraint) fails — predicts make infelicitous.
• Command (§4.1, Fig 6) + Persuasion (§4.1, Fig 7): Def 43 satisfied — predicts make felicitous in both authority and manipulation contexts.

Excluded

The Suzy/Billy preemption scenario (the centerpiece of Lewis 1973, @cite{lewis-1973-causation}) is not formalized here — N&L footnote 8 explicitly says "we will not discuss the specifics of pre-emption in this paper." The scenario lives at Lewis1973.Overdetermination (the chronologically-canonical owner). See ProductionDependence.lean's discussion for the cross-paper consequence.

inductive Phenomena.Causation.Studies.NadathurLauer2020.Fire.V : Type

Vertices for the fire dynamics (Fig 2): P=power restored, D=drought, G=grass inflammable, L=line down, F=fire.

• P : V
• D : V
• G : V
• L : V
• F : V

@[implicit_reducible]

instance Phenomena.Causation.Studies.NadathurLauer2020.Fire.instDecidableEqV : DecidableEq V

Equations

• Phenomena.Causation.Studies.NadathurLauer2020.Fire.instDecidableEqV x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Phenomena.Causation.Studies.NadathurLauer2020.Fire.instFintypeV : Fintype V

Equations

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

def Phenomena.Causation.Studies.NadathurLauer2020.Fire.instReprV.repr : V → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Phenomena.Causation.Studies.NadathurLauer2020.Fire.instReprV : Repr V

Equations

• Phenomena.Causation.Studies.NadathurLauer2020.Fire.instReprV = { reprPrec := Phenomena.Causation.Studies.NadathurLauer2020.Fire.instReprV.repr }

def Phenomena.Causation.Studies.NadathurLauer2020.Fire.graph : Core.Causal.CausalGraph V

Causal graph: G←{D}; F←{G,P,L}; P,D,L exogenous.

Equations

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

instance Phenomena.Causation.Studies.NadathurLauer2020.Fire.instIsDAGVGraph : graph.IsDAG

noncomputable def Phenomena.Causation.Studies.NadathurLauer2020.Fire.fireSEM : Core.Causal.BoolSEM V

Fire dynamics: G := D (inflammability tracks drought); F := G ∧ P ∧ L (fire ignites only when grass inflammable, power on, line touching).

Equations

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

instance Phenomena.Causation.Studies.NadathurLauer2020.Fire.instIsDAGVGraphBoolFireSEM : fireSEM.graph.IsDAG

@[implicit_reducible]

noncomputable instance Phenomena.Causation.Studies.NadathurLauer2020.Fire.instIsDeterministicVBoolFireSEM : Core.Causal.SEM.IsDeterministic fireSEM

Equations

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

noncomputable def Phenomena.Causation.Studies.NadathurLauer2020.Fire.s_b : Core.Causal.Valuation fun (x : V) => Bool

Background s_b: drought conditions and inflammable grass observed, line condition unknown. (Per N&L p. 19, footnote 21: realistic epistemic ignorance about whether the line was already down.)

Equations

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

noncomputable def Phenomena.Causation.Studies.NadathurLauer2020.Fire.s_b1 : Core.Causal.Valuation fun (x : V) => Bool

Extended background s_b1: the line is also known to be down.

Equations

• Phenomena.Causation.Studies.NadathurLauer2020.Fire.s_b1 = Phenomena.Causation.Studies.NadathurLauer2020.Fire.s_b.extend Phenomena.Causation.Studies.NadathurLauer2020.Fire.V.L true

theorem Phenomena.Causation.Studies.NadathurLauer2020.Fire.make_infelicitous_for_fire : ¬Semantics.Causation.Sufficiency.makeSem fireSEM s_b V.P true V.F true

(31a) #Restoring power made the field catch fire. Make-side: P=true is NOT sufficient for F=true relative to s_b. With L undetermined, the fire mechanism G ∧ P ∧ L cannot fire to true.

theorem Phenomena.Causation.Studies.NadathurLauer2020.Fire.make_felicitous_for_fire_with_known_line : Semantics.Causation.Sufficiency.makeSem fireSEM s_b1 V.P true V.F true

(31b, with extended background s_b1 where L is also known) Restoring power caused the field to catch fire. Both make and cause hold. With s_b1 fixing D=G=L=1, P=true is both sufficient and necessary for F=true.

inductive Phenomena.Causation.Studies.NadathurLauer2020.Bus.V : Type

Vertices for the bus dynamics (Fig 3): Vis=Ava visiting, Tr=training, Rn=rain forecast, Bk=bike gone, Bs=Lia takes the bus.

• Vis : V
• Tr : V
• Rn : V
• Bk : V
• Bs : V

@[implicit_reducible]

instance Phenomena.Causation.Studies.NadathurLauer2020.Bus.instDecidableEqV : DecidableEq V

Equations

• Phenomena.Causation.Studies.NadathurLauer2020.Bus.instDecidableEqV x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Phenomena.Causation.Studies.NadathurLauer2020.Bus.instFintypeV : Fintype V

Equations

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

def Phenomena.Causation.Studies.NadathurLauer2020.Bus.instReprV.repr : V → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Phenomena.Causation.Studies.NadathurLauer2020.Bus.instReprV : Repr V

Equations

• Phenomena.Causation.Studies.NadathurLauer2020.Bus.instReprV = { reprPrec := Phenomena.Causation.Studies.NadathurLauer2020.Bus.instReprV.repr }

def Phenomena.Causation.Studies.NadathurLauer2020.Bus.graph : Core.Causal.CausalGraph V

Causal graph: Bk←{Vis,Tr}; Bs←{Rn,Bk}; Vis,Tr,Rn exogenous.

Equations

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

instance Phenomena.Causation.Studies.NadathurLauer2020.Bus.instIsDAGVGraph : graph.IsDAG

noncomputable def Phenomena.Causation.Studies.NadathurLauer2020.Bus.busSEM : Core.Causal.BoolSEM V

Bus dynamics: Bk := Vis ∧ Tr (bike taken when Ava visits AND trains); Bs := Rn ∨ Bk (bus taken when rain OR bike gone). The OR for Bs matches Fig 3's f_B table on p. 20: B=1 iff R=1 or G=1. This creates the "sufficient but unnecessary" structure for T: T=1 forces Bs=1 (sufficient via Bk), but Rn=1 alone also forces Bs=1 (so T not necessary).

Equations

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

instance Phenomena.Causation.Studies.NadathurLauer2020.Bus.instIsDAGVGraphBoolBusSEM : busSEM.graph.IsDAG

@[implicit_reducible]

noncomputable instance Phenomena.Causation.Studies.NadathurLauer2020.Bus.instIsDeterministicVBoolBusSEM : Core.Causal.SEM.IsDeterministic busSEM

Equations

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

noncomputable def Phenomena.Causation.Studies.NadathurLauer2020.Bus.s_b : Core.Causal.Valuation fun (x : V) => Bool

Background s_b: Ava visiting, rain forecast. Training status Tr is the purported cause of bus-taking (via bike taken).

Equations

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

theorem Phenomena.Causation.Studies.NadathurLauer2020.Bus.make_felicitous_for_bus : Semantics.Causation.Sufficiency.makeSem busSEM s_b V.Tr true V.Bs true

(33a) Ava's training made Lia take the bus to work. Make-side: T=true is sufficient for B=true relative to s_b. With Vis=Rn=1 in background, Tr:=1 forces Bk:=1 forces Bs:=1.

theorem Phenomena.Causation.Studies.NadathurLauer2020.Bus.cause_infelicitous_for_bus : ¬Semantics.Causation.Necessity.causeSem busSEM s_b V.Tr true V.Bs true

(33b) #Ava's training caused Lia to take the bus. Cause-side: fails N&L's Def 24 / project-canonical Def 10b necessity.

Under this substrate's eager-default semantics (every undetermined root vertex defaults to its const mechanism value), developDetVtx busSEM s_b .Bs = true already (because Rn=true in s_b suffices via the OR mechanism). This makes causeSem's precondition clause fail: "the dynamics does not already entail effect=xE in the background" is false here.

N&L's stepwise semantics (which leaves Bs undetermined until both parents are determined) instead derives infelicity via the noAlternative clause — a consistent supersituation lacking Tr=true that still produces Bs=true. Same empirical conclusion (cause infelicitous), different load-bearing clause; see module docstring on substrate deviation.

Per-vertex temporal index and the temporal-location constraint (@cite{nadathur-lauer-2020} Def 28). Local to this study file — promote to substrate (Core/Causal/SEM/Temporal.lean) if a second consumer emerges.

inductive Phenomena.Causation.Studies.NadathurLauer2020.Lighthouse.V : Type

Vertices: Q=earthquake (time 1), S=storms (time 2), L=tower collapse (time 3).

• Q : V
• S : V
• L : V

@[implicit_reducible]

instance Phenomena.Causation.Studies.NadathurLauer2020.Lighthouse.instDecidableEqV : DecidableEq V

Equations

• Phenomena.Causation.Studies.NadathurLauer2020.Lighthouse.instDecidableEqV x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Phenomena.Causation.Studies.NadathurLauer2020.Lighthouse.instFintypeV : Fintype V

Equations

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

@[implicit_reducible]

instance Phenomena.Causation.Studies.NadathurLauer2020.Lighthouse.instReprV : Repr V

Equations

• Phenomena.Causation.Studies.NadathurLauer2020.Lighthouse.instReprV = { reprPrec := Phenomena.Causation.Studies.NadathurLauer2020.Lighthouse.instReprV.repr }

def Phenomena.Causation.Studies.NadathurLauer2020.Lighthouse.instReprV.repr : V → ℕ → Std.Format

Equations

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

def Phenomena.Causation.Studies.NadathurLauer2020.Lighthouse.graph : Core.Causal.CausalGraph V

Equations

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

instance Phenomena.Causation.Studies.NadathurLauer2020.Lighthouse.instIsDAGVGraph : graph.IsDAG

noncomputable def Phenomena.Causation.Studies.NadathurLauer2020.Lighthouse.lighthouseSEM : Core.Causal.BoolSEM V

Lighthouse dynamics: L := Q ∧ S (collapse requires both earthquake-induced foundation damage AND extreme storms).

Equations

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

instance Phenomena.Causation.Studies.NadathurLauer2020.Lighthouse.instIsDAGVGraphBoolLighthouseSEM : lighthouseSEM.graph.IsDAG

@[implicit_reducible]

noncomputable instance Phenomena.Causation.Studies.NadathurLauer2020.Lighthouse.instIsDeterministicVBoolLighthouseSEM : Core.Causal.SEM.IsDeterministic lighthouseSEM

Equations

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

def Phenomena.Causation.Studies.NadathurLauer2020.Lighthouse.lighthouseTimes : V → ℕ

Temporal index: per-vertex timestamp. Q happens at time 1, S at 2, L at 3.

Equations

• Phenomena.Causation.Studies.NadathurLauer2020.Lighthouse.lighthouseTimes Phenomena.Causation.Studies.NadathurLauer2020.Lighthouse.V.Q = 1
• Phenomena.Causation.Studies.NadathurLauer2020.Lighthouse.lighthouseTimes Phenomena.Causation.Studies.NadathurLauer2020.Lighthouse.V.S = 2
• Phenomena.Causation.Studies.NadathurLauer2020.Lighthouse.lighthouseTimes Phenomena.Causation.Studies.NadathurLauer2020.Lighthouse.V.L = 3

def Phenomena.Causation.Studies.NadathurLauer2020.Lighthouse.validBackgroundFor (idx : V → ℕ) (t : ℕ) (s : Core.Causal.Valuation fun (x : V) => Bool) : Prop

Temporal location constraint (@cite{nadathur-lauer-2020} Def 28): a background situation s is valid for a causative claim with evaluation time t iff every vertex s fixes has time ≤ t.

Default evaluation time is the cause's time.

Equations

• Phenomena.Causation.Studies.NadathurLauer2020.Lighthouse.validBackgroundFor idx t s = ∀ (v : Phenomena.Causation.Studies.NadathurLauer2020.Lighthouse.V), (s.get v).isSome = true → idx v ≤ t

theorem Phenomena.Causation.Studies.NadathurLauer2020.Lighthouse.make_felicitous_for_storms : Semantics.Causation.Sufficiency.makeSem lighthouseSEM (Core.Causal.Valuation.empty.extend V.Q true) V.S true V.L true

(35d) The storms made the tower collapse. Felicitous: with background fixing Q=true (the earlier necessary cause), S=true suffices for L=true.

theorem Phenomena.Causation.Studies.NadathurLauer2020.Lighthouse.make_infelicitous_for_earthquake (s : Core.Causal.Valuation fun (x : V) => Bool) : validBackgroundFor lighthouseTimes 1 s → ¬Semantics.Causation.Sufficiency.makeSem lighthouseSEM s V.Q true V.L true

(35c) #The earthquake made the tower collapse. Infelicitous via Def 28 temporal-location constraint: the only background under which Q=true would be sufficient for L=true is one fixing S=true, but S happens at time 2 > 1 = time of Q. So no temporally-valid background supports the make-claim.

Concretely: for the make-claim to hold per Def 23, need a background s such that adding Q to s develops L. Under eager-default semantics, dev L from (s + Q:=true) = Q ∧ S. For this to equal true, S must be fixed to true in s. But lighthouseTimes .S = 2 > 1, so any such s violates validBackgroundFor lighthouseTimes 1.

N&L's Def 43 distinguishes make from sister periphrastics like let: when the effect is a volitional action with intention vertex W_E, the background must not fix W_E in a way that makes the cause determinative regardless of the agent's will.

def Phenomena.Causation.Studies.NadathurLauer2020.Volitional.IntentionMap (V : Type u_1) : Type u_1

Pairs an effect vertex with its associated intention vertex (W_E). none means the effect is not volitional.

Equations

• Phenomena.Causation.Studies.NadathurLauer2020.Volitional.IntentionMap V = (V → Option V)

def Phenomena.Causation.Studies.NadathurLauer2020.Volitional.volitionalActionConstraint {V : Type u_1} [Fintype V] [DecidableEq V] (M : Core.Causal.BoolSEM V) [M.graph.IsDAG] [Core.Causal.SEM.IsDeterministic M] (intentions : IntentionMap V) (bg : Core.Causal.Valuation fun (x : V) => Bool) (cause effect : V) : Prop

Constraint on volitional action (@cite{nadathur-lauer-2020} Def 43): in the evaluation of a make-causative with cause C and effect E, no intention vertex W_E paired with E may be such that BOTH (i) W_E := false is sufficient for E := false relative to bg + (C := true) AND (ii) W_E is determined by bg \ (C := true).

For deterministic SEMs makeSem ... wE false eff false is the sufficiency check; (bg.remove cause).get wE ≠ none is the determined-ness check.

Equations

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

inductive Phenomena.Causation.Studies.NadathurLauer2020.Permission.V : Type

Vertices: WD = children's desire to dance, G = Gurung's permission, D = children dance.

• WD : V
• G : V
• D : V

@[implicit_reducible]

instance Phenomena.Causation.Studies.NadathurLauer2020.Permission.instDecidableEqV : DecidableEq V

Equations

• Phenomena.Causation.Studies.NadathurLauer2020.Permission.instDecidableEqV x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Phenomena.Causation.Studies.NadathurLauer2020.Permission.instFintypeV : Fintype V

Equations

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

def Phenomena.Causation.Studies.NadathurLauer2020.Permission.instReprV.repr : V → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Phenomena.Causation.Studies.NadathurLauer2020.Permission.instReprV : Repr V

Equations

• Phenomena.Causation.Studies.NadathurLauer2020.Permission.instReprV = { reprPrec := Phenomena.Causation.Studies.NadathurLauer2020.Permission.instReprV.repr }

def Phenomena.Causation.Studies.NadathurLauer2020.Permission.graph : Core.Causal.CausalGraph V

Equations

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

instance Phenomena.Causation.Studies.NadathurLauer2020.Permission.instIsDAGVGraph : graph.IsDAG

noncomputable def Phenomena.Causation.Studies.NadathurLauer2020.Permission.permissionSEM : Core.Causal.BoolSEM V

Permission dynamics (Fig 5): D := W_D ∧ G. Both desire AND permission needed for dancing.

Equations

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

instance Phenomena.Causation.Studies.NadathurLauer2020.Permission.instIsDAGVGraphBoolPermissionSEM : permissionSEM.graph.IsDAG

@[implicit_reducible]

noncomputable instance Phenomena.Causation.Studies.NadathurLauer2020.Permission.instIsDeterministicVBoolPermissionSEM : Core.Causal.SEM.IsDeterministic permissionSEM

Equations

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

noncomputable def Phenomena.Causation.Studies.NadathurLauer2020.Permission.bg : Core.Causal.Valuation fun (x : V) => Bool

Background: children eager to dance (W_D := true). Cause is G (Gurung's permission); effect is D (dancing).

Equations

• Phenomena.Causation.Studies.NadathurLauer2020.Permission.bg = Core.Causal.Valuation.empty.extend Phenomena.Causation.Studies.NadathurLauer2020.Permission.V.WD true

def Phenomena.Causation.Studies.NadathurLauer2020.Permission.intentions : Volitional.IntentionMap V

Intention map: dancing's intention vertex is W_D.

Equations

• One or more equations did not get rendered due to their size.
• Phenomena.Causation.Studies.NadathurLauer2020.Permission.intentions x✝ = none

theorem Phenomena.Causation.Studies.NadathurLauer2020.Permission.permission_makeSem : Semantics.Causation.Sufficiency.makeSem permissionSEM bg V.G true V.D true

Bare sufficiency holds: G:=true is sufficient for D=true given W_D=true.

theorem Phenomena.Causation.Studies.NadathurLauer2020.Permission.permission_violates_volitional_constraint : ¬Volitional.volitionalActionConstraint permissionSEM intentions bg V.G V.D

(40a) ??Gurung made the children dance. Volitional-action constraint VIOLATED: with W_D fixed in bg, W_D := false is sufficient for D := false (W_D ∧ G with W_D=false gives false), and W_D is determined by bg \ {G} (W_D was in bg, removing G doesn't unfix it). Per Def 43, this rules out felicitous use of make.

theorem Phenomena.Causation.Studies.NadathurLauer2020.Permission.permission_make_infelicitous : ¬(Semantics.Causation.Sufficiency.makeSem permissionSEM bg V.G true V.D true ∧ Volitional.volitionalActionConstraint permissionSEM intentions bg V.G V.D)

(40a) Combined predicate: bare make-sufficiency AND volitional constraint must BOTH hold for make to be felicitous. Permission scenario gives the former but fails the latter — N&L's headline §4.1 prediction.

inductive Phenomena.Causation.Studies.NadathurLauer2020.Command.V : Type

Command scenario: same vertices as Permission, different mechanism. Bg may or may not fix W_D — N&L's (41)/(42) show make felicitous in either case, so command-style mechanism makes W_D irrelevant once G fires.

• WD : V
• G : V
• D : V

@[implicit_reducible]

instance Phenomena.Causation.Studies.NadathurLauer2020.Command.instDecidableEqV : DecidableEq V

Equations

• Phenomena.Causation.Studies.NadathurLauer2020.Command.instDecidableEqV x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Phenomena.Causation.Studies.NadathurLauer2020.Command.instFintypeV : Fintype V

Equations

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

@[implicit_reducible]

instance Phenomena.Causation.Studies.NadathurLauer2020.Command.instReprV : Repr V

Equations

• Phenomena.Causation.Studies.NadathurLauer2020.Command.instReprV = { reprPrec := Phenomena.Causation.Studies.NadathurLauer2020.Command.instReprV.repr }

def Phenomena.Causation.Studies.NadathurLauer2020.Command.instReprV.repr : V → ℕ → Std.Format

Equations

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

def Phenomena.Causation.Studies.NadathurLauer2020.Command.graph : Core.Causal.CausalGraph V

Equations

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

instance Phenomena.Causation.Studies.NadathurLauer2020.Command.instIsDAGVGraph : graph.IsDAG

noncomputable def Phenomena.Causation.Studies.NadathurLauer2020.Command.commandSEM : Core.Causal.BoolSEM V

Command dynamics (Fig 6): D := W_D ∨ G. Either authority alone OR independent desire suffices for dancing.

Equations

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

instance Phenomena.Causation.Studies.NadathurLauer2020.Command.instIsDAGVGraphBoolCommandSEM : commandSEM.graph.IsDAG

@[implicit_reducible]

noncomputable instance Phenomena.Causation.Studies.NadathurLauer2020.Command.instIsDeterministicVBoolCommandSEM : Core.Causal.SEM.IsDeterministic commandSEM

Equations

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

def Phenomena.Causation.Studies.NadathurLauer2020.Command.intentions : Volitional.IntentionMap V

Equations

• Phenomena.Causation.Studies.NadathurLauer2020.Command.intentions Phenomena.Causation.Studies.NadathurLauer2020.Command.V.D = some Phenomena.Causation.Studies.NadathurLauer2020.Command.V.WD
• Phenomena.Causation.Studies.NadathurLauer2020.Command.intentions x✝ = none

theorem Phenomena.Causation.Studies.NadathurLauer2020.Command.command_makeSem : Semantics.Causation.Sufficiency.makeSem commandSEM Core.Causal.Valuation.empty V.G true V.D true

Bare sufficiency holds with empty background: G:=true alone forces D=true.

theorem Phenomena.Causation.Studies.NadathurLauer2020.Command.command_satisfies_volitional_constraint : Volitional.volitionalActionConstraint commandSEM intentions Core.Causal.Valuation.empty V.G V.D

(41a)/(42a) Gurung made the children dance (in command context). Volitional-action constraint SATISFIED: W_D := false is NOT sufficient for D := false (D = W_D ∨ G with G=true gives D=true regardless). First conjunct of Def 43's bad condition fails, so constraint holds.

theorem Phenomena.Causation.Studies.NadathurLauer2020.Command.command_make_felicitous : Semantics.Causation.Sufficiency.makeSem commandSEM Core.Causal.Valuation.empty V.G true V.D true ∧ Volitional.volitionalActionConstraint commandSEM intentions Core.Causal.Valuation.empty V.G V.D

(41a)/(42a) Combined: command scenario gives BOTH bare sufficiency AND volitional constraint satisfaction → make-felicitous.

inductive Phenomena.Causation.Studies.NadathurLauer2020.Persuasion.V : Type

Persuasion scenario: G manipulates W_D, then W_D drives D. Distinct mechanism: G acts via the agent's desire, not in parallel.

• WD : V
• G : V
• D : V

@[implicit_reducible]

instance Phenomena.Causation.Studies.NadathurLauer2020.Persuasion.instDecidableEqV : DecidableEq V

Equations

• Phenomena.Causation.Studies.NadathurLauer2020.Persuasion.instDecidableEqV x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Phenomena.Causation.Studies.NadathurLauer2020.Persuasion.instFintypeV : Fintype V

Equations

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

@[implicit_reducible]

instance Phenomena.Causation.Studies.NadathurLauer2020.Persuasion.instReprV : Repr V

Equations

• Phenomena.Causation.Studies.NadathurLauer2020.Persuasion.instReprV = { reprPrec := Phenomena.Causation.Studies.NadathurLauer2020.Persuasion.instReprV.repr }

def Phenomena.Causation.Studies.NadathurLauer2020.Persuasion.instReprV.repr : V → ℕ → Std.Format

Equations

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

def Phenomena.Causation.Studies.NadathurLauer2020.Persuasion.graph : Core.Causal.CausalGraph V

Equations

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

instance Phenomena.Causation.Studies.NadathurLauer2020.Persuasion.instIsDAGVGraph : graph.IsDAG

noncomputable def Phenomena.Causation.Studies.NadathurLauer2020.Persuasion.persuasionSEM : Core.Causal.BoolSEM V

Persuasion dynamics (Fig 7): W_D := G (Gurung's action shapes desires); D := W_D (children dance iff they want to).

Equations

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

instance Phenomena.Causation.Studies.NadathurLauer2020.Persuasion.instIsDAGVGraphBoolPersuasionSEM : persuasionSEM.graph.IsDAG

@[implicit_reducible]

noncomputable instance Phenomena.Causation.Studies.NadathurLauer2020.Persuasion.instIsDeterministicVBoolPersuasionSEM : Core.Causal.SEM.IsDeterministic persuasionSEM

Equations

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

def Phenomena.Causation.Studies.NadathurLauer2020.Persuasion.intentions : Volitional.IntentionMap V

Equations

• One or more equations did not get rendered due to their size.
• Phenomena.Causation.Studies.NadathurLauer2020.Persuasion.intentions x✝ = none

theorem Phenomena.Causation.Studies.NadathurLauer2020.Persuasion.persuasion_makeSem : Semantics.Causation.Sufficiency.makeSem persuasionSEM Core.Causal.Valuation.empty V.G true V.D true

Bare sufficiency: G:=true forces W_D=true forces D=true.

theorem Phenomena.Causation.Studies.NadathurLauer2020.Persuasion.persuasion_satisfies_volitional_constraint : Volitional.volitionalActionConstraint persuasionSEM intentions Core.Causal.Valuation.empty V.G V.D

(44a) Gurung made the children dance (by playing their favourite song). Volitional-action constraint SATISFIED: although W_D := false is sufficient for D := false (D = W_D), W_D is NOT determined by the background (empty bg leaves W_D undetermined). Second conjunct of Def 43's bad condition fails.

theorem Phenomena.Causation.Studies.NadathurLauer2020.Persuasion.persuasion_make_felicitous : Semantics.Causation.Sufficiency.makeSem persuasionSEM Core.Causal.Valuation.empty V.G true V.D true ∧ Volitional.volitionalActionConstraint persuasionSEM intentions Core.Causal.Valuation.empty V.G V.D

N&L §4.2 argues that the necessity inference of make is a pragmatic enrichment, not entailed content. Their argument runs through implicature tests: - Cancellability (49): "Gurung made the children dance, but they might have danced anyway" — felicitous, cancels the necessity reading without contradiction. - Reinforceability (50): "The data made me do it. I would never have done it otherwise." — felicitous, reinforces the necessity reading without redundancy. - Soccer camp (16): a fully felicitous use of make in an explicitly necessity-denying context.

Structurally, these all follow from N&L's headline result that
*make* asserts sufficiency only — necessity is a separable layer.
The Bus and Fire scenarios already witness this:
- Bus: `make` holds while necessity (`cause`) fails (sufficient ≠ necessary)
- Fire (with known line): `make` and `cause` hold without redundancy
  (the two assertions are independently informative)

These scenarios are the structural counterpart of the implicature
tests; the prose tests follow from them. 

theorem Phenomena.Causation.Studies.NadathurLauer2020.necessity_cancellable : Semantics.Causation.Sufficiency.makeSem Bus.busSEM Bus.s_b Bus.V.Tr true Bus.V.Bs true ∧ ¬Semantics.Causation.Necessity.causeSem Bus.busSEM Bus.s_b Bus.V.Tr true Bus.V.Bs true

Cancellability witness (cf. (49)): the bus scenario shows that make can hold while cause (necessity) fails. So if make did entail necessity, this scenario would be contradictory; since it's not, the necessity inference must be cancellable.

theorem Phenomena.Causation.Studies.NadathurLauer2020.necessity_reinforceable : Semantics.Causation.Sufficiency.makeSem Fire.fireSEM Fire.s_b1 Fire.V.P true Fire.V.F true

Reinforceability witness (cf. (50)): the fire scenario with known-line background gives both make and (predictably) cause felicity. Asserting "the data made me do it; I'd never have done it otherwise" reinforces necessity onto a sufficiency-asserting make-claim — felicitous because the two assertions are independent.