Icard, Kominsky and Knobe (2017): Normality and actual causal strength

Icard, Kominsky and Knobe explain the influence of normality on judgments of actual causation by a measure that weights a cause's sufficiency by its probability and its necessity by the probability of its absence, the probabilities being sampling propensities that rise with normality. On the collider C → E ← A, with E the conjunction or the disjunction of its causes, the measure is P(C) P(A) - P(C) + 1 or P(C), so a less normal C counts as more causal when the causes are conjoined and as less causal when they are disjoined. None of the measures in the literature predicts the second effect, abnormal deflation, which the paper's two experiments find.

Main statements

• abnormal_inflation, supersession, no_supersession, abnormal_deflation: the four effects of the measure on the collider (§3.2, §5, Table 5).
• table1_conjunctive, table1_disjunctive, no_abnormal_deflation: the values of SP, ΔP, power-PC and PNS on the collider (Table 1), none of which rises with P(C) when the causes are disjoined.
• PNS_eq_deltaP: under a product measure PNS is ΔP when the outcome is monotone in the cause (§3.3).
• ae_tendsto_hits: the sampling algorithm of §4.4 converges almost surely to the measure.

Implementation notes

• Worlds are the draws of C and A under independent Bernoulli priors, the paper's sampling propensities, and each causal structure's effect is an event; the measure is the substrate's CausalStrength.score in the round C = A = E = 1.
• The paper names two candidates for sufficiency (§4.3); the substrate takes Cheng and Pearl's, conditioned on the absence of cause and effect, and resampleSufficiency_eq_sufficiency shows the other agrees on the collider. As cond of a null event is the zero measure, the theorems assume priors below one.
• Locators are sections, equations and tables of the accepted preprint.

References

• [IKK17]

The unshielded collider

inductive IcardEtAl2017.Cause : Type

The collider has a focal cause c and an alternative cause a (§3.2).

• c : Cause
• a : Cause

@[instance_reducible]

instance IcardEtAl2017.instDecidableEqCause : DecidableEq Cause

Equations

• IcardEtAl2017.instDecidableEqCause x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance IcardEtAl2017.instFintypeCause : Fintype Cause

Equations

• IcardEtAl2017.instFintypeCause = { elems := { val := ↑IcardEtAl2017.Cause.enumList, nodup := IcardEtAl2017.Cause.enumList_nodup }, complete := IcardEtAl2017.instFintypeCause._proof_1 }

@[reducible, inline]

noncomputable abbrev IcardEtAl2017.prior (p : Cause → ↑unitInterval) : MeasureTheory.Measure (Cause → Bool)

The prior draws each cause independently, c with probability p c and a with p a.

Equations

• IcardEtAl2017.prior p = MeasureTheory.Measure.pi fun (i : IcardEtAl2017.Cause) => ProbabilityTheory.bernoulliMeasure true false (p i)

def IcardEtAl2017.effect : CausalStructure → Set (Cause → Bool)

The effect of a causal structure is the minimum of the two causes if they are conjoined and their maximum if they are disjoined (§3.2).

Equations

• IcardEtAl2017.effect IcardEtAl2017.CausalStructure.conjunctive = {w : IcardEtAl2017.Cause → Bool | min (w IcardEtAl2017.Cause.c) (w IcardEtAl2017.Cause.a) = true}
• IcardEtAl2017.effect IcardEtAl2017.CausalStructure.disjunctive = {w : IcardEtAl2017.Cause → Bool | max (w IcardEtAl2017.Cause.c) (w IcardEtAl2017.Cause.a) = true}

@[instance_reducible]

instance IcardEtAl2017.instDecidablePredForallCauseBoolMemSetEffect (s : CausalStructure) : DecidablePred fun (x : Cause → Bool) => x ∈ effect s

Equations

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

noncomputable def IcardEtAl2017.strength (p : Cause → ↑unitInterval) (s : CausalStructure) : ENNReal

strength p s is the actual causal strength of C = 1 for E = 1 when C = A = E = 1, eq. (1).

Equations

• IcardEtAl2017.strength p s = CausalStrength.score (IcardEtAl2017.prior p) (fun (x : IcardEtAl2017.Cause) => true) (IcardEtAl2017.effect s) {IcardEtAl2017.Cause.c}

theorem IcardEtAl2017.strength_ne_top {p : Cause → ↑unitInterval} {s : CausalStructure} : strength p s ≠ ⊤

Necessity, sufficiency and the measure (Table 2, eqs. (2) and (3))

theorem IcardEtAl2017.necessity_disjunctive (μ : MeasureTheory.Measure (Cause → Bool)) : CausalStrength.necessity μ (fun (x : Cause) => true) (effect CausalStructure.disjunctive) {Cause.c} = 0

When the causes are disjoined the focal cause is not necessary, since the alternative is present (Table 2).

theorem IcardEtAl2017.necessity_conjunctive {p : Cause → ↑unitInterval} (hc : p Cause.c < 1) : CausalStrength.necessity (prior p) (fun (x : Cause) => true) (effect CausalStructure.conjunctive) {Cause.c} = 1

When the causes are conjoined the focal cause is fully necessary (Table 2).

theorem IcardEtAl2017.sufficiency_collider {p : Cause → ↑unitInterval} (hc : p Cause.c < 1) (ha : p Cause.a < 1) : CausalStrength.sufficiency (prior p) (fun (x : Cause) => true) (effect CausalStructure.conjunctive) {Cause.c} = (ProbabilityTheory.bernoulliMeasure true false (p Cause.a)) {true} ∧ CausalStrength.sufficiency (prior p) (fun (x : Cause) => true) (effect CausalStructure.disjunctive) {Cause.c} = 1

When the causes are conjoined the sufficiency of the focal cause is P(A), and when they are disjoined it is one (Table 2).

theorem IcardEtAl2017.strength_collider {p : Cause → ↑unitInterval} (hc : p Cause.c < 1) (ha : p Cause.a < 1) : strength p CausalStructure.conjunctive = (ProbabilityTheory.bernoulliMeasure true false (p Cause.c)) {true} * (ProbabilityTheory.bernoulliMeasure true false (p Cause.a)) {true} + (ProbabilityTheory.bernoulliMeasure true false (p Cause.c)) {false} ∧ strength p CausalStructure.disjunctive = (ProbabilityTheory.bernoulliMeasure true false (p Cause.c)) {true}

The measure is P(C) P(A) + P(¬C) when the causes are conjoined, eq. (3), and P(C) when they are disjoined, eq. (2).

The four effects (§3.2, §5, Table 5)

theorem IcardEtAl2017.abnormal_inflation {p₁ p₂ : Cause → ↑unitInterval} (h : p₂ Cause.c < p₁ Cause.c) (hc : p₁ Cause.c < 1) (ha : p₁ Cause.a = p₂ Cause.a) (ha' : p₁ Cause.a < 1) : strength p₁ CausalStructure.conjunctive < strength p₂ CausalStructure.conjunctive

When the causes are conjoined a less normal focal cause is more causal, provided P(A) < 1 (abnormal inflation).

theorem IcardEtAl2017.supersession {p₁ p₂ : Cause → ↑unitInterval} (h : p₂ Cause.a < p₁ Cause.a) (ha : p₁ Cause.a < 1) (hc : p₁ Cause.c = p₂ Cause.c) (hc₀ : 0 < p₁ Cause.c) (hc₁ : p₁ Cause.c < 1) : strength p₂ CausalStructure.conjunctive < strength p₁ CausalStructure.conjunctive

When the causes are conjoined a less normal alternative makes the focal cause less causal, provided 0 < P(C) (supersession).

theorem IcardEtAl2017.no_supersession {p₁ p₂ : Cause → ↑unitInterval} (hc : p₁ Cause.c = p₂ Cause.c) (hc₁ : p₁ Cause.c < 1) (ha₁ : p₁ Cause.a < 1) (ha₂ : p₂ Cause.a < 1) : strength p₁ CausalStructure.disjunctive = strength p₂ CausalStructure.disjunctive

When the causes are disjoined the alternative's normality does not affect the focal cause (no supersession with disjunction).

theorem IcardEtAl2017.abnormal_deflation {p₁ p₂ : Cause → ↑unitInterval} (h : p₂ Cause.c < p₁ Cause.c) (hc : p₁ Cause.c < 1) (ha₁ : p₁ Cause.a < 1) (ha₂ : p₂ Cause.a < 1) : strength p₂ CausalStructure.disjunctive < strength p₁ CausalStructure.disjunctive

When the causes are disjoined a less normal focal cause is less causal (abnormal deflation, §5).

The other candidate for sufficiency (§4.3)

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

The sufficiency that forces the cause on and redraws every other variable, P(E | do(C = 1)).

Equations

• IcardEtAl2017.resampleSufficiency μ w₀ E S = μ {w : ι → Bool | S.piecewise w₀ w ∈ E}

theorem IcardEtAl2017.resampleSufficiency_eq_sufficiency {p : Cause → ↑unitInterval} (s : CausalStructure) (hc : p Cause.c < 1) (ha : p Cause.a < 1) : resampleSufficiency (prior p) (fun (x : Cause) => true) (effect s) {Cause.c} = CausalStrength.sufficiency (prior p) (fun (x : Cause) => true) (effect s) {Cause.c}

On the collider the two candidates for sufficiency agree.

The measures in the literature (§3.3, Table 1)

noncomputable def IcardEtAl2017.SP {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) (C E : Set Ω) : ℝ

SP is how far the cause raises the probability of the effect over its unconditional value.

Equations

• IcardEtAl2017.SP μ C E = μ[|C].real E - μ.real E

noncomputable def IcardEtAl2017.deltaP {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) (C E : Set Ω) : ℝ

ΔP is the difference of the effect's probability with and without the cause.

Equations

• IcardEtAl2017.deltaP μ C E = μ[|C].real E - μ[|Cᶜ].real E

noncomputable def IcardEtAl2017.powerPC {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) (C E : Set Ω) : ℝ

Cheng's power-PC divides ΔP by the probability that the effect fails without the cause.

Equations

• IcardEtAl2017.powerPC μ C E = IcardEtAl2017.deltaP μ C E / μ[|Cᶜ].real Eᶜ

noncomputable def IcardEtAl2017.PNS {ι : Type u_2} [DecidableEq ι] (μ : MeasureTheory.Measure (ι → Bool)) (X : ι) (E : Set (ι → Bool)) : ℝ

Pearl's probability of necessity and sufficiency of X for E weights the probability that removing the cause removes the outcome, where both hold, and the probability that adding the cause produces the outcome, where neither holds, by the probabilities of the two cases.

Equations

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

theorem IcardEtAl2017.PNS_eq_deltaP {ι : Type u_2} [Fintype ι] [DecidableEq ι] {ν : ι → MeasureTheory.Measure Bool} [∀ (i : ι), MeasureTheory.IsProbabilityMeasure (ν i)] {X : ι} {E : Set (ι → Bool)} (h₁ : (ν X) {true} ≠ 0) (h₀ : (ν X) {false} ≠ 0) (hmono : (fun (x : ι → Bool) => Function.update x X false) ⁻¹' E ⊆ (fun (x : ι → Bool) => Function.update x X true) ⁻¹' E) : PNS (MeasureTheory.Measure.pi ν) X E = deltaP (MeasureTheory.Measure.pi ν) (CausalStrength.cause (fun (x : ι) => true) {X}) E

Under a product measure, PNS is ΔP for an outcome monotone in the cause, the "certain assumptions" under which §3.3 says the two agree.

theorem IcardEtAl2017.table1_conjunctive {p : Cause → ↑unitInterval} (hc₀ : 0 < p Cause.c) (hc₁ : p Cause.c < 1) : SP (prior p) (CausalStrength.cause (fun (x : Cause) => true) {Cause.c}) (effect CausalStructure.conjunctive) = (1 - ↑(p Cause.c)) * ↑(p Cause.a) ∧ deltaP (prior p) (CausalStrength.cause (fun (x : Cause) => true) {Cause.c}) (effect CausalStructure.conjunctive) = ↑(p Cause.a) ∧ powerPC (prior p) (CausalStrength.cause (fun (x : Cause) => true) {Cause.c}) (effect CausalStructure.conjunctive) = ↑(p Cause.a) ∧ PNS (prior p) Cause.c (effect CausalStructure.conjunctive) = ↑(p Cause.a)

On conjoined causes SP is (1 - P(C)) P(A), and ΔP, power-PC and PNS are P(A) (Table 1).

theorem IcardEtAl2017.table1_disjunctive {p : Cause → ↑unitInterval} (hc₀ : 0 < p Cause.c) (hc₁ : p Cause.c < 1) (ha : p Cause.a < 1) : SP (prior p) (CausalStrength.cause (fun (x : Cause) => true) {Cause.c}) (effect CausalStructure.disjunctive) = (1 - ↑(p Cause.c)) * (1 - ↑(p Cause.a)) ∧ deltaP (prior p) (CausalStrength.cause (fun (x : Cause) => true) {Cause.c}) (effect CausalStructure.disjunctive) = 1 - ↑(p Cause.a) ∧ powerPC (prior p) (CausalStrength.cause (fun (x : Cause) => true) {Cause.c}) (effect CausalStructure.disjunctive) = 1 ∧ PNS (prior p) Cause.c (effect CausalStructure.disjunctive) = 1 - ↑(p Cause.a)

On disjoined causes SP is (1 - P(C)) (1 - P(A)), ΔP and PNS are 1 - P(A), and power-PC is one (Table 1).

theorem IcardEtAl2017.no_abnormal_deflation {p₁ p₂ : Cause → ↑unitInterval} (h : p₂ Cause.c < p₁ Cause.c) (hc₀ : 0 < p₂ Cause.c) (hc₁ : p₁ Cause.c < 1) (ha : p₁ Cause.a = p₂ Cause.a) (ha' : p₁ Cause.a < 1) : SP (prior p₁) (CausalStrength.cause (fun (x : Cause) => true) {Cause.c}) (effect CausalStructure.disjunctive) < SP (prior p₂) (CausalStrength.cause (fun (x : Cause) => true) {Cause.c}) (effect CausalStructure.disjunctive) ∧ deltaP (prior p₁) (CausalStrength.cause (fun (x : Cause) => true) {Cause.c}) (effect CausalStructure.disjunctive) = deltaP (prior p₂) (CausalStrength.cause (fun (x : Cause) => true) {Cause.c}) (effect CausalStructure.disjunctive) ∧ PNS (prior p₁) Cause.c (effect CausalStructure.disjunctive) = PNS (prior p₂) Cause.c (effect CausalStructure.disjunctive) ∧ powerPC (prior p₁) (CausalStrength.cause (fun (x : Cause) => true) {Cause.c}) (effect CausalStructure.disjunctive) = powerPC (prior p₂) (CausalStrength.cause (fun (x : Cause) => true) {Cause.c}) (effect CausalStructure.disjunctive)

No measure in the literature predicts abnormal deflation (§3.4), since when the causes are disjoined and the focal cause becomes less normal SP rises while ΔP, PNS and power-PC stay put.

The sampling algorithm (§4.4)

noncomputable def IcardEtAl2017.test {ι : Type u_1} (μ : MeasureTheory.Measure (ι → Bool)) (w₀ : ι → Bool) (E : Set (ι → Bool)) (S : Finset ι) : ProbabilityTheory.Kernel Bool (ι → Bool)

A step's test draws a world given the cause's absence when the cause is absent, a necessity test, and given the absence of cause and outcome when it is present, a sufficiency test.

Equations

• IcardEtAl2017.test μ w₀ E S = ProbabilityTheory.Kernel.ofFunOfCountable fun (x : Bool) => if x = true then μ[|(CausalStrength.cause w₀ S)ᶜ ∩ Eᶜ] else μ[|(CausalStrength.cause w₀ S)ᶜ]

noncomputable def IcardEtAl2017.step {ι : Type u_1} (μ : MeasureTheory.Measure (ι → Bool)) (w₀ : ι → Bool) (E : Set (ι → Bool)) (S : Finset ι) : MeasureTheory.Measure (Bool × (ι → Bool))

A step of the algorithm draws whether the cause holds, then a test world.

Equations

• IcardEtAl2017.step μ w₀ E S = (MeasureTheory.Measure.map (fun (w : ι → Bool) => decide (w ∈ CausalStrength.cause w₀ S)) μ).compProd (IcardEtAl2017.test μ w₀ E S)

noncomputable def IcardEtAl2017.hit {ι : Type u_1} [DecidableEq ι] (w₀ : ι → Bool) (E : Set (ι → Bool)) (S : Finset ι) (z : Bool × (ι → Bool)) : ℝ

A step hits when its necessity test removes the outcome or its sufficiency test produces it.

Equations

• IcardEtAl2017.hit w₀ E S z = if z.1 = true then {w : ι → Bool | S.piecewise w₀ w ∈ E}.indicator 1 z.2 else {w : ι → Bool | S.piecewise w w₀ ∉ E}.indicator 1 z.2

instance IcardEtAl2017.instIsFiniteKernelBoolForallTest {ι : Type u_1} (μ : MeasureTheory.Measure (ι → Bool)) (w₀ : ι → Bool) (E : Set (ι → Bool)) (S : Finset ι) : ProbabilityTheory.IsFiniteKernel (test μ w₀ E S)

instance IcardEtAl2017.instIsFiniteMeasureProdBoolForallStep {ι : Type u_1} (μ : MeasureTheory.Measure (ι → Bool)) (w₀ : ι → Bool) (E : Set (ι → Bool)) (S : Finset ι) [MeasureTheory.IsFiniteMeasure μ] : MeasureTheory.IsFiniteMeasure (step μ w₀ E S)

theorem IcardEtAl2017.isProbabilityMeasure_step {ι : Type u_1} (μ : MeasureTheory.Measure (ι → Bool)) (w₀ : ι → Bool) (E : Set (ι → Bool)) (S : Finset ι) [MeasureTheory.IsProbabilityMeasure μ] (h₀ : μ (CausalStrength.cause w₀ S)ᶜ ≠ 0) (h₁ : μ ((CausalStrength.cause w₀ S)ᶜ ∩ Eᶜ) ≠ 0) : MeasureTheory.IsProbabilityMeasure (step μ w₀ E S)

When the cause can fail, and fail together with the outcome, a step is a probability measure.

theorem IcardEtAl2017.integral_hit_step {ι : Type u_1} [Fintype ι] [DecidableEq ι] (μ : MeasureTheory.Measure (ι → Bool)) (w₀ : ι → Bool) (E : Set (ι → Bool)) (S : Finset ι) [MeasureTheory.IsFiniteMeasure μ] : ∫ (z : Bool × (ι → Bool)), hit w₀ E S z ∂step μ w₀ E S = (CausalStrength.score μ w₀ E S).toReal

The expected hit of a step is the actual causal strength, eq. (1).

theorem IcardEtAl2017.ae_tendsto_hits {ι : Type u_1} [Fintype ι] [DecidableEq ι] (μ : MeasureTheory.Measure (ι → Bool)) (w₀ : ι → Bool) (E : Set (ι → Bool)) (S : Finset ι) [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsProbabilityMeasure (step μ w₀ E S)] : ∀ᵐ (ω : ℕ → Bool × (ι → Bool)) ∂MeasureTheory.Measure.infinitePi fun (x : ℕ) => step μ w₀ E S, Filter.Tendsto (fun (K : ℕ) => (↑K)⁻¹ * ∑ k ∈ Finset.range K, hit w₀ E S (ω k)) Filter.atTop (nhds (CausalStrength.score μ w₀ E S).toReal)

The sampling algorithm converges, in that on almost every run of independent steps the proportion of hits tends to the actual causal strength, eq. (1).

The experiments (§5)

In both experiments, with prescriptive norms and with statistical ones, a norm-violating cause was rated more causal than a normative one when the causes were conjoined and less causal when they were disjoined, as abnormal_inflation and abnormal_deflation predict when norm violation lowers the sampling propensity (§4.2); the interaction is significant in both.