Progressive Aspect and Causal Structure

[NBS24] [BS26b] [Dow79]

The progressive picks out type-level causal processes rather than token-level completed events. This module formalizes the distinction using V2 SEMs, following [NBS24]'s reframing of the imperfective paradox through causal models.

Type-Level vs Token-Level

[BS26b]: SEM models distinguish two levels:

• Type-level: General causal structure (graph + mechanisms).
• Token-level: A specific causal trajectory completed in the actual world.

The Imperfective Paradox

"Mary was opening the door" (progressive) vs "Mary opened the door" (perfective). The progressive entails the process is underway but NOT that it completed. "Mary was opening the door (when it got stuck)" is coherent — type-level process in progress, token-level result never obtained.

V2 substrate

CausalProcess V is polymorphic over the vertex type. progressiveTrue checks type-level sufficiency (BoolSEM.causallySufficient); perfectiveTrue adds token-level but-for completion (CCSelection.completesForEffect).

structure Causation.Progressive.CausalProcess (V : Type u_1) [Fintype V] [DecidableEq V] : Type u_1

A causal process for telic predicates, parameterized over a vertex type V.

Bundles a BoolSEM V (the type-level causal model), an explicit vertex list (proof-side only: feeds developDetOn computations in decide-based proofs), the initiating action vertex, the result vertex, and any enabling-condition valuation.

• M : BoolSEM V

  The type-level causal model.

• vertexList : List V

  Topologically-ordered vertex list. Proof-side only: not consumed by the semantic predicates, but useful for developDetOn-based decide proofs about concrete processes.

• initiator : V

  The initiating action vertex.

• result : V

  The result-state vertex.

• enablingConditions : Valuation fun (x : V) => Bool

  Background enabling conditions (default: empty).

noncomputable def Causation.Progressive.CausalProcess.typeLevelHolds {V : Type u_1} [Fintype V] [DecidableEq V] (proc : CausalProcess V) [proc.M.graph.IsDAG] [SEM.IsDeterministic proc.M] : Prop

Type-level sufficiency: the causal trajectory from initiator to result exists. The progressive asserts this — no commitment to the result actually obtaining in the actual world.

Equations

• proc.typeLevelHolds = proc.M.causallySufficient proc.enablingConditions proc.initiator proc.result

@[implicit_reducible]

noncomputable instance Causation.Progressive.CausalProcess.instDecidableTypeLevelHolds {V : Type u_1} [Fintype V] [DecidableEq V] (proc : CausalProcess V) [proc.M.graph.IsDAG] [SEM.IsDeterministic proc.M] : Decidable proc.typeLevelHolds

Equations

• proc.instDecidableTypeLevelHolds = Classical.dec proc.typeLevelHolds

noncomputable def Causation.Progressive.CausalProcess.progressiveTrue {V : Type u_1} [Fintype V] [DecidableEq V] (proc : CausalProcess V) [proc.M.graph.IsDAG] [SEM.IsDeterministic proc.M] : Prop

Progressive semantics: type-level process underway, completion open.

Equations

• proc.progressiveTrue = proc.typeLevelHolds

@[implicit_reducible]

noncomputable instance Causation.Progressive.CausalProcess.instDecidableProgressiveTrue {V : Type u_1} [Fintype V] [DecidableEq V] (proc : CausalProcess V) [proc.M.graph.IsDAG] [SEM.IsDeterministic proc.M] : Decidable proc.progressiveTrue

Equations

• proc.instDecidableProgressiveTrue = Classical.dec proc.progressiveTrue

noncomputable def Causation.Progressive.CausalProcess.completesForEffect {V : Type u_1} [Fintype V] [DecidableEq V] (proc : CausalProcess V) [proc.M.graph.IsDAG] [SEM.IsDeterministic proc.M] : Prop

But-for completion test (CCSelection.completesForEffect): cause being true → effect; cause being false → ¬ effect.

Equations

• proc.completesForEffect = Causation.CCSelection.completesForEffect proc.M proc.enablingConditions proc.initiator true false proc.result true

@[implicit_reducible]

noncomputable instance Causation.Progressive.CausalProcess.instDecidableCompletesForEffect {V : Type u_1} [Fintype V] [DecidableEq V] (proc : CausalProcess V) [proc.M.graph.IsDAG] [SEM.IsDeterministic proc.M] : Decidable proc.completesForEffect

Equations

• proc.instDecidableCompletesForEffect = Classical.dec proc.completesForEffect

noncomputable def Causation.Progressive.CausalProcess.perfectiveTrue {V : Type u_1} [Fintype V] [DecidableEq V] (proc : CausalProcess V) [proc.M.graph.IsDAG] [SEM.IsDeterministic proc.M] : Prop

Perfective semantics: token-level causation completed.

Holds when the causal chain ran to completion AND the initiator was necessary (removing it would prevent the result). This captures "Mary opened the door."

Equations

• proc.perfectiveTrue = proc.completesForEffect

@[implicit_reducible]

noncomputable instance Causation.Progressive.CausalProcess.instDecidablePerfectiveTrue {V : Type u_1} [Fintype V] [DecidableEq V] (proc : CausalProcess V) [proc.M.graph.IsDAG] [SEM.IsDeterministic proc.M] : Decidable proc.perfectiveTrue

Equations

• proc.instDecidablePerfectiveTrue = Classical.dec proc.perfectiveTrue

Example: "Mary was opening the door" / "Mary opened the door." Simple model: Mary's action → door opens.

inductive Causation.Progressive.MaryVar : Type

Vertex type for the door-opening example.

• action : MaryVar
• doorOpen : MaryVar

@[implicit_reducible]

instance Causation.Progressive.instDecidableEqMaryVar : DecidableEq MaryVar

Equations

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

@[implicit_reducible]

instance Causation.Progressive.instFintypeMaryVar : Fintype MaryVar

Equations

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

@[implicit_reducible]

instance Causation.Progressive.instReprMaryVar : Repr MaryVar

Equations

• Causation.Progressive.instReprMaryVar = { reprPrec := Causation.Progressive.instReprMaryVar.repr }

def Causation.Progressive.instReprMaryVar.repr : MaryVar → ℕ → Std.Format

Equations

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

def Causation.Progressive.maryVarList : List MaryVar

Equations

• Causation.Progressive.maryVarList = [Causation.Progressive.MaryVar.action, Causation.Progressive.MaryVar.doorOpen]

def Causation.Progressive.maryGraph : CausalGraph MaryVar

Door-opening graph: doorOpen ← action.

Equations

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

instance Causation.Progressive.instIsDAGMaryVarMaryGraph : maryGraph.IsDAG

noncomputable def Causation.Progressive.marySEM : BoolSEM MaryVar

Door-opening SEM: doorOpen := action.

Equations

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

@[implicit_reducible]

noncomputable instance Causation.Progressive.instIsDeterministicMaryVarBoolMarySEM : SEM.IsDeterministic marySEM

Equations

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

noncomputable def Causation.Progressive.maryOpening : CausalProcess MaryVar

Equations

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

@[implicit_reducible]

noncomputable instance Causation.Progressive.instIsDeterministicMaryVarBoolMMaryOpening : SEM.IsDeterministic maryOpening.M

Equations

• Causation.Progressive.instIsDeterministicMaryVarBoolMMaryOpening = { mech_det := Causation.Progressive.instIsDeterministicMaryVarBoolMMaryOpening._aux_1 }

instance Causation.Progressive.instIsDAGMaryVarGraphBoolMMaryOpening : maryOpening.M.graph.IsDAG

theorem Causation.Progressive.maryOpening_progressive : maryOpening.progressiveTrue

The progressive is true: Mary's action is type-level sufficient.

theorem Causation.Progressive.maryOpening_perfective : maryOpening.perfectiveTrue

The perfective is true: Mary's action completed the process.

theorem Causation.Progressive.perfective_entails_progressive {V : Type u_1} [Fintype V] [DecidableEq V] (proc : CausalProcess V) [proc.M.graph.IsDAG] [SEM.IsDeterministic proc.M] (h : proc.perfectiveTrue) : proc.progressiveTrue

Perfective entails progressive (for the same process).

Witness for progressive ∧ ¬ perfective: an overdetermination model where the type-level process exists but the actual outcome would obtain regardless of the initiator.

inductive Causation.Progressive.OdVar : Type

3-vertex overdetermination model: A and B both cause R (disjunctively). With B in the background, A is sufficient but not necessary.

• a : OdVar
• b : OdVar
• r : OdVar

@[implicit_reducible]

instance Causation.Progressive.instDecidableEqOdVar : DecidableEq OdVar

Equations

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

@[implicit_reducible]

instance Causation.Progressive.instFintypeOdVar : Fintype OdVar

Equations

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

@[implicit_reducible]

instance Causation.Progressive.instReprOdVar : Repr OdVar

Equations

• Causation.Progressive.instReprOdVar = { reprPrec := Causation.Progressive.instReprOdVar.repr }

def Causation.Progressive.instReprOdVar.repr : OdVar → ℕ → Std.Format

Equations

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

def Causation.Progressive.odVarList : List OdVar

Equations

• Causation.Progressive.odVarList = [Causation.Progressive.OdVar.a, Causation.Progressive.OdVar.b, Causation.Progressive.OdVar.r]

def Causation.Progressive.odGraph : CausalGraph OdVar

Equations

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

instance Causation.Progressive.instIsDAGOdVarOdGraph : odGraph.IsDAG

noncomputable def Causation.Progressive.odSEM : BoolSEM OdVar

R := A ∨ B (disjunctive overdetermination).

Equations

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

@[implicit_reducible]

noncomputable instance Causation.Progressive.instIsDeterministicOdVarBoolOdSEM : SEM.IsDeterministic odSEM

Equations

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

noncomputable def Causation.Progressive.overdetProc : CausalProcess OdVar

Equations

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

@[implicit_reducible]

noncomputable instance Causation.Progressive.instIsDeterministicOdVarBoolMOverdetProc : SEM.IsDeterministic overdetProc.M

Equations

• Causation.Progressive.instIsDeterministicOdVarBoolMOverdetProc = { mech_det := Causation.Progressive.instIsDeterministicOdVarBoolMOverdetProc._aux_1 }

instance Causation.Progressive.instIsDAGOdVarGraphBoolMOverdetProc : overdetProc.M.graph.IsDAG

theorem Causation.Progressive.overdet_progressive : overdetProc.progressiveTrue

Progressive holds for the overdetermination witness.

theorem Causation.Progressive.overdet_not_perfective : ¬overdetProc.perfectiveTrue

Perfective FAILS for the overdetermination witness — even with initiator = false, the backup B in enablingConditions produces the result, so the but-for half of completesForEffect fails.

theorem Causation.Progressive.progressive_not_entails_perfective : overdetProc.progressiveTrue ∧ ¬overdetProc.perfectiveTrue

Imperfective paradox: progressive does NOT entail perfective. Witnessed by the overdetermination scenario.

theorem Causation.Progressive.typeLevelHolds_is_develop {V : Type u_1} [Fintype V] [DecidableEq V] (proc : CausalProcess V) [proc.M.graph.IsDAG] [SEM.IsDeterministic proc.M] : proc.typeLevelHolds ↔ (SEM.developDet proc.M (proc.enablingConditions.extend proc.initiator true)).hasValue proc.result true

[Dow79]: the progressive is true iff the outcome holds in all inertia worlds (normal continuations). The causal model account refines this: "normal continuation" means "the SEM develops the initiator into the result" — i.e., type-level sufficiency.

structure Causation.Progressive.CausallyGroundedEvent (V : Type u_1) [Fintype V] [DecidableEq V] (Time : Type u_2) [LinearOrder Time] : Type (max u_1 u_2)

A causally grounded telic event: bridges CausalProcess (causal explanation) with SubeventPhases (temporal realization).

[NBS24]: telic predicates encode structured causal models. The activity phase corresponds to the initiating action; the result phase corresponds to the effect variable. The causal model explains WHY the activity leads to the result: the initiator is type-level sufficient.

• process : CausalProcess V

  The causal process underlying the event

• dagInst : self.process.M.graph.IsDAG

  IsDAG instance for process.M.graph (carried explicitly).

• detInst : SEM.IsDeterministic self.process.M

  IsDeterministic instance for proc.M (carried explicitly).

• phases : Semantics.Aspect.SubeventStructure.SubeventPhases Time

  The temporal phases: activity and result with ordering

• causallyViable : self.process.typeLevelHolds

  The causal trajectory is viable: initiator is type-level sufficient.