@cite{cruse-1973} Agentivity Decomposition

@cite{cruse-1973} "Some Thoughts on Agentivity" argues that agentivity is not a single feature but decomposes into 4 independent sub-features:

Feature	Cruse's gloss	Example
volitive	an act of will is stated or implied	John deliberately…
effective	force from position/motion/energy	The bullet smashed…
initiative	initiating action by command	The warder marched…
agentive	using own body's internal energy	John ran

The do-test ("NP did something") passes iff at least one feature is present. @cite{parsons-1990} neo-Davidsonian agent role captures specifically the agentive sub-feature (own energy + dynamic), which is strictly narrower than passing the do-test.

This analysis has been superseded by @cite{grimm-2011}'s agentivity lattice (formalized in AgentivityLattice.lean), which organizes proto-agent entailments into a lattice with privative features. The Cruse decomposition is preserved here as a historically important precursor.

Connections

• ThematicRoles.ThematicFrame.agent — Parsons' agent captures Cruse's agentive_
• CoerciveImplication.ActionType — initiative ↔ volitional action
• CausativeBuilder — initiative ↔ causative constructions
• VendlerClass / DiagnosticResult — aspect diagnostics

Aspect bridge

The do-test prediction for each Vendler class is derived from the agentivity theory: the do-test accepts durative dynamic classes (activity, accomplishment) and is marginal for others.

inductive Phenomena.TenseAspect.Studies.Cruse1973.AgentivityFeature : Type

The four independent sub-features of agentivity (@cite{cruse-1973} pp.17–21).

Cruse argues that "agentivity" is not a single binary feature but decomposes into at least four independent components, each with distinct linguistic diagnostics.

• volitive : AgentivityFeature

  Volitive: an act of will is stated or implied (Cruse p.18). "John deliberately drifted downstream."

• effective : AgentivityFeature

  Effective: force deriving from position, motion, or kinetic energy (Cruse p.19). "The bullet smashed the collar-bone."

• initiative : AgentivityFeature

  Initiative: initiating action by command or instruction to another agent (Cruse p.19). "The warder marched the prisoners."

• agentive_ : AgentivityFeature

  Agentive: use of one's own body's internal energy source (Cruse p.20). "John ran." The prototypical agent feature.

instance Phenomena.TenseAspect.Studies.Cruse1973.instDecidableEqAgentivityFeature : DecidableEq AgentivityFeature

Equations

• Phenomena.TenseAspect.Studies.Cruse1973.instDecidableEqAgentivityFeature x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Phenomena.TenseAspect.Studies.Cruse1973.instReprAgentivityFeature : Repr AgentivityFeature

Equations

• Phenomena.TenseAspect.Studies.Cruse1973.instReprAgentivityFeature = { reprPrec := Phenomena.TenseAspect.Studies.Cruse1973.instReprAgentivityFeature.repr }

def Phenomena.TenseAspect.Studies.Cruse1973.instReprAgentivityFeature.repr : AgentivityFeature → ℕ → Std.Format

Equations

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

instance Phenomena.TenseAspect.Studies.Cruse1973.instBEqAgentivityFeature : BEq AgentivityFeature

Equations

• Phenomena.TenseAspect.Studies.Cruse1973.instBEqAgentivityFeature = { beq := Phenomena.TenseAspect.Studies.Cruse1973.instBEqAgentivityFeature.beq }

def Phenomena.TenseAspect.Studies.Cruse1973.instBEqAgentivityFeature.beq : AgentivityFeature → AgentivityFeature → Bool

Equations

• Phenomena.TenseAspect.Studies.Cruse1973.instBEqAgentivityFeature.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

structure Phenomena.TenseAspect.Studies.Cruse1973.AgentivityProfile (Entity : Type u_1) (Time : Type u_2) [LE Time] : Type (max u_1 u_2)

An agentivity profile assigns Prop-valued feature predicates over entity–event pairs for each of Cruse's four sub-features.

Each field hasF x e means "entity x exhibits feature F in event e".

• hasVolitive : Entity → Semantics.Events.Ev Time → Prop

  Does x exhibit an act of will in e?

• hasEffective : Entity → Semantics.Events.Ev Time → Prop

  Does x exert force (from position/motion/energy) in e?

• hasInitiative : Entity → Semantics.Events.Ev Time → Prop

  Does x initiate action by command/instruction in e?

• hasAgentive : Entity → Semantics.Events.Ev Time → Prop

  Does x use own body's internal energy in e?

def Phenomena.TenseAspect.Studies.Cruse1973.passesDoTest {Entity : Type u_1} {Time : Type u_2} [LE Time] (x : Entity) (e : Semantics.Events.Ev Time) (profile : AgentivityProfile Entity Time) : Prop

The do-test (@cite{cruse-1973} pp.13–14): "NP VP" entails "NP did something" iff at least one agentivity sub-feature is present.

This is the disjunction of all four features.

Equations

• Phenomena.TenseAspect.Studies.Cruse1973.passesDoTest x e profile = (profile.hasVolitive x e ∨ profile.hasEffective x e ∨ profile.hasInitiative x e ∨ profile.hasAgentive x e)

theorem Phenomena.TenseAspect.Studies.Cruse1973.passesDo_iff_or {Entity : Type u_1} {Time : Type u_2} [LE Time] (x : Entity) (e : Semantics.Events.Ev Time) (p : AgentivityProfile Entity Time) : passesDoTest x e p ↔ p.hasVolitive x e ∨ p.hasEffective x e ∨ p.hasInitiative x e ∨ p.hasAgentive x e

The do-test is equivalent to the 4-way disjunction (definitional).

class Phenomena.TenseAspect.Studies.Cruse1973.CruseIndependence (Entity : Type u_1) (Time : Type u_2) [LE Time] (profile : AgentivityProfile Entity Time) : Prop

Axiom class witnessing that the four agentivity features are logically independent: each can be present without the others.

• volitive_without_agentive: "John deliberately drifted downstream" (will present, no own-energy expenditure)
• effective_without_volitive: "The bullet smashed the collar-bone" (force present, no will)
• initiative_without_agentive_: "The warder marched the prisoners" (command present, prisoners do the marching)
• agentive_without_initiative: "John ran" (own energy, no command to another)

• volitive_without_agentive : ∃ (x : Entity) (e : Semantics.Events.Ev Time), profile.hasVolitive x e ∧ ¬profile.hasAgentive x e

  Volitive without agentive: "John deliberately drifted downstream"

• effective_without_volitive : ∃ (x : Entity) (e : Semantics.Events.Ev Time), profile.hasEffective x e ∧ ¬profile.hasVolitive x e

  Effective without volitive: "The bullet smashed the collar-bone"

• initiative_without_agentive_ : ∃ (x : Entity) (e : Semantics.Events.Ev Time), profile.hasInitiative x e ∧ ¬profile.hasAgentive x e

  Initiative without agentive: "The warder marched the prisoners"

• agentive_without_initiative : ∃ (x : Entity) (e : Semantics.Events.Ev Time), profile.hasAgentive x e ∧ ¬profile.hasInitiative x e

  Agentive without initiative: "John ran"

class Phenomena.TenseAspect.Studies.Cruse1973.AgentAgentiveLink (Entity : Type u_1) (Time : Type u_2) [LE Time] (frame : Semantics.Events.ThematicRoles.ThematicFrame Entity Time) (profile : AgentivityProfile Entity Time) : Prop

Link between Parsons' agent role and Cruse's agentive_ sub-feature.

The Parsonian agent(x,e) captures specifically the own-energy sub-feature: an agent uses its own body's internal energy source. This is strictly narrower than the full do-test.

• agent_implies_agentive (x : Entity) (e : Semantics.Events.Ev Time) : frame.agent x e → profile.hasAgentive x e

  Parsons' agent implies Cruse's agentive_ feature.

theorem Phenomena.TenseAspect.Studies.Cruse1973.agent_implies_passesDo {Entity : Type u_1} {Time : Type u_2} [LE Time] {frame : Semantics.Events.ThematicRoles.ThematicFrame Entity Time} {profile : AgentivityProfile Entity Time} [link : AgentAgentiveLink Entity Time frame profile] (x : Entity) (e : Semantics.Events.Ev Time) (h : frame.agent x e) : passesDoTest x e profile

Parsons' agent(x,e) entails passesDoTest(x,e), since agentive_ is one of the four disjuncts.

In any model where agent → hasAgentive, the result follows immediately from the fact that agentive_ is the fourth disjunct.

theorem Phenomena.TenseAspect.Studies.Cruse1973.agent_is_agentive_subfeature {Entity : Type u_1} {Time : Type u_2} [LE Time] {frame : Semantics.Events.ThematicRoles.ThematicFrame Entity Time} {profile : AgentivityProfile Entity Time} [link : AgentAgentiveLink Entity Time frame profile] [ax : Semantics.Events.ThematicRoles.ThematicAxioms Entity Time frame] (x : Entity) (e : Semantics.Events.Ev Time) (h : frame.agent x e) : profile.hasAgentive x e ∧ e.sort = Semantics.Events.EventSort.action

Parsons' agent role captures specifically Cruse's agentive_ sub-feature (own energy, dynamic), not the full do-test notion.

This is stated as: any model satisfying AgentAgentiveLink and ThematicAxioms has agent entail agentive_ (from the link) and agent entail action (from the axioms). Together these characterize the prototypical "own-energy + dynamic" combination.

def Phenomena.TenseAspect.Studies.Cruse1973.AgentivityFeature.toActionType : AgentivityFeature → NadathurLauer2020.CoerciveImplication.ActionType

Map agentivity features to CoerciveImplication's ActionType.

• volitive → Volitional (Cruse: act of will ↔ N&L: volitional action)
• effective → NonVolitional (force without will)
• initiative → Volitional (initiating by command is volitional for initiator)
• agentive_ → Ambiguous (own energy can be volitional or habitual)

Equations

• Phenomena.TenseAspect.Studies.Cruse1973.AgentivityFeature.volitive.toActionType = NadathurLauer2020.CoerciveImplication.ActionType.Volitional
• Phenomena.TenseAspect.Studies.Cruse1973.AgentivityFeature.effective.toActionType = NadathurLauer2020.CoerciveImplication.ActionType.NonVolitional
• Phenomena.TenseAspect.Studies.Cruse1973.AgentivityFeature.initiative.toActionType = NadathurLauer2020.CoerciveImplication.ActionType.Volitional
• Phenomena.TenseAspect.Studies.Cruse1973.AgentivityFeature.agentive_.toActionType = NadathurLauer2020.CoerciveImplication.ActionType.Ambiguous

theorem Phenomena.TenseAspect.Studies.Cruse1973.volitive_toActionType : AgentivityFeature.volitive.toActionType = NadathurLauer2020.CoerciveImplication.ActionType.Volitional

Volitive maps to Volitional.

theorem Phenomena.TenseAspect.Studies.Cruse1973.effective_toActionType : AgentivityFeature.effective.toActionType = NadathurLauer2020.CoerciveImplication.ActionType.NonVolitional

Effective maps to NonVolitional.

theorem Phenomena.TenseAspect.Studies.Cruse1973.initiative_toActionType : AgentivityFeature.initiative.toActionType = NadathurLauer2020.CoerciveImplication.ActionType.Volitional

Initiative maps to Volitional.

theorem Phenomena.TenseAspect.Studies.Cruse1973.agentive_toActionType : AgentivityFeature.agentive_.toActionType = NadathurLauer2020.CoerciveImplication.ActionType.Ambiguous

Agentive maps to Ambiguous.

theorem Phenomena.TenseAspect.Studies.Cruse1973.coercion_requires_volitive (f : AgentivityFeature) : f.toActionType = NadathurLauer2020.CoerciveImplication.ActionType.Volitional ↔ f = AgentivityFeature.volitive ∨ f = AgentivityFeature.initiative

Coercive implication (@cite{nadathur-lauer-2020}) arises exactly when the causee's action is volitional — i.e., when the causee has at least the volitive sub-feature.

This bridges Cruse's agentivity decomposition to N&L's coercion analysis: "X made Y do Z" implies coercion when Z is volitional for Y, which Cruse would analyze as Y having the volitive feature.

structure Phenomena.TenseAspect.Studies.Cruse1973.InitiativeCausativeLink (Entity : Type u_1) (Time : Type u_2) [LE Time] (profile : AgentivityProfile Entity Time) : Prop

Cruse's initiative feature (initiating action by command) corresponds to causative constructions where the subject causes an agentive action by the object.

"The warder marched the prisoners" → the warder has initiative, the prisoners are the agentive doers. This pattern is lexicalized by CausativeBuilder.make and .force: the subject (causer) initiates, the object (causee) performs the action.

The bridge: initiative ↔ {make, force} builders, where the causer has initiative and the causee has agentive_.

• causer_has_initiative (causer causee : Entity) (e : Semantics.Events.Ev Time) : profile.hasInitiative causer e → ¬profile.hasAgentive causer e → profile.hasAgentive causee e

  In a causative construction, the causer has initiative.

theorem Phenomena.TenseAspect.Studies.Cruse1973.force_lexicalizes_coercive_initiative : NadathurLauer2020.Builder.CausativeBuilder.force.isCoercive = true

The force builder is coercive — it lexicalizes coercion of a volitional causee, which is precisely the initiative pattern where the initiator overrides the causee's will.

theorem Phenomena.TenseAspect.Studies.Cruse1973.make_lexicalizes_sufficient_initiative : NadathurLauer2020.Builder.CausativeBuilder.make.assertsSufficiency = true

The make builder asserts sufficiency — the initiator's action is sufficient for the causee to act.

theorem Phenomena.TenseAspect.Studies.Cruse1973.stative_can_pass_doTest : ∃ (profile : AgentivityProfile Unit ℤ) (x : Unit) (e : Semantics.Events.Ev ℤ), e.sort = Semantics.Events.EventSort.state ∧ passesDoTest x e profile

There exist stative eventualities that pass the do-test.

Witness: "John is standing" — volitive (John can stop standing) but stative (no change over the interval). The do-test passes via the volitive feature, even though e.sort =.state.

This shows the do-test is strictly broader than Parsons' agent role, which requires e.sort =.action.

theorem Phenomena.TenseAspect.Studies.Cruse1973.agent_selects_action_consistent {Entity : Type u_1} {Time : Type u_2} [LE Time] {frame : Semantics.Events.ThematicRoles.ThematicFrame Entity Time} [ax : Semantics.Events.ThematicRoles.ThematicAxioms Entity Time frame] (x : Entity) (e : Semantics.Events.Ev Time) (hState : e.sort = Semantics.Events.EventSort.state) (hAgent : frame.agent x e) : False

Parsons' agent_selects_action is NOT contradicted by stative do-verbs, because agent captures the narrower agentive_ feature (own energy → dynamic), while the do-test also detects volitive which can apply to states.

Formally: given ThematicAxioms (which assert agent → action), and AgentAgentiveLink (which assert agent → agentive_), if an entity is agent of a stative event we get a contradiction — so no stative event has a Parsonian agent. The do-test still passes for statives via other features (volitive, effective).

def Phenomena.TenseAspect.Studies.Cruse1973.doTestPrediction : Semantics.Tense.Aspect.LexicalAspect.VendlerClass → Diagnostics.DiagnosticResult

Predict the do-test result for each Vendler class.

• State → marginal: some pass (stand, sit, hold — via volitive) but most don't (know, love — no agentivity features)
• Activity → accept: paradigmatic do-sentences ("John ran" → "What John did was run")
• Achievement → marginal: some pass ("die in order to save…" — arguably volitive), most don't
• Accomplishment → accept: all dynamic + extended → do-test

Equations

• Phenomena.TenseAspect.Studies.Cruse1973.doTestPrediction Semantics.Tense.Aspect.LexicalAspect.VendlerClass.state = Phenomena.TenseAspect.Diagnostics.DiagnosticResult.marginal
• Phenomena.TenseAspect.Studies.Cruse1973.doTestPrediction Semantics.Tense.Aspect.LexicalAspect.VendlerClass.activity = Phenomena.TenseAspect.Diagnostics.DiagnosticResult.accept
• Phenomena.TenseAspect.Studies.Cruse1973.doTestPrediction Semantics.Tense.Aspect.LexicalAspect.VendlerClass.achievement = Phenomena.TenseAspect.Diagnostics.DiagnosticResult.marginal
• Phenomena.TenseAspect.Studies.Cruse1973.doTestPrediction Semantics.Tense.Aspect.LexicalAspect.VendlerClass.accomplishment = Phenomena.TenseAspect.Diagnostics.DiagnosticResult.accept

theorem Phenomena.TenseAspect.Studies.Cruse1973.doTest_accepts_durative_dynamic (c : Semantics.Tense.Aspect.LexicalAspect.VendlerClass) : doTestPrediction c = Diagnostics.DiagnosticResult.accept ↔ c.duration = Semantics.Tense.Aspect.LexicalAspect.Duration.durative ∧ c.dynamicity = Semantics.Tense.Aspect.LexicalAspect.Dynamicity.dynamic

The do-test accepts exactly the durative dynamic classes (activity, accomplishment).

theorem Phenomena.TenseAspect.Studies.Cruse1973.doTest_accept_implies_dynamic (c : Semantics.Tense.Aspect.LexicalAspect.VendlerClass) : doTestPrediction c = Diagnostics.DiagnosticResult.accept → c.dynamicity = Semantics.Tense.Aspect.LexicalAspect.Dynamicity.dynamic

Passing the do-test (for a whole Vendler class, not marginal) implies either a dynamic event or a volitive state.

Formally: if a Vendler class fully accepts the do-test (not just marginally), then it must be dynamic. Statives only get marginal because the do-test passes only for select volitive statives.

theorem Phenomena.TenseAspect.Studies.Cruse1973.doTest_agrees_imperative_for_dynamic_durative (c : Semantics.Tense.Aspect.LexicalAspect.VendlerClass) (hDyn : c.dynamicity = Semantics.Tense.Aspect.LexicalAspect.Dynamicity.dynamic) (hDur : c.duration = Semantics.Tense.Aspect.LexicalAspect.Duration.durative) : doTestPrediction c = Diagnostics.imperativePrediction c

The do-test and imperative test agree on activities and accomplishments (both diagnostics accept dynamic durative events). They diverge on states (do-test: marginal; imperative: reject) and achievements (do-test: marginal; imperative: marginal — but for different reasons).