Actual causal strength

Icard, Kominsky and Knobe measure how strongly a cause brought about an outcome by weighting its sufficiency by the probability of the cause and its necessity by the probability of its absence. Here worlds are draws ι → Bool of binary variables under a probability measure μ, and a cause is a set S of variables showing the draws of an actual round w₀, as Konuk, Quillien and Mascarenhas extend the measure to plural causes.

Main definitions

• CausalStrength.cause: the event that the variables of S show their actual draws.
• CausalStrength.necessity: the probability that the outcome fails when the cause's variables are redrawn short of the cause and the others keep their actual draws.
• CausalStrength.sufficiency: the probability, where neither cause nor outcome holds, that forcing the cause on produces the outcome.
• CausalStrength.score: sufficiency weighted by the cause's probability plus necessity weighted by its absence's.

Main results

• CausalStrength.score_singleton: under a product measure, a single cause scores its probability times its sufficiency, plus its absence's probability when flipping it removes the outcome.
• CausalStrength.score_pi_cause: under a product measure, when the outcome is that the variables T show their actual draws, a part of T scores the probability of its absence plus that of the outcome.

References

• [IKK17]
• [KQM26]

def CausalStrength.cause {ι : Type u_1} (w₀ : ι → Bool) (S : Finset ι) : Set (ι → Bool)

The plural cause S in the actual round w₀ is the event that every urn of S shows its actual draw.

Equations

• CausalStrength.cause w₀ S = (↑S).pi fun (i : ι) => {w₀ i}

theorem CausalStrength.mem_cause {ι : Type u_1} {w₀ w : ι → Bool} {S : Finset ι} : w ∈ cause w₀ S ↔ ∀ i ∈ S, w i = w₀ i

@[instance_reducible]

instance CausalStrength.instDecidablePredForallBoolMemSetCause {ι : Type u_1} {w₀ : ι → Bool} {S : Finset ι} : DecidablePred fun (x : ι → Bool) => x ∈ cause w₀ S

Equations

• CausalStrength.instDecidablePredForallBoolMemSetCause x✝ = decidable_of_iff (∀ i ∈ S, x✝ i = w₀ i) ⋯

theorem CausalStrength.cause_subset_cause {ι : Type u_1} {w₀ : ι → Bool} {S T : Finset ι} (h : S ⊆ T) : cause w₀ T ⊆ cause w₀ S

A plurality of causes is a stronger event than any part of it.

theorem CausalStrength.dependsOn_cause {ι : Type u_1} {w₀ : ι → Bool} {S : Finset ι} : DependsOn (fun (x : ι → Bool) => x ∈ cause w₀ S) ↑S

theorem CausalStrength.cause_inter_cause_sdiff {ι : Type u_1} {w₀ : ι → Bool} {S T : Finset ι} [DecidableEq ι] (h : S ⊆ T) : cause w₀ S ∩ cause w₀ (T \ S) = cause w₀ T

theorem CausalStrength.compl_cause_singleton {ι : Type u_1} {w₀ : ι → Bool} (X : ι) : (cause w₀ {X})ᶜ = cause (fun (x : ι) => !w₀ X) {X}

theorem CausalStrength.piecewise_mem_cause {ι : Type u_1} {w₀ w : ι → Bool} {S T : Finset ι} [DecidableEq ι] : S.piecewise w w₀ ∈ cause w₀ T ↔ w ∈ cause w₀ (S ∩ T)

theorem CausalStrength.piecewise_self_mem_cause {ι : Type u_1} {w₀ w : ι → Bool} {S T : Finset ι} [DecidableEq ι] : S.piecewise w₀ w ∈ cause w₀ T ↔ w ∈ cause w₀ (T \ S)

noncomputable def CausalStrength.necessity {ι : Type u_1} [DecidableEq ι] (μ : MeasureTheory.Measure (ι → Bool)) (w₀ : ι → Bool) (E : Set (ι → Bool)) (S : Finset ι) : ENNReal

The necessity of the plural cause S for the outcome E is the probability that the outcome fails when the urns of S are redrawn from μ, short of all showing their actual draws, and every other urn keeps its actual draw.

Equations

• CausalStrength.necessity μ w₀ E S = μ[{w : ι → Bool | S.piecewise w w₀ ∉ E} | (CausalStrength.cause w₀ S)ᶜ]

noncomputable def CausalStrength.sufficiency {ι : Type u_1} [DecidableEq ι] (μ : MeasureTheory.Measure (ι → Bool)) (w₀ : ι → Bool) (E : Set (ι → Bool)) (S : Finset ι) : ENNReal

The sufficiency of the plural cause S for the outcome E is the probability, over the worlds of μ where neither the cause nor the outcome holds, that forcing the cause on produces the outcome.

Equations

• CausalStrength.sufficiency μ w₀ E S = μ[{w : ι → Bool | S.piecewise w₀ w ∈ E} | (CausalStrength.cause w₀ S)ᶜ ∩ Eᶜ]

noncomputable def CausalStrength.score {ι : Type u_1} [DecidableEq ι] (μ : MeasureTheory.Measure (ι → Bool)) (w₀ : ι → Bool) (E : Set (ι → Bool)) (S : Finset ι) : ENNReal

The score of the plural cause S for the outcome E weights its sufficiency by its probability and its necessity by the probability of its absence.

Equations

• CausalStrength.score μ w₀ E S = μ (CausalStrength.cause w₀ S) * CausalStrength.sufficiency μ w₀ E S + μ (CausalStrength.cause w₀ S)ᶜ * CausalStrength.necessity μ w₀ E S

theorem CausalStrength.necessity_eq_zero {ι : Type u_1} {w₀ : ι → Bool} {S : Finset ι} [DecidableEq ι] {μ : MeasureTheory.Measure (ι → Bool)} {E : Set (ι → Bool)} (h : ∀ (w : ι → Bool), S.piecewise w w₀ ∈ E) : necessity μ w₀ E S = 0

A cause whose absence never removes the outcome, the other urns keeping their actual draws, is not necessary at all.

theorem CausalStrength.necessity_eq_one {ι : Type u_1} {w₀ : ι → Bool} {S : Finset ι} [DecidableEq ι] [Fintype ι] {μ : MeasureTheory.Measure (ι → Bool)} {E : Set (ι → Bool)} [MeasureTheory.IsFiniteMeasure μ] (h : ∀ w ∉ cause w₀ S, S.piecewise w w₀ ∉ E) (hc : μ (cause w₀ S)ᶜ ≠ 0) : necessity μ w₀ E S = 1

A cause whose absence always removes the outcome is fully necessary.

theorem CausalStrength.sufficiency_eq_one {ι : Type u_1} {w₀ : ι → Bool} {S : Finset ι} [DecidableEq ι] {μ : MeasureTheory.Measure (ι → Bool)} {E : Set (ι → Bool)} [MeasureTheory.IsFiniteMeasure μ] (h : ∀ (w : ι → Bool), S.piecewise w₀ w ∈ E) (hc : μ ((cause w₀ S)ᶜ ∩ Eᶜ) ≠ 0) : sufficiency μ w₀ E S = 1

A cause that produces the outcome whenever it is forced on is fully sufficient.

theorem CausalStrength.mul_necessity {ι : Type u_1} {w₀ : ι → Bool} {S : Finset ι} [DecidableEq ι] [Fintype ι] {μ : MeasureTheory.Measure (ι → Bool)} {E : Set (ι → Bool)} [MeasureTheory.IsFiniteMeasure μ] : μ (cause w₀ S)ᶜ * necessity μ w₀ E S = μ ((cause w₀ S)ᶜ ∩ {w : ι → Bool | S.piecewise w w₀ ∉ E})

theorem CausalStrength.score_le_one {ι : Type u_1} {w₀ : ι → Bool} {S : Finset ι} [DecidableEq ι] [Fintype ι] {μ : MeasureTheory.Measure (ι → Bool)} {E : Set (ι → Bool)} [MeasureTheory.IsProbabilityMeasure μ] : score μ w₀ E S ≤ 1

theorem CausalStrength.score_ne_top {ι : Type u_1} {w₀ : ι → Bool} {S : Finset ι} [DecidableEq ι] [Fintype ι] {μ : MeasureTheory.Measure (ι → Bool)} {E : Set (ι → Bool)} [MeasureTheory.IsProbabilityMeasure μ] : score μ w₀ E S ≠ ⊤

theorem CausalStrength.score_eq_one {ι : Type u_1} {w₀ : ι → Bool} {S : Finset ι} [DecidableEq ι] [Fintype ι] {μ : MeasureTheory.Measure (ι → Bool)} {E : Set (ι → Bool)} [MeasureTheory.IsProbabilityMeasure μ] (hsuf : ∀ (w : ι → Bool), S.piecewise w₀ w ∈ E) (hnec : ∀ w ∉ cause w₀ S, S.piecewise w w₀ ∉ E) (hc : μ ((cause w₀ S)ᶜ ∩ Eᶜ) ≠ 0) : score μ w₀ E S = 1

A cause that is fully sufficient and fully necessary scores one.

theorem CausalStrength.necessity_singleton {ι : Type u_1} {w₀ : ι → Bool} [DecidableEq ι] [Fintype ι] {μ : MeasureTheory.Measure (ι → Bool)} {E : Set (ι → Bool)} [MeasureTheory.IsFiniteMeasure μ] [DecidablePred fun (x : ι → Bool) => x ∈ E] {X : ι} (hc : μ (cause w₀ {X})ᶜ ≠ 0) : necessity μ w₀ E {X} = if (Function.update w₀ X !w₀ X) ∈ E then 0 else 1

A single cause is necessary exactly when flipping it in the actual round, the other urns kept, removes the outcome.

theorem CausalStrength.sufficiency_le_one {ι : Type u_1} {w₀ : ι → Bool} {S : Finset ι} [DecidableEq ι] {μ : MeasureTheory.Measure (ι → Bool)} {E : Set (ι → Bool)} : sufficiency μ w₀ E S ≤ 1

theorem CausalStrength.necessity_le_one {ι : Type u_1} {w₀ : ι → Bool} {S : Finset ι} [DecidableEq ι] {μ : MeasureTheory.Measure (ι → Bool)} {E : Set (ι → Bool)} : necessity μ w₀ E S ≤ 1

theorem CausalStrength.sufficiency_ne_top {ι : Type u_1} {w₀ : ι → Bool} {S : Finset ι} [DecidableEq ι] {μ : MeasureTheory.Measure (ι → Bool)} {E : Set (ι → Bool)} : sufficiency μ w₀ E S ≠ ⊤

theorem CausalStrength.necessity_ne_top {ι : Type u_1} {w₀ : ι → Bool} {S : Finset ι} [DecidableEq ι] {μ : MeasureTheory.Measure (ι → Bool)} {E : Set (ι → Bool)} : necessity μ w₀ E S ≠ ⊤

theorem CausalStrength.measure_pi_cause {ι : Type u_1} [Fintype ι] {ν : ι → MeasureTheory.Measure Bool} [∀ (i : ι), MeasureTheory.IsProbabilityMeasure (ν i)] {v : ι → Bool} {S : Finset ι} : (MeasureTheory.Measure.pi ν) (cause v S) = ∏ i ∈ S, (ν i) {v i}

theorem CausalStrength.measureReal_pi_cause {ι : Type u_1} [Fintype ι] {ν : ι → MeasureTheory.Measure Bool} [∀ (i : ι), MeasureTheory.IsProbabilityMeasure (ν i)] {v : ι → Bool} {S : Finset ι} : (MeasureTheory.Measure.pi ν).real (cause v S) = ∏ i ∈ S, (ν i).real {v i}

theorem CausalStrength.measure_pi_compl_cause_singleton {ι : Type u_1} [Fintype ι] {ν : ι → MeasureTheory.Measure Bool} [∀ (i : ι), MeasureTheory.IsProbabilityMeasure (ν i)] {v : ι → Bool} (X : ι) : (MeasureTheory.Measure.pi ν) (cause v {X})ᶜ = (ν X) {!v X}

theorem CausalStrength.measure_pi_inter_of_dependsOn {ι : Type u_1} [Fintype ι] {ν : ι → MeasureTheory.Measure Bool} [∀ (i : ι), MeasureTheory.IsProbabilityMeasure (ν i)] {S T : Finset ι} {A B : Set (ι → Bool)} (hA : DependsOn (fun (x : ι → Bool) => x ∈ A) ↑S) (hB : DependsOn (fun (x : ι → Bool) => x ∈ B) ↑T) (h : Disjoint S T) : (MeasureTheory.Measure.pi ν) (A ∩ B) = (MeasureTheory.Measure.pi ν) A * (MeasureTheory.Measure.pi ν) B

Under a product measure, events that depend on disjoint sets of urns are independent.

theorem CausalStrength.measure_pi_cause_singleton_inter {ι : Type u_1} [Fintype ι] {ν : ι → MeasureTheory.Measure Bool} [∀ (i : ι), MeasureTheory.IsProbabilityMeasure (ν i)] {v : ι → Bool} [DecidableEq ι] {X : ι} {B : Set (ι → Bool)} (hB : ∀ (w : ι → Bool) (b : Bool), Function.update w X b ∈ B ↔ w ∈ B) : (MeasureTheory.Measure.pi ν) (cause v {X} ∩ B) = (ν X) {v X} * (MeasureTheory.Measure.pi ν) B

An urn's draw is independent of any event that changing the urn cannot affect.

theorem CausalStrength.update_mem_cause_iff {ι : Type u_1} {v : ι → Bool} {S : Finset ι} [DecidableEq ι] {X : ι} (hX : X ∉ S) (w : ι → Bool) (b : Bool) : Function.update w X b ∈ cause v S ↔ w ∈ cause v S

theorem CausalStrength.sufficiency_singleton {ι : Type u_1} [Fintype ι] {ν : ι → MeasureTheory.Measure Bool} [∀ (i : ι), MeasureTheory.IsProbabilityMeasure (ν i)] {w₀ : ι → Bool} {E : Set (ι → Bool)} [DecidableEq ι] {X : ι} (hX : (ν X) {!w₀ X} ≠ 0) : sufficiency (MeasureTheory.Measure.pi ν) w₀ E {X} = (MeasureTheory.Measure.pi ν) ((fun (x : ι → Bool) => Function.update x X (w₀ X)) ⁻¹' E \ (fun (x : ι → Bool) => Function.update x X !w₀ X) ⁻¹' E) / (MeasureTheory.Measure.pi ν) ((fun (x : ι → Bool) => Function.update x X !w₀ X) ⁻¹' E)ᶜ

The sufficiency of a single cause is the probability, over the other urns, that the outcome holds with the cause and fails without it, given that it fails without it.

theorem CausalStrength.score_singleton {ι : Type u_1} [Fintype ι] {ν : ι → MeasureTheory.Measure Bool} [∀ (i : ι), MeasureTheory.IsProbabilityMeasure (ν i)] {w₀ : ι → Bool} {E : Set (ι → Bool)} [DecidableEq ι] [DecidablePred fun (x : ι → Bool) => x ∈ E] {X : ι} (hX : (ν X) {!w₀ X} ≠ 0) : score (MeasureTheory.Measure.pi ν) w₀ E {X} = (ν X) {w₀ X} * sufficiency (MeasureTheory.Measure.pi ν) w₀ E {X} + if (Function.update w₀ X !w₀ X) ∈ E then 0 else (ν X) {!w₀ X}

The score of a single cause is its probability times its sufficiency, plus the probability of its absence when flipping it in the actual round removes the outcome.

theorem CausalStrength.score_pi_cause {ι : Type u_1} [Fintype ι] {ν : ι → MeasureTheory.Measure Bool} [∀ (i : ι), MeasureTheory.IsProbabilityMeasure (ν i)] {w₀ : ι → Bool} {S T : Finset ι} [DecidableEq ι] (hST : S ⊆ T) (hc : (MeasureTheory.Measure.pi ν) (cause w₀ S)ᶜ ≠ 0) : score (MeasureTheory.Measure.pi ν) w₀ (cause w₀ T) S = (MeasureTheory.Measure.pi ν) (cause w₀ S)ᶜ + (MeasureTheory.Measure.pi ν) (cause w₀ T)

When the outcome is that the urns T all show their actual draws, the score of a part S of T is the probability that S is absent plus the probability of the outcome.

theorem CausalStrength.score_pi_cause_lt_iff {ι : Type u_1} [Fintype ι] {ν : ι → MeasureTheory.Measure Bool} [∀ (i : ι), MeasureTheory.IsProbabilityMeasure (ν i)] {w₀ : ι → Bool} {S T : Finset ι} [DecidableEq ι] {S' : Finset ι} (hS : S ⊆ T) (hS' : S' ⊆ T) (hc : (MeasureTheory.Measure.pi ν) (cause w₀ S)ᶜ ≠ 0) (hc' : (MeasureTheory.Measure.pi ν) (cause w₀ S')ᶜ ≠ 0) : score (MeasureTheory.Measure.pi ν) w₀ (cause w₀ T) S < score (MeasureTheory.Measure.pi ν) w₀ (cause w₀ T) S' ↔ (MeasureTheory.Measure.pi ν) (cause w₀ S') < (MeasureTheory.Measure.pi ν) (cause w₀ S)

When the outcome is that the urns T all show their actual draws, of two parts of T the less likely scores higher.