The agentivity lattice

Grimm combines the lattice of agentivity properties with the persistence lattice by taking their Cartesian product, ordered componentwise, and excludes the conceptually impossible nodes: an argument not entailed to exist when the event begins has no agentivity property. Each remaining node is a participant type, and together they form the agentivity lattice, a sublattice of the product. The named participant types anchor the case regions, CaseRegion, and Tsunoda's transitivity hierarchy places a canonical patient for each class.

Main definitions

• ParticipantType: an agentivity and a persistence level.
• ParticipantType.lattice: the valid participant types, Grimm's agentivity lattice.
• maximalAgent, maximalPatient, effectorAgent, sentientNonInstigator: named nodes.
• TransitivityRank: Tsunoda's transitivity hierarchy.

References

• [Gri11]
• [Tsu85]

@[reducible, inline]

abbrev ArgumentStructure.ParticipantType : Type

A participant type, a node of the product of the agentivity and persistence lattices.

Equations

• ArgumentStructure.ParticipantType = (ArgumentStructure.Agentivity × ArgumentStructure.PersistenceLevel)

def ArgumentStructure.ParticipantType.CrossValid (n : ParticipantType) : Prop

An argument not entailed to exist when the event begins has no agentivity property.

Equations

• n.CrossValid = (ArgumentStructure.PersistenceLevel.Feature.exPB ∈ n.2 ∨ n.1 = ∅)

@[instance_reducible]

instance ArgumentStructure.ParticipantType.instDecidablePredCrossValid : DecidablePred CrossValid

Equations

• x✝.instDecidablePredCrossValid = { decide := decide (ArgumentStructure.PersistenceLevel.Feature.exPB ∈ x✝.2) || decide (x✝.1 = ∅), reflects_decide := ⋯ }

def ArgumentStructure.ParticipantType.Valid (n : ParticipantType) : Prop

A participant type respects both the relation among the agentivity properties and the dependence of agentivity on initial existence.

Equations

• n.Valid = (n.1.Valid ∧ n.CrossValid)

@[instance_reducible]

instance ArgumentStructure.ParticipantType.instDecidablePredValid : DecidablePred Valid

Equations

• x✝.instDecidablePredValid = { decide := decide x✝.1.Valid && decide x✝.CrossValid, reflects_decide := ⋯ }

def ArgumentStructure.ParticipantType.lattice : Sublattice ParticipantType

The valid participant types form a sublattice of the product, Grimm's agentivity lattice.

Equations

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

@[simp]

theorem ArgumentStructure.ParticipantType.mem_lattice {n : ParticipantType} : n ∈ lattice ↔ n.Valid

theorem ArgumentStructure.ParticipantType.card_valid : (Finset.filter Valid Finset.univ).card = 38

Of the eighty nodes of the product, thirty-eight are valid.

Named participant types

def ArgumentStructure.maximalAgent : ParticipantType

The maximal agent has every agentivity property at total persistence; it is the top of the lattice and the prototypical transitive subject.

Equations

• ArgumentStructure.maximalAgent = ⊤

def ArgumentStructure.maximalPatient : ParticipantType

The maximal patient has no agentivity property and exists when the event begins but not after it, as the object of break or destroy does.

Equations

• ArgumentStructure.maximalPatient = (∅, ArgumentStructure.PersistenceLevel.exPersBeginning)

def ArgumentStructure.effectorAgent : ParticipantType

The effector has instigation and motion at total persistence, as the agent of the effective action verbs kill and break does ([Gri11] §3, Ia and IIa in Fig. 5).

Equations

• ArgumentStructure.effectorAgent = ({ArgumentStructure.Agentivity.Feature.instigation, ArgumentStructure.Agentivity.Feature.motion}, ArgumentStructure.PersistenceLevel.totalPersistence)

def ArgumentStructure.sentientNonInstigator : ParticipantType

Sentience without instigation at qualitative persistence (beginning), where Grimm's dative uses converge: recipients, dative experiencers and the second arguments of two-place communication and service verbs (§5.1, Fig. 7).

Equations

• ArgumentStructure.sentientNonInstigator = ({ArgumentStructure.Agentivity.Feature.sentience}, ArgumentStructure.PersistenceLevel.quPersBeginning)

The transitivity region

def ArgumentStructure.ParticipantType.InTransitiveRegion (n : ParticipantType) : Prop

A participant type is in the transitivity region when the argument exists at the beginning of the event, which both participants of the prototypical transitive event do ([Gri11] pp.529–530).

Equations

• n.InTransitiveRegion = (ArgumentStructure.PersistenceLevel.Feature.exPB ∈ n.2)

@[instance_reducible]

instance ArgumentStructure.instDecidablePredParticipantTypeInTransitiveRegion : DecidablePred ParticipantType.InTransitiveRegion

Equations

• ArgumentStructure.instDecidablePredParticipantTypeInTransitiveRegion x✝ = ArgumentStructure.instDecidablePredParticipantTypeInTransitiveRegion._aux_1 x✝

inductive ArgumentStructure.TransitivityRank : Type

Tsunoda's transitivity hierarchy ([Gri11] §3, example 8), distinct from the Burzio classification AuxiliarySelection.TransitivityClass.

• resultativeEffective : TransitivityRank

  Resultative effective action, kill and break: the object is destroyed.

• contact : TransitivityRank

  Contact, shoot and hit: the object is affected but persists.

• pursuit : TransitivityRank

  Pursuit, search and seek: the object need not exist.

@[instance_reducible]

instance ArgumentStructure.instDecidableEqTransitivityRank : DecidableEq TransitivityRank

Equations

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

@[instance_reducible]

instance ArgumentStructure.instReprTransitivityRank : Repr TransitivityRank

Equations

• ArgumentStructure.instReprTransitivityRank = { reprPrec := ArgumentStructure.instReprTransitivityRank.repr }

def ArgumentStructure.instReprTransitivityRank.repr : TransitivityRank → ℕ → Std.Format

Equations

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

def ArgumentStructure.TransitivityRank.patientType : TransitivityRank → ParticipantType

The canonical patient of each transitivity class (Fig. 5); the agent of classes I and II is effectorAgent, and the agent of class III adds sentience to it.

Equations

• ArgumentStructure.TransitivityRank.resultativeEffective.patientType = (∅, ArgumentStructure.PersistenceLevel.exPersBeginning)
• ArgumentStructure.TransitivityRank.contact.patientType = (∅, ArgumentStructure.PersistenceLevel.quPersBeginning)
• ArgumentStructure.TransitivityRank.pursuit.patientType = (∅, ArgumentStructure.PersistenceLevel.totalNonPersistence)