inductive NadathurLauer2020.CoerciveImplication.ActionType : Type

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

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

instance NadathurLauer2020.CoerciveImplication.instDecidableEqActionType : DecidableEq ActionType

Equations

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

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

Equations

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

instance NadathurLauer2020.CoerciveImplication.instReprActionType : Repr ActionType

Equations

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

def NadathurLauer2020.CoerciveImplication.instBEqActionType.beq : ActionType → ActionType → Bool

Equations

• NadathurLauer2020.CoerciveImplication.instBEqActionType.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance NadathurLauer2020.CoerciveImplication.instBEqActionType : BEq ActionType

Equations

• NadathurLauer2020.CoerciveImplication.instBEqActionType = { beq := NadathurLauer2020.CoerciveImplication.instBEqActionType.beq }

def NadathurLauer2020.CoerciveImplication.instInhabitedActionType.default : ActionType

Equations

• NadathurLauer2020.CoerciveImplication.instInhabitedActionType.default = NadathurLauer2020.CoerciveImplication.ActionType.Volitional

instance NadathurLauer2020.CoerciveImplication.instInhabitedActionType : Inhabited ActionType

Equations

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

structure NadathurLauer2020.CoerciveImplication.TaggedEvent : Type

An event tagged with volitionality.

• event : Core.StructuralEquationModel.Variable
• actionType : ActionType

instance NadathurLauer2020.CoerciveImplication.instReprTaggedEvent : Repr TaggedEvent

Equations

• NadathurLauer2020.CoerciveImplication.instReprTaggedEvent = { reprPrec := NadathurLauer2020.CoerciveImplication.instReprTaggedEvent.repr }

def NadathurLauer2020.CoerciveImplication.instReprTaggedEvent.repr : TaggedEvent → ℕ → Std.Format

Equations

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

def NadathurLauer2020.CoerciveImplication.TaggedEvent.volitional (v : Core.StructuralEquationModel.Variable) : TaggedEvent

Create a volitional event

Equations

• NadathurLauer2020.CoerciveImplication.TaggedEvent.volitional v = { event := v, actionType := NadathurLauer2020.CoerciveImplication.ActionType.Volitional }

def NadathurLauer2020.CoerciveImplication.TaggedEvent.nonVolitional (v : Core.StructuralEquationModel.Variable) : TaggedEvent

Create a non-volitional event

Equations

• NadathurLauer2020.CoerciveImplication.TaggedEvent.nonVolitional v = { event := v, actionType := NadathurLauer2020.CoerciveImplication.ActionType.NonVolitional }

def NadathurLauer2020.CoerciveImplication.TaggedEvent.isVolitional (te : TaggedEvent) : Bool

Check if an event is volitional

Equations

• te.isVolitional = (te.actionType == NadathurLauer2020.CoerciveImplication.ActionType.Volitional)

structure NadathurLauer2020.CoerciveImplication.CoerciveContext : Type

A situation where "make" creates coercive implication.

• dynamics : Core.StructuralEquationModel.CausalDynamics

  The causal dynamics

• background : Core.StructuralEquationModel.Situation

  The background situation

• causerAction : Core.StructuralEquationModel.Variable

  The causer's action

• causeeAction : TaggedEvent

  The causee's action (the effect)

def NadathurLauer2020.CoerciveImplication.CoerciveContext.hasCoerciveImplication (ctx : CoerciveContext) : Bool

Coercion arises when effect is volitional and cause is sufficient.

Equations

• ctx.hasCoerciveImplication = (ctx.causeeAction.isVolitional && Core.StructuralEquationModel.causallySufficient ctx.dynamics ctx.background ctx.causerAction ctx.causeeAction.event)

inductive NadathurLauer2020.CoerciveImplication.CoerciveContext.CoercionStrength : Type

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

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

instance NadathurLauer2020.CoerciveImplication.CoerciveContext.instDecidableEqCoercionStrength : DecidableEq CoercionStrength

Equations

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

instance NadathurLauer2020.CoerciveImplication.CoerciveContext.instReprCoercionStrength : Repr CoercionStrength

Equations

• NadathurLauer2020.CoerciveImplication.CoerciveContext.instReprCoercionStrength = { reprPrec := NadathurLauer2020.CoerciveImplication.CoerciveContext.instReprCoercionStrength.repr }

def NadathurLauer2020.CoerciveImplication.CoerciveContext.instReprCoercionStrength.repr : CoercionStrength → ℕ → Std.Format

Equations

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

instance NadathurLauer2020.CoerciveImplication.CoerciveContext.instBEqCoercionStrength : BEq CoercionStrength

Equations

• NadathurLauer2020.CoerciveImplication.CoerciveContext.instBEqCoercionStrength = { beq := NadathurLauer2020.CoerciveImplication.CoerciveContext.instBEqCoercionStrength.beq }

def NadathurLauer2020.CoerciveImplication.CoerciveContext.instBEqCoercionStrength.beq : CoercionStrength → CoercionStrength → Bool

Equations

• NadathurLauer2020.CoerciveImplication.CoerciveContext.instBEqCoercionStrength.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def NadathurLauer2020.CoerciveImplication.CoerciveContext.coercionStrength (ctx : CoerciveContext) : CoercionStrength

Compute coercion strength.

Equations

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

def NadathurLauer2020.CoerciveImplication.kim : Core.StructuralEquationModel.Variable

Kim (causer)

Equations

• NadathurLauer2020.CoerciveImplication.kim = Core.StructuralEquationModel.mkVar "kim_acts"

def NadathurLauer2020.CoerciveImplication.sandy : Core.StructuralEquationModel.Variable

Sandy (causee)

Equations

• NadathurLauer2020.CoerciveImplication.sandy = Core.StructuralEquationModel.mkVar "sandy"

def NadathurLauer2020.CoerciveImplication.sandyLeaves : TaggedEvent

Sandy leaving (volitional)

Equations

• NadathurLauer2020.CoerciveImplication.sandyLeaves = NadathurLauer2020.CoerciveImplication.TaggedEvent.volitional (Core.StructuralEquationModel.mkVar "sandy_leaves")

def NadathurLauer2020.CoerciveImplication.sandySneezes : TaggedEvent

Sandy sneezing (non-volitional)

Equations

• NadathurLauer2020.CoerciveImplication.sandySneezes = NadathurLauer2020.CoerciveImplication.TaggedEvent.nonVolitional (Core.StructuralEquationModel.mkVar "sandy_sneezes")

def NadathurLauer2020.CoerciveImplication.kimSandyDynamics : Core.StructuralEquationModel.CausalDynamics

Dynamics where Kim's action causes Sandy to leave.

Equations

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

theorem NadathurLauer2020.CoerciveImplication.kim_sandy_coercive : have ctx := { dynamics := kimSandyDynamics, background := Core.StructuralEquationModel.Situation.empty, causerAction := kim, causeeAction := sandyLeaves }; ctx.hasCoerciveImplication = true

"Kim made Sandy leave" - has coercive implication.

Kim's action was sufficient + Sandy leaving is volitional → Sandy was coerced (didn't freely choose to leave)

def NadathurLauer2020.CoerciveImplication.kimSneezeDynamics : Core.StructuralEquationModel.CausalDynamics

Dynamics where Kim causes Sandy to sneeze (odd construction).

Equations

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

theorem NadathurLauer2020.CoerciveImplication.kim_sneeze_not_coercive : have ctx := { dynamics := kimSneezeDynamics, background := Core.StructuralEquationModel.Situation.empty, causerAction := kim, causeeAction := sandySneezes }; ctx.hasCoerciveImplication = false

"Kim made Sandy sneeze" - NO coercive implication.

Kim's action was sufficient, but sneezing is non-volitional → No coercion inference (you can't override an involuntary action)

theorem NadathurLauer2020.CoerciveImplication.coercion_strong_volitional : have ctx := { dynamics := kimSandyDynamics, background := Core.StructuralEquationModel.Situation.empty, causerAction := kim, causeeAction := sandyLeaves }; ctx.coercionStrength = CoerciveContext.CoercionStrength.Strong

Coercion strength is strong for volitional actions.

theorem NadathurLauer2020.CoerciveImplication.coercion_none_nonvolitional : have ctx := { dynamics := kimSneezeDynamics, background := Core.StructuralEquationModel.Situation.empty, causerAction := kim, causeeAction := sandySneezes }; ctx.coercionStrength = CoerciveContext.CoercionStrength.None

Coercion strength is none for non-volitional actions.