Causative Construction Selection (CC-Selection)

@cite{baglini-bar-asher-siegal-2020} @cite{baglini-bar-asher-siegal-2025} @cite{bar-asher-siegal-2026}

CC-selection is the mechanism by which causative constructions constrain which element of a causal model can be linguistically realized as "the cause."

Two modes:

• memberOfSufficientSet (verb cause): any necessary condition
• completionOfSufficientSet (CoS verbs like open): the completing condition

The legacy CausalDynamics-based completesForEffect, ccConstraintSatisfied, typeLevelSufficiency, tokenLevelCausation, actualizationHolds, CausalDependency were deleted in Phase D-H. The polymorphic V2 versions are promoted to canonical here.

inductive Semantics.Causation.CCSelection.CCSelectionMode : Type

How a causative construction selects its cause from a causal model.

• memberOfSufficientSet : CCSelectionMode
• completionOfSufficientSet : CCSelectionMode

def Semantics.Causation.CCSelection.instReprCCSelectionMode.repr : CCSelectionMode → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Semantics.Causation.CCSelection.instReprCCSelectionMode : Repr CCSelectionMode

Equations

• Semantics.Causation.CCSelection.instReprCCSelectionMode = { reprPrec := Semantics.Causation.CCSelection.instReprCCSelectionMode.repr }

@[implicit_reducible]

instance Semantics.Causation.CCSelection.instDecidableEqCCSelectionMode : DecidableEq CCSelectionMode

Equations

• Semantics.Causation.CCSelection.instDecidableEqCCSelectionMode x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

noncomputable def Semantics.Causation.CCSelection.completesForEffect {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] (background : Core.Causal.Valuation α) (cause : V) (xC xC_alt : α cause) (effect : V) (xE : α effect) : Prop

V2 completesForEffect: cause-as-xC develops effect-as-xE; cause-as-xC_alt does not. Polymorphic but-for completion check. Bool models pass xC = xE = true, xC_alt = false.

Equations

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

@[implicit_reducible]

noncomputable instance Semantics.Causation.CCSelection.instDecidableCompletesForEffect {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 α) (cause : V) (xC xC_alt : α cause) (effect : V) (xE : α effect) : Decidable (completesForEffect M bg cause xC xC_alt effect xE)

Equations

• Semantics.Causation.CCSelection.instDecidableCompletesForEffect M bg cause xC xC_alt effect xE = Classical.dec (Semantics.Causation.CCSelection.completesForEffect M bg cause xC xC_alt effect xE)

@[reducible, inline]

abbrev Semantics.Causation.CCSelection.actualizationHolds {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 α) (cause : V) (xC xC_alt : α cause) (effect : V) (xE : α effect) : Prop

actualizationHolds: alias for completesForEffect.

Equations

• Semantics.Causation.CCSelection.actualizationHolds M bg cause xC xC_alt effect xE = Semantics.Causation.CCSelection.completesForEffect M bg cause xC xC_alt effect xE