Grimm's agentivity features

Grimm reformulates Dowty's Proto-Agent entailments as four privative features, volition, sentience, instigation and motion, the Proto-Patient being the unmarked pole of each, and decomposes Dowty's relational causation into instigation, which is bound to a single participant. An argument's agentivity is the set of features its predicate entails, ordered by inclusion. The only relation among the features, that volition entails sentience, picks out the combinations Grimm organizes into a lattice, and they are closed under union and intersection. Grimm reserves the name agentivity lattice for its product with the persistence lattice.

Main definitions

• Agentivity: the agentivity features of an argument.
• Agentivity.Valid: volition entails sentience.
• Agentivity.lattice: the valid combinations, as a sublattice of all feature sets.

Implementation notes

The persistence features are PersistenceLevel.Feature, their product with the agentivity features is ParticipantType, and the projection from Dowty's profiles is EntailmentProfile.toAgentivity.

References

• [Gri11]
• [Dow91]

inductive ArgumentStructure.Agentivity.Feature : Type

The four agentivity features ([Gri11] Table 2), each privative: its absence is the non-agentive pole.

• volition : Feature

  The participant intends to bring about the event.

• sentience : Feature

  Conscious involvement in the action or state.

• instigation : Feature

  Prior independent action whose effects can be attributed to the participant, Grimm's replacement for Dowty's causation.

• motion : Feature

  The participant is in motion during the event.

@[instance_reducible]

instance ArgumentStructure.Agentivity.instDecidableEqFeature : DecidableEq Feature

Equations

• ArgumentStructure.Agentivity.instDecidableEqFeature x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def ArgumentStructure.Agentivity.instReprFeature.repr : Feature → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance ArgumentStructure.Agentivity.instReprFeature : Repr Feature

Equations

• ArgumentStructure.Agentivity.instReprFeature = { reprPrec := ArgumentStructure.Agentivity.instReprFeature.repr }

@[instance_reducible]

instance ArgumentStructure.Agentivity.instFintypeFeature : Fintype Feature

Equations

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

@[reducible, inline]

abbrev ArgumentStructure.Agentivity : Type

The agentivity features a predicate entails for an argument.

Equations

• ArgumentStructure.Agentivity = Finset ArgumentStructure.Agentivity.Feature

def ArgumentStructure.Agentivity.Valid (a : Agentivity) : Prop

Volition entails sentience.

Equations

• a.Valid = (ArgumentStructure.Agentivity.Feature.volition ∈ a → ArgumentStructure.Agentivity.Feature.sentience ∈ a)

@[instance_reducible]

instance ArgumentStructure.Agentivity.instDecidablePredValid : DecidablePred Valid

Equations

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

def ArgumentStructure.Agentivity.lattice : Sublattice Agentivity

The valid combinations of features form a sublattice of the feature sets, Grimm's lattice of agentivity properties, with union and intersection as join and meet.

Equations

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

@[simp]

theorem ArgumentStructure.Agentivity.mem_lattice {a : Agentivity} : a ∈ lattice ↔ a.Valid

theorem ArgumentStructure.Agentivity.card_valid : (Finset.filter Valid Finset.univ).card = 12

Of the sixteen feature sets, twelve are valid.