Glass (2023)

Glass explains why cause favours undesirable complements. Over a deterministic causal model in the sense of Halpern and Pearl, a value is locally sufficient for a downstream value when some setting of the other variables guarantees it, as in Mackie's sufficient sets, and globally sufficient when every setting does; necessity is the mirror image (GloballySufficient, LocallySufficient, GloballyNecessary, LocallyNecessary). C causes E, asserted on a state of knowledge, requires the effect to develop in every settlement of what is unknown (Cause), so knowing the cause alone it is assertable exactly when the cause is globally sufficient (cause_update_bot_iff), the asymmetry of the paper's Table 2. The Anna Karenina Principle gives desired outcomes conjunctive models and undesired ones disjunctive models, so C causes E holds in more states of knowledge when E is bad. Glass's cause asserts local sufficiency where Nadathur and Lauer's asserts necessity, and the two diverge on their bus scenario (glass_nl_diverge_on_bus).

Implementation notes

• A background is a setting of some variables, imposed on a causal model in a context; "no matter what happens to any other variable" quantifies over every context and every setting leaving the effect open.
• The lightbulb of the paper's figures, on exactly when both switches are, is the conjunctive model for the light being on and the disjunctive model for its being off.
• The derivation of the Anna Karenina Principle from strategic model construction, the experiment supporting it (wanted outcomes drew "you had to do everything right" far more often than unwanted ones) and the corpus skew that motivates the paper stay in prose.

References

• [Gla23b]
• [NL20]
• [HP05]
• [Mac65]

Local and global necessity and sufficiency

def Glass2023.GloballySufficient {U : Type u_1} {V : Type u_2} (M : CausalModel U V fun (x : V) => Bool) [M.IsAcyclic] (C : V) (c : Bool) (E : V) (e : Bool) : Prop

C = c is globally sufficient for E = e when, in every context and under every background leaving E open in which C = c, E = e.

Equations

• Glass2023.GloballySufficient M C c E e = ∀ (u : U) (I : V → Flat Bool), I E = ⊥ → I C = ↑c → M.solve I u E = e

def Glass2023.LocallySufficient {U : Type u_1} {V : Type u_2} (M : CausalModel U V fun (x : V) => Bool) [M.IsAcyclic] (C : V) (c : Bool) (E : V) (e : Bool) : Prop

C = c is locally sufficient for E = e when, in some context and under some background leaving E open in which C = c, E = e.

Equations

• Glass2023.LocallySufficient M C c E e = ∃ (u : U) (I : V → Flat Bool), I E = ⊥ ∧ I C = ↑c ∧ M.solve I u E = e

def Glass2023.GloballyNecessary {U : Type u_1} {V : Type u_2} (M : CausalModel U V fun (x : V) => Bool) [M.IsAcyclic] (C : V) (c : Bool) (E : V) (e : Bool) : Prop

C = c is globally necessary for E = e when, without it, E = e fails in every context and under every background leaving E open.

Equations

• Glass2023.GloballyNecessary M C c E e = ∀ (u : U) (I : V → Flat Bool), I E = ⊥ → I C = ↑!c → M.solve I u E = !e

def Glass2023.LocallyNecessary {U : Type u_1} {V : Type u_2} (M : CausalModel U V fun (x : V) => Bool) [M.IsAcyclic] (C : V) (c : Bool) (E : V) (e : Bool) : Prop

C = c is locally necessary for E = e when, without it, E = e fails in some context and under some background leaving E open.

Equations

• Glass2023.LocallyNecessary M C c E e = ∃ (u : U) (I : V → Flat Bool), I E = ⊥ ∧ I C = ↑!c ∧ M.solve I u E = !e

def Glass2023.Cause {U : Type u_1} {V : Type u_2} (M : CausalModel U V fun (x : V) => Bool) [M.IsAcyclic] (k : V → Flat Bool) (C : V) (c : Bool) (E : V) (e : Bool) : Prop

C causes E is assertable on the state of knowledge k when the cause is known and the effect holds in every context under every background that keeps what is known and leaves it open.

Equations

• Glass2023.Cause M k C c E e = (k C = ↑c ∧ ∀ (u : U) (I : V → Flat Bool), k ≤ I → I E = ⊥ → M.solve I u E = e)

theorem Glass2023.globallyNecessary_iff {U : Type u_1} {V : Type u_2} {M : CausalModel U V fun (x : V) => Bool} [M.IsAcyclic] {C E : V} {c e : Bool} : GloballyNecessary M C c E e ↔ GloballySufficient M C (!c) E !e

Necessity is the mirror image of sufficiency: the absence of a necessary cause suffices for the absence of the effect.

theorem Glass2023.locallyNecessary_iff {U : Type u_1} {V : Type u_2} {M : CausalModel U V fun (x : V) => Bool} [M.IsAcyclic] {C E : V} {c e : Bool} : LocallyNecessary M C c E e ↔ LocallySufficient M C (!c) E !e

theorem Glass2023.Cause.of_globallySufficient {U : Type u_1} {V : Type u_2} {M : CausalModel U V fun (x : V) => Bool} [M.IsAcyclic] {C E : V} {c e : Bool} {k : V → Flat Bool} (h : GloballySufficient M C c E e) (hk : k C = ↑c) : Cause M k C c E e

A globally sufficient cause licenses cause whatever else is known or unknown.

theorem Glass2023.LocallySufficient.of_globally {U : Type u_1} {V : Type u_2} {M : CausalModel U V fun (x : V) => Bool} [M.IsAcyclic] {C E : V} {c e : Bool} [DecidableEq V] [Inhabited U] (hCE : C ≠ E) (h : GloballySufficient M C c E e) : LocallySufficient M C c E e

Global sufficiency entails local sufficiency (22a).

theorem Glass2023.LocallyNecessary.of_globally {U : Type u_1} {V : Type u_2} {M : CausalModel U V fun (x : V) => Bool} [M.IsAcyclic] {C E : V} {c e : Bool} [DecidableEq V] [Inhabited U] (hCE : C ≠ E) (h : GloballyNecessary M C c E e) : LocallyNecessary M C c E e

Global necessity entails local necessity (21a).

theorem Glass2023.cause_update_bot_iff {U : Type u_1} {V : Type u_2} {M : CausalModel U V fun (x : V) => Bool} [M.IsAcyclic] {C E : V} {c e : Bool} [DecidableEq V] : Cause M (Function.update ⊥ C ↑c) C c E e ↔ GloballySufficient M C c E e

Knowing the cause alone, C causes E is assertable exactly when the cause is globally sufficient: the asymmetry of the paper's Table 2.

The lightbulb (Figure 2, Tables 1 and 2)

Two switches and a light that is on exactly when both are: each switch being on is necessary but insufficient for the light to be on, and each being off suffices for it to be off.

inductive Glass2023.Light.V : Type

The two switches and the light.

• S1 : V
• S2 : V
• L : V

@[instance_reducible]

instance Glass2023.Light.instDecidableEqV : DecidableEq V

Equations

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

@[instance_reducible]

instance Glass2023.Light.instFintypeV : Fintype V

Equations

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

def Glass2023.Light.instReprV.repr : V → ℕ → Std.Format

Equations

• Glass2023.Light.instReprV.repr Glass2023.Light.V.S1 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Glass2023.Light.V.S1")).group prec✝
• Glass2023.Light.instReprV.repr Glass2023.Light.V.S2 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Glass2023.Light.V.S2")).group prec✝
• Glass2023.Light.instReprV.repr Glass2023.Light.V.L prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Glass2023.Light.V.L")).group prec✝

@[instance_reducible]

instance Glass2023.Light.instReprV : Repr V

Equations

• Glass2023.Light.instReprV = { reprPrec := Glass2023.Light.instReprV.repr }

def Glass2023.Light.edges : Finset (V × V)

The light reads the two switches.

Equations

• Glass2023.Light.edges = {(Glass2023.Light.V.S1, Glass2023.Light.V.L), (Glass2023.Light.V.S2, Glass2023.Light.V.L)}

structure Glass2023.Light.Context : Type

The context settles the two switches.

• S1 : Bool
• S2 : Bool

def Glass2023.Light.instDecidableEqContext.decEq (x✝ x✝¹ : Context) : Decidable (x✝ = x✝¹)

Equations

• Glass2023.Light.instDecidableEqContext.decEq { S1 := a, S2 := a_1 } { S1 := b, S2 := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

@[instance_reducible]

instance Glass2023.Light.instDecidableEqContext : DecidableEq Context

Equations

• Glass2023.Light.instDecidableEqContext = Glass2023.Light.instDecidableEqContext.decEq

@[instance_reducible]

instance Glass2023.Light.instFintypeContext : Fintype Context

Equations

• Glass2023.Light.instFintypeContext = Fintype.ofEquiv ((_ : Bool) × Bool) Glass2023.Light.Context.proxyTypeEquiv

@[instance_reducible]

instance Glass2023.Light.instInhabitedContext : Inhabited Context

Equations

• Glass2023.Light.instInhabitedContext = { default := Glass2023.Light.instInhabitedContext.default }

def Glass2023.Light.instReprContext.repr : Context → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Glass2023.Light.instReprContext : Repr Context

Equations

• Glass2023.Light.instReprContext = { reprPrec := Glass2023.Light.instReprContext.repr }

def Glass2023.Light.light : CausalModel Context V fun (x : V) => Bool

The light is on exactly when both switches are.

Equations

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

@[instance_reducible]

instance Glass2023.Light.instDecidableRelVAdjGraphContextBoolLight : DecidableRel light.graph.Adj

Equations

• Glass2023.Light.instDecidableRelVAdjGraphContextBoolLight w v = Glass2023.Light.instDecidableRelVAdjGraphContextBoolLight._aux_1 w v

instance Glass2023.Light.instIsAcyclicContextVBoolLight : light.IsAcyclic

theorem Glass2023.Light.solve_L {I : V → Flat Bool} (h : I V.L = ⊥) (u : Context) : light.solve I u V.L = (light.solve I u V.S1 && light.solve I u V.S2)

The light's equation, under a background that leaves it open.

theorem Glass2023.Light.s1_off_globallySufficient : GloballySufficient light V.S1 false V.L false

Switch 1 being off is globally sufficient for the light to be off.

theorem Glass2023.Light.s1_on_globallyNecessary : GloballyNecessary light V.S1 true V.L true

Switch 1 being on is globally necessary for the light to be on.

theorem Glass2023.Light.s1_on_not_globallySufficient : ¬GloballySufficient light V.S1 true V.L true

Switch 1 being on is not globally sufficient for the light to be on, since with switch 2 off the light stays off.

theorem Glass2023.Light.s1_off_causes_off_uncertain : Cause light (Function.update ⊥ V.S1 ↑false) V.S1 false V.L false

Knowing only that switch 1 is off, it caused the light to be off (Table 2, bottom right).

theorem Glass2023.Light.not_s1_on_causes_on_uncertain : ¬Cause light (Function.update ⊥ V.S1 ↑true) V.S1 true V.L true

Knowing only that switch 1 is on, one cannot say it caused the light to be on (Table 2, bottom left).

def Glass2023.Light.bothOn : V → Flat Bool

The background with both switches on.

Equations

• Glass2023.Light.bothOn = Function.update (Function.update ⊥ Glass2023.Light.V.S2 ↑true) Glass2023.Light.V.S1 ↑true

theorem Glass2023.Light.s1_on_causes_on_certain : Cause light bothOn V.S1 true V.L true

With both switches known to be on, switch 1 caused the light to be on (Table 2, top left).

Against necessity-based cause

theorem Glass2023.Bus.glass_nl_diverge_on_bus : Cause NadathurLauer2020.Bus.busModel (Function.update NadathurLauer2020.Bus.s_b NadathurLauer2020.Bus.V.Tr ↑true) NadathurLauer2020.Bus.V.Tr true NadathurLauer2020.Bus.V.Bs true ∧ ¬NadathurLauer2020.Cause NadathurLauer2020.Bus.busModel NadathurLauer2020.Bus.s_b NadathurLauer2020.Bus.actual NadathurLauer2020.Bus.V.Tr true NadathurLauer2020.Bus.V.Bs true

In the bus scenario, with Ava's visit and the rain forecast known, Ava's training is a sufficient cause of Lia's taking the bus in every settlement of the rest, rain alone sufficing, so Glass's cause accepts "Ava's training caused Lia to take the bus", which [NL20]'s necessity-based cause rejects: the same verb, the same scenario, opposite verdicts.