Linglib.Theories.Semantics.Causation.Examples

"The lightning caused the fire" is true when only lightning is present: without lightning, no fire. Under @cite{nadathur-2024} Def 10b, the background must NOT include the cause; instead, the arsonist's absence is encoded directly.

source

theorem NadathurLauer2020.Examples.lightning_not_necessary_overdetermination :

Core.StructuralEquationModel.causallyNecessary fireDynamics bothCausesBackground lightning fire = false

Lightning is NOT necessary in overdetermination.

"The lightning caused the fire" is FALSE when both causes are present: without lightning, arsonist would have caused the fire anyway.

This is the key overdetermination result!

source

theorem NadathurLauer2020.Examples.arsonist_not_necessary_overdetermination :

Core.StructuralEquationModel.causallyNecessary fireDynamics bothCausesBackground arsonist fire = false

Arsonist is NOT necessary in overdetermination.

Symmetrically, arsonist isn't necessary when lightning is also present.

source

theorem NadathurLauer2020.Examples.overdetermination_make_not_cause :

Sufficiency.makeSem fireDynamics bothCausesBackground lightning fire = true ∧ Necessity.causeSem fireDynamics bothCausesBackground lightning fire = false

Overdetermination: "make" but NOT "cause"

In the overdetermination scenario:

"The lightning made the fire start" is TRUE (sufficiency)
"The lightning caused the fire" is FALSE (necessity fails)

This demonstrates the semantic difference between "make" and "cause".

source

theorem NadathurLauer2020.Examples.solo_make_and_cause :

have soloContext := Core.StructuralEquationModel.Situation.empty.extend arsonist false; Sufficiency.makeSem fireDynamics soloContext lightning fire = true ∧ Necessity.causeSem fireDynamics soloContext lightning fire = true

Solo cause: both "make" AND "cause"

When lightning is the only cause:

"The lightning made the fire start" is TRUE
"The lightning caused the fire" is TRUE

Both verbs are felicitous when there's no overdetermination. Under @cite{nadathur-2024} Def 10b, the background encodes the arsonist's absence rather than the lightning's presence.

source

theorem NadathurLauer2020.Examples.overdetermination_not_actually_caused :

Necessity.actuallyCaused fireDynamics bothCausesBackground lightning fire = false

Actual causation in overdetermination: lightning did NOT actually cause the fire when the arsonist is also present — actuallyCaused returns false because necessity fails (the arsonist backup blocks it).

source

theorem NadathurLauer2020.Examples.solo_actually_caused :

have soloSituation := (Core.StructuralEquationModel.Situation.empty.extend lightning true).extend arsonist false; Necessity.actuallyCaused fireDynamics soloSituation lightning fire = true

Actual causation as sole cause: when lightning is the only cause, actuallyCaused holds — lightning both occurred and was necessary.

source

def NadathurLauer2020.Examples.shortCircuit :

Core.StructuralEquationModel.Variable

Short circuit variable

Equations

NadathurLauer2020.Examples.shortCircuit = Core.StructuralEquationModel.mkVar "short_circuit"

Instances For

source

def NadathurLauer2020.Examples.buildingFire :

Core.StructuralEquationModel.Variable

Building fire variable

Equations

NadathurLauer2020.Examples.buildingFire = Core.StructuralEquationModel.mkVar "building_fire"

Instances For

source

def NadathurLauer2020.Examples.circuitDynamics :

Core.StructuralEquationModel.CausalDynamics

Circuit dynamics: short circuit causes fire.

Simple causation: one cause, one effect.

Equations

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

Instances For

source

def NadathurLauer2020.Examples.circuitBackground :

Core.StructuralEquationModel.Situation

Background where short circuit occurred.

Equations

NadathurLauer2020.Examples.circuitBackground = Core.StructuralEquationModel.Situation.empty.extend NadathurLauer2020.Examples.shortCircuit true

Instances For

source

theorem NadathurLauer2020.Examples.circuit_sufficient :

Core.StructuralEquationModel.causallySufficient circuitDynamics Core.StructuralEquationModel.Situation.empty shortCircuit buildingFire = true

Short circuit is sufficient for fire.

source

theorem NadathurLauer2020.Examples.circuit_necessary :

Core.StructuralEquationModel.causallyNecessary circuitDynamics Core.StructuralEquationModel.Situation.empty shortCircuit buildingFire = true

Short circuit is necessary for fire (when it's the only cause).

source

theorem NadathurLauer2020.Examples.circuit_both_verbs :

Sufficiency.makeSem circuitDynamics Core.StructuralEquationModel.Situation.empty shortCircuit buildingFire = true ∧ Necessity.causeSem circuitDynamics Core.StructuralEquationModel.Situation.empty shortCircuit buildingFire = true

Both "make" and "cause" are true for simple causation.

source

theorem NadathurLauer2020.Examples.circuit_actually_caused :

Necessity.actuallyCaused circuitDynamics circuitBackground shortCircuit buildingFire = true

Actual causation: short circuit actually caused the fire.

The short circuit occurred and was necessary — actuallyCaused holds.

source

def NadathurLauer2020.Examples.flip :

Core.StructuralEquationModel.Variable

Initial cause

Equations

NadathurLauer2020.Examples.flip = Core.StructuralEquationModel.mkVar "flip"

Instances For

source

def NadathurLauer2020.Examples.switch :

Core.StructuralEquationModel.Variable

Intermediate event

Equations

NadathurLauer2020.Examples.switch = Core.StructuralEquationModel.mkVar "switch"

Instances For

source

def NadathurLauer2020.Examples.light :

Core.StructuralEquationModel.Variable

Final effect

Equations

NadathurLauer2020.Examples.light = Core.StructuralEquationModel.mkVar "light"

Instances For

source

def NadathurLauer2020.Examples.chainDynamics :

Core.StructuralEquationModel.CausalDynamics

Chain dynamics: flip → switch → light

Causal chain: initial cause triggers intermediate which triggers final effect.

Equations

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

Instances For

source

def NadathurLauer2020.Examples.chainBackground :

Core.StructuralEquationModel.Situation

Background where flip occurred.

Equations

NadathurLauer2020.Examples.chainBackground = Core.StructuralEquationModel.Situation.empty.extend NadathurLauer2020.Examples.flip true

Instances For

source

theorem NadathurLauer2020.Examples.chain_sufficient :

Core.StructuralEquationModel.causallySufficient chainDynamics Core.StructuralEquationModel.Situation.empty flip light = true

Flip is sufficient for light (through the chain).

source

theorem NadathurLauer2020.Examples.chain_root_not_necessary :

Core.StructuralEquationModel.causallyNecessary chainDynamics Core.StructuralEquationModel.Situation.empty flip light = false

Under @cite{nadathur-2024} Def 10b, the initial cause in a chain is NOT necessary for the final effect: the intermediate (switch) can be set directly, bypassing the root cause. This is correct for Def 10b's intended domain (prerequisites for complements) where the cause variable is the only path to the effect.

source

theorem NadathurLauer2020.Examples.chain_intermediate_result :

have background := (Core.StructuralEquationModel.Situation.empty.extend flip true).extend switch true; Core.StructuralEquationModel.causallyNecessary chainDynamics background switch light = false

Switch is also necessary for light (as intermediate).

Note: The chain dynamics flip → switch → light means switch depends on flip. When we test necessity of switch, we set switch=false and check if light still happens. But flip=true triggers switch=true again through the dynamics, so this is subtle.

In this model, with flip already in background, removing switch doesn't help because flip will re-trigger switch. This shows the interaction between necessity testing and causal chains.

source

def NadathurLauer2020.Examples.oxygen :

Core.StructuralEquationModel.Variable

Oxygen

Equations