Progressive Aspect and Causal Structure

@cite{nadathur-bar-asher-siegal-2024} @cite{bar-asher-siegal-2026} @cite{dowty-1979}

The progressive picks out type-level causal processes rather than token-level completed events. This module formalizes the distinction using V2 SEMs, following @cite{nadathur-bar-asher-siegal-2024}'s reframing of the imperfective paradox through causal models.

Type-Level vs Token-Level

@cite{bar-asher-siegal-2026}: 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 (the cause develops to the result via developDetOn). perfectiveTrue adds token-level completion via a local completesForEffect (defined inline to avoid the CCSelection cascade during the V2 migration period).

structure Semantics.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 (for developDetOn-based kernel reduction), the initiating action vertex, the result vertex, and any enabling-condition valuation.

• M : Core.Causal.BoolSEM V

  The type-level causal model.

• vertexList : List V

  Topologically-ordered vertex list for structural unfolding.

• initiator : V

  The initiating action vertex.

• result : V

  The result-state vertex.

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

  Background enabling conditions (default: empty).

noncomputable def Semantics.Causation.Progressive.CausalProcess.typeLevelHolds {V : Type u_1} [Fintype V] [DecidableEq V] (proc : CausalProcess V) [Core.Causal.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 = (Core.Causal.SEM.developDetOn proc.M proc.vertexList 1 (proc.enablingConditions.extend proc.initiator true)).hasValue proc.result true

@[implicit_reducible]

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

Equations

• proc.instDecidableTypeLevelHolds = Classical.dec proc.typeLevelHolds

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

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

Equations

• proc.progressiveTrue = proc.typeLevelHolds

@[implicit_reducible]

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

Equations

• proc.instDecidableProgressiveTrue = Classical.dec proc.progressiveTrue

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

Local but-for completion test (avoids CCSelection import during migration): cause being true → effect; cause being false → ¬ effect.

Equations

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

@[implicit_reducible]

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

Equations

• proc.instDecidableCompletesForEffect = Classical.dec proc.completesForEffect

noncomputable def Semantics.Causation.Progressive.CausalProcess.perfectiveTrue {V : Type u_1} [Fintype V] [DecidableEq V] (proc : CausalProcess V) [Core.Causal.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 Semantics.Causation.Progressive.CausalProcess.instDecidablePerfectiveTrue {V : Type u_1} [Fintype V] [DecidableEq V] (proc : CausalProcess V) [Core.Causal.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 Semantics.Causation.Progressive.MaryVar : Type

Vertex type for the door-opening example.

• action : MaryVar
• doorOpen : MaryVar

@[implicit_reducible]

instance Semantics.Causation.Progressive.instDecidableEqMaryVar : DecidableEq MaryVar

Equations

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

@[implicit_reducible]

instance Semantics.Causation.Progressive.instFintypeMaryVar : Fintype MaryVar

Equations

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

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

Equations

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

@[implicit_reducible]

instance Semantics.Causation.Progressive.instReprMaryVar : Repr MaryVar

Equations

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

def Semantics.Causation.Progressive.maryVarList : List MaryVar

Equations

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

def Semantics.Causation.Progressive.maryGraph : Core.Causal.CausalGraph MaryVar

Door-opening graph: doorOpen ← action.

Equations

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

noncomputable def Semantics.Causation.Progressive.marySEM : Core.Causal.BoolSEM MaryVar

Door-opening SEM: doorOpen := action.

Equations

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

@[implicit_reducible]

noncomputable instance Semantics.Causation.Progressive.instIsDeterministicMaryVarBoolMarySEM : Core.Causal.SEM.IsDeterministic marySEM

Equations

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

noncomputable def Semantics.Causation.Progressive.maryOpening : CausalProcess MaryVar

Equations

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

@[implicit_reducible]

noncomputable instance Semantics.Causation.Progressive.instIsDeterministicMaryVarBoolMMaryOpening : Core.Causal.SEM.IsDeterministic maryOpening.M

Equations

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

theorem Semantics.Causation.Progressive.maryOpening_progressive : maryOpening.progressiveTrue

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

theorem Semantics.Causation.Progressive.maryOpening_perfective : maryOpening.perfectiveTrue

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

theorem Semantics.Causation.Progressive.perfective_entails_progressive {V : Type u_1} [Fintype V] [DecidableEq V] (proc : CausalProcess V) [Core.Causal.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 Semantics.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 Semantics.Causation.Progressive.instDecidableEqOdVar : DecidableEq OdVar

Equations

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

@[implicit_reducible]

instance Semantics.Causation.Progressive.instFintypeOdVar : Fintype OdVar

Equations

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

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

Equations

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

@[implicit_reducible]

instance Semantics.Causation.Progressive.instReprOdVar : Repr OdVar

Equations

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

def Semantics.Causation.Progressive.odVarList : List OdVar

Equations

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

def Semantics.Causation.Progressive.odGraph : Core.Causal.CausalGraph OdVar

Equations

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

noncomputable def Semantics.Causation.Progressive.odSEM : Core.Causal.BoolSEM OdVar

R := A ∨ B (disjunctive overdetermination).

Equations

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

@[implicit_reducible]

noncomputable instance Semantics.Causation.Progressive.instIsDeterministicOdVarBoolOdSEM : Core.Causal.SEM.IsDeterministic odSEM

Equations

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

noncomputable def Semantics.Causation.Progressive.overdetProc : CausalProcess OdVar

Equations

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

@[implicit_reducible]

noncomputable instance Semantics.Causation.Progressive.instIsDeterministicOdVarBoolMOverdetProc : Core.Causal.SEM.IsDeterministic overdetProc.M

Equations

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

theorem Semantics.Causation.Progressive.overdet_progressive : overdetProc.progressiveTrue

Progressive holds for the overdetermination witness.

theorem Semantics.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.

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

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

theorem Semantics.Causation.Progressive.typeLevelHolds_is_developOn {V : Type u_1} [Fintype V] [DecidableEq V] (proc : CausalProcess V) [Core.Causal.SEM.IsDeterministic proc.M] : proc.typeLevelHolds ↔ (Core.Causal.SEM.developDetOn proc.M proc.vertexList 1 (proc.enablingConditions.extend proc.initiator true)).hasValue proc.result true

@cite{dowty-1979}: 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 Semantics.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).

@cite{nadathur-bar-asher-siegal-2024}: 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

• detInst : Core.Causal.SEM.IsDeterministic self.process.M

  IsDeterministic instance for proc.M (carried explicitly).

• phases : 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.