A Communication-First Account of Explanation

@cite{halpern-pearl-2005} @cite{harding-gerstenberg-icard-2025} @cite{sumers-etal-2023} @cite{frank-goodman-2012}

Formalization of @cite{harding-gerstenberg-icard-2025} §3: "why FACT?" / "FACT because X = x" modeled as an RSA communication game where the literal listener interprets via Halpern-Pearl actual causation, the speaker reasons about a downstream decision problem (the manipulation game of Def 3), and Goodness (eq. 8) is Δ expected utility under the pragmatic listener.

The framework (paper §3)

• Worlds: pairs (M, u) of a structural causal model with an exogenous context. K is a finite set of such pairs (the listener's epistemic state).
• Messages: "FACT because X = x". Semantic value is actualCause at (M, u). We use a simple existential-witness form (paper p. 8 licenses any extant actual-cause account); the existential ranges over Boolean valuations and reduces structurally on the concrete scenarios. UNVERIFIED: the full HP definition with off-pathway W-witnesses is stronger; for the disjunctive Milk-Theft case the two definitions agree on which messages are true.
• L0 (eq. 2): P_{L0}(M, u | m) ∝ Prior(M, u) · 1_{(M,u) ⊨ m}.
• Manipulation Game (Def 3): action set A = endogenous variables other than FACT; reward R(X, M, u) = E_{u'}[Manipulates(X, FACT | M, u')] built from BoolSEM.manipulates.
• Speaker (eqs. 3-5): π_{L0}(a | m) ∝ exp(β_L · E_{P_{L0}}[R(a, M, u)]), U_S(m, M, u) = Σ_a π_{L0}(a | m) · R(a, M, u), P_S(m | M, u) ∝ exp(β_S · U_S(m, M, u)).
• Pragmatic Listener (eq. 7): P_L(M, u | m) ∝ Prior(M, u) · P_S(m | M, u).
• Goodness (eq. 8): Σ_a π_L(a | m) · R(a, M, u) - Σ_a π_Prior(a) · R(a, M, u).

We work in the β → ∞ regime the paper adopts most often ("agents are maximizing"): policies become argmax over expected reward, and the softmax collapses. This makes the worked theorems exact-rational and kernel-decidable.

Scenarios

Each scenario lives in its own namespace with a per-scenario World type, ExplanationGame instance, message inventory, and worked predictions:

• Late Meeting (Example 5, p. 13): K = {M_T, M_∧} × {u = (T=1, B=1)}. Predicts: citing T (tardiness) is the unique best explanation under M_T; citing B fails the manipulation game in M_T because B doesn't manipulate C there.
• Roof Replacement (Example 3, p. 10): K = 4 structures × {u = (R=1, D=1)}. Predicts: citing R (thatched roof) and citing D (drought) have the same manipulation reward profile under the manipulation game, but a decision-relevant downstream task (e.g., "what to repair") breaks the tie toward R.
• Milk Theft (Example 4, p. 11): K = {M_∨} × {u_C, u_D, u_{C,D}}. Predicts: in u_{C,D} (overdetermination), neither single-cite uniquely manipulates; the conjoint message "Ch and Da" gets a higher Goodness.

§3 Substrate: ExplanationGame

structure HardingGerstenbergIcard2025.ExplanationGame (V : Type u_1) (W : Type u_2) [Fintype V] [DecidableEq V] [Fintype W] [DecidableEq W] : Type (max u_1 u_2)

A configuration for the explanation framework: a finite world space of causal-situation pairs (M, u), with prior, plus a designated explanandum variable.

• modelOf : W → Core.Causal.BoolSEM V

  World w → its structural causal model.

• contextOf : W → Core.Causal.Valuation fun (x : V) => Bool

  World w → its exogenous context (a partial valuation over V).

• vs : List V

  Vertex list for developDetOn (typically all of V in some order).

• n : ℕ

  Iteration depth for developDetOn (typically Fintype.card V).

• isDet (w : W) : Core.Causal.SEM.IsDeterministic (self.modelOf w)

  Each world's model is deterministic.

• isDag (w : W) : (self.modelOf w).graph.IsDAG

  Each world's graph is acyclic.

• prior : W → ℚ

  Unnormalized world prior.

• prior_nonneg (w : W) : 0 ≤ self.prior w
• factVar : V

  The explanandum FACT (single variable, value = true assumed).

Actual causation (literal meaning of "because")

Simplified Halpern-Pearl: cause is an actual cause of effect under (M, u) iff there exists a witness valuation under which cause = true is but-for effect = true (sufficiency + non-redundance).

This collapses to plain but-for when u itself is the witness, and extends to overdetermination cases via off-actual witnesses (see Milk-Theft Example 4).

noncomputable def HardingGerstenbergIcard2025.actualCause {V : Type u_1} [Fintype V] [DecidableEq V] (M : Core.Causal.BoolSEM V) [Core.Causal.SEM.IsDeterministic M] (vs : List V) (u : Core.Causal.Valuation fun (x : V) => Bool) (n : ℕ) (cause effect : V) : Prop

Halpern-Pearl-style actual causation, simplified to existential Boolean witness. AC1: cause and effect both fired at (M, u). AC2 (witness form): some valuation s' makes cause but-for effect via BoolSEM.completesForEffectOn.

Equations

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

@[implicit_reducible]

noncomputable instance HardingGerstenbergIcard2025.instDecidableActualCause {V : Type u_1} [Fintype V] [DecidableEq V] (M : Core.Causal.BoolSEM V) [Core.Causal.SEM.IsDeterministic M] (vs : List V) (u : Core.Causal.Valuation fun (x : V) => Bool) (n : ℕ) (cause effect : V) : Decidable (actualCause M vs u n cause effect)

Equations

• HardingGerstenbergIcard2025.instDecidableActualCause M vs u n cause effect = Classical.dec (HardingGerstenbergIcard2025.actualCause M vs u n cause effect)

Messages and meaning

structure HardingGerstenbergIcard2025.Message (V : Type u_1) : Type u_1

A "FACT because X = x" message. Restricts to the Boolean case where the cited cause-value and explanandum-value are both true (paper's convention for the worked examples).

• cause : V

@[implicit_reducible]

instance HardingGerstenbergIcard2025.instDecidableEqMessage {V✝ : Type u_1} [DecidableEq V✝] : DecidableEq (Message V✝)

Equations

• HardingGerstenbergIcard2025.instDecidableEqMessage = HardingGerstenbergIcard2025.instDecidableEqMessage.decEq

def HardingGerstenbergIcard2025.instDecidableEqMessage.decEq {V✝ : Type u_1} [DecidableEq V✝] (x✝ x✝¹ : Message V✝) : Decidable (x✝ = x✝¹)

Equations

• HardingGerstenbergIcard2025.instDecidableEqMessage.decEq { cause := a } { cause := b } = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance HardingGerstenbergIcard2025.instReprMessage {V✝ : Type u_1} [Repr V✝] : Repr (Message V✝)

Equations

• HardingGerstenbergIcard2025.instReprMessage = { reprPrec := HardingGerstenbergIcard2025.instReprMessage.repr }

def HardingGerstenbergIcard2025.instReprMessage.repr {V✝ : Type u_1} [Repr V✝] : Message V✝ → ℕ → Std.Format

Equations

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

noncomputable def HardingGerstenbergIcard2025.ExplanationGame.meaning {V : Type u_1} {W : Type u_2} [Fintype V] [DecidableEq V] [Fintype W] [DecidableEq W] (G : ExplanationGame V W) (m : Message V) (w : W) : Prop

Whether m is true at world w: actualCause of factVar by m.cause.

Equations

• G.meaning m w = HardingGerstenbergIcard2025.actualCause (G.modelOf w) G.vs (G.contextOf w) G.n m.cause G.factVar

@[implicit_reducible]

noncomputable instance HardingGerstenbergIcard2025.ExplanationGame.meaning_decidable {V : Type u_1} {W : Type u_2} [Fintype V] [DecidableEq V] [Fintype W] [DecidableEq W] (G : ExplanationGame V W) (m : Message V) (w : W) : Decidable (G.meaning m w)

Equations

• G.meaning_decidable m w = Classical.dec (G.meaning m w)

§3.1 L0 posterior

P_{L0}(w | m) ∝ Prior(w) · 1_{w ⊨ m} (eq. 2). We provide both the unnormalized score and the normalized posterior.

noncomputable def HardingGerstenbergIcard2025.ExplanationGame.l0Score {V : Type u_1} {W : Type u_2} [Fintype V] [DecidableEq V] [Fintype W] [DecidableEq W] (G : ExplanationGame V W) (m : Message V) (w : W) : ℚ

Unnormalized L0 weight: prior × meaning indicator.

Equations

• G.l0Score m w = if G.meaning m w then G.prior w else 0

noncomputable def HardingGerstenbergIcard2025.ExplanationGame.l0Z {V : Type u_1} {W : Type u_2} [Fintype V] [DecidableEq V] [Fintype W] [DecidableEq W] (G : ExplanationGame V W) (m : Message V) : ℚ

Normalizer: sum of L0 scores over the world fintype.

Equations

• G.l0Z m = ∑ w : W, G.l0Score m w

noncomputable def HardingGerstenbergIcard2025.ExplanationGame.l0 {V : Type u_1} {W : Type u_2} [Fintype V] [DecidableEq V] [Fintype W] [DecidableEq W] (G : ExplanationGame V W) (m : Message V) (w : W) : ℚ

Normalized L0 posterior. Returns 0 when the normalizer is 0 (vacuous message).

Equations

• G.l0 m w = if G.l0Z m = 0 then 0 else G.l0Score m w / G.l0Z m

§3.3 Manipulation Game (Def 3)

R(X, M, u') = 1 iff X manipulates FACT in (M, u') (some Boolean intervention on X flips FACT). Aggregated reward over the world space: R(X, w) = E_{w'}[1_{Manipulates(X, FACT | M_{w'}, u_{w'})}] weighted by prior on w'.

Note: paper's Def 3 averages over u' for fixed M; here we average over the entire world w' (including model uncertainty), matching the formalization choices made for the listener's epistemic state.

noncomputable def HardingGerstenbergIcard2025.ExplanationGame.worldManipulates {V : Type u_1} {W : Type u_2} [Fintype V] [DecidableEq V] [Fintype W] [DecidableEq W] (G : ExplanationGame V W) (X : V) (w : W) : Prop

Whether action variable X manipulates FACT at world w.

Equations

• G.worldManipulates X w = (G.modelOf w).manipulates (G.contextOf w) X G.factVar

@[implicit_reducible]

noncomputable instance HardingGerstenbergIcard2025.instDecidableWorldManipulates {V : Type u_1} {W : Type u_2} [Fintype V] [DecidableEq V] [Fintype W] [DecidableEq W] (G : ExplanationGame V W) (X : V) (w : W) : Decidable (G.worldManipulates X w)

Equations

• HardingGerstenbergIcard2025.instDecidableWorldManipulates G X w = Classical.dec (G.worldManipulates X w)

noncomputable def HardingGerstenbergIcard2025.ExplanationGame.reward {V : Type u_1} {W : Type u_2} [Fintype V] [DecidableEq V] [Fintype W] [DecidableEq W] (G : ExplanationGame V W) (X : V) : ℚ

Manipulation-game reward for action X: prior-weighted indicator of X manipulating FACT across worlds.

Equations

• G.reward X = ∑ w : W, G.prior w * if G.worldManipulates X w then 1 else 0

noncomputable def HardingGerstenbergIcard2025.ExplanationGame.condReward {V : Type u_1} {W : Type u_2} [Fintype V] [DecidableEq V] [Fintype W] [DecidableEq W] (G : ExplanationGame V W) (X : V) (m : Message V) : ℚ

Conditional reward: prior-weighted manipulation under L0's posterior.

Equations

• G.condReward X m = ∑ w : W, G.l0 m w * if G.worldManipulates X w then 1 else 0

§3.2 Speaker (β = ∞ specialization)

In the β → ∞ regime, π_{L0}(a | m) puts all mass on argmax_a condReward(a, m). We expose the argmax as a predicate isBestAction (any action whose conditional reward dominates all others); when the argmax is unique, uS reduces to that action's actual-world reward.

noncomputable def HardingGerstenbergIcard2025.ExplanationGame.isBestAction {V : Type u_1} {W : Type u_2} [Fintype V] [DecidableEq V] [Fintype W] [DecidableEq W] (G : ExplanationGame V W) (m : Message V) (X : V) : Prop

An action X is L0's best response to message m: its conditional reward dominates every other action.

Equations

• G.isBestAction m X = ∀ (Y : V), G.condReward Y m ≤ G.condReward X m

@[implicit_reducible]

noncomputable instance HardingGerstenbergIcard2025.instDecidableIsBestAction {V : Type u_1} {W : Type u_2} [Fintype V] [DecidableEq V] [Fintype W] [DecidableEq W] (G : ExplanationGame V W) (m : Message V) (X : V) : Decidable (G.isBestAction m X)

Equations

• HardingGerstenbergIcard2025.instDecidableIsBestAction G m X = Classical.dec (G.isBestAction m X)

noncomputable def HardingGerstenbergIcard2025.ExplanationGame.uS {V : Type u_1} {W : Type u_2} [Fintype V] [DecidableEq V] [Fintype W] [DecidableEq W] (G : ExplanationGame V W) (bestAction : V) (w : W) : ℚ

Speaker utility (β = ∞) at world w, given an L0 best response bestAction selected by the caller (typically a witness for isBestAction m bestAction): the reward of bestAction at w.

Equations

• G.uS bestAction w = if (G.modelOf w).manipulates (G.contextOf w) bestAction G.factVar then 1 else 0

§3.4 Pragmatic Listener and Goodness (eq. 8)

In the β → ∞ regime, P_S puts all mass on argmax-utility messages, and π_L behaves like π_{L0} after Bayesian inversion against the speaker's choice. We collapse Goodness (eq. 8) to a single comparable scalar at the actual world w*: post-explanation reward of the chosen best action minus the prior-best action's reward. Positive Goodness means the explanation strictly improved the listener's expected outcome at w*.

noncomputable def HardingGerstenbergIcard2025.ExplanationGame.goodness {V : Type u_1} {W : Type u_2} [Fintype V] [DecidableEq V] [Fintype W] [DecidableEq W] (G : ExplanationGame V W) (priorBest postBest : V) (wStar : W) : ℚ

Goodness of message m at the actual world w*, given the pre-explanation prior-best action (priorBest) and the post- explanation L0-best action (postBest). Δ expected utility at the actual world (β = ∞).

Equations

• G.goodness priorBest postBest wStar = G.uS postBest wStar - G.uS priorBest wStar

Bob is late (T = 1) and forgot Charlie's birthday (B = 1); Charlie is cross (C = 1). K = {(M_T, u), (M_∧, u)} where M_T has C ← T and M_∧ has C ← T ∧ B. Actual world is M_T.

inductive HardingGerstenbergIcard2025.LateMeeting.V : Type

Endogenous variables.

• T : V
• B : V
• C : V

@[implicit_reducible]

instance HardingGerstenbergIcard2025.LateMeeting.instDecidableEqV : DecidableEq V

Equations

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

@[implicit_reducible]

instance HardingGerstenbergIcard2025.LateMeeting.instFintypeV : Fintype V

Equations

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

@[implicit_reducible]

instance HardingGerstenbergIcard2025.LateMeeting.instReprV : Repr V

Equations

• HardingGerstenbergIcard2025.LateMeeting.instReprV = { reprPrec := HardingGerstenbergIcard2025.LateMeeting.instReprV.repr }

def HardingGerstenbergIcard2025.LateMeeting.instReprV.repr : V → ℕ → Std.Format

Equations

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

def HardingGerstenbergIcard2025.LateMeeting.lmVarList : List V

Equations

• HardingGerstenbergIcard2025.LateMeeting.lmVarList = [HardingGerstenbergIcard2025.LateMeeting.V.T, HardingGerstenbergIcard2025.LateMeeting.V.B, HardingGerstenbergIcard2025.LateMeeting.V.C]

def HardingGerstenbergIcard2025.LateMeeting.graphT : Core.Causal.CausalGraph V

Equations

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

def HardingGerstenbergIcard2025.LateMeeting.graphConj : Core.Causal.CausalGraph V

Equations

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

noncomputable def HardingGerstenbergIcard2025.LateMeeting.semT : Core.Causal.BoolSEM V

Equations

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

@[implicit_reducible]

noncomputable instance HardingGerstenbergIcard2025.LateMeeting.instIsDeterministicVBoolSemT : Core.Causal.SEM.IsDeterministic semT

Equations

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

instance HardingGerstenbergIcard2025.LateMeeting.instIsDAGVGraphBoolSemT : semT.graph.IsDAG

noncomputable def HardingGerstenbergIcard2025.LateMeeting.semConj : Core.Causal.BoolSEM V

Equations

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

@[implicit_reducible]

noncomputable instance HardingGerstenbergIcard2025.LateMeeting.instIsDeterministicVBoolSemConj : Core.Causal.SEM.IsDeterministic semConj

Equations

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

instance HardingGerstenbergIcard2025.LateMeeting.instIsDAGVGraphBoolSemConj : semConj.graph.IsDAG

def HardingGerstenbergIcard2025.LateMeeting.lateBg : Core.Causal.Valuation fun (x : V) => Bool

Single shared exogenous context: T = 1, B = 1.

Equations

• HardingGerstenbergIcard2025.LateMeeting.lateBg = (Core.Causal.Valuation.empty.extend HardingGerstenbergIcard2025.LateMeeting.V.T true).extend HardingGerstenbergIcard2025.LateMeeting.V.B true

inductive HardingGerstenbergIcard2025.LateMeeting.World : Type

World enum: which structural alternative (single shared context).

• mT : World
• mConj : World

@[implicit_reducible]

instance HardingGerstenbergIcard2025.LateMeeting.instDecidableEqWorld : DecidableEq World

Equations

• HardingGerstenbergIcard2025.LateMeeting.instDecidableEqWorld x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance HardingGerstenbergIcard2025.LateMeeting.instFintypeWorld : Fintype World

Equations

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

def HardingGerstenbergIcard2025.LateMeeting.instReprWorld.repr : World → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance HardingGerstenbergIcard2025.LateMeeting.instReprWorld : Repr World

Equations

• HardingGerstenbergIcard2025.LateMeeting.instReprWorld = { reprPrec := HardingGerstenbergIcard2025.LateMeeting.instReprWorld.repr }

@[reducible]

noncomputable def HardingGerstenbergIcard2025.LateMeeting.modelOf : World → Core.Causal.BoolSEM V

Per-world structural model (pattern match unfolds by iota).

Equations

• HardingGerstenbergIcard2025.LateMeeting.modelOf HardingGerstenbergIcard2025.LateMeeting.World.mT = HardingGerstenbergIcard2025.LateMeeting.semT
• HardingGerstenbergIcard2025.LateMeeting.modelOf HardingGerstenbergIcard2025.LateMeeting.World.mConj = HardingGerstenbergIcard2025.LateMeeting.semConj

@[implicit_reducible]

noncomputable instance HardingGerstenbergIcard2025.LateMeeting.instIsDeterministicVBoolModelOf (w : World) : Core.Causal.SEM.IsDeterministic (modelOf w)

Equations

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

instance HardingGerstenbergIcard2025.LateMeeting.instIsDAGVGraphBoolModelOf (w : World) : (modelOf w).graph.IsDAG

noncomputable def HardingGerstenbergIcard2025.LateMeeting.game : ExplanationGame V World

Equations

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

theorem HardingGerstenbergIcard2025.LateMeeting.T_manipulates_in_mT : game.worldManipulates V.T World.mT

Tardiness manipulates crossness in the actual world (M_T).

theorem HardingGerstenbergIcard2025.LateMeeting.B_doesnt_manipulate_in_mT : ¬game.worldManipulates V.B World.mT

Forgotten birthday does NOT manipulate crossness in M_T (B doesn't appear in C's mechanism in M_T).

theorem HardingGerstenbergIcard2025.LateMeeting.T_manipulates_in_mConj : game.worldManipulates V.T World.mConj

Tardiness manipulates crossness in M_∧ (with B = 1 fixed by lateBg).

theorem HardingGerstenbergIcard2025.LateMeeting.B_manipulates_in_mConj : game.worldManipulates V.B World.mConj

Forgotten birthday manipulates crossness in M_∧ (with T = 1 fixed by lateBg, flipping B flips C from true to false).

theorem HardingGerstenbergIcard2025.LateMeeting.msg_T_true_in_mT : game.meaning { cause := V.T } World.mT

The "because T" message is true at the actual world M_T: T = 1 is an actual cause of C = 1 there.

theorem HardingGerstenbergIcard2025.LateMeeting.msg_T_true_in_mConj : game.meaning { cause := V.T } World.mConj

The "because T" message is also true at M_∧: T = 1 is an actual cause of C = 1 (with B = 1 fixed by lateBg, flipping T flips C).

theorem HardingGerstenbergIcard2025.LateMeeting.B_not_butFor_at_lateBg : ¬semT.completesForEffectOn lmVarList lateBg 1 V.B V.C

B is not but-for C in M_T even at the actual context lateBg: flipping B from 1 to 0 leaves C at true, since semT's mechanism for C reads only T. (The full ¬ meaning ⟨B⟩ mT claim — that NO witness valuation makes B but-for C — requires a witness-irrelevance lemma about C's parent set; deferred.)

Two potential causes (R = thatched roof, D = drought) of one effect (F = fire). K = {(M_R, u), (M_D, u), (M_∧, u), (M_∨, u)} where u = (R = 1, D = 1). The framework predicts that under the actual structure M_R, citing R "tracks" F's manipulation more reliably than citing D — even though both are equally informative under the bare manipulation game (a downstream-relevant decision such as "what to repair" breaks the tie).

inductive HardingGerstenbergIcard2025.RoofReplacement.V : Type

• R : V
• D : V
• F : V

@[implicit_reducible]

instance HardingGerstenbergIcard2025.RoofReplacement.instDecidableEqV : DecidableEq V

Equations

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

@[implicit_reducible]

instance HardingGerstenbergIcard2025.RoofReplacement.instFintypeV : Fintype V

Equations

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

@[implicit_reducible]

instance HardingGerstenbergIcard2025.RoofReplacement.instReprV : Repr V

Equations

• HardingGerstenbergIcard2025.RoofReplacement.instReprV = { reprPrec := HardingGerstenbergIcard2025.RoofReplacement.instReprV.repr }

def HardingGerstenbergIcard2025.RoofReplacement.instReprV.repr : V → ℕ → Std.Format

Equations

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

def HardingGerstenbergIcard2025.RoofReplacement.roofVarList : List V

Equations

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

def HardingGerstenbergIcard2025.RoofReplacement.graphR : Core.Causal.CausalGraph V

Equations

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

def HardingGerstenbergIcard2025.RoofReplacement.graphD : Core.Causal.CausalGraph V

Equations

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

def HardingGerstenbergIcard2025.RoofReplacement.graphRD : Core.Causal.CausalGraph V

Equations

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

noncomputable def HardingGerstenbergIcard2025.RoofReplacement.semR : Core.Causal.BoolSEM V

Equations

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

noncomputable def HardingGerstenbergIcard2025.RoofReplacement.semD : Core.Causal.BoolSEM V

Equations

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

noncomputable def HardingGerstenbergIcard2025.RoofReplacement.semConj : Core.Causal.BoolSEM V

Equations

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

noncomputable def HardingGerstenbergIcard2025.RoofReplacement.semDisj : Core.Causal.BoolSEM V

Equations

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

@[implicit_reducible]

noncomputable instance HardingGerstenbergIcard2025.RoofReplacement.instIsDeterministicVBoolSemR : Core.Causal.SEM.IsDeterministic semR

Equations

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

@[implicit_reducible]

noncomputable instance HardingGerstenbergIcard2025.RoofReplacement.instIsDeterministicVBoolSemD : Core.Causal.SEM.IsDeterministic semD

Equations

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

@[implicit_reducible]

noncomputable instance HardingGerstenbergIcard2025.RoofReplacement.instIsDeterministicVBoolSemConj : Core.Causal.SEM.IsDeterministic semConj

Equations

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

@[implicit_reducible]

noncomputable instance HardingGerstenbergIcard2025.RoofReplacement.instIsDeterministicVBoolSemDisj : Core.Causal.SEM.IsDeterministic semDisj

Equations

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

instance HardingGerstenbergIcard2025.RoofReplacement.instIsDAGVGraphBoolSemR : semR.graph.IsDAG

instance HardingGerstenbergIcard2025.RoofReplacement.instIsDAGVGraphBoolSemD : semD.graph.IsDAG

instance HardingGerstenbergIcard2025.RoofReplacement.instIsDAGVGraphBoolSemConj : semConj.graph.IsDAG

instance HardingGerstenbergIcard2025.RoofReplacement.instIsDAGVGraphBoolSemDisj : semDisj.graph.IsDAG

def HardingGerstenbergIcard2025.RoofReplacement.roofBg : Core.Causal.Valuation fun (x : V) => Bool

Equations

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

inductive HardingGerstenbergIcard2025.RoofReplacement.World : Type

• mR : World
• mD : World
• mConj : World
• mDisj : World

@[implicit_reducible]

instance HardingGerstenbergIcard2025.RoofReplacement.instDecidableEqWorld : DecidableEq World

Equations

• HardingGerstenbergIcard2025.RoofReplacement.instDecidableEqWorld x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance HardingGerstenbergIcard2025.RoofReplacement.instFintypeWorld : Fintype World

Equations

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

def HardingGerstenbergIcard2025.RoofReplacement.instReprWorld.repr : World → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance HardingGerstenbergIcard2025.RoofReplacement.instReprWorld : Repr World

Equations

• HardingGerstenbergIcard2025.RoofReplacement.instReprWorld = { reprPrec := HardingGerstenbergIcard2025.RoofReplacement.instReprWorld.repr }

@[reducible]

noncomputable def HardingGerstenbergIcard2025.RoofReplacement.modelOf : World → Core.Causal.BoolSEM V

Equations

• HardingGerstenbergIcard2025.RoofReplacement.modelOf HardingGerstenbergIcard2025.RoofReplacement.World.mR = HardingGerstenbergIcard2025.RoofReplacement.semR
• HardingGerstenbergIcard2025.RoofReplacement.modelOf HardingGerstenbergIcard2025.RoofReplacement.World.mD = HardingGerstenbergIcard2025.RoofReplacement.semD
• HardingGerstenbergIcard2025.RoofReplacement.modelOf HardingGerstenbergIcard2025.RoofReplacement.World.mConj = HardingGerstenbergIcard2025.RoofReplacement.semConj
• HardingGerstenbergIcard2025.RoofReplacement.modelOf HardingGerstenbergIcard2025.RoofReplacement.World.mDisj = HardingGerstenbergIcard2025.RoofReplacement.semDisj

@[implicit_reducible]

noncomputable instance HardingGerstenbergIcard2025.RoofReplacement.instIsDeterministicVBoolModelOf (w : World) : Core.Causal.SEM.IsDeterministic (modelOf w)

Equations

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

instance HardingGerstenbergIcard2025.RoofReplacement.instIsDAGVGraphBoolModelOf (w : World) : (modelOf w).graph.IsDAG

noncomputable def HardingGerstenbergIcard2025.RoofReplacement.game : ExplanationGame V World

Equations

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

theorem HardingGerstenbergIcard2025.RoofReplacement.R_manipulates_in_mR : game.worldManipulates V.R World.mR

R manipulates F in M_R (the actual structure).

theorem HardingGerstenbergIcard2025.RoofReplacement.R_doesnt_manipulate_in_mD : ¬game.worldManipulates V.R World.mD

R does NOT manipulate F in M_D (only D matters there).

theorem HardingGerstenbergIcard2025.RoofReplacement.R_manipulates_in_mConj : game.worldManipulates V.R World.mConj

R manipulates F in M_∧ (both are needed; with D = 1 fixed, R is but-for).

theorem HardingGerstenbergIcard2025.RoofReplacement.R_doesnt_manipulate_in_mDisj : ¬game.worldManipulates V.R World.mDisj

R does NOT manipulate F in M_∨ at the actual context (overdetermination: D = 1 alone fires F regardless of R).

theorem HardingGerstenbergIcard2025.RoofReplacement.D_manipulates_in_mD : game.worldManipulates V.D World.mD

D manipulates F in M_D (the symmetric case).

Single causal model M_∨: M ← Ch ∨ Da. K varies over the exogenous context: u_C (Charlie alone), u_D (Dana alone), u_{C,D} (both). Actual world: u_{C,D}. Predicts overdetermination: in u_{C,D}, neither single variable manipulates M. The conjunctive message "Ch ∧ Da" would be needed to manipulate M as a joint intervention — the action set must include subsets of V; deferred.

inductive HardingGerstenbergIcard2025.MilkTheft.V : Type

• Ch : V
• Da : V
• M : V

@[implicit_reducible]

instance HardingGerstenbergIcard2025.MilkTheft.instDecidableEqV : DecidableEq V

Equations

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

@[implicit_reducible]

instance HardingGerstenbergIcard2025.MilkTheft.instFintypeV : Fintype V

Equations

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

@[implicit_reducible]

instance HardingGerstenbergIcard2025.MilkTheft.instReprV : Repr V

Equations

• HardingGerstenbergIcard2025.MilkTheft.instReprV = { reprPrec := HardingGerstenbergIcard2025.MilkTheft.instReprV.repr }

def HardingGerstenbergIcard2025.MilkTheft.instReprV.repr : V → ℕ → Std.Format

Equations

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

def HardingGerstenbergIcard2025.MilkTheft.milkVarList : List V

Equations

• HardingGerstenbergIcard2025.MilkTheft.milkVarList = [HardingGerstenbergIcard2025.MilkTheft.V.Ch, HardingGerstenbergIcard2025.MilkTheft.V.Da, HardingGerstenbergIcard2025.MilkTheft.V.M]

def HardingGerstenbergIcard2025.MilkTheft.milkGraph : Core.Causal.CausalGraph V

Equations

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

noncomputable def HardingGerstenbergIcard2025.MilkTheft.semDisj : Core.Causal.BoolSEM V

Equations

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

@[implicit_reducible]

noncomputable instance HardingGerstenbergIcard2025.MilkTheft.instIsDeterministicVBoolSemDisj : Core.Causal.SEM.IsDeterministic semDisj

Equations

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

instance HardingGerstenbergIcard2025.MilkTheft.instIsDAGVGraphBoolSemDisj : semDisj.graph.IsDAG

def HardingGerstenbergIcard2025.MilkTheft.bgC : Core.Causal.Valuation fun (x : V) => Bool

Equations

• HardingGerstenbergIcard2025.MilkTheft.bgC = (Core.Causal.Valuation.empty.extend HardingGerstenbergIcard2025.MilkTheft.V.Ch true).extend HardingGerstenbergIcard2025.MilkTheft.V.Da false

def HardingGerstenbergIcard2025.MilkTheft.bgD : Core.Causal.Valuation fun (x : V) => Bool

Equations

• HardingGerstenbergIcard2025.MilkTheft.bgD = (Core.Causal.Valuation.empty.extend HardingGerstenbergIcard2025.MilkTheft.V.Ch false).extend HardingGerstenbergIcard2025.MilkTheft.V.Da true

def HardingGerstenbergIcard2025.MilkTheft.bgBoth : Core.Causal.Valuation fun (x : V) => Bool

Equations

• HardingGerstenbergIcard2025.MilkTheft.bgBoth = (Core.Causal.Valuation.empty.extend HardingGerstenbergIcard2025.MilkTheft.V.Ch true).extend HardingGerstenbergIcard2025.MilkTheft.V.Da true

inductive HardingGerstenbergIcard2025.MilkTheft.World : Type

• uC : World
• uD : World
• uBoth : World

@[implicit_reducible]

instance HardingGerstenbergIcard2025.MilkTheft.instDecidableEqWorld : DecidableEq World

Equations

• HardingGerstenbergIcard2025.MilkTheft.instDecidableEqWorld x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance HardingGerstenbergIcard2025.MilkTheft.instFintypeWorld : Fintype World

Equations

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

@[implicit_reducible]

instance HardingGerstenbergIcard2025.MilkTheft.instReprWorld : Repr World

Equations

• HardingGerstenbergIcard2025.MilkTheft.instReprWorld = { reprPrec := HardingGerstenbergIcard2025.MilkTheft.instReprWorld.repr }

def HardingGerstenbergIcard2025.MilkTheft.instReprWorld.repr : World → ℕ → Std.Format

Equations

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

@[reducible]

noncomputable def HardingGerstenbergIcard2025.MilkTheft.modelOf : World → Core.Causal.BoolSEM V

Equations

• HardingGerstenbergIcard2025.MilkTheft.modelOf x✝ = HardingGerstenbergIcard2025.MilkTheft.semDisj

@[reducible]

def HardingGerstenbergIcard2025.MilkTheft.contextOf : World → Core.Causal.Valuation fun (x : V) => Bool

Equations

• HardingGerstenbergIcard2025.MilkTheft.contextOf HardingGerstenbergIcard2025.MilkTheft.World.uC = HardingGerstenbergIcard2025.MilkTheft.bgC
• HardingGerstenbergIcard2025.MilkTheft.contextOf HardingGerstenbergIcard2025.MilkTheft.World.uD = HardingGerstenbergIcard2025.MilkTheft.bgD
• HardingGerstenbergIcard2025.MilkTheft.contextOf HardingGerstenbergIcard2025.MilkTheft.World.uBoth = HardingGerstenbergIcard2025.MilkTheft.bgBoth

@[implicit_reducible]

noncomputable instance HardingGerstenbergIcard2025.MilkTheft.instIsDeterministicVBoolModelOf (w : World) : Core.Causal.SEM.IsDeterministic (modelOf w)

Equations

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

instance HardingGerstenbergIcard2025.MilkTheft.instIsDAGVGraphBoolModelOf (w : World) : (modelOf w).graph.IsDAG

noncomputable def HardingGerstenbergIcard2025.MilkTheft.game : ExplanationGame V World

Equations

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

theorem HardingGerstenbergIcard2025.MilkTheft.Ch_manipulates_in_uC : game.worldManipulates V.Ch World.uC

Charlie manipulates M when only Charlie drank (u_C).

theorem HardingGerstenbergIcard2025.MilkTheft.Da_doesnt_manipulate_in_uC : ¬game.worldManipulates V.Da World.uC

Dana does NOT manipulate M when only Charlie drank (Dana = 0 in u_C).

theorem HardingGerstenbergIcard2025.MilkTheft.Ch_doesnt_manipulate_in_uBoth : ¬game.worldManipulates V.Ch World.uBoth

Overdetermination: Charlie does NOT manipulate M when both drank (Da = 1 still fires M regardless of Ch). The paper's Milk-Theft point.

theorem HardingGerstenbergIcard2025.MilkTheft.Da_doesnt_manipulate_in_uBoth : ¬game.worldManipulates V.Da World.uBoth

Symmetric overdetermination: Dana does NOT manipulate M when both drank.

theorem HardingGerstenbergIcard2025.MilkTheft.msg_Ch_true_in_uC : game.meaning { cause := V.Ch } World.uC

"Charlie because M" is true at u_C: Charlie's drinking actually caused M (sole cause; lateBg-as-witness suffices).

theorem HardingGerstenbergIcard2025.MilkTheft.msg_Ch_true_in_uBoth : game.meaning { cause := V.Ch } World.uBoth

HP-style actual cause via off-actual witness: Charlie IS an actual cause of M at u_{C,D} despite not being but-for there. Witness: bgC (sets Da = false off-actual), where Charlie becomes but-for.