Nadathur and Lauer (2020)

Nadathur and Lauer analyse periphrastic make as asserting causal sufficiency and cause as asserting causal necessity, both relative to a background situation in a structural-equation dynamics. The two relations come apart: restoring power is necessary but not sufficient for a fire whose other condition is unknown, so cause is felicitous and make is not, while Ava's training is sufficient but not necessary for Lia's taking the bus. A temporal constraint on backgrounds blocks make for the earlier of two necessary causes, and a constraint on volitional action, presupposed by make, separates it from let.

Main definitions

• NadathurLauer2020.Make, NadathurLauer2020.Cause: the lexical entries (25)
• NadathurLauer2020.TemporalLocationConstraint: the constraint (28) on backgrounds
• NadathurLauer2020.VolitionalActionConstraint: the constraint on volitional action (43)

Main results

• NadathurLauer2020.Make.solve_eq: make entails that the effect occurs (footnote 20)
• NadathurLauer2020.not_forall_causallySufficient_imp_causallyNecessary, NadathurLauer2020.not_forall_causallyNecessary_imp_causallySufficient: neither relation implies the other
• the judgments on the circuit (26), fire (31), bus (33), lighthouse (35) and dancing (40)–(44) scenarios

Implementation notes

A dynamics is a CausalModel whose exogenous variables read the context, a situation is a partial assignment, and the evaluation world of an entry is the actual world of a context. Necessity is (24) over every supersituation, CausalModel.CausallyNecessary (· ≤ ·); a supersituation settling a variable between cause and effect can then reach the effect without the cause, as in the persuasion chain, but each of the paper's necessity claims concerns a parent of the effect. Adding a fact (22a) is Function.update, which overrides a value the situation already fixes, as (43) needs when the background fixes the intention. The subtraction s ∖ (C = 1) of (25) clears the cause whether or not s fixes it, and the requirement s ⊆ w_e is a hypothesis where it is used. In (43) a background determines the intention when its strict development settles it. The paper sets preemption aside, and so does the formalization.

References

• [NL20]

Lexical entries

def NadathurLauer2020.Make {U : Type u_1} {V : Type u_2} {α : V → Type u_3} [DecidableEq V] [∀ (v : V), Nonempty (α v)] (M : CausalModel U V α) [M.IsAcyclic] (s : (v : V) → Flat (α v)) (u : U) (c : V) (x : α c) (e : V) (y : α e) : Prop

The make entry (25a) says that, with the cause removed from the background s, c = x is causally sufficient for e = y, and that the cause occurs in the actual world of the context u.

Equations

• NadathurLauer2020.Make M s u c x e y = (M.CausallySufficient (Function.update s c ⊥) c x e y ∧ M.solve ⊥ u c = x)

def NadathurLauer2020.Cause {U : Type u_1} {V : Type u_2} {α : V → Type u_3} [DecidableEq V] [∀ (v : V), Nonempty (α v)] (M : CausalModel U V α) [M.IsAcyclic] (s : (v : V) → Flat (α v)) (u : U) (c : V) (x : α c) (e : V) (y : α e) : Prop

The cause entry (25b) says that, with the cause removed from the background s, c = x is causally necessary for e = y, and that cause and effect both occur in the actual world of the context u.

Equations

• NadathurLauer2020.Cause M s u c x e y = (M.CausallyNecessary (fun (x1 x2 : (v : V) → Flat (α v)) => x1 ≤ x2) (Function.update s c ⊥) c x e y ∧ M.solve ⊥ u c = x ∧ M.solve ⊥ u e = y)

theorem NadathurLauer2020.Make.solve_eq {U : Type u_1} {V : Type u_2} {α : V → Type u_3} [DecidableEq V] [∀ (v : V), Nonempty (α v)] {M : CausalModel U V α} [M.IsAcyclic] {s : (v : V) → Flat (α v)} {u : U} {c : V} {x : α c} {e : V} {y : α e} (h : Make M s u c x e y) (hu : u ∈ M.contexts s) : M.solve ⊥ u e = y

Make entails that the effect occurs (footnote 20). The background with the cause added holds in the evaluation world, so the effect it settles occurs there.

@[instance_reducible]

instance NadathurLauer2020.instDecidableMake {U : Type u_1} {V : Type u_2} {α : V → Type u_3} [DecidableEq V] [∀ (v : V), Nonempty (α v)] {M : CausalModel U V α} [M.IsAcyclic] [Fintype U] [Inhabited U] [(v : V) → Inhabited (α v)] [(v : V) → DecidableEq (α v)] [Fintype V] [DecidableRel M.graph.Adj] (s : (v : V) → Flat (α v)) (u : U) (c : V) (x : α c) (e : V) (y : α e) : Decidable (Make M s u c x e y)

Equations

• NadathurLauer2020.instDecidableMake s u c x e y = { decide := decide (M.CausallySufficient (Function.update s c ⊥) c x e y) && decide (M.solve ⊥ u c = x), reflects_decide := ⋯ }

@[instance_reducible]

instance NadathurLauer2020.instDecidableCauseOfFintype {U : Type u_1} {V : Type u_2} {α : V → Type u_3} [DecidableEq V] [∀ (v : V), Nonempty (α v)] {M : CausalModel U V α} [M.IsAcyclic] [Fintype U] [Inhabited U] [(v : V) → Inhabited (α v)] [(v : V) → DecidableEq (α v)] [Fintype V] [DecidableRel M.graph.Adj] [(v : V) → Fintype (α v)] (s : (v : V) → Flat (α v)) (u : U) (c : V) (x : α c) (e : V) (y : α e) : Decidable (Cause M s u c x e y)

Equations

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

Constraints on background situations

def NadathurLauer2020.TemporalLocationConstraint {V : Type u_2} {α : V → Type u_3} (time : V → ℕ) (t : ℕ) (s : (v : V) → Flat (α v)) : Prop

A background s meets the temporal location constraint (28) at the evaluation time t when every fact it fixes is settled by t, the time of each variable being given by time.

Equations

• NadathurLauer2020.TemporalLocationConstraint time t s = ∀ (v : V), s v ≠ ⊥ → time v ≤ t

@[instance_reducible]

instance NadathurLauer2020.instDecidableTemporalLocationConstraintOfFintypeOfDecidableEq {V : Type u_2} {α : V → Type u_3} [Fintype V] [(v : V) → DecidableEq (α v)] (time : V → ℕ) (t : ℕ) (s : (v : V) → Flat (α v)) : Decidable (TemporalLocationConstraint time t s)

Equations

• NadathurLauer2020.instDecidableTemporalLocationConstraintOfFintypeOfDecidableEq time t s = { decide := decide (∀ a ∈ Finset.univ, (fun (x : V) => s x ≠ ⊥ → time x ≤ t) a), reflects_decide := ⋯ }

def NadathurLauer2020.VolitionalActionConstraint {U : Type u_1} {V : Type u_2} [DecidableEq V] (M : CausalModel U V fun (x : V) => Bool) [M.IsAcyclic] (s : V → Flat Bool) (c e w : V) : Prop

A make claim with cause c and effect e meets the constraint on volitional action (43) for the agent's intention w to perform e unless w = 0 is sufficient for e = 0 relative to the background s with the cause added and w is determined by s with the cause removed.

Equations

• NadathurLauer2020.VolitionalActionConstraint M s c e w = ¬(M.CausallySufficient (Function.update s c ↑true) w false e false ∧ ∃ (z : Bool), M.CausallyEntails (Function.update s c ⊥) w z)

@[instance_reducible]

instance NadathurLauer2020.instDecidableVolitionalActionConstraintOfInhabitedOfFintypeOfDecidableRelAdjGraphBool {U : Type u_1} {V : Type u_2} [DecidableEq V] (M : CausalModel U V fun (x : V) => Bool) [M.IsAcyclic] [Fintype U] [Inhabited U] [Fintype V] [DecidableRel M.graph.Adj] (s : V → Flat Bool) (c e w : V) : Decidable (VolitionalActionConstraint M s c e w)

Equations

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

The circuit

inductive NadathurLauer2020.Circuit.V : Type

The circuit (20) has two switches S₁ and S₂, each up or down, and a light L.

• S₁ : V
• S₂ : V
• L : V

@[instance_reducible]

instance NadathurLauer2020.Circuit.instDecidableEqV : DecidableEq V

Equations

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

@[instance_reducible]

instance NadathurLauer2020.Circuit.instFintypeV : Fintype V

Equations

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

def NadathurLauer2020.Circuit.instReprV.repr : V → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance NadathurLauer2020.Circuit.instReprV : Repr V

Equations

• NadathurLauer2020.Circuit.instReprV = { reprPrec := NadathurLauer2020.Circuit.instReprV.repr }

def NadathurLauer2020.Circuit.edges : Finset (V × V)

The light reads both switches.

Equations

• NadathurLauer2020.Circuit.edges = {(NadathurLauer2020.Circuit.V.S₁, NadathurLauer2020.Circuit.V.L), (NadathurLauer2020.Circuit.V.S₂, NadathurLauer2020.Circuit.V.L)}

structure NadathurLauer2020.Circuit.Context : Type

The context settles the two switches.

• S₁ : Bool
• S₂ : Bool

def NadathurLauer2020.Circuit.instDecidableEqContext.decEq (x✝ x✝¹ : Context) : Decidable (x✝ = x✝¹)

Equations

• NadathurLauer2020.Circuit.instDecidableEqContext.decEq { S₁ := a, S₂ := a_1 } { S₁ := b, S₂ := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

@[instance_reducible]

instance NadathurLauer2020.Circuit.instDecidableEqContext : DecidableEq Context

Equations

• NadathurLauer2020.Circuit.instDecidableEqContext = NadathurLauer2020.Circuit.instDecidableEqContext.decEq

@[instance_reducible]

instance NadathurLauer2020.Circuit.instFintypeContext : Fintype Context

Equations

• NadathurLauer2020.Circuit.instFintypeContext = Fintype.ofEquiv ((_ : Bool) × Bool) NadathurLauer2020.Circuit.Context.proxyTypeEquiv

@[instance_reducible]

instance NadathurLauer2020.Circuit.instInhabitedContext : Inhabited Context

Equations

• NadathurLauer2020.Circuit.instInhabitedContext = { default := NadathurLauer2020.Circuit.instInhabitedContext.default }

@[instance_reducible]

instance NadathurLauer2020.Circuit.instReprContext : Repr Context

Equations

• NadathurLauer2020.Circuit.instReprContext = { reprPrec := NadathurLauer2020.Circuit.instReprContext.repr }

def NadathurLauer2020.Circuit.instReprContext.repr : Context → ℕ → Std.Format

Equations

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

def NadathurLauer2020.Circuit.circuit : CausalModel Context V fun (x : V) => Bool

In the circuit dynamics (Figure 1) the light is on exactly when the switches agree.

Equations

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

@[instance_reducible]

instance NadathurLauer2020.Circuit.instDecidableRelVAdjGraphContextBoolCircuit : DecidableRel circuit.graph.Adj

Equations

• NadathurLauer2020.Circuit.instDecidableRelVAdjGraphContextBoolCircuit w v = NadathurLauer2020.Circuit.instDecidableRelVAdjGraphContextBoolCircuit._aux_1 w v

instance NadathurLauer2020.Circuit.instIsAcyclicContextVBoolCircuit : circuit.IsAcyclic

def NadathurLauer2020.Circuit.actual : Context

In the situation (20b) switch 1 is down and switch 2 is up.

Equations

• NadathurLauer2020.Circuit.actual = { S₁ := false, S₂ := true }

theorem NadathurLauer2020.Circuit.make : Make circuit (Function.update ⊥ V.S₁ ↑false) actual V.S₂ true V.L false

(26a) Turning the second switch on makes the light go off is true when switch 1 is known to be down.

theorem NadathurLauer2020.Circuit.cause : Cause circuit (Function.update ⊥ V.S₁ ↑false) actual V.S₂ true V.L false

(26b) Turning the second switch on causes the light to go off is true when switch 1 is known to be down.

The fire scenario

inductive NadathurLauer2020.Fire.V : Type

The fire scenario (30) has the power restored P, the drought D, the grass inflammable G, the line down L, and the field on fire F.

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

@[instance_reducible]

instance NadathurLauer2020.Fire.instDecidableEqV : DecidableEq V

Equations

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

@[instance_reducible]

instance NadathurLauer2020.Fire.instFintypeV : Fintype V

Equations

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

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

Equations

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

@[instance_reducible]

instance NadathurLauer2020.Fire.instReprV : Repr V

Equations

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

def NadathurLauer2020.Fire.edges : Finset (V × V)

Inflammability reads drought, and fire reads inflammability, power, and the line.

Equations

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

structure NadathurLauer2020.Fire.Context : Type

The context settles power, drought, and the line.

• P : Bool
• D : Bool
• L : Bool

@[instance_reducible]

instance NadathurLauer2020.Fire.instDecidableEqContext : DecidableEq Context

Equations

• NadathurLauer2020.Fire.instDecidableEqContext = NadathurLauer2020.Fire.instDecidableEqContext.decEq

def NadathurLauer2020.Fire.instDecidableEqContext.decEq (x✝ x✝¹ : Context) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance NadathurLauer2020.Fire.instFintypeContext : Fintype Context

Equations

• NadathurLauer2020.Fire.instFintypeContext = Fintype.ofEquiv ((_ : Bool) × (_ : Bool) × Bool) NadathurLauer2020.Fire.Context.proxyTypeEquiv

@[instance_reducible]

instance NadathurLauer2020.Fire.instInhabitedContext : Inhabited Context

Equations

• NadathurLauer2020.Fire.instInhabitedContext = { default := NadathurLauer2020.Fire.instInhabitedContext.default }

@[instance_reducible]

instance NadathurLauer2020.Fire.instReprContext : Repr Context

Equations

• NadathurLauer2020.Fire.instReprContext = { reprPrec := NadathurLauer2020.Fire.instReprContext.repr }

def NadathurLauer2020.Fire.instReprContext.repr : Context → ℕ → Std.Format

Equations

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

def NadathurLauer2020.Fire.fireModel : CausalModel Context V fun (x : V) => Bool

In the fire dynamics (Figure 2) the grass is inflammable in a drought, and the field burns when the grass is inflammable, the power is on and the line is down.

Equations

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

@[instance_reducible]

instance NadathurLauer2020.Fire.instDecidableRelVAdjGraphContextBoolFireModel : DecidableRel fireModel.graph.Adj

Equations

• NadathurLauer2020.Fire.instDecidableRelVAdjGraphContextBoolFireModel w v = NadathurLauer2020.Fire.instDecidableRelVAdjGraphContextBoolFireModel._aux_1 w v

instance NadathurLauer2020.Fire.instIsAcyclicContextVBoolFireModel : fireModel.IsAcyclic

def NadathurLauer2020.Fire.actual : Context

In the scenario the power was restored in a drought, and the line was down.

Equations

• NadathurLauer2020.Fire.actual = { P := true, D := true, L := true }

def NadathurLauer2020.Fire.s_b : V → Flat Bool

The background s_b fixes the drought and the inflammable grass and leaves the line open.

Equations

• NadathurLauer2020.Fire.s_b = Function.update (Function.update ⊥ NadathurLauer2020.Fire.V.G ↑true) NadathurLauer2020.Fire.V.D ↑true

def NadathurLauer2020.Fire.s_b1 : V → Flat Bool

The background s_b1 also fixes the line as down.

Equations

• NadathurLauer2020.Fire.s_b1 = Function.update NadathurLauer2020.Fire.s_b NadathurLauer2020.Fire.V.L ↑true

theorem NadathurLauer2020.Fire.power_of_fire {s : V → Flat Bool} (hs : s V.F = ⊥) (h : fireModel.CausallyEntails s V.F true) : fireModel.CausallyEntails s V.P true

Every route to the fire passes through the power: a situation leaving the fire open that settles it settles the power as restored.

theorem NadathurLauer2020.Fire.not_make : ¬Make fireModel s_b actual V.P true V.F true

(31a) #Restoring power made the field catch fire is infelicitous, since with the line open the power is not sufficient for the fire.

theorem NadathurLauer2020.Fire.cause : Cause fireModel s_b actual V.P true V.F true

(31b) Restoring power caused the field to catch fire is felicitous. The power is necessary for the fire, the line being settled down in the supersituation that brings the fire about.

theorem NadathurLauer2020.Fire.make_of_line_down : Make fireModel s_b1 actual V.P true V.F true

With the line known to be down, restoring power made the field catch fire is felicitous.

theorem NadathurLauer2020.Fire.cause_of_line_down : Cause fireModel s_b1 actual V.P true V.F true

With the line known to be down, restoring power caused the field to catch fire stays felicitous.

The bus scenario

inductive NadathurLauer2020.Bus.V : Type

The bus scenario (32) has Ava visiting Vis, Ava training Tr, rain forecast Rn, the bike gone Bk, and Lia taking the bus Bs.

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

@[instance_reducible]

instance NadathurLauer2020.Bus.instDecidableEqV : DecidableEq V

Equations

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

@[instance_reducible]

instance NadathurLauer2020.Bus.instFintypeV : Fintype V

Equations

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

@[instance_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.

def NadathurLauer2020.Bus.edges : Finset (V × V)

The bike's absence reads the visit and the training; the bus reads the rain and the bike.

Equations

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

structure NadathurLauer2020.Bus.Context : Type

The context settles Ava's visit, her training, and the forecast.

• Vis : Bool
• Tr : Bool
• Rn : Bool

@[instance_reducible]

instance NadathurLauer2020.Bus.instDecidableEqContext : DecidableEq Context

Equations

• NadathurLauer2020.Bus.instDecidableEqContext = NadathurLauer2020.Bus.instDecidableEqContext.decEq

def NadathurLauer2020.Bus.instDecidableEqContext.decEq (x✝ x✝¹ : Context) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance NadathurLauer2020.Bus.instFintypeContext : Fintype Context

Equations

• NadathurLauer2020.Bus.instFintypeContext = Fintype.ofEquiv ((_ : Bool) × (_ : Bool) × Bool) NadathurLauer2020.Bus.Context.proxyTypeEquiv

@[instance_reducible]

instance NadathurLauer2020.Bus.instInhabitedContext : Inhabited Context

Equations

• NadathurLauer2020.Bus.instInhabitedContext = { default := NadathurLauer2020.Bus.instInhabitedContext.default }

def NadathurLauer2020.Bus.instReprContext.repr : Context → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance NadathurLauer2020.Bus.instReprContext : Repr Context

Equations

• NadathurLauer2020.Bus.instReprContext = { reprPrec := NadathurLauer2020.Bus.instReprContext.repr }

def NadathurLauer2020.Bus.busModel : CausalModel Context V fun (x : V) => Bool

In the bus dynamics (Figure 3) the bike is gone when Ava visits and trains, and Lia takes the bus when rain is forecast or the bike is gone.

Equations

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

@[instance_reducible]

instance NadathurLauer2020.Bus.instDecidableRelVAdjGraphContextBoolBusModel : DecidableRel busModel.graph.Adj

Equations

• NadathurLauer2020.Bus.instDecidableRelVAdjGraphContextBoolBusModel w v = NadathurLauer2020.Bus.instDecidableRelVAdjGraphContextBoolBusModel._aux_1 w v

instance NadathurLauer2020.Bus.instIsAcyclicContextVBoolBusModel : busModel.IsAcyclic

def NadathurLauer2020.Bus.actual : Context

In the scenario Ava is visiting and training, and rain is forecast.

Equations

• NadathurLauer2020.Bus.actual = { Vis := true, Tr := true, Rn := true }

def NadathurLauer2020.Bus.s_b : V → Flat Bool

The background s_b fixes the visit and the forecast.

Equations

• NadathurLauer2020.Bus.s_b = Function.update (Function.update ⊥ NadathurLauer2020.Bus.V.Rn ↑true) NadathurLauer2020.Bus.V.Vis ↑true

theorem NadathurLauer2020.Bus.make : Make busModel s_b actual V.Tr true V.Bs true

(33a) Ava's training made Lia take the bus to work is felicitous.

theorem NadathurLauer2020.Bus.not_cause : ¬Cause busModel s_b actual V.Tr true V.Bs true

(33b) #Ava's training caused Lia to take the bus to work is infelicitous. The training is not necessary, since the supersituation in which the bike stays takes Lia to the bus by the rain alone.

The lighthouse scenario

inductive NadathurLauer2020.Lighthouse.V : Type

The lighthouse scenario (34) has the earthquake Q, the storms S, and the collapse L.

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

@[instance_reducible]

instance NadathurLauer2020.Lighthouse.instDecidableEqV : DecidableEq V

Equations

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

@[instance_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.

@[instance_reducible]

instance NadathurLauer2020.Lighthouse.instReprV : Repr V

Equations

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

def NadathurLauer2020.Lighthouse.edges : Finset (V × V)

The collapse reads the earthquake and the storms.

Equations

• NadathurLauer2020.Lighthouse.edges = {(NadathurLauer2020.Lighthouse.V.Q, NadathurLauer2020.Lighthouse.V.L), (NadathurLauer2020.Lighthouse.V.S, NadathurLauer2020.Lighthouse.V.L)}

structure NadathurLauer2020.Lighthouse.Context : Type

The context settles the earthquake and the storms.

• Q : Bool
• S : Bool

def NadathurLauer2020.Lighthouse.instDecidableEqContext.decEq (x✝ x✝¹ : Context) : Decidable (x✝ = x✝¹)

Equations

• NadathurLauer2020.Lighthouse.instDecidableEqContext.decEq { Q := a, S := a_1 } { Q := b, S := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

@[instance_reducible]

instance NadathurLauer2020.Lighthouse.instDecidableEqContext : DecidableEq Context

Equations

• NadathurLauer2020.Lighthouse.instDecidableEqContext = NadathurLauer2020.Lighthouse.instDecidableEqContext.decEq

@[instance_reducible]

instance NadathurLauer2020.Lighthouse.instFintypeContext : Fintype Context

Equations

• NadathurLauer2020.Lighthouse.instFintypeContext = Fintype.ofEquiv ((_ : Bool) × Bool) NadathurLauer2020.Lighthouse.Context.proxyTypeEquiv

@[instance_reducible]

instance NadathurLauer2020.Lighthouse.instInhabitedContext : Inhabited Context

Equations

• NadathurLauer2020.Lighthouse.instInhabitedContext = { default := NadathurLauer2020.Lighthouse.instInhabitedContext.default }

def NadathurLauer2020.Lighthouse.instReprContext.repr : Context → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance NadathurLauer2020.Lighthouse.instReprContext : Repr Context

Equations

• NadathurLauer2020.Lighthouse.instReprContext = { reprPrec := NadathurLauer2020.Lighthouse.instReprContext.repr }

def NadathurLauer2020.Lighthouse.lighthouseModel : CausalModel Context V fun (x : V) => Bool

In the lighthouse dynamics (Figure 4) the tower collapses when both happen.

Equations

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

@[instance_reducible]

instance NadathurLauer2020.Lighthouse.instDecidableRelVAdjGraphContextBoolLighthouseModel : DecidableRel lighthouseModel.graph.Adj

Equations

• NadathurLauer2020.Lighthouse.instDecidableRelVAdjGraphContextBoolLighthouseModel w v = NadathurLauer2020.Lighthouse.instDecidableRelVAdjGraphContextBoolLighthouseModel._aux_1 w v

instance NadathurLauer2020.Lighthouse.instIsAcyclicContextVBoolLighthouseModel : lighthouseModel.IsAcyclic

def NadathurLauer2020.Lighthouse.actual : Context

In the scenario both the earthquake and the storms happened.

Equations

• NadathurLauer2020.Lighthouse.actual = { Q := true, S := true }

def NadathurLauer2020.Lighthouse.time : V → ℕ

The earthquake precedes the storms, which precede the collapse.

Equations

• NadathurLauer2020.Lighthouse.time NadathurLauer2020.Lighthouse.V.Q = 0
• NadathurLauer2020.Lighthouse.time NadathurLauer2020.Lighthouse.V.S = 1
• NadathurLauer2020.Lighthouse.time NadathurLauer2020.Lighthouse.V.L = 2

theorem NadathurLauer2020.Lighthouse.earthquake_of_collapse {s : V → Flat Bool} (hs : s V.L = ⊥) (h : lighthouseModel.CausallyEntails s V.L true) : lighthouseModel.CausallyEntails s V.Q true

A situation leaving the collapse open that settles it settles the earthquake.

theorem NadathurLauer2020.Lighthouse.storms_of_collapse {s : V → Flat Bool} (hs : s V.L = ⊥) (h : lighthouseModel.CausallyEntails s V.L true) : lighthouseModel.CausallyEntails s V.S true

A situation leaving the collapse open that settles it settles the storms.

theorem NadathurLauer2020.Lighthouse.cause_earthquake : Cause lighthouseModel ⊥ actual V.Q true V.L true

(35a) The earthquake caused the tower to collapse is felicitous relative to the empty situation.

theorem NadathurLauer2020.Lighthouse.cause_storms : Cause lighthouseModel ⊥ actual V.S true V.L true

(35b) The storms caused the tower to collapse is felicitous relative to the empty situation.

theorem NadathurLauer2020.Lighthouse.make_storms : TemporalLocationConstraint time (time V.S) (Function.update ⊥ V.Q ↑true) ∧ Make lighthouseModel (Function.update ⊥ V.Q ↑true) actual V.S true V.L true

(35d) The storms made the tower collapse is felicitous relative to the earthquake, a background that meets the temporal location constraint at the time of the storms.

theorem NadathurLauer2020.Lighthouse.not_make_earthquake (s : V → Flat Bool) (hs : TemporalLocationConstraint time (time V.Q) s) : ¬Make lighthouseModel s actual V.Q true V.L true

(35c) #The earthquake made the tower collapse is infelicitous. No background meeting the temporal location constraint at the time of the earthquake makes it sufficient, since every such background leaves the storms open.

Neither relation implies the other

theorem NadathurLauer2020.not_forall_causallySufficient_imp_causallyNecessary : ¬∀ (U V : Type) [inst : DecidableEq V] (M : CausalModel U V fun (x : V) => Bool) [inst_1 : M.IsAcyclic] (s : V → Flat Bool) (c : V) (x : Bool) (e : V) (y : Bool), M.CausallySufficient s c x e y → M.CausallyNecessary (fun (x1 x2 : V → Flat Bool) => x1 ≤ x2) s c x e y

Causal sufficiency does not imply causal necessity, by the bus scenario.

theorem NadathurLauer2020.not_forall_causallyNecessary_imp_causallySufficient : ¬∀ (U V : Type) [inst : DecidableEq V] (M : CausalModel U V fun (x : V) => Bool) [inst_1 : M.IsAcyclic] (s : V → Flat Bool) (c : V) (x : Bool) (e : V) (y : Bool), M.CausallyNecessary (fun (x1 x2 : V → Flat Bool) => x1 ≤ x2) s c x e y → M.CausallySufficient s c x e y

Causal necessity does not imply causal sufficiency, by the fire scenario.

The dancing scenarios

inductive NadathurLauer2020.Dancing.V : Type

The dancing scenarios have the children's wanting to dance WD, Gurung's action G, and the children dancing D.

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

@[instance_reducible]

instance NadathurLauer2020.Dancing.instDecidableEqV : DecidableEq V

Equations

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

@[instance_reducible]

instance NadathurLauer2020.Dancing.instFintypeV : Fintype V

Equations

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

@[instance_reducible]

instance NadathurLauer2020.Dancing.instReprV : Repr V

Equations

• NadathurLauer2020.Dancing.instReprV = { reprPrec := NadathurLauer2020.Dancing.instReprV.repr }

def NadathurLauer2020.Dancing.instReprV.repr : V → ℕ → Std.Format

Equations

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

def NadathurLauer2020.Dancing.edges : Finset (V × V)

In the permission and command scenarios dancing reads the desire and Gurung's action.

Equations

• NadathurLauer2020.Dancing.edges = {(NadathurLauer2020.Dancing.V.WD, NadathurLauer2020.Dancing.V.D), (NadathurLauer2020.Dancing.V.G, NadathurLauer2020.Dancing.V.D)}

structure NadathurLauer2020.Dancing.Context : Type

The context of the permission and command scenarios settles the desire and the action.

• WD : Bool
• G : Bool

def NadathurLauer2020.Dancing.instDecidableEqContext.decEq (x✝ x✝¹ : Context) : Decidable (x✝ = x✝¹)

Equations

• NadathurLauer2020.Dancing.instDecidableEqContext.decEq { WD := a, G := a_1 } { WD := b, G := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

@[instance_reducible]

instance NadathurLauer2020.Dancing.instDecidableEqContext : DecidableEq Context

Equations

• NadathurLauer2020.Dancing.instDecidableEqContext = NadathurLauer2020.Dancing.instDecidableEqContext.decEq

@[instance_reducible]

instance NadathurLauer2020.Dancing.instFintypeContext : Fintype Context

Equations

• NadathurLauer2020.Dancing.instFintypeContext = Fintype.ofEquiv ((_ : Bool) × Bool) NadathurLauer2020.Dancing.Context.proxyTypeEquiv

@[instance_reducible]

instance NadathurLauer2020.Dancing.instInhabitedContext : Inhabited Context

Equations

• NadathurLauer2020.Dancing.instInhabitedContext = { default := NadathurLauer2020.Dancing.instInhabitedContext.default }

@[instance_reducible]

instance NadathurLauer2020.Dancing.instReprContext : Repr Context

Equations

• NadathurLauer2020.Dancing.instReprContext = { reprPrec := NadathurLauer2020.Dancing.instReprContext.repr }

def NadathurLauer2020.Dancing.instReprContext.repr : Context → ℕ → Std.Format

Equations

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

def NadathurLauer2020.Dancing.permission : CausalModel Context V fun (x : V) => Bool

In the permission dynamics (Figure 5) the children dance when they want to and Gurung permits it.

Equations

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

@[instance_reducible]

instance NadathurLauer2020.Dancing.instDecidableRelVAdjGraphContextBoolPermission : DecidableRel permission.graph.Adj

Equations

• NadathurLauer2020.Dancing.instDecidableRelVAdjGraphContextBoolPermission w v = NadathurLauer2020.Dancing.instDecidableRelVAdjGraphContextBoolPermission._aux_1 w v

instance NadathurLauer2020.Dancing.instIsAcyclicContextVBoolPermission : permission.IsAcyclic

def NadathurLauer2020.Dancing.command : CausalModel Context V fun (x : V) => Bool

In the command dynamics (Figure 6) the children dance when they want to or Gurung commands it.

Equations

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

@[instance_reducible]

instance NadathurLauer2020.Dancing.instDecidableRelVAdjGraphContextBoolCommand : DecidableRel command.graph.Adj

Equations

• NadathurLauer2020.Dancing.instDecidableRelVAdjGraphContextBoolCommand w v = NadathurLauer2020.Dancing.instDecidableRelVAdjGraphContextBoolCommand._aux_1 w v

instance NadathurLauer2020.Dancing.instIsAcyclicContextVBoolCommand : command.IsAcyclic

def NadathurLauer2020.Dancing.chain : Finset (V × V)

In the persuasion scenario the desire reads Gurung's song, and dancing reads the desire.

Equations

• NadathurLauer2020.Dancing.chain = {(NadathurLauer2020.Dancing.V.G, NadathurLauer2020.Dancing.V.WD), (NadathurLauer2020.Dancing.V.WD, NadathurLauer2020.Dancing.V.D)}

structure NadathurLauer2020.Dancing.PersuasionContext : Type

The context of the persuasion scenario settles whether Gurung plays the song.

• G : Bool

def NadathurLauer2020.Dancing.instDecidableEqPersuasionContext.decEq (x✝ x✝¹ : PersuasionContext) : Decidable (x✝ = x✝¹)

Equations

• NadathurLauer2020.Dancing.instDecidableEqPersuasionContext.decEq { G := a } { G := b } = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance NadathurLauer2020.Dancing.instDecidableEqPersuasionContext : DecidableEq PersuasionContext

Equations

• NadathurLauer2020.Dancing.instDecidableEqPersuasionContext = NadathurLauer2020.Dancing.instDecidableEqPersuasionContext.decEq

@[instance_reducible]

instance NadathurLauer2020.Dancing.instFintypePersuasionContext : Fintype PersuasionContext

Equations

• NadathurLauer2020.Dancing.instFintypePersuasionContext = Fintype.ofEquiv Bool NadathurLauer2020.Dancing.PersuasionContext.proxyTypeEquiv

@[instance_reducible]

instance NadathurLauer2020.Dancing.instInhabitedPersuasionContext : Inhabited PersuasionContext

Equations

• NadathurLauer2020.Dancing.instInhabitedPersuasionContext = { default := NadathurLauer2020.Dancing.instInhabitedPersuasionContext.default }

def NadathurLauer2020.Dancing.instReprPersuasionContext.repr : PersuasionContext → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance NadathurLauer2020.Dancing.instReprPersuasionContext : Repr PersuasionContext

Equations

• NadathurLauer2020.Dancing.instReprPersuasionContext = { reprPrec := NadathurLauer2020.Dancing.instReprPersuasionContext.repr }

def NadathurLauer2020.Dancing.persuasion : CausalModel PersuasionContext V fun (x : V) => Bool

In the persuasion dynamics (Figure 7) the children want to dance when Gurung plays their song, and dance when they want to.

Equations

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

@[instance_reducible]

instance NadathurLauer2020.Dancing.instDecidableRelVAdjGraphPersuasionContextBoolPersuasion : DecidableRel persuasion.graph.Adj

Equations

• NadathurLauer2020.Dancing.instDecidableRelVAdjGraphPersuasionContextBoolPersuasion w v = NadathurLauer2020.Dancing.instDecidableRelVAdjGraphPersuasionContextBoolPersuasion._aux_1 w v

instance NadathurLauer2020.Dancing.instIsAcyclicPersuasionContextVBoolPersuasion : persuasion.IsAcyclic

theorem NadathurLauer2020.Dancing.make_permission : Make permission (Function.update ⊥ V.WD ↑true) { WD := true, G := true } V.G true V.D true

In the permission scenario (40) the eager children dance once Gurung permits it, and his permission is sufficient for the dancing.

theorem NadathurLauer2020.Dancing.not_volitionalActionConstraint_permission : ¬VolitionalActionConstraint permission (Function.update ⊥ V.WD ↑true) V.G V.D V.WD

(40a) ??Gurung made the children dance in the permission scenario. The children's desire is fixed and suffices to stop the dancing, so the constraint on volitional action fails; this is the context in which let is felicitous (46).

theorem NadathurLauer2020.Dancing.make_command (b : Bool) : Make command (Function.update ⊥ V.WD ↑b) { WD := b, G := true } V.G true V.D true

In the command scenarios, with the children reluctant (41) or eager (42), Gurung's command is sufficient for the dancing.

theorem NadathurLauer2020.Dancing.volitionalActionConstraint_command (b : Bool) : VolitionalActionConstraint command (Function.update ⊥ V.WD ↑b) V.G V.D V.WD

(41a), (42a) Gurung made the children dance in the command scenarios. Whatever the children want, their desire cannot stop the dancing once Gurung commands it, so the constraint on volitional action holds and let is out (46).

theorem NadathurLauer2020.Dancing.make_persuasion : Make persuasion ⊥ { G := true } V.G true V.D true

In the persuasion scenario (44) Gurung's song is sufficient for the dancing.

theorem NadathurLauer2020.Dancing.volitionalActionConstraint_persuasion : VolitionalActionConstraint persuasion ⊥ V.G V.D V.WD

(44a) Gurung made the children dance (by playing their favourite song). The children's desire, though sufficient to stop the dancing, is settled only by the song, so the constraint on volitional action holds and let is out (46).