Causative Construction Selection (CC-Selection)

[BBS20] [BBS25] [BS26b]

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 Causation.CCSelection.CCSelectionMode : Type

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

• memberOfSufficientSet : CCSelectionMode
• completionOfSufficientSet : CCSelectionMode

@[implicit_reducible]

instance Causation.CCSelection.instReprCCSelectionMode : Repr CCSelectionMode

Equations

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

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

Equations

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

@[implicit_reducible]

instance Causation.CCSelection.instDecidableEqCCSelectionMode : DecidableEq CCSelectionMode

Equations

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

noncomputable def Causation.CCSelection.completesForEffect {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 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

• Causation.CCSelection.completesForEffect M background cause xC xC_alt effect xE = (M.causallySufficient background cause xC effect xE ∧ ¬M.causallySufficient background cause xC_alt effect xE)

@[implicit_reducible]

noncomputable instance Causation.CCSelection.instDecidableCompletesForEffect {V : Type u_1} {α : V → Type u_2} [Fintype V] [DecidableEq V] [DecidableValuation α] (M : SEM V α) [M.graph.IsDAG] [M.IsDeterministic] (bg : Valuation α) (cause : V) (xC xC_alt : α cause) (effect : V) (xE : α effect) : Decidable (completesForEffect M bg cause xC xC_alt effect xE)

Equations

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

theorem Causation.CCSelection.completesForEffect_of_developDetOn {V : Type u_1} [Fintype V] [DecidableEq V] {M : BoolSEM V} [M.graph.IsDAG] [SEM.IsDeterministic M] {bg : Valuation fun (x : V) => Bool} {c e : V} (vs : List V) (n : ℕ) (h1 : (SEM.developDetOn M vs n (bg.extend c true)).hasValue e true) (h2 : (SEM.developDetOn M vs n (bg.extend c false)).hasValue e false) : completesForEffect M bg c true false e true

Bool-model bridge: prove canonical completesForEffect from a pair of developDetOn computations (cause-on develops the effect true; cause-off develops it false). The computations close by decide.

theorem Causation.CCSelection.not_completesForEffect_of_developDetOn {V : Type u_1} [Fintype V] [DecidableEq V] {M : BoolSEM V} [M.graph.IsDAG] [SEM.IsDeterministic M] {bg : Valuation fun (x : V) => Bool} {c e : V} (vs : List V) (n : ℕ) (h1 : (SEM.developDetOn M vs n (bg.extend c true)).hasValue e false) : ¬completesForEffect M bg c true false e true

Bool-model bridge, negative: the sufficiency half fails — the cause-on development reaches the effect false, so no completion.