Documentation

Linglib.Semantics.Causation.Sufficiency

Causal Sufficiency #

[NL20] [Sch11b]

Causal sufficiency semantics for the verb "make" based on [NL20] Definition 23.

Insight #

"X made Y happen" asserts that X was sufficient for Y: given the background situation, adding X guarantees Y. The effect is inevitable once the cause is in place.

Formalization #

makeSem is a polymorphic alias of SEM.causallySufficient over the V2 SEM V α substrate. Bool models pass xC = xE = true at the call site; multi-valued models supply genuine values.

The legacy CausalDynamics-based makeSem (with disjunctive_each_sufficient, conjunctive_neither_sufficient_alone, conjunctive_sufficient_with_other helper theorems over applyLawsOnce) was deleted in Phase D-H. The qualitative claims are recoverable via concrete BoolSEM models in study files (e.g., Levin2026.HammerFlat).

source
def Causation.Sufficiency.makeSem {V : Type u_1} {α : V → Type u_2} [Fintype V] [DecidableEq V] [DecidableValuation α] (M : SEM V α) [M.graph.IsDAG] [M.IsDeterministic] (background : Valuation α) (cause : V) (xC : α cause) (effect : V) (xE : α effect) :
Prop

V2 sufficiency for "make" ([NL20] Definition 23, both clauses, over the strict T_D development):

  • (a) non-inevitability: the development of background does not already fix effect = xE;
  • (b) sufficiency: the development of background + (cause = xC) fixes effect = xE.

Bool models pass xC = xE = true at the call site. The bare clause-(b)-only predicate (over the eager-total development) remains available as SEM.causallySufficient.

Equations
Instances For
    source
    @[implicit_reducible]
    noncomputable instance Causation.Sufficiency.instDecidableMakeSem {V : Type u_1} {α : V → Type u_2} [Fintype V] [DecidableEq V] [DecidableValuation α] (M : SEM V α) [M.graph.IsDAG] [M.IsDeterministic] (background : Valuation α) (cause : V) (xC : α cause) (effect : V) (xE : α effect) :
    Decidable (makeSem M background cause xC effect xE)
    Equations