Bar-Asher Siegal 2026: causation and causal relations

A review of how natural language encodes causation, from causative constructions and conditionals to discourse coherence and the progressive, arguing that language is evidence for the architecture of causal cognition. Its central proposal takes causal knowledge to be a structural equation model in which several sets of conditions are each sufficient for an effect: the door of Figure 1 opens when the handle is turned with the lock off, or when the circuit is closed with the power on and the lock off. Causative constructions then differ in which condition they may select as the cause. A change-of-state verb selects the temporally final condition of a sufficient set, cause selects any of its conditions, and both select only from the one sufficient set completed in the world of evaluation. Fodor's entailment from Sam opened the door to Sam caused the door to open follows, its converse fails, and when two sufficient sets are completed at once neither construction applies.

Implementation notes

The door is a causal model whose exogenous variables (handle, lock, power, button) read the context, and situations are observations. Sufficient sets and the two selection constraints are stated over the Kleene development of an observation (CausalModel.Forced), after [BBS25].

References

• [BS26b]
• [BBS25]
• [Fod70]

Sufficient sets and selection

def BarAsherSiegal2026.IsSufficientSet {U : Type u_1} {W : Type u_2} {α : W → Type u_3} (M : CausalModel U W α) [M.IsAcyclic] (S : (v : W) → Flat (α v)) (effect : W) (xE : α effect) : Prop

A sufficient set for effect = xE is a situation not settling the effect that forces it.

Equations

• BarAsherSiegal2026.IsSufficientSet M S effect xE = (S effect = ⊥ ∧ M.Forced S effect xE)

def BarAsherSiegal2026.IsMinimalSufficientSet {U : Type u_1} {W : Type u_2} {α : W → Type u_3} [DecidableEq W] (M : CausalModel U W α) [M.IsAcyclic] (S : (v : W) → Flat (α v)) (effect : W) (xE : α effect) : Prop

A sufficient set each of whose conditions is necessary within it.

Equations

• BarAsherSiegal2026.IsMinimalSufficientSet M S effect xE = (BarAsherSiegal2026.IsSufficientSet M S effect xE ∧ ∀ (v : W), S v ≠ ⊥ → ¬M.Forced (Function.update S v ⊥) effect xE)

def BarAsherSiegal2026.IsTheCompletedSet {U : Type u_1} {W : Type u_2} {α : W → Type u_3} [DecidableEq W] (M : CausalModel U W α) [M.IsAcyclic] (w S : (v : W) → Flat (α v)) (effect : W) (xE : α effect) : Prop

S is the only minimal sufficient set completed in the world w.

Equations

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

def BarAsherSiegal2026.SelectsMember {U : Type u_1} {W : Type u_2} {α : W → Type u_3} [DecidableEq W] (M : CausalModel U W α) [M.IsAcyclic] (w : (v : W) → Flat (α v)) (c effect : W) (xE : α effect) : Prop

The verb cause selects any condition of the completed sufficient set.

Equations

• BarAsherSiegal2026.SelectsMember M w c effect xE = ∃ (S : (v : W) → Flat (α v)), BarAsherSiegal2026.IsTheCompletedSet M w S effect xE ∧ S c ≠ ⊥

def BarAsherSiegal2026.SelectsFinal {U : Type u_1} {W : Type u_2} {α : W → Type u_3} [DecidableEq W] (M : CausalModel U W α) [M.IsAcyclic] (w : (v : W) → Flat (α v)) (time : W → ℕ) (c effect : W) (xE : α effect) : Prop

A change-of-state verb selects the temporally final condition of the completed sufficient set, time ordering the world's realizations.

Equations

• BarAsherSiegal2026.SelectsFinal M w time c effect xE = ∃ (S : (v : W) → Flat (α v)), BarAsherSiegal2026.IsTheCompletedSet M w S effect xE ∧ S c ≠ ⊥ ∧ ∀ (v : W), S v ≠ ⊥ → time v ≤ time c

theorem BarAsherSiegal2026.SelectsFinal.selectsMember {U : Type u_1} {W : Type u_2} {α : W → Type u_3} [DecidableEq W] {M : CausalModel U W α} [M.IsAcyclic] {effect : W} {xE : α effect} {w : (v : W) → Flat (α v)} {time : W → ℕ} {c : W} (h : SelectsFinal M w time c effect xE) : SelectsMember M w c effect xE

The change-of-state verb entails cause.

theorem BarAsherSiegal2026.not_selectsMember_of_two {U : Type u_1} {W : Type u_2} {α : W → Type u_3} [DecidableEq W] {M : CausalModel U W α} [M.IsAcyclic] {effect : W} {xE : α effect} {w S₁ S₂ : (v : W) → Flat (α v)} {c : W} (h₁ : IsMinimalSufficientSet M S₁ effect xE) (h₂ : IsMinimalSufficientSet M S₂ effect xE) (hne : S₁ ≠ S₂) (hw₁ : S₁ ≤ w) (hw₂ : S₂ ≤ w) : ¬SelectsMember M w c effect xE

Under overdetermination, two completed minimal sufficient sets leave nothing selectable.

@[instance_reducible]

instance BarAsherSiegal2026.instDecidableIsSufficientSet {U : Type u_1} {W : Type u_2} {α : W → Type u_3} [DecidableEq W] {M : CausalModel U W α} [M.IsAcyclic] {effect : W} {xE : α effect} [Fintype U] [Inhabited U] [(v : W) → Inhabited (α v)] [(v : W) → DecidableEq (α v)] [(v : W) → Fintype (α v)] [Fintype W] [DecidableRel M.graph.Adj] (S : (v : W) → Flat (α v)) : Decidable (IsSufficientSet M S effect xE)

Equations

• BarAsherSiegal2026.instDecidableIsSufficientSet S = { decide := decide (S effect = ⊥) && decide (M.Forced S effect xE), reflects_decide := ⋯ }

@[instance_reducible]

instance BarAsherSiegal2026.instDecidableIsMinimalSufficientSet {U : Type u_1} {W : Type u_2} {α : W → Type u_3} [DecidableEq W] {M : CausalModel U W α} [M.IsAcyclic] {effect : W} {xE : α effect} [Fintype U] [Inhabited U] [(v : W) → Inhabited (α v)] [(v : W) → DecidableEq (α v)] [(v : W) → Fintype (α v)] [Fintype W] [DecidableRel M.graph.Adj] (S : (v : W) → Flat (α v)) : Decidable (IsMinimalSufficientSet M S effect xE)

Equations

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

@[instance_reducible]

instance BarAsherSiegal2026.instDecidableIsTheCompletedSet {U : Type u_1} {W : Type u_2} {α : W → Type u_3} [DecidableEq W] {M : CausalModel U W α} [M.IsAcyclic] {effect : W} {xE : α effect} [Fintype U] [Inhabited U] [(v : W) → Inhabited (α v)] [(v : W) → DecidableEq (α v)] [(v : W) → Fintype (α v)] [Fintype W] [DecidableRel M.graph.Adj] (w S : (v : W) → Flat (α v)) : Decidable (IsTheCompletedSet M w S effect xE)

Equations

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

@[instance_reducible]

instance BarAsherSiegal2026.instDecidableSelectsMember {U : Type u_1} {W : Type u_2} {α : W → Type u_3} [DecidableEq W] {M : CausalModel U W α} [M.IsAcyclic] {effect : W} {xE : α effect} [Fintype U] [Inhabited U] [(v : W) → Inhabited (α v)] [(v : W) → DecidableEq (α v)] [(v : W) → Fintype (α v)] [Fintype W] [DecidableRel M.graph.Adj] (w : (v : W) → Flat (α v)) (c : W) : Decidable (SelectsMember M w c effect xE)

Equations

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

@[instance_reducible]

instance BarAsherSiegal2026.instDecidableSelectsFinal {U : Type u_1} {W : Type u_2} {α : W → Type u_3} [DecidableEq W] {M : CausalModel U W α} [M.IsAcyclic] {effect : W} {xE : α effect} [Fintype U] [Inhabited U] [(v : W) → Inhabited (α v)] [(v : W) → DecidableEq (α v)] [(v : W) → Fintype (α v)] [Fintype W] [DecidableRel M.graph.Adj] (w : (v : W) → Flat (α v)) (time : W → ℕ) (c : W) : Decidable (SelectsFinal M w time c effect xE)

Equations

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

The door of Figure 1

inductive BarAsherSiegal2026.V : Type

The variables of Figure 1.

• handle : V
• lock : V
• circuit : V
• electricity : V
• button : V
• doorOpens : V

@[instance_reducible]

instance BarAsherSiegal2026.instDecidableEqV : DecidableEq V

Equations

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

@[instance_reducible]

instance BarAsherSiegal2026.instFintypeV : Fintype V

Equations

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

@[instance_reducible]

instance BarAsherSiegal2026.instReprV : Repr V

Equations

• BarAsherSiegal2026.instReprV = { reprPrec := BarAsherSiegal2026.instReprV.repr }

def BarAsherSiegal2026.instReprV.repr : V → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• BarAsherSiegal2026.instReprV.repr BarAsherSiegal2026.V.lock prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "BarAsherSiegal2026.V.lock")).group prec✝

def BarAsherSiegal2026.edges : Finset (V × V)

The button closes the circuit; handle, lock, circuit and power bear on the door.

Equations

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

structure BarAsherSiegal2026.Context : Type

The context settles the handle, the lock, the power, and the button.

• handle : Bool
• lock : Bool
• electricity : Bool
• button : Bool

@[instance_reducible]

instance BarAsherSiegal2026.instDecidableEqContext : DecidableEq Context

Equations

• BarAsherSiegal2026.instDecidableEqContext = BarAsherSiegal2026.instDecidableEqContext.decEq

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

Equations

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

@[instance_reducible]

instance BarAsherSiegal2026.instFintypeContext : Fintype Context

Equations

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

@[instance_reducible]

instance BarAsherSiegal2026.instInhabitedContext : Inhabited Context

Equations

• BarAsherSiegal2026.instInhabitedContext = { default := BarAsherSiegal2026.instInhabitedContext.default }

def BarAsherSiegal2026.instReprContext.repr : Context → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance BarAsherSiegal2026.instReprContext : Repr Context

Equations

• BarAsherSiegal2026.instReprContext = { reprPrec := BarAsherSiegal2026.instReprContext.repr }

def BarAsherSiegal2026.model : CausalModel Context V fun (x : V) => Bool

The structural entailments G, H and I: the circuit closes when the button is pressed, and the door opens manually (handle on, lock off) or automatically (circuit and power on, lock off).

Equations

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

@[instance_reducible]

instance BarAsherSiegal2026.instDecidableRelVAdjGraphContextBoolModel : DecidableRel model.graph.Adj

Equations

• BarAsherSiegal2026.instDecidableRelVAdjGraphContextBoolModel w v = BarAsherSiegal2026.instDecidableRelVAdjGraphContextBoolModel._aux_1 w v

instance BarAsherSiegal2026.instIsAcyclicContextVBoolModel : model.IsAcyclic

def BarAsherSiegal2026.manual : V → Flat Bool

Sufficient set I: handle on, lock off.

Equations

• BarAsherSiegal2026.manual = Function.update (Function.update ⊥ BarAsherSiegal2026.V.lock ↑false) BarAsherSiegal2026.V.handle ↑true

def BarAsherSiegal2026.automatic : V → Flat Bool

Sufficient set H: circuit and power on, lock off.

Equations

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

def BarAsherSiegal2026.handleWorld : V → Flat Bool

The world in which the handle is turned on an unlocked, unpowered door.

Equations

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

def BarAsherSiegal2026.bothWorld : V → Flat Bool

The overdetermined world: handle turned and button pressed on a powered, unlocked door.

Equations

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

def BarAsherSiegal2026.time : V → ℕ

The lock was disengaged first, the handle turned last.

Equations

• BarAsherSiegal2026.time BarAsherSiegal2026.V.lock = 0
• BarAsherSiegal2026.time BarAsherSiegal2026.V.handle = 2
• BarAsherSiegal2026.time x✝ = 1

theorem BarAsherSiegal2026.manual_minimal : IsMinimalSufficientSet model manual V.doorOpens true

theorem BarAsherSiegal2026.automatic_minimal : IsMinimalSufficientSet model automatic V.doorOpens true

theorem BarAsherSiegal2026.handle_selectsFinal : SelectsFinal model handleWorld time V.handle V.doorOpens true

John opened the door, John caused the door to open: the handle is the final condition of the only completed set.

theorem BarAsherSiegal2026.handle_selectsMember : SelectsMember model handleWorld V.handle V.doorOpens true

theorem BarAsherSiegal2026.lock_selectsMember : SelectsMember model handleWorld V.lock V.doorOpens true

The converse of Fodor's entailment fails: the unlocked lock is a condition cause may select but not the final one.

theorem BarAsherSiegal2026.lock_not_selectsFinal : ¬SelectsFinal model handleWorld time V.lock V.doorOpens true

theorem BarAsherSiegal2026.overdetermined : ¬SelectsMember model bothWorld V.handle V.doorOpens true

With both sets completed, neither construction can select the handle.