inductive Semantics.Events.Agentivity.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 Semantics.Events.Agentivity.instDecidableEqAgentivityFeature : DecidableEq AgentivityFeature

Equations

• Semantics.Events.Agentivity.instDecidableEqAgentivityFeature x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Semantics.Events.Agentivity.instReprAgentivityFeature : Repr AgentivityFeature

Equations

• Semantics.Events.Agentivity.instReprAgentivityFeature = { reprPrec := Semantics.Events.Agentivity.instReprAgentivityFeature.repr }

def Semantics.Events.Agentivity.instReprAgentivityFeature.repr : AgentivityFeature → ℕ → Std.Format

Equations

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

def Semantics.Events.Agentivity.instBEqAgentivityFeature.beq : AgentivityFeature → AgentivityFeature → Bool

Equations

• Semantics.Events.Agentivity.instBEqAgentivityFeature.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Semantics.Events.Agentivity.instBEqAgentivityFeature : BEq AgentivityFeature

Equations

• Semantics.Events.Agentivity.instBEqAgentivityFeature = { beq := Semantics.Events.Agentivity.instBEqAgentivityFeature.beq }

structure Semantics.Events.Agentivity.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 → Ev Time → Prop

  Does x exhibit an act of will in e?

• hasEffective : Entity → Ev Time → Prop

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

• hasInitiative : Entity → Ev Time → Prop

  Does x initiate action by command/instruction in e?

• hasAgentive : Entity → Ev Time → Prop

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

def Semantics.Events.Agentivity.passesDoTest {Entity : Type u_1} {Time : Type u_2} [LE Time] (x : Entity) (e : 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

• Semantics.Events.Agentivity.passesDoTest x e profile = (profile.hasVolitive x e ∨ profile.hasEffective x e ∨ profile.hasInitiative x e ∨ profile.hasAgentive x e)

theorem Semantics.Events.Agentivity.passesDo_iff_or {Entity : Type u_1} {Time : Type u_2} [LE Time] (x : Entity) (e : 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 Semantics.Events.Agentivity.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 : Ev Time), profile.hasVolitive x e ∧ ¬profile.hasAgentive x e

  Volitive without agentive: "John deliberately drifted downstream"

• effective_without_volitive : ∃ (x : Entity) (e : 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 : Ev Time), profile.hasInitiative x e ∧ ¬profile.hasAgentive x e

  Initiative without agentive: "The warder marched the prisoners"

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

  Agentive without initiative: "John ran"

class Semantics.Events.Agentivity.AgentAgentiveLink (Entity : Type u_1) (Time : Type u_2) [LE Time] (frame : 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 : Ev Time) : frame.agent x e → profile.hasAgentive x e

  Parsons' agent implies Cruse's agentive_ feature.

theorem Semantics.Events.Agentivity.agent_implies_passesDo {Entity : Type u_1} {Time : Type u_2} [LE Time] {frame : ThematicRoles.ThematicFrame Entity Time} {profile : AgentivityProfile Entity Time} [link : AgentAgentiveLink Entity Time frame profile] (x : Entity) (e : 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 Semantics.Events.Agentivity.agent_is_agentive_subfeature {Entity : Type u_1} {Time : Type u_2} [LE Time] {frame : ThematicRoles.ThematicFrame Entity Time} {profile : AgentivityProfile Entity Time} [link : AgentAgentiveLink Entity Time frame profile] [ax : ThematicRoles.ThematicAxioms Entity Time frame] (x : Entity) (e : Ev Time) (h : frame.agent x e) : profile.hasAgentive x e ∧ e.sort = 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 Semantics.Events.Agentivity.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

• Semantics.Events.Agentivity.AgentivityFeature.volitive.toActionType = NadathurLauer2020.CoerciveImplication.ActionType.Volitional
• Semantics.Events.Agentivity.AgentivityFeature.effective.toActionType = NadathurLauer2020.CoerciveImplication.ActionType.NonVolitional
• Semantics.Events.Agentivity.AgentivityFeature.initiative.toActionType = NadathurLauer2020.CoerciveImplication.ActionType.Volitional
• Semantics.Events.Agentivity.AgentivityFeature.agentive_.toActionType = NadathurLauer2020.CoerciveImplication.ActionType.Ambiguous

theorem Semantics.Events.Agentivity.volitive_toActionType : AgentivityFeature.volitive.toActionType = NadathurLauer2020.CoerciveImplication.ActionType.Volitional

Volitive maps to Volitional.

theorem Semantics.Events.Agentivity.effective_toActionType : AgentivityFeature.effective.toActionType = NadathurLauer2020.CoerciveImplication.ActionType.NonVolitional

Effective maps to NonVolitional.

theorem Semantics.Events.Agentivity.initiative_toActionType : AgentivityFeature.initiative.toActionType = NadathurLauer2020.CoerciveImplication.ActionType.Volitional

Initiative maps to Volitional.

theorem Semantics.Events.Agentivity.agentive_toActionType : AgentivityFeature.agentive_.toActionType = NadathurLauer2020.CoerciveImplication.ActionType.Ambiguous

Agentive maps to Ambiguous.

theorem Semantics.Events.Agentivity.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 Semantics.Events.Agentivity.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 : Ev Time) : profile.hasInitiative causer e → ¬profile.hasAgentive causer e → profile.hasAgentive causee e

  In a causative construction, the causer has initiative.

theorem Semantics.Events.Agentivity.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 Semantics.Events.Agentivity.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 Semantics.Events.Agentivity.stative_can_pass_doTest : ∃ (profile : AgentivityProfile Unit ℤ) (x : Unit) (e : Ev ℤ), e.sort = 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 Semantics.Events.Agentivity.agent_selects_action_consistent {Entity : Type u_1} {Time : Type u_2} [LE Time] {frame : ThematicRoles.ThematicFrame Entity Time} [ax : ThematicRoles.ThematicAxioms Entity Time frame] (x : Entity) (e : Ev Time) (hState : e.sort = 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).