Coercive Implication ([NL20])

"X made Y do Z" with volitional Z implies coercion: sufficiency (Z was determined) + volitionality (Y could choose otherwise) → Y's choice was overridden.

The legacy CausalDynamics-based CoerciveContext + Kim/Sandy examples were deleted in Phase D-H. The polymorphic V2 hasCoerciveImplication is promoted to canonical here.

inductive Causation.CoerciveImplication.ActionType : Type

Action volitionality (volitional/non-volitional/ambiguous).

• Volitional : ActionType
• NonVolitional : ActionType
• Ambiguous : ActionType

@[implicit_reducible]

instance Causation.CoerciveImplication.instDecidableEqActionType : DecidableEq ActionType

Equations

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

def Causation.CoerciveImplication.instReprActionType.repr : ActionType → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Causation.CoerciveImplication.instReprActionType : Repr ActionType

Equations

• Causation.CoerciveImplication.instReprActionType = { reprPrec := Causation.CoerciveImplication.instReprActionType.repr }

@[implicit_reducible]

instance Causation.CoerciveImplication.instInhabitedActionType : Inhabited ActionType

Equations

• Causation.CoerciveImplication.instInhabitedActionType = { default := Causation.CoerciveImplication.instInhabitedActionType.default }

inductive Causation.CoerciveImplication.CoercionStrength : Type

Coercion strength: strong (volitional), weak (ambiguous), none.

• Strong : CoercionStrength
• Weak : CoercionStrength
• None : CoercionStrength

@[implicit_reducible]

instance Causation.CoerciveImplication.instDecidableEqCoercionStrength : DecidableEq CoercionStrength

Equations

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

@[implicit_reducible]

instance Causation.CoerciveImplication.instReprCoercionStrength : Repr CoercionStrength

Equations

• Causation.CoerciveImplication.instReprCoercionStrength = { reprPrec := Causation.CoerciveImplication.instReprCoercionStrength.repr }

def Causation.CoerciveImplication.instReprCoercionStrength.repr : CoercionStrength → ℕ → Std.Format

Equations

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

noncomputable def Causation.CoerciveImplication.hasCoerciveImplication {V : Type u_1} {α : V → Type u_2} [Fintype V] [DecidableEq V] [DecidableValuation α] (M : SEM V α) [M.graph.IsDAG] [M.IsDeterministic] (background : Valuation α) (causerAction : V) (xCauser : α causerAction) (causeeIsVolitional : Bool) (causeeEvent : V) (xEvent : α causeeEvent) : Prop

V2 coercive implication: causer's action-as-xCauser is causally sufficient for a volitional causee action-as-xEvent. Polymorphic.

Equations

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

@[implicit_reducible]

noncomputable instance Causation.CoerciveImplication.instDecidableHasCoerciveImplication {V : Type u_1} {α : V → Type u_2} [Fintype V] [DecidableEq V] [DecidableValuation α] (M : SEM V α) [M.graph.IsDAG] [M.IsDeterministic] (bg : Valuation α) (causer : V) (xC : α causer) (vol : Bool) (effect : V) (xE : α effect) : Decidable (hasCoerciveImplication M bg causer xC vol effect xE)

Equations

• Causation.CoerciveImplication.instDecidableHasCoerciveImplication M bg causer xC vol effect xE = Classical.dec (Causation.CoerciveImplication.hasCoerciveImplication M bg causer xC vol effect xE)