Documentation

Linglib.Theories.Semantics.Causation.Prevention

Prevention Semantics #

@cite{sloman-barbey-hotaling-2009}

preventSem formalizes the SEM semantics of "prevent": the preventer blocks an effect that would otherwise occur. Behavioral, not structural: setting preventer := xPrev blocks effect = xE, AND there exists some alternative preventer value that would have allowed effect = xE to develop.

Bool models recover the standard "false vs true" flip via the ∃ xPrev_alt ≠ xPrev clause (with xPrev = true, the only alternative is false).

The legacy structural preventSem over CausalDynamics (which introspected an inhibitory law's structure rather than checking behavior) was deleted in Phase D-H. The behavioral V2 form here is arity-uniform with causallySufficient/causeSem so Causative.toSemantics dispatches uniformly across all five force-dynamic variants.

source
noncomputable def Semantics.Causation.Prevention.preventSem {V : Type u_1} {α : V → Type u_2} [Fintype V] [DecidableEq V] [Core.Causal.DecidableValuation α] (M : Core.Causal.SEM V α) [M.graph.IsDAG] [M.IsDeterministic] (bg : Core.Causal.Valuation α) (preventer : V) (xPrev : α preventer) (effect : V) (xE : α effect) :
Prop

V2 prevention semantics: preventer-as-xPrev blocks effect-from- being-xE, AND there exists some alternative preventer value that would have allowed effect = xE to develop. Polymorphic over value types.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[implicit_reducible]
    noncomputable instance Semantics.Causation.Prevention.instDecidablePreventSem {V : Type u_1} {α : V → Type u_2} [Fintype V] [DecidableEq V] [Core.Causal.DecidableValuation α] (M : Core.Causal.SEM V α) [M.graph.IsDAG] [M.IsDeterministic] (bg : Core.Causal.Valuation α) (preventer : V) (xP : α preventer) (effect : V) (xE : α effect) :
    Decidable (preventSem M bg preventer xP effect xE)
    Equations