Documentation

Linglib.Studies.NadathurLauer2020

[NL20]: Causal Necessity, Causal Sufficiency, and the Implications of Causative Verbs #

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 Semantics/Causation/) implements [Nad23b] 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 the sufficiency clause (b) of N&L's Def 23; the non-inevitability precondition (clause a) is not yet represented in the substrate (it would be falsified by the eager-default development — see the substrate TODO in SEM/Counterfactual.lean).

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 #

Preemption (Suzy/Billy) is not formalized here — N&L footnote 8 explicitly says "we will not discuss the specifics of pre-emption in this paper" — and is not formalized in Studies/Lewis1973.lean either: that file's Overdetermination namespace is symmetric overdetermination (which Lewis's fn. 12 sets aside), not late preemption. See ProductionDependence.lean's discussion for the cross-paper consequence.

inductive NadathurLauer2020.Fire.V :

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

Instances For

@[implicit_reducible]

instance NadathurLauer2020.Fire.instDecidableEqV :

DecidableEq V

Equations

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

@[implicit_reducible]

instance NadathurLauer2020.Fire.instFintypeV :

Fintype V

Equations

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

@[implicit_reducible]

instance NadathurLauer2020.Fire.instReprV :

Repr V

Equations

NadathurLauer2020.Fire.instReprV = { reprPrec := NadathurLauer2020.Fire.instReprV.repr }

def NadathurLauer2020.Fire.instReprV.repr :

V → ℕ → Std.Format

Equations

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

Instances For

def NadathurLauer2020.Fire.graph :

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

Instances For

def NadathurLauer2020.Fire.depth :

V → ℕ

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

Equations

Instances For

instance NadathurLauer2020.Fire.instIsDAGVGraph :

noncomputable def NadathurLauer2020.Fire.fireSEM :

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

Instances For

instance NadathurLauer2020.Fire.instIsDAGVGraphBoolFireSEM :

fireSEM.graph.IsDAG

@[implicit_reducible]

noncomputable instance NadathurLauer2020.Fire.instIsDeterministicVBoolFireSEM :

Causation.SEM.IsDeterministic fireSEM

Equations

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

noncomputable def NadathurLauer2020.Fire.s_b :

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

NadathurLauer2020.Fire.s_b = (Causation.Valuation.empty.extend NadathurLauer2020.Fire.V.D true).extend NadathurLauer2020.Fire.V.G true

Instances For

noncomputable def NadathurLauer2020.Fire.s_b1 :

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

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

Equations

NadathurLauer2020.Fire.s_b1 = NadathurLauer2020.Fire.s_b.extend NadathurLauer2020.Fire.V.L true

Instances For

theorem NadathurLauer2020.Fire.make_infelicitous_for_fire :

¬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 stays unsettled (Def 23's clause (b) fails).

theorem NadathurLauer2020.Fire.make_felicitous_for_fire_with_known_line :

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 NadathurLauer2020.Bus.V :

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

Instances For

@[implicit_reducible]

instance NadathurLauer2020.Bus.instDecidableEqV :

DecidableEq V

Equations

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

@[implicit_reducible]

instance NadathurLauer2020.Bus.instFintypeV :

Fintype V

Equations

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

@[implicit_reducible]

instance NadathurLauer2020.Bus.instReprV :

Repr V

Equations

NadathurLauer2020.Bus.instReprV = { reprPrec := NadathurLauer2020.Bus.instReprV.repr }

def NadathurLauer2020.Bus.instReprV.repr :

V → ℕ → Std.Format

Equations

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

Instances For

def NadathurLauer2020.Bus.graph :

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

Instances For

def NadathurLauer2020.Bus.depth :

V → ℕ

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

Equations

Instances For

instance NadathurLauer2020.Bus.instIsDAGVGraph :

noncomputable def NadathurLauer2020.Bus.busSEM :

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

Instances For

instance NadathurLauer2020.Bus.instIsDAGVGraphBoolBusSEM :

busSEM.graph.IsDAG

@[implicit_reducible]

noncomputable instance NadathurLauer2020.Bus.instIsDeterministicVBoolBusSEM :

Causation.SEM.IsDeterministic busSEM

Equations

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

noncomputable def NadathurLauer2020.Bus.s_b :

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

NadathurLauer2020.Bus.s_b = (Causation.Valuation.empty.extend NadathurLauer2020.Bus.V.Vis true).extend NadathurLauer2020.Bus.V.Rn true

Instances For

theorem NadathurLauer2020.Bus.make_felicitous_for_bus :

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: under the strict dynamics Bs stays unsettled in the background (Bk waits on Tr), so Def 23's non-inevitability clause (a) holds, and Tr:=1 forces Bk:=1 forces Bs:=1 for clause (b).

theorem NadathurLauer2020.Bus.cause_infelicitous_for_bus :

¬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 Def 10b necessity via the no-alternative clause, exactly N&L's route: the exogenous settlement s_b[Tr ↦ 0] still entails Bs = 1 (rain alone suffices via the OR mechanism) without entailing Tr = 1.

Per-vertex temporal index and the temporal-location constraint ([NL20] Def 28). Local to this study file — promote to substrate (Core/Causal/SEM/Temporal.lean) if a second consumer emerges.

inductive NadathurLauer2020.Lighthouse.V :

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

Q : V
S : V
L : V

Instances For

@[implicit_reducible]

instance NadathurLauer2020.Lighthouse.instDecidableEqV :

DecidableEq V

Equations

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

@[implicit_reducible]

instance NadathurLauer2020.Lighthouse.instFintypeV :

Fintype V

Equations

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

def NadathurLauer2020.Lighthouse.instReprV.repr :

V → ℕ → Std.Format

Equations

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

Instances For

@[implicit_reducible]

instance NadathurLauer2020.Lighthouse.instReprV :

Repr V

Equations

NadathurLauer2020.Lighthouse.instReprV = { reprPrec := NadathurLauer2020.Lighthouse.instReprV.repr }

def NadathurLauer2020.Lighthouse.graph :

Causation.CausalGraph V

Equations

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

Instances For

def NadathurLauer2020.Lighthouse.depth :

V → ℕ

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

Equations

Instances For

instance NadathurLauer2020.Lighthouse.instIsDAGVGraph :

noncomputable def NadathurLauer2020.Lighthouse.lighthouseSEM :

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

Instances For

instance NadathurLauer2020.Lighthouse.instIsDAGVGraphBoolLighthouseSEM :

lighthouseSEM.graph.IsDAG

@[implicit_reducible]

noncomputable instance NadathurLauer2020.Lighthouse.instIsDeterministicVBoolLighthouseSEM :

Causation.SEM.IsDeterministic lighthouseSEM

Equations

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

def NadathurLauer2020.Lighthouse.lighthouseTimes :

V → ℕ

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

Equations

Instances For

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

Temporal location constraint ([NL20] 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

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

Instances For

theorem NadathurLauer2020.Lighthouse.make_felicitous_for_storms :

Causation.Sufficiency.makeSem lighthouseSEM (Causation.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 NadathurLauer2020.Lighthouse.make_infelicitous_for_earthquake (s : Causation.Valuation fun (x : V) => Bool) :

validBackgroundFor lighthouseTimes 1 s → ¬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(b), the strict development of s + (Q := true) must fix L = 1, which requires S to be fixed in s. But lighthouseTimes .S = 2 > 1, so any such s violates validBackgroundFor lighthouseTimes 1 — S stays u-valued and L = Q ∧ S stays unsettled.

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

NadathurLauer2020.Volitional.IntentionMap V = (V → Option V)

Instances For

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

Constraint on volitional action ([NL20] 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.

Instances For

inductive NadathurLauer2020.Permission.V :

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

WD : V
G : V
D : V

Instances For

@[implicit_reducible]

instance NadathurLauer2020.Permission.instDecidableEqV :

DecidableEq V

Equations

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

@[implicit_reducible]

instance NadathurLauer2020.Permission.instFintypeV :

Fintype V

Equations

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

@[implicit_reducible]

instance NadathurLauer2020.Permission.instReprV :

Repr V

Equations

NadathurLauer2020.Permission.instReprV = { reprPrec := NadathurLauer2020.Permission.instReprV.repr }

def NadathurLauer2020.Permission.instReprV.repr :

V → ℕ → Std.Format

Equations

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

Instances For

def NadathurLauer2020.Permission.graph :

Causation.CausalGraph V

Equations

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

Instances For

def NadathurLauer2020.Permission.depth :

V → ℕ

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

Equations

Instances For

instance NadathurLauer2020.Permission.instIsDAGVGraph :

noncomputable def NadathurLauer2020.Permission.permissionSEM :

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

Instances For

instance NadathurLauer2020.Permission.instIsDAGVGraphBoolPermissionSEM :

permissionSEM.graph.IsDAG

@[implicit_reducible]

noncomputable instance NadathurLauer2020.Permission.instIsDeterministicVBoolPermissionSEM :

Causation.SEM.IsDeterministic permissionSEM

Equations

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

noncomputable def NadathurLauer2020.Permission.bg :

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

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

Equations

NadathurLauer2020.Permission.bg = Causation.Valuation.empty.extend NadathurLauer2020.Permission.V.WD true

Instances For

def NadathurLauer2020.Permission.intentions :

Volitional.IntentionMap V

Intention map: dancing's intention vertex is W_D.

Equations

Instances For

theorem NadathurLauer2020.Permission.permission_makeSem :

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 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 NadathurLauer2020.Permission.permission_make_infelicitous :

¬(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 NadathurLauer2020.Command.V :

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

Instances For

@[implicit_reducible]

instance NadathurLauer2020.Command.instDecidableEqV :

DecidableEq V

Equations

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

@[implicit_reducible]

instance NadathurLauer2020.Command.instFintypeV :

Fintype V

Equations

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

@[implicit_reducible]

instance NadathurLauer2020.Command.instReprV :

Repr V

Equations

NadathurLauer2020.Command.instReprV = { reprPrec := NadathurLauer2020.Command.instReprV.repr }

def NadathurLauer2020.Command.instReprV.repr :

V → ℕ → Std.Format

Equations

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

Instances For

def NadathurLauer2020.Command.graph :

Causation.CausalGraph V

Equations

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

Instances For

def NadathurLauer2020.Command.depth :

V → ℕ

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

Equations

Instances For

instance NadathurLauer2020.Command.instIsDAGVGraph :

noncomputable def NadathurLauer2020.Command.commandSEM :

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

Instances For

instance NadathurLauer2020.Command.instIsDAGVGraphBoolCommandSEM :

commandSEM.graph.IsDAG

@[implicit_reducible]

noncomputable instance NadathurLauer2020.Command.instIsDeterministicVBoolCommandSEM :

Causation.SEM.IsDeterministic commandSEM

Equations

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

def NadathurLauer2020.Command.intentions :

Volitional.IntentionMap V

Equations

Instances For

noncomputable def NadathurLauer2020.Command.bgEager :

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

(41) context: the children are independently eager (W_D = 1).

Equations

NadathurLauer2020.Command.bgEager = Causation.Valuation.empty.extend NadathurLauer2020.Command.V.WD true

Instances For

noncomputable def NadathurLauer2020.Command.bgReluctant :

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

(42) context: the children are reluctant (W_D = 0).

Equations

NadathurLauer2020.Command.bgReluctant = Causation.Valuation.empty.extend NadathurLauer2020.Command.V.WD false

Instances For

theorem NadathurLauer2020.Command.command_makeSem_eager :

Causation.Sufficiency.makeSem commandSEM bgEager V.G true V.D true

(41) Bare sufficiency in the eager context: with W_D = 1 fixed, D = W_D ∨ G stays unsettled while G is (Def 23a holds under the strict dynamics), and G := 1 settles it. N&L's (41)/(42) contexts differ only in the background setting of W_D; make is felicitous in both.

theorem NadathurLauer2020.Command.command_makeSem_reluctant :

Causation.Sufficiency.makeSem commandSEM bgReluctant V.G true V.D true

(42) Bare sufficiency in the reluctant context (W_D = 0).

theorem NadathurLauer2020.Command.command_satisfies_volitional_constraint :

Volitional.volitionalActionConstraint commandSEM intentions bgReluctant V.G V.D

(42a) Gurung made the children dance (reluctant context). Volitional-action constraint SATISFIED: W_D := false is NOT sufficient for D := false (D = W_D ∨ G with G = 1 settles true regardless), so Def 43's bad condition fails on its first conjunct.

theorem NadathurLauer2020.Command.command_make_felicitous :

Causation.Sufficiency.makeSem commandSEM bgReluctant V.G true V.D true ∧ Volitional.volitionalActionConstraint commandSEM intentions bgReluctant V.G V.D

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

inductive NadathurLauer2020.Persuasion.V :

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

Instances For

@[implicit_reducible]

instance NadathurLauer2020.Persuasion.instDecidableEqV :

DecidableEq V

Equations

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

@[implicit_reducible]

instance NadathurLauer2020.Persuasion.instFintypeV :

Fintype V

Equations

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

def NadathurLauer2020.Persuasion.instReprV.repr :

V → ℕ → Std.Format

Equations

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

Instances For

@[implicit_reducible]

instance NadathurLauer2020.Persuasion.instReprV :

Repr V

Equations

NadathurLauer2020.Persuasion.instReprV = { reprPrec := NadathurLauer2020.Persuasion.instReprV.repr }

def NadathurLauer2020.Persuasion.graph :

Causation.CausalGraph V

Equations

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

Instances For

def NadathurLauer2020.Persuasion.depth :

V → ℕ

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

Equations

Instances For

instance NadathurLauer2020.Persuasion.instIsDAGVGraph :

noncomputable def NadathurLauer2020.Persuasion.persuasionSEM :

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

Instances For

instance NadathurLauer2020.Persuasion.instIsDAGVGraphBoolPersuasionSEM :

persuasionSEM.graph.IsDAG

@[implicit_reducible]

noncomputable instance NadathurLauer2020.Persuasion.instIsDeterministicVBoolPersuasionSEM :

Causation.SEM.IsDeterministic persuasionSEM

Equations

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

def NadathurLauer2020.Persuasion.intentions :

Volitional.IntentionMap V

Equations

Instances For

theorem NadathurLauer2020.Persuasion.persuasion_makeSem :

Causation.Sufficiency.makeSem persuasionSEM Causation.Valuation.empty V.G true V.D true

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

theorem NadathurLauer2020.Persuasion.persuasion_satisfies_volitional_constraint :

Volitional.volitionalActionConstraint persuasionSEM intentions Causation.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 NadathurLauer2020.Persuasion.persuasion_make_felicitous :

Causation.Sufficiency.makeSem persuasionSEM Causation.Valuation.empty V.G true V.D true ∧ Volitional.volitionalActionConstraint persuasionSEM intentions Causation.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 NadathurLauer2020.necessity_cancellable :

Causation.Sufficiency.makeSem Bus.busSEM Bus.s_b Bus.V.Tr true Bus.V.Bs true ∧ ¬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 NadathurLauer2020.necessity_reinforceable :

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.

N&L's central observation against entailment-based taxonomy: periphrastic causatives share [Kar71]'s sufficient-only entailment cell while differing in causal mechanism (sufficiency for make vs necessity for cause). The comparison is N&L's, so it lives here; necessity_cancellable above is its kernel-checked witness.

def NadathurLauer2020.KarttunenCells.karttunenOfImplicative (b : Features.Implicative) :

Karttunen1971.KarttunenClass

Derive the KarttunenClass cell from an Implicative polarity (two-way cell: complement entailment under both polarities).

Equations

NadathurLauer2020.KarttunenCells.karttunenOfImplicative b = { isSufficient := true, isNecessary := true, polarity := b }

Instances For

def NadathurLauer2020.KarttunenCells.karttunenOfCausative :

Features.Causative → Karttunen1971.KarttunenClass

Map modern Causative to the Karttunen cell that matches the builder's entailment pattern (Karttunen's original criterion).

All positive causative builders (make, force, enable, cause) share the same Karttunen cell: sufficient-only. This is because:

Affirmative "V-ed X to VP" → VP (all require the effect occurred)
Negation "didn't V X to VP" ↛ ¬VP (effect might occur from other causes)

[NL20]'s insight: these verbs differ in causal MECHANISM (sufficiency vs necessity) despite sharing the same ENTAILMENT PATTERN. See cause_make_same_cell_different_mechanism.

Equations

NadathurLauer2020.KarttunenCells.karttunenOfCausative Features.Causative.make = { isSufficient := true, isNecessary := false, polarity := Features.Implicative.positive }
NadathurLauer2020.KarttunenCells.karttunenOfCausative Features.Causative.force = { isSufficient := true, isNecessary := false, polarity := Features.Implicative.positive }
NadathurLauer2020.KarttunenCells.karttunenOfCausative Features.Causative.enable = { isSufficient := true, isNecessary := false, polarity := Features.Implicative.positive }
NadathurLauer2020.KarttunenCells.karttunenOfCausative Features.Causative.cause = { isSufficient := true, isNecessary := false, polarity := Features.Implicative.positive }
NadathurLauer2020.KarttunenCells.karttunenOfCausative Features.Causative.prevent = { isSufficient := true, isNecessary := false, polarity := Features.Implicative.negative }

Instances For

theorem NadathurLauer2020.KarttunenCells.manage_karttunen_class :

karttunenOfImplicative Features.Implicative.positive = Karttunen1971.KarttunenClass.manage

theorem NadathurLauer2020.KarttunenCells.fail_karttunen_class :

karttunenOfImplicative Features.Implicative.negative = Karttunen1971.KarttunenClass.fail

theorem NadathurLauer2020.KarttunenCells.force_karttunen_class :

karttunenOfCausative Features.Causative.force = Karttunen1971.KarttunenClass.force

theorem NadathurLauer2020.KarttunenCells.prevent_karttunen_class :

karttunenOfCausative Features.Causative.prevent = Karttunen1971.KarttunenClass.prevent

theorem NadathurLauer2020.KarttunenCells.cause_karttunen_class :

karttunenOfCausative Features.Causative.cause = Karttunen1971.KarttunenClass.force

All positive causative builders map to KarttunenClass.force (Karttunen's sufficient-only cell).

theorem NadathurLauer2020.KarttunenCells.cause_make_same_cell_different_mechanism :

karttunenOfCausative Features.Causative.cause = karttunenOfCausative Features.Causative.make ∧ Features.Causative.cause.assertsNecessity ≠ Features.Causative.make.assertsNecessity

cause and make have the same Karttunen entailment cell (sufficient-only) despite having different causal mechanisms. This is the central insight of [NL20]: same entailment pattern ≠ same truth conditions. The difference is kernel-checked at NadathurLauer2020.necessity_cancellable (the Bus scenario: makeSem holds while causeSem fails).