The Agentivity Lattice [Gri11]: carriers and order structure

[Gri11] reformulates [Dow91]'s proto-role entailments as privative features organized into a lattice via subset inclusion. The key innovations over Dowty:

1. Privative opposition (Table 2, §2.1): Proto-Patient is not a separate cluster but the underspecified (∅) pole of each agentivity feature. "Patient" = lacking agentive properties.

2. Instigation replaces causation: Dowty's "causing an event in another participant" is decomposed into "instigation" — independent action whose effects can be attributed to the argument. This removes the relational aspect (causation implies a second participant; instigation does not).

3. Persistence replaces P-Patient features (§2.2, Fig. 2): Dowty's 5 P-Patient entailments (CoS, IT, CA, stationary, DE) are replaced by 4 persistence dimensions tracking whether the entity persists existentially and qualitatively at the beginning and end of the event.

4. Lattice structure (§2.2): the possible feature combinations, ordered by inclusion and constrained by logical dependencies (volition → sentience), form a lattice. Cases are connected regions of this lattice (see Agentivity/CaseRegions.lean).

Carriers vs. Grimm's lattices

The carrier types here are implementation supersets of Grimm's lattices; the validity predicates carve out the paper's objects:

• AgentivityNode is the full Boolean cube on the four agentivity primitives (16 elements). Grimm's Fig. 1 lattice is its 12-node AgentivityNode.Valid subset (volition → sentience).
• PersistenceLevel is exactly Grimm's five valid persistence levels (Fig. 2) — here the carrier is the paper's object.
• GrimmNode is the full product carrier (80 elements). Grimm's Fig. 3 agentivity lattice is its 38-node GrimmNode.Valid subset (AgentivityValid ∧ CrossValid).

Mathlib integration

All ordering infrastructure uses Mathlib typeclasses:

• AgentivityNode: Lattice, BoundedOrder, Fintype
• PersistenceLevel: Lattice, BoundedOrder, Fintype
• GrimmNode: Lattice, BoundedOrder, Fintype

The bridges to [Dow91]'s EntailmentProfile live in EntailmentProfile.lean; the case-region geometry lives in Agentivity/CaseRegions.lean.

Agentivity primitives (Table 2, §2.1)

structure ArgumentStructure.AgentivityLattice.AgentivityNode : Type

The four agentivity primitives (Table 2 (agentive properties), p.520).

Each has an agentive (+) and non-agentive (∅) pole. The non-agentive pole is not a separate feature — it is simply the absence of the agentive property. This is the privative opposition that replaces Dowty's two independent clusters.

The carrier is the full 16-element Boolean cube; Grimm's Fig. 1 lattice is the 12-node Valid subset.

• volition : Bool

  +volition: the participant intends to bring about the event.

• sentience : Bool

  +sentience: conscious involvement in the action or state.

• instigation : Bool

  +instigation: prior independent action whose effects can be attributed to this argument. Replaces Dowty's "causation" (p.521).

• motion : Bool

  +motion: the argument is in motion during the event.

def ArgumentStructure.AgentivityLattice.instDecidableEqAgentivityNode.decEq (x✝ x✝¹ : AgentivityNode) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance ArgumentStructure.AgentivityLattice.instDecidableEqAgentivityNode : DecidableEq AgentivityNode

Equations

• ArgumentStructure.AgentivityLattice.instDecidableEqAgentivityNode = ArgumentStructure.AgentivityLattice.instDecidableEqAgentivityNode.decEq

def ArgumentStructure.AgentivityLattice.instReprAgentivityNode.repr : AgentivityNode → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance ArgumentStructure.AgentivityLattice.instReprAgentivityNode : Repr AgentivityNode

Equations

• ArgumentStructure.AgentivityLattice.instReprAgentivityNode = { reprPrec := ArgumentStructure.AgentivityLattice.instReprAgentivityNode.repr }

def ArgumentStructure.AgentivityLattice.AgentivityNode.Valid (a : AgentivityNode) : Prop

Validity constraint: volition presupposes sentience (p.521, following [Dow91] p.607). Carves Grimm's 12-node Fig. 1 lattice out of the 16-element carrier.

Equations

• a.Valid = (a.volition = true → a.sentience = true)

@[implicit_reducible]

instance ArgumentStructure.AgentivityLattice.instDecidableValid (a : AgentivityNode) : Decidable a.Valid

Equations

• ArgumentStructure.AgentivityLattice.instDecidableValid a = id inferInstance

def ArgumentStructure.AgentivityLattice.AgentivityNode.featureCount (a : AgentivityNode) : ℕ

Number of positive agentivity features (= height in the lattice).

Equations

• a.featureCount = a.volition.toNat + a.sentience.toNat + a.instigation.toNat + a.motion.toNat

def ArgumentStructure.AgentivityLattice.AgentivityNode.equiv : AgentivityNode ≃ Bool × Bool × Bool × Bool

Equivalence with Bool⁴ for Fintype derivation.

Equations

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

@[implicit_reducible]

instance ArgumentStructure.AgentivityLattice.instFintypeAgentivityNode : Fintype AgentivityNode

Equations

• ArgumentStructure.AgentivityLattice.instFintypeAgentivityNode = Fintype.ofEquiv (Bool × Bool × Bool × Bool) ArgumentStructure.AgentivityLattice.AgentivityNode.equiv.symm

@[implicit_reducible]

instance ArgumentStructure.AgentivityLattice.instPartialOrderAgentivityNode : PartialOrder AgentivityNode

Equations

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

@[implicit_reducible]

instance ArgumentStructure.AgentivityLattice.instDecidableRelAgentivityNodeLe : DecidableRel fun (x1 x2 : AgentivityNode) => x1 ≤ x2

Equations

• ArgumentStructure.AgentivityLattice.instDecidableRelAgentivityNodeLe a b = instDecidableEqBool (ArgumentStructure.AgentivityLattice.AgentivityNode.leBool✝ a b) true

@[implicit_reducible]

instance ArgumentStructure.AgentivityLattice.instDecidableRelAgentivityNodeLt : DecidableRel fun (x1 x2 : AgentivityNode) => x1 < x2

Equations

• ArgumentStructure.AgentivityLattice.instDecidableRelAgentivityNodeLt x✝¹ x✝ = decidable_of_iff' (x✝¹ ≤ x✝ ∧ ¬x✝ ≤ x✝¹) ⋯

@[implicit_reducible]

instance ArgumentStructure.AgentivityLattice.instLatticeAgentivityNode : Lattice AgentivityNode

Lattice: componentwise ∨ for join, ∧ for meet.

Equations

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

@[implicit_reducible]

instance ArgumentStructure.AgentivityLattice.instOrderBotAgentivityNode : OrderBot AgentivityNode

Equations

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

@[implicit_reducible]

instance ArgumentStructure.AgentivityLattice.instOrderTopAgentivityNode : OrderTop AgentivityNode

Equations

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

theorem ArgumentStructure.AgentivityLattice.AgentivityNode.le_iff (a b : AgentivityNode) : a ≤ b ↔ (a.volition = true → b.volition = true) ∧ (a.sentience = true → b.sentience = true) ∧ (a.instigation = true → b.instigation = true) ∧ (a.motion = true → b.motion = true)

Characterisation of the inclusion order by componentwise implication. Public interface to the private leBool; verified by decide over the 16 × 16 pairs.

theorem ArgumentStructure.AgentivityLattice.AgentivityNode.le_instigation_mono {a b : AgentivityNode} (hab : a ≤ b) (h : a.instigation = true) : b.instigation = true

theorem ArgumentStructure.AgentivityLattice.AgentivityNode.le_sentience_mono {a b : AgentivityNode} (hab : a ≤ b) (h : a.sentience = true) : b.sentience = true

theorem ArgumentStructure.AgentivityLattice.AgentivityNode.ge_instigation_mono {a b : AgentivityNode} (hab : a ≤ b) (h : b.instigation = false) : a.instigation = false

Persistence levels (§2.2, Fig. 2)

inductive ArgumentStructure.AgentivityLattice.PersistenceLevel : Type

The five valid persistence levels (p.524–525, Fig. 2).

Each level is a valid combination of four persistence dimensions:

• ExPB: existential persistence (beginning) — entity exists before event
• ExPE: existential persistence (end) — entity exists after event
• QuPB: qualitative persistence (beginning) — qualities unchanged before
• QuPE: qualitative persistence (end) — qualities unchanged after

Constraints (ExPB→QuPB, QuPE→ExPE, etc.) reduce the 16 possible combinations to exactly 5.

• totalNonPersistence : PersistenceLevel

  ∅ExPB, ∅ExPE, ∅QuPB, ∅QuPE — entity has no entailed existence. Arguments of seek, want; negated copulas.

• exPersEnd : PersistenceLevel

  ∅ExPB, +ExPE, ∅QuPB, +QuPE — entity comes into existence. Objects of build, invent; subjects of appear.

• exPersBeginning : PersistenceLevel

  +ExPB, ∅ExPE, +QuPB, ∅QuPE — entity exists before, ceases to exist. Subjects of die, evaporate; objects of destroy, ruin.

• quPersBeginning : PersistenceLevel

  +ExPB, +ExPE, +QuPB, ∅QuPE — entity persists but is qualitatively changed. Objects of transitive move, dim, frighten; intransitive subjects of fall.

• totalPersistence : PersistenceLevel

  +ExPB, +ExPE, +QuPB, +QuPE — entity persists unchanged throughout. Prototypical transitive subjects; unaffected objects of see, cut at.

@[implicit_reducible]

instance ArgumentStructure.AgentivityLattice.instDecidableEqPersistenceLevel : DecidableEq PersistenceLevel

Equations

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

@[implicit_reducible]

instance ArgumentStructure.AgentivityLattice.instReprPersistenceLevel : Repr PersistenceLevel

Equations

• ArgumentStructure.AgentivityLattice.instReprPersistenceLevel = { reprPrec := ArgumentStructure.AgentivityLattice.instReprPersistenceLevel.repr }

def ArgumentStructure.AgentivityLattice.instReprPersistenceLevel.repr : PersistenceLevel → ℕ → Std.Format

Equations

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

def ArgumentStructure.AgentivityLattice.PersistenceLevel.exPersB : PersistenceLevel → Bool

Existential persistence at beginning (positive feature). Also serves as "entity exists at the beginning of the event."

Equations

• ArgumentStructure.AgentivityLattice.PersistenceLevel.exPersBeginning.exPersB = true
• ArgumentStructure.AgentivityLattice.PersistenceLevel.quPersBeginning.exPersB = true
• ArgumentStructure.AgentivityLattice.PersistenceLevel.totalPersistence.exPersB = true
• x✝.exPersB = false

def ArgumentStructure.AgentivityLattice.PersistenceLevel.exPersE : PersistenceLevel → Bool

Existential persistence at end (positive feature).

Equations

• ArgumentStructure.AgentivityLattice.PersistenceLevel.exPersEnd.exPersE = true
• ArgumentStructure.AgentivityLattice.PersistenceLevel.quPersBeginning.exPersE = true
• ArgumentStructure.AgentivityLattice.PersistenceLevel.totalPersistence.exPersE = true
• x✝.exPersE = false

def ArgumentStructure.AgentivityLattice.PersistenceLevel.quPersB : PersistenceLevel → Bool

Qualitative persistence at beginning (positive feature).

Equations

• ArgumentStructure.AgentivityLattice.PersistenceLevel.exPersBeginning.quPersB = true
• ArgumentStructure.AgentivityLattice.PersistenceLevel.quPersBeginning.quPersB = true
• ArgumentStructure.AgentivityLattice.PersistenceLevel.totalPersistence.quPersB = true
• x✝.quPersB = false

def ArgumentStructure.AgentivityLattice.PersistenceLevel.quPersE : PersistenceLevel → Bool

Qualitative persistence at end (positive feature).

Equations

• ArgumentStructure.AgentivityLattice.PersistenceLevel.exPersEnd.quPersE = true
• ArgumentStructure.AgentivityLattice.PersistenceLevel.totalPersistence.quPersE = true
• x✝.quPersE = false

def ArgumentStructure.AgentivityLattice.PersistenceLevel.featureCount : PersistenceLevel → ℕ

Number of positive persistence features.

Equations

• ArgumentStructure.AgentivityLattice.PersistenceLevel.totalNonPersistence.featureCount = 0
• ArgumentStructure.AgentivityLattice.PersistenceLevel.exPersEnd.featureCount = 2
• ArgumentStructure.AgentivityLattice.PersistenceLevel.exPersBeginning.featureCount = 2
• ArgumentStructure.AgentivityLattice.PersistenceLevel.quPersBeginning.featureCount = 3
• ArgumentStructure.AgentivityLattice.PersistenceLevel.totalPersistence.featureCount = 4

@[implicit_reducible]

instance ArgumentStructure.AgentivityLattice.instFintypePersistenceLevel : Fintype PersistenceLevel

Equations

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

@[implicit_reducible]

instance ArgumentStructure.AgentivityLattice.instPartialOrderPersistenceLevel : PartialOrder PersistenceLevel

Equations

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

@[implicit_reducible]

instance ArgumentStructure.AgentivityLattice.instDecidableRelPersistenceLevelLe : DecidableRel fun (x1 x2 : PersistenceLevel) => x1 ≤ x2

Equations

• ArgumentStructure.AgentivityLattice.instDecidableRelPersistenceLevelLe a b = instDecidableEqBool (ArgumentStructure.AgentivityLattice.PersistenceLevel.leBool✝ a b) true

@[implicit_reducible]

instance ArgumentStructure.AgentivityLattice.instOrderBotPersistenceLevel : OrderBot PersistenceLevel

Equations

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

@[implicit_reducible]

instance ArgumentStructure.AgentivityLattice.instOrderTopPersistenceLevel : OrderTop PersistenceLevel

Equations

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

def ArgumentStructure.AgentivityLattice.PersistenceLevel.sup' (a b : PersistenceLevel) : PersistenceLevel

Join on persistence levels. The 5 valid levels do not form a sublattice of the powerset on {ExPB, ExPE, QuPB, QuPE} — the join is the smallest valid level containing the union of features.

Equations

• One or more equations did not get rendered due to their size.
• ArgumentStructure.AgentivityLattice.PersistenceLevel.totalNonPersistence.sup' b = b
• a.sup' ArgumentStructure.AgentivityLattice.PersistenceLevel.totalNonPersistence = a
• ArgumentStructure.AgentivityLattice.PersistenceLevel.totalPersistence.sup' b = ArgumentStructure.AgentivityLattice.PersistenceLevel.totalPersistence
• a.sup' ArgumentStructure.AgentivityLattice.PersistenceLevel.totalPersistence = ArgumentStructure.AgentivityLattice.PersistenceLevel.totalPersistence

def ArgumentStructure.AgentivityLattice.PersistenceLevel.inf' (a b : PersistenceLevel) : PersistenceLevel

Meet on persistence levels. The largest valid level contained in the intersection of features.

Equations

• One or more equations did not get rendered due to their size.
• ArgumentStructure.AgentivityLattice.PersistenceLevel.totalPersistence.inf' b = b
• a.inf' ArgumentStructure.AgentivityLattice.PersistenceLevel.totalPersistence = a
• ArgumentStructure.AgentivityLattice.PersistenceLevel.totalNonPersistence.inf' b = ArgumentStructure.AgentivityLattice.PersistenceLevel.totalNonPersistence
• a.inf' ArgumentStructure.AgentivityLattice.PersistenceLevel.totalNonPersistence = ArgumentStructure.AgentivityLattice.PersistenceLevel.totalNonPersistence

@[implicit_reducible]

instance ArgumentStructure.AgentivityLattice.instLatticePersistenceLevel : Lattice PersistenceLevel

Equations

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

Combined agentivity-lattice node (§2.2, Fig. 3)

structure ArgumentStructure.AgentivityLattice.GrimmNode : Type

A node of the product carrier: agentivity features × persistence level (80 elements). Grimm's Fig. 3 agentivity lattice is the 38-node Valid subset, carved by:

1. volition → sentience (AgentivityValid)
2. If the argument does not exist at the beginning (totalNonPersistence or exPersEnd), it cannot have any agentivity properties (CrossValid, p.526–527).

• agentivity : AgentivityNode
• persistence : PersistenceLevel

def ArgumentStructure.AgentivityLattice.instDecidableEqGrimmNode.decEq (x✝ x✝¹ : GrimmNode) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance ArgumentStructure.AgentivityLattice.instDecidableEqGrimmNode : DecidableEq GrimmNode

Equations

• ArgumentStructure.AgentivityLattice.instDecidableEqGrimmNode = ArgumentStructure.AgentivityLattice.instDecidableEqGrimmNode.decEq

@[implicit_reducible]

instance ArgumentStructure.AgentivityLattice.instReprGrimmNode : Repr GrimmNode

Equations

• ArgumentStructure.AgentivityLattice.instReprGrimmNode = { reprPrec := ArgumentStructure.AgentivityLattice.instReprGrimmNode.repr }

def ArgumentStructure.AgentivityLattice.instReprGrimmNode.repr : GrimmNode → ℕ → Std.Format

Equations

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

def ArgumentStructure.AgentivityLattice.GrimmNode.AgentivityValid (n : GrimmNode) : Prop

The agentivity constraint: volition → sentience.

Equations

• n.AgentivityValid = n.agentivity.Valid

@[implicit_reducible]

instance ArgumentStructure.AgentivityLattice.instDecidableAgentivityValid (n : GrimmNode) : Decidable n.AgentivityValid

Equations

• ArgumentStructure.AgentivityLattice.instDecidableAgentivityValid n = id inferInstance

def ArgumentStructure.AgentivityLattice.GrimmNode.CrossValid (n : GrimmNode) : Prop

The cross-lattice constraint: if the argument does not exist at the beginning of the event, it cannot have any agentivity properties.

Equations

• n.CrossValid = (n.persistence.exPersB = true ∨ n.agentivity = ⊥)

@[implicit_reducible]

instance ArgumentStructure.AgentivityLattice.instDecidableCrossValid (n : GrimmNode) : Decidable n.CrossValid

Equations

• ArgumentStructure.AgentivityLattice.instDecidableCrossValid n = id inferInstance

def ArgumentStructure.AgentivityLattice.GrimmNode.Valid (n : GrimmNode) : Prop

Full validity: both constraints satisfied. Carves Grimm's 38-node Fig. 3 lattice out of the 80-element carrier.

Equations

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

@[implicit_reducible]

instance ArgumentStructure.AgentivityLattice.instDecidableValid_1 (n : GrimmNode) : Decidable n.Valid

Equations

• ArgumentStructure.AgentivityLattice.instDecidableValid_1 n = id inferInstance

def ArgumentStructure.AgentivityLattice.GrimmNode.featureCount (n : GrimmNode) : ℕ

Total feature count (agentivity + persistence).

Equations

• n.featureCount = n.agentivity.featureCount + n.persistence.featureCount

def ArgumentStructure.AgentivityLattice.GrimmNode.equiv : GrimmNode ≃ AgentivityNode × PersistenceLevel

Equations

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

@[implicit_reducible]

instance ArgumentStructure.AgentivityLattice.instFintypeGrimmNode : Fintype GrimmNode

Equations

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

@[implicit_reducible]

instance ArgumentStructure.AgentivityLattice.instLEGrimmNode : LE GrimmNode

Product order: componentwise ≤ on agentivity and persistence.

Equations

• ArgumentStructure.AgentivityLattice.instLEGrimmNode = { le := fun (a b : ArgumentStructure.AgentivityLattice.GrimmNode) => a.agentivity ≤ b.agentivity ∧ a.persistence ≤ b.persistence }

@[implicit_reducible]

instance ArgumentStructure.AgentivityLattice.instLTGrimmNode : LT GrimmNode

Equations

• ArgumentStructure.AgentivityLattice.instLTGrimmNode = { lt := fun (a b : ArgumentStructure.AgentivityLattice.GrimmNode) => a ≤ b ∧ ¬b ≤ a }

@[implicit_reducible]

instance ArgumentStructure.AgentivityLattice.instPartialOrderGrimmNode : PartialOrder GrimmNode

Equations

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

@[implicit_reducible]

instance ArgumentStructure.AgentivityLattice.instDecidableRelGrimmNodeLe : DecidableRel fun (x1 x2 : GrimmNode) => x1 ≤ x2

Equations

• ArgumentStructure.AgentivityLattice.instDecidableRelGrimmNodeLe a b = instDecidableAnd

@[implicit_reducible]

instance ArgumentStructure.AgentivityLattice.instOrderBotGrimmNode : OrderBot GrimmNode

Equations

• ArgumentStructure.AgentivityLattice.instOrderBotGrimmNode = { bot := { agentivity := ⊥, persistence := ⊥ }, bot_le := ArgumentStructure.AgentivityLattice.instOrderBotGrimmNode._proof_1 }

@[implicit_reducible]

instance ArgumentStructure.AgentivityLattice.instOrderTopGrimmNode : OrderTop GrimmNode

Equations

• ArgumentStructure.AgentivityLattice.instOrderTopGrimmNode = { top := { agentivity := ⊤, persistence := ⊤ }, le_top := ArgumentStructure.AgentivityLattice.instOrderTopGrimmNode._proof_1 }

@[implicit_reducible]

instance ArgumentStructure.AgentivityLattice.instLatticeGrimmNode : Lattice GrimmNode

Componentwise lattice: meet/join on each axis independently.

Equations

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

Named participant types

def ArgumentStructure.AgentivityLattice.maximalAgent : GrimmNode

Maximal Agent (Fig. 4): all agentivity features, total persistence. The prototypical transitive subject.

Equations

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

def ArgumentStructure.AgentivityLattice.maximalPatient : GrimmNode

Maximal Patient (Fig. 4): no agentivity features, existential persistence (beginning). The prototypical affected object that ceases to exist (break, destroy).

Equations

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

def ArgumentStructure.AgentivityLattice.effectorAgent : GrimmNode

The "effector" participant type: instigation + motion, total persistence. The canonical agent of effective action verbs (kill, break). §3, labeled Ia/IIa in Fig. 5.

Equations

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

def ArgumentStructure.AgentivityLattice.sentientNonInstigatorNode : GrimmNode

The lattice position {sentience} × qualitative persistence (beginning). Per Grimm 2011 §5.1, diverse uses of the dative converge on this single region — recipients, experiencers, and benefactives are aliases below.

Equations

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

@[reducible, inline]

abbrev ArgumentStructure.AgentivityLattice.experiencerNode : GrimmNode

Dative experiencer of psych verbs (§5.1.1). Alias of sentientNonInstigatorNode — the convergence with recipientNode is by construction, not a theorem.

Equations

• ArgumentStructure.AgentivityLattice.experiencerNode = ArgumentStructure.AgentivityLattice.sentientNonInstigatorNode

@[reducible, inline]

abbrev ArgumentStructure.AgentivityLattice.recipientNode : GrimmNode

Canonical dative recipient (Fig. 7). Alias of sentientNonInstigatorNode — see the docstring there for the unified treatment.

Equations

• ArgumentStructure.AgentivityLattice.recipientNode = ArgumentStructure.AgentivityLattice.sentientNonInstigatorNode

Transitivity region (§3, Fig. 4)

def ArgumentStructure.AgentivityLattice.GrimmNode.InTransitiveRegion (n : GrimmNode) : Prop

A node is in the transitivity region iff its persistence level is in {exPersBeginning, quPersBeginning, totalPersistence}.

The transitivity region excludes totalNonPersistence and exPersEnd because the prototypical transitive event requires both participants to exist at the beginning (p.529–530).

Equations

• n.InTransitiveRegion = (n.persistence.exPersB = true)

@[implicit_reducible]

instance ArgumentStructure.AgentivityLattice.instDecidableInTransitiveRegion (n : GrimmNode) : Decidable n.InTransitiveRegion

Equations

• ArgumentStructure.AgentivityLattice.instDecidableInTransitiveRegion n = id inferInstance

inductive ArgumentStructure.AgentivityLattice.TransitivityRank : Type

Tsunoda's transitivity hierarchy (§3, example 8).

Class	Example verbs	Transitivity
I	kill, break	Highest
II	shoot, hit	Middle
III	search, seek	Lowest

Named TransitivityRank (rank on Tsunoda's hierarchy) to avoid collision with ArgumentStructure.AuxiliarySelection.TransitivityClass (the Burzio unaccusative/unergative/transitive classification).

• resultativeEffective : TransitivityRank

  Resultative Effective Action: kill, break. Object is destroyed (exPersBeginning). Maximal opposition between agent and patient.

• contact : TransitivityRank

  Contact: shoot, hit. Object is affected but persists (quPersBeginning). Less opposition than Class I.

• pursuit : TransitivityRank

  Pursuit: search, seek. Object may not even exist (totalNonPersistence). Outside the transitivity region.

@[implicit_reducible]

instance ArgumentStructure.AgentivityLattice.instDecidableEqTransitivityRank : DecidableEq TransitivityRank

Equations

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

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

Equations

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

@[implicit_reducible]

instance ArgumentStructure.AgentivityLattice.instReprTransitivityRank : Repr TransitivityRank

Equations

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

def ArgumentStructure.AgentivityLattice.TransitivityRank.patientNode : TransitivityRank → GrimmNode

The canonical patient position for each transitivity class (Fig. 5). The agent position for all three classes is effectorAgent (Fig. 5, Ia/IIa share the same agent node; Grimm doesn't separately label IIIa).

Equations

• ArgumentStructure.AgentivityLattice.TransitivityRank.resultativeEffective.patientNode = { agentivity := ⊥, persistence := ArgumentStructure.AgentivityLattice.PersistenceLevel.exPersBeginning }
• ArgumentStructure.AgentivityLattice.TransitivityRank.contact.patientNode = { agentivity := ⊥, persistence := ArgumentStructure.AgentivityLattice.PersistenceLevel.quPersBeginning }
• ArgumentStructure.AgentivityLattice.TransitivityRank.pursuit.patientNode = { agentivity := ⊥, persistence := ArgumentStructure.AgentivityLattice.PersistenceLevel.totalNonPersistence }

Lattice properties (from Mathlib instances)

Reflexivity, transitivity, antisymmetry are provided by PartialOrder; ⊥ ≤ a, a ≤ ⊤ by OrderBot/OrderTop; join/meet associativity, commutativity, absorption by Lattice.

theorem ArgumentStructure.AgentivityLattice.exPersEnd_incomparable_exPersBeginning : ¬PersistenceLevel.exPersEnd ≤ PersistenceLevel.exPersBeginning ∧ ¬PersistenceLevel.exPersBeginning ≤ PersistenceLevel.exPersEnd

Persistence incomparability: exPersEnd and exPersBeginning are incomparable — neither is a subset of the other's features.

theorem ArgumentStructure.AgentivityLattice.exPersEnd_sup_exPersBeginning : PersistenceLevel.exPersEnd ⊔ PersistenceLevel.exPersBeginning = ⊤

Their join is ⊤ (totalPersistence).

theorem ArgumentStructure.AgentivityLattice.exPersEnd_inf_exPersBeginning : PersistenceLevel.exPersEnd ⊓ PersistenceLevel.exPersBeginning = ⊥

Their meet is ⊥ (totalNonPersistence).

@[simp]

theorem ArgumentStructure.AgentivityLattice.maximalAgent_eq_top : maximalAgent = ⊤

Maximal agent is ⊤ on the combined lattice.

Named participant verification

theorem ArgumentStructure.AgentivityLattice.maximalAgent_valid : maximalAgent.Valid

theorem ArgumentStructure.AgentivityLattice.maximalPatient_valid : maximalPatient.Valid

theorem ArgumentStructure.AgentivityLattice.effectorAgent_valid : effectorAgent.Valid

theorem ArgumentStructure.AgentivityLattice.experiencerNode_valid : experiencerNode.Valid

theorem ArgumentStructure.AgentivityLattice.maximalAgent_featureCount : maximalAgent.featureCount = 8

theorem ArgumentStructure.AgentivityLattice.maximalPatient_featureCount : maximalPatient.featureCount = 2

theorem ArgumentStructure.AgentivityLattice.maximalPatient_le_maximalAgent : maximalPatient ≤ maximalAgent

theorem ArgumentStructure.AgentivityLattice.maximalAgent_not_le_maximalPatient : ¬maximalAgent ≤ maximalPatient

theorem ArgumentStructure.AgentivityLattice.maximalAgent_in_transitiveRegion : maximalAgent.InTransitiveRegion

theorem ArgumentStructure.AgentivityLattice.maximalPatient_in_transitiveRegion : maximalPatient.InTransitiveRegion

Upward/downward closure (§2.3, p.528)

theorem ArgumentStructure.AgentivityLattice.agent_upward_closed (minReq a b : AgentivityNode) (ha : minReq ≤ a) (hab : a ≤ b) : minReq ≤ b

Agents are upwards closed in the agentivity dimension (p.528): if a qualifies as agent for a predicate (i.e., a has at least the entailments required by the verb), then any b ≥ a also qualifies. An entity with more agentive properties can always fill an agent role requiring fewer.

Formally: the set of acceptable agents for a verb with minimum requirement minReq is {a | minReq ≤ a}, which is an upper set.

theorem ArgumentStructure.AgentivityLattice.patient_downward_closed (maxPers p q : PersistenceLevel) (hp : p ≤ maxPers) (hqp : q ≤ p) : q ≤ maxPers

Patients are downwards closed in the persistence dimension (p.528): if p qualifies as patient (i.e., p has at most the persistence features of the verb's patient slot), then any q ≤ p also qualifies. A more affected entity (less persistence) can always fill a patient role.

Formally: the set of acceptable patients for a verb with maximum persistence maxPers is {p | p ≤ maxPers}, which is a lower set.

Persistence covering relations (Fig. 2)

theorem ArgumentStructure.AgentivityLattice.exPersEnd_incomparable_quPersBeginning : ¬PersistenceLevel.exPersEnd ≤ PersistenceLevel.quPersBeginning ∧ ¬PersistenceLevel.quPersBeginning ≤ PersistenceLevel.exPersEnd

exPersEnd and quPersBeginning are incomparable (neither ≤ the other). Their feature sets are {ExPE, QuPE} and {ExPB, ExPE, QuPB} — QuPE ∉ {ExPB, ExPE, QuPB} and ExPB ∉ {ExPE, QuPE}. This means the persistence lattice has TWO independent paths from ⊥ to ⊤: (1) ⊥ → exPersEnd → ⊤ (2) ⊥ → exPersBeginning → quPersBeginning → ⊤

theorem ArgumentStructure.AgentivityLattice.persistence_chain : PersistenceLevel.exPersBeginning ≤ PersistenceLevel.quPersBeginning ∧ PersistenceLevel.quPersBeginning ≤ PersistenceLevel.totalPersistence

The persistence lattice inclusion chain (2) from Fig. 2: exPersBeginning ≤ quPersBeginning ≤ totalPersistence.