The Agentivity Lattice @cite{grimm-2011} #

@cite{grimm-2011} reformulates @cite{dowty-1991}'s proto-role entailments as privative features organized into a lattice via subset inclusion. The key innovations over Dowty:

Privative opposition: Proto-Patient is not a separate cluster but the underspecified (∅) pole of each agentivity feature. "Patient" = lacking agentive properties.
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).
Persistence replaces P-Patient features: 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.
Lattice structure: The powerset of features, ordered by inclusion and constrained by logical dependencies (volition → sentience), forms a lattice. Cases are connected regions of this lattice.

Mathlib integration #

All ordering infrastructure uses Mathlib typeclasses:

AgentivityNode: Lattice, BoundedOrder, Fintype (16 elements)
PersistenceLevel: Lattice, BoundedOrder, Fintype (5 elements)
GrimmNode: PartialOrder, BoundedOrder, Fintype (80 elements)

Bridges #

AgentivityNode.fromEntailmentProfile → EntailmentProfile (proto-roles)
PersistenceLevel.fromEntailmentProfile → EntailmentProfile (proto-roles)
GrimmNode.toCaseRegion → Core.Case (case assignment)
Transitivity hierarchy → Tsunoda verb classification

source

structure Semantics.Events.AgentivityLattice.AgentivityNode :

Type

The four agentivity primitives (@cite{grimm-2011} 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.

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" (@cite{grimm-2011} p.521).
motion : Bool
+motion: the argument is in motion during the event.

Instances For

source

def Semantics.Events.AgentivityLattice.instDecidableEqAgentivityNode.decEq (x✝ x✝¹ : AgentivityNode) :

Decidable (x✝ = x✝¹)

Equations

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

Instances For

source

instance Semantics.Events.AgentivityLattice.instDecidableEqAgentivityNode :

DecidableEq AgentivityNode

Equations

Semantics.Events.AgentivityLattice.instDecidableEqAgentivityNode = Semantics.Events.AgentivityLattice.instDecidableEqAgentivityNode.decEq

source

instance Semantics.Events.AgentivityLattice.instReprAgentivityNode :

Repr AgentivityNode

Equations

Semantics.Events.AgentivityLattice.instReprAgentivityNode = { reprPrec := Semantics.Events.AgentivityLattice.instReprAgentivityNode.repr }

source

def Semantics.Events.AgentivityLattice.instReprAgentivityNode.repr :

AgentivityNode → ℕ → Std.Format

Equations

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

Instances For

source

def Semantics.Events.AgentivityLattice.instBEqAgentivityNode.beq :

AgentivityNode → AgentivityNode → Bool

Equations

One or more equations did not get rendered due to their size.
Semantics.Events.AgentivityLattice.instBEqAgentivityNode.beq x✝¹ x✝ = false

Instances For

source

instance Semantics.Events.AgentivityLattice.instBEqAgentivityNode :

BEq AgentivityNode

Equations

Semantics.Events.AgentivityLattice.instBEqAgentivityNode = { beq := Semantics.Events.AgentivityLattice.instBEqAgentivityNode.beq }

source

def Semantics.Events.AgentivityLattice.AgentivityNode.valid (a : AgentivityNode) :

Bool

Validity constraint: volition presupposes sentience (@cite{grimm-2011} p.521, following @cite{dowty-1991} p.607).

Equations

a.valid = (!a.volition || a.sentience)

Instances For

source

def Semantics.Events.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

Instances For

source

def Semantics.Events.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.

Instances For

source

instance Semantics.Events.AgentivityLattice.instFintypeAgentivityNode :

Fintype AgentivityNode

Equations

Semantics.Events.AgentivityLattice.instFintypeAgentivityNode = Fintype.ofEquiv (Bool × Bool × Bool × Bool) Semantics.Events.AgentivityLattice.AgentivityNode.equiv.symm

source

instance Semantics.Events.AgentivityLattice.instPartialOrderAgentivityNode :

PartialOrder AgentivityNode

Equations

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

source

instance Semantics.Events.AgentivityLattice.instDecidableRelAgentivityNodeLe :

DecidableRel fun (x1 x2 : AgentivityNode) => x1 ≤ x2

Equations

Semantics.Events.AgentivityLattice.instDecidableRelAgentivityNodeLe a b = inferInstanceAs (Decidable (Semantics.Events.AgentivityLattice.AgentivityNode.leBool✝ a b = true))

source

instance Semantics.Events.AgentivityLattice.instLatticeAgentivityNode :

Lattice AgentivityNode

Lattice: componentwise ∨ for join, ∧ for meet.

Equations

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

source

instance Semantics.Events.AgentivityLattice.instOrderBotAgentivityNode :

OrderBot AgentivityNode

Equations

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

source

instance Semantics.Events.AgentivityLattice.instOrderTopAgentivityNode :

OrderTop AgentivityNode

Equations

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

source

inductive Semantics.Events.AgentivityLattice.PersistenceLevel :

Type

The five valid persistence levels (@cite{grimm-2011} 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.

Instances For

source

instance Semantics.Events.AgentivityLattice.instDecidableEqPersistenceLevel :

DecidableEq PersistenceLevel

Equations

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

source

def Semantics.Events.AgentivityLattice.instReprPersistenceLevel.repr :

PersistenceLevel → ℕ → Std.Format

Equations

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

Instances For

source

instance Semantics.Events.AgentivityLattice.instReprPersistenceLevel :

Repr PersistenceLevel

Equations

Semantics.Events.AgentivityLattice.instReprPersistenceLevel = { reprPrec := Semantics.Events.AgentivityLattice.instReprPersistenceLevel.repr }

source

def Semantics.Events.AgentivityLattice.instBEqPersistenceLevel.beq :

PersistenceLevel → PersistenceLevel → Bool

Equations

Semantics.Events.AgentivityLattice.instBEqPersistenceLevel.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

source

instance Semantics.Events.AgentivityLattice.instBEqPersistenceLevel :

BEq PersistenceLevel

Equations

Semantics.Events.AgentivityLattice.instBEqPersistenceLevel = { beq := Semantics.Events.AgentivityLattice.instBEqPersistenceLevel.beq }

source

def Semantics.Events.AgentivityLattice.PersistenceLevel.exPersB :

PersistenceLevel → Bool

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

Equations

Instances For

source

def Semantics.Events.AgentivityLattice.PersistenceLevel.exPersE :

PersistenceLevel → Bool

Existential persistence at end (positive feature).

Equations

Instances For

source

def Semantics.Events.AgentivityLattice.PersistenceLevel.quPersB :

PersistenceLevel → Bool

Qualitative persistence at beginning (positive feature).

Equations

Instances For

source

def Semantics.Events.AgentivityLattice.PersistenceLevel.quPersE :

PersistenceLevel → Bool

Qualitative persistence at end (positive feature).

Equations

Instances For

source

def Semantics.Events.AgentivityLattice.PersistenceLevel.featureCount :

PersistenceLevel → ℕ

Number of positive persistence features.

Equations

Instances For

source

instance Semantics.Events.AgentivityLattice.instFintypePersistenceLevel :

Fintype PersistenceLevel

Equations

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

source

instance Semantics.Events.AgentivityLattice.instPartialOrderPersistenceLevel :

PartialOrder PersistenceLevel

Equations

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

source

instance Semantics.Events.AgentivityLattice.instDecidableRelPersistenceLevelLe :

DecidableRel fun (x1 x2 : PersistenceLevel) => x1 ≤ x2

Equations

Semantics.Events.AgentivityLattice.instDecidableRelPersistenceLevelLe a b = inferInstanceAs (Decidable (Semantics.Events.AgentivityLattice.PersistenceLevel.leBool✝ a b = true))

source

instance Semantics.Events.AgentivityLattice.instOrderBotPersistenceLevel :

OrderBot PersistenceLevel

Equations

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

source

instance Semantics.Events.AgentivityLattice.instOrderTopPersistenceLevel :

OrderTop PersistenceLevel

Equations

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

source

def Semantics.Events.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

Instances For

source

def Semantics.Events.AgentivityLattice.PersistenceLevel.inf' (a b : PersistenceLevel) :

PersistenceLevel

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

Equations

Instances For

source

instance Semantics.Events.AgentivityLattice.instLatticePersistenceLevel :

Lattice PersistenceLevel

Equations

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

source

structure Semantics.Events.AgentivityLattice.GrimmNode :

Type

A node in the full agentivity lattice = agentivity features × persistence level, subject to:

volition → sentience (agentivity constraint)
If the argument does not exist at the beginning (totalNonPersistence or exPersEnd), it cannot have any agentivity properties (@cite{grimm-2011} p.526–527).

agentivity : AgentivityNode
persistence : PersistenceLevel

Instances For

source

def Semantics.Events.AgentivityLattice.instDecidableEqGrimmNode.decEq (x✝ x✝¹ : GrimmNode) :

Decidable (x✝ = x✝¹)

Equations

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

Instances For

source

instance Semantics.Events.AgentivityLattice.instDecidableEqGrimmNode :

DecidableEq GrimmNode

Equations

Semantics.Events.AgentivityLattice.instDecidableEqGrimmNode = Semantics.Events.AgentivityLattice.instDecidableEqGrimmNode.decEq

source

instance Semantics.Events.AgentivityLattice.instReprGrimmNode :

Repr GrimmNode

Equations

Semantics.Events.AgentivityLattice.instReprGrimmNode = { reprPrec := Semantics.Events.AgentivityLattice.instReprGrimmNode.repr }

source

def Semantics.Events.AgentivityLattice.instReprGrimmNode.repr :

GrimmNode → ℕ → Std.Format

Equations

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

Instances For

source

def Semantics.Events.AgentivityLattice.instBEqGrimmNode.beq :

GrimmNode → GrimmNode → Bool

Equations

Semantics.Events.AgentivityLattice.instBEqGrimmNode.beq { agentivity := a, persistence := a_1 } { agentivity := b, persistence := b_1 } = (a == b && a_1 == b_1)
Semantics.Events.AgentivityLattice.instBEqGrimmNode.beq x✝¹ x✝ = false

Instances For

source

instance Semantics.Events.AgentivityLattice.instBEqGrimmNode :

BEq GrimmNode

Equations

Semantics.Events.AgentivityLattice.instBEqGrimmNode = { beq := Semantics.Events.AgentivityLattice.instBEqGrimmNode.beq }

source

def Semantics.Events.AgentivityLattice.GrimmNode.agentivityValid (n : GrimmNode) :

Bool

The agentivity constraint: volition → sentience.

Equations

n.agentivityValid = n.agentivity.valid

Instances For

source

def Semantics.Events.AgentivityLattice.GrimmNode.crossValid (n : GrimmNode) :

Bool

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 || n.agentivity == ⊥)

Instances For

source

def Semantics.Events.AgentivityLattice.GrimmNode.valid (n : GrimmNode) :

Bool

Full validity: both constraints satisfied.

Equations

n.valid = (n.agentivityValid && n.crossValid)

Instances For

source

def Semantics.Events.AgentivityLattice.GrimmNode.featureCount (n : GrimmNode) :

ℕ

Total feature count (agentivity + persistence).

Equations

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

Instances For

source

def Semantics.Events.AgentivityLattice.GrimmNode.equiv :

GrimmNode ≃ AgentivityNode × PersistenceLevel

Equations

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

Instances For

source

instance Semantics.Events.AgentivityLattice.instFintypeGrimmNode :

Fintype GrimmNode

Equations

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

source

instance Semantics.Events.AgentivityLattice.instLEGrimmNode :

LE GrimmNode

Product order: componentwise ≤ on agentivity and persistence.

Equations

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

source

instance Semantics.Events.AgentivityLattice.instLTGrimmNode :

LT GrimmNode

Equations

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

source

instance Semantics.Events.AgentivityLattice.instPartialOrderGrimmNode :

PartialOrder GrimmNode

Equations

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

source

instance Semantics.Events.AgentivityLattice.instDecidableRelGrimmNodeLe :

DecidableRel fun (x1 x2 : GrimmNode) => x1 ≤ x2

Equations

Semantics.Events.AgentivityLattice.instDecidableRelGrimmNodeLe a b = inferInstanceAs (Decidable (a.agentivity ≤ b.agentivity ∧ a.persistence ≤ b.persistence))

source

instance Semantics.Events.AgentivityLattice.instOrderBotGrimmNode :

OrderBot GrimmNode

Equations

Semantics.Events.AgentivityLattice.instOrderBotGrimmNode = { bot := { agentivity := ⊥, persistence := ⊥ }, bot_le := Semantics.Events.AgentivityLattice.instOrderBotGrimmNode._proof_1 }

source

instance Semantics.Events.AgentivityLattice.instOrderTopGrimmNode :

OrderTop GrimmNode

Equations

Semantics.Events.AgentivityLattice.instOrderTopGrimmNode = { top := { agentivity := ⊤, persistence := ⊤ }, le_top := Semantics.Events.AgentivityLattice.instOrderTopGrimmNode._proof_1 }

source

def Semantics.Events.AgentivityLattice.maximalAgent :

GrimmNode

Maximal Agent (@cite{grimm-2011} Fig. 4): all agentivity features, total persistence. The prototypical transitive subject.

Equations

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

Instances For

source

def Semantics.Events.AgentivityLattice.maximalPatient :

GrimmNode

Maximal Patient (@cite{grimm-2011} 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.

Instances For

source

def Semantics.Events.AgentivityLattice.effectorAgent :

GrimmNode

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

Equations

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

Instances For

source

def Semantics.Events.AgentivityLattice.experiencerNode :

GrimmNode

Experiencer: sentience only, qualitative persistence (beginning). The dative experiencer of psych verbs (@cite{grimm-2011} §5.1.1).

Equations

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

Instances For

source

def Semantics.Events.AgentivityLattice.recipientNode :

GrimmNode

Recipient: sentience, qualitative persistence (beginning). The canonical dative recipient (@cite{grimm-2011} Fig. 7).

Equations

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

Instances For

source

def Semantics.Events.AgentivityLattice.GrimmNode.inTransitiveRegion (n : GrimmNode) :

Bool

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 (@cite{grimm-2011} p.529–530).

Equations

n.inTransitiveRegion = n.persistence.exPersB

Instances For

source

inductive Semantics.Events.AgentivityLattice.TransitivityClass :

Type

Tsunoda's transitivity hierarchy (@cite{grimm-2011} §3, example 8).

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

resultativeEffective : TransitivityClass
Resultative Effective Action: kill, break. Object is destroyed (exPersBeginning). Maximal opposition between agent and patient.
contact : TransitivityClass
Contact: shoot, hit. Object is affected but persists (quPersBeginning). Less opposition than Class I.
pursuit : TransitivityClass
Pursuit: search, seek. Object may not even exist (totalNonPersistence). Outside the transitivity region.

Instances For

source

instance Semantics.Events.AgentivityLattice.instDecidableEqTransitivityClass :

DecidableEq TransitivityClass

Equations

Semantics.Events.AgentivityLattice.instDecidableEqTransitivityClass x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

source

instance Semantics.Events.AgentivityLattice.instReprTransitivityClass :

Repr TransitivityClass

Equations

Semantics.Events.AgentivityLattice.instReprTransitivityClass = { reprPrec := Semantics.Events.AgentivityLattice.instReprTransitivityClass.repr }

source

def Semantics.Events.AgentivityLattice.instReprTransitivityClass.repr :

TransitivityClass → ℕ → Std.Format

Equations

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

Instances For

source

def Semantics.Events.AgentivityLattice.instBEqTransitivityClass.beq :

TransitivityClass → TransitivityClass → Bool

Equations

Semantics.Events.AgentivityLattice.instBEqTransitivityClass.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

source

instance Semantics.Events.AgentivityLattice.instBEqTransitivityClass :

BEq TransitivityClass

Equations

Semantics.Events.AgentivityLattice.instBEqTransitivityClass = { beq := Semantics.Events.AgentivityLattice.instBEqTransitivityClass.beq }

source

def Semantics.Events.AgentivityLattice.TransitivityClass.agentNode :

TransitivityClass → GrimmNode

The canonical agent position for each transitivity class. All classes share the same agent type: instigation + motion, total persistence (@cite{grimm-2011} Fig. 5, labeled Ia/IIa).

Equations

x✝.agentNode = Semantics.Events.AgentivityLattice.effectorAgent

Instances For

source

def Semantics.Events.AgentivityLattice.TransitivityClass.patientNode :

TransitivityClass → GrimmNode

The canonical patient position for each transitivity class (@cite{grimm-2011} Fig. 5).

Equations

Instances For

source

inductive Semantics.Events.AgentivityLattice.CaseRegion :

Type

Case regions on the agentivity lattice. A case marker corresponds to a connected region of the lattice (@cite{grimm-2011} §4).

nomErg : CaseRegion
Nominative (accusative systems) / Ergative (ergative systems): the region spreading from maximal agent. Marks subjects.
accAbs : CaseRegion
Accusative (accusative systems) / Absolutive (ergative systems): the region spreading from maximal patient and existential persistence (beginning). Marks objects.
dative : CaseRegion
Dative: the region around sentience + qualitative persistence (beginning). Marks recipients, experiencers, benefactives (@cite{grimm-2011} §5.1, Fig. 7).
oblique : CaseRegion
Oblique: the middle region between core cases.

Instances For

source

instance Semantics.Events.AgentivityLattice.instDecidableEqCaseRegion :

DecidableEq CaseRegion

Equations

Semantics.Events.AgentivityLattice.instDecidableEqCaseRegion x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

source

def Semantics.Events.AgentivityLattice.instReprCaseRegion.repr :

CaseRegion → ℕ → Std.Format

Equations

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

Instances For

source

instance Semantics.Events.AgentivityLattice.instReprCaseRegion :

Repr CaseRegion

Equations

Semantics.Events.AgentivityLattice.instReprCaseRegion = { reprPrec := Semantics.Events.AgentivityLattice.instReprCaseRegion.repr }

source

instance Semantics.Events.AgentivityLattice.instBEqCaseRegion :

BEq CaseRegion

Equations

Semantics.Events.AgentivityLattice.instBEqCaseRegion = { beq := Semantics.Events.AgentivityLattice.instBEqCaseRegion.beq }

source

def Semantics.Events.AgentivityLattice.instBEqCaseRegion.beq :

CaseRegion → CaseRegion → Bool

Equations

Semantics.Events.AgentivityLattice.instBEqCaseRegion.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

source

def Semantics.Events.AgentivityLattice.GrimmNode.toCaseRegion (n : GrimmNode) :

CaseRegion

Predicts the case region for a node based on its lattice position.

nomErg: has instigation + total persistence — the prototypical transitive subject region.
accAbs: no agentivity + persistence with existsBeginning — the prototypical affected object region.
dative: sentience (without instigation) + qualitative persistence (beginning) — recipients, experiencers, benefactives.
oblique: everything else.

Equations

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

Instances For

source

def Semantics.Events.AgentivityLattice.CaseRegion.toAccusativeCase :

CaseRegion → Core.Case

Maps a case region to its canonical morphological case in an accusative alignment system.

Equations

Instances For

source

def Semantics.Events.AgentivityLattice.CaseRegion.toErgativeCase :

CaseRegion → Core.Case

Maps a case region to its canonical morphological case in an ergative alignment system.

Equations

Instances For

source

def Semantics.Events.AgentivityLattice.AgentivityNode.fromEntailmentProfile (p : ProtoRoles.EntailmentProfile) :

AgentivityNode

Map Dowty's P-Agent entailments to Grimm's agentivity features.

The correspondence is direct for 3 of 4 features:

volition = volition
sentience = sentience
causation → instigation (@cite{grimm-2011} p.521)
movement = motion

Independent existence is handled by the persistence dimension.

Equations

Semantics.Events.AgentivityLattice.AgentivityNode.fromEntailmentProfile p = { volition := p.volition, sentience := p.sentience, instigation := p.causation, motion := p.movement }

Instances For

source

def Semantics.Events.AgentivityLattice.PersistenceLevel.fromPatientProfile (p : ProtoRoles.EntailmentProfile) :

PersistenceLevel

Map Dowty's P-Patient entailments to Grimm's persistence level.

This is an approximate mapping — Grimm's system is genuinely different from Dowty's. The diagnostic features:

DE + IT → exPersEnd: entity created incrementally (build, invent)
DE + ¬IT → exPersBeginning: entity ceases to exist (die, evaporate)
IT + ¬DE → exPersBeginning: entity consumed incrementally (eat)
CoS + ¬IT + ¬DE → quPersBeginning: changed but persists (kick, move)
¬CoS + ¬DE → totalPersistence or totalNonPersistence

Dowty's DE ("does not exist independently of the event") maps to Grimm's creation/destruction axis. IT (incremental theme) disambiguates: DE+IT = creation (exPersEnd), DE+¬IT = destruction (exPersBeginning).

Equations

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

Instances For

source

def Semantics.Events.AgentivityLattice.GrimmNode.fromSubjectProfile (p : ProtoRoles.EntailmentProfile) :

GrimmNode

Map a full EntailmentProfile to a GrimmNode.

The agentivity features come from the P-Agent entailments; the persistence level comes from the P-Patient entailments.

Equations

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

Instances For

source

def Semantics.Events.AgentivityLattice.GrimmNode.fromObjectProfile (p : ProtoRoles.EntailmentProfile) :

GrimmNode

Equations

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

Instances For

source

theorem Semantics.Events.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.

source

theorem Semantics.Events.AgentivityLattice.exPersEnd_sup_exPersBeginning :

PersistenceLevel.exPersEnd ⊔ PersistenceLevel.exPersBeginning = ⊤

Their join is ⊤ (totalPersistence).

source

theorem Semantics.Events.AgentivityLattice.exPersEnd_inf_exPersBeginning :

PersistenceLevel.exPersEnd ⊓ PersistenceLevel.exPersBeginning = ⊥

Their meet is ⊥ (totalNonPersistence).

source

theorem Semantics.Events.AgentivityLattice.maximalAgent_eq_top :

maximalAgent = ⊤

Maximal agent is ⊤ on the combined lattice.

source

theorem Semantics.Events.AgentivityLattice.maximalAgent_valid :

maximalAgent.valid = true

source

theorem Semantics.Events.AgentivityLattice.maximalPatient_valid :

maximalPatient.valid = true

source

theorem Semantics.Events.AgentivityLattice.effectorAgent_valid :

effectorAgent.valid = true

source

theorem Semantics.Events.AgentivityLattice.experiencerNode_valid :

experiencerNode.valid = true

source

theorem Semantics.Events.AgentivityLattice.maximalAgent_featureCount :

maximalAgent.featureCount = 8

source

theorem Semantics.Events.AgentivityLattice.maximalPatient_featureCount :

maximalPatient.featureCount = 2

source

theorem Semantics.Events.AgentivityLattice.maximalPatient_le_maximalAgent :

maximalPatient ≤ maximalAgent

source

theorem Semantics.Events.AgentivityLattice.maximalAgent_not_le_maximalPatient :

¬maximalAgent ≤ maximalPatient

source

theorem Semantics.Events.AgentivityLattice.maximalAgent_in_transitiveRegion :

maximalAgent.inTransitiveRegion = true

source

theorem Semantics.Events.AgentivityLattice.maximalPatient_in_transitiveRegion :

maximalPatient.inTransitiveRegion = true

source

theorem Semantics.Events.AgentivityLattice.classI_patient_in_region :

TransitivityClass.resultativeEffective.patientNode.inTransitiveRegion = true

Class I patients (break) are in the transitivity region.

source

theorem Semantics.Events.AgentivityLattice.classII_patient_in_region :

TransitivityClass.contact.patientNode.inTransitiveRegion = true

Class II patients (shoot) are in the transitivity region.

source

theorem Semantics.Events.AgentivityLattice.classIII_patient_outside_region :

TransitivityClass.pursuit.patientNode.inTransitiveRegion = false

Class III patients (search) are OUTSIDE the transitivity region. This captures Tsunoda's observation that pursuit verbs deviate most strongly from the prototypical transitive paradigm.

source

theorem Semantics.Events.AgentivityLattice.classI_patient_lower_persistence :

TransitivityClass.resultativeEffective.patientNode.persistence.featureCount < TransitivityClass.contact.patientNode.persistence.featureCount

Class I patient (break: exPersBeginning) has lower persistence than Class II patient (shoot: quPersBeginning). The Class I object is more affected — it ceases to exist.

source

theorem Semantics.Events.AgentivityLattice.classI_patient_le_classII :

TransitivityClass.resultativeEffective.patientNode ≤ TransitivityClass.contact.patientNode

Class I patient ≤ Class II patient on the lattice (exPersBeginning ≤ quPersBeginning).

source

theorem Semantics.Events.AgentivityLattice.classIII_patient_le_classI :

TransitivityClass.pursuit.patientNode ≤ TransitivityClass.resultativeEffective.patientNode

Class III patient ≤ Class I patient (totalNonPersistence ≤ exPersBeginning).

source

theorem Semantics.Events.AgentivityLattice.maximalAgent_nomErg :

maximalAgent.toCaseRegion = CaseRegion.nomErg

Maximal agent maps to NOM/ERG region.

source

theorem Semantics.Events.AgentivityLattice.maximalPatient_accAbs :

maximalPatient.toCaseRegion = CaseRegion.accAbs

Maximal patient maps to ACC/ABS region.

source

theorem Semantics.Events.AgentivityLattice.effectorAgent_nomErg :

effectorAgent.toCaseRegion = CaseRegion.nomErg

The effector agent (instigation + motion, total persistence) maps to NOM/ERG. This is the agent of break/kill (@cite{grimm-2011} Fig. 5, Ia).

source

theorem Semantics.Events.AgentivityLattice.experiencer_dative :

experiencerNode.toCaseRegion = CaseRegion.dative

The experiencer/recipient maps to the dative region (@cite{grimm-2011} §5.1, Fig. 7).

source

theorem Semantics.Events.AgentivityLattice.recipient_dative :

recipientNode.toCaseRegion = CaseRegion.dative

The recipient maps to the dative region.

source

theorem Semantics.Events.AgentivityLattice.classI_patient_accAbs :

TransitivityClass.resultativeEffective.patientNode.toCaseRegion = CaseRegion.accAbs

Class I patient (break object: destroyed) maps to ACC/ABS.

source

theorem Semantics.Events.AgentivityLattice.classII_patient_accAbs :

TransitivityClass.contact.patientNode.toCaseRegion = CaseRegion.accAbs

Class II patient (shoot object: affected but persists) maps to ACC/ABS.

source

theorem Semantics.Events.AgentivityLattice.accusative_alignment :

maximalAgent.toCaseRegion.toAccusativeCase = Core.Case.nom ∧ maximalPatient.toCaseRegion.toAccusativeCase = Core.Case.acc

Accusative alignment: maximal agent → NOM, maximal patient → ACC.

source

theorem Semantics.Events.AgentivityLattice.ergative_alignment :

maximalAgent.toCaseRegion.toErgativeCase = Core.Case.erg ∧ maximalPatient.toCaseRegion.toErgativeCase = Core.Case.abs

Ergative alignment: maximal agent → ERG, maximal patient → ABS.

source

theorem Semantics.Events.AgentivityLattice.kick_subject_agentivity :

AgentivityNode.fromEntailmentProfile ProtoRoles.kickSubjectProfile = { volition := true, sentience := true, instigation := true, motion := true }

kick subject → agentivity {V,S,I,M} (full agent).

source

theorem Semantics.Events.AgentivityLattice.kick_object_persistence :

PersistenceLevel.fromPatientProfile ProtoRoles.kickObjectProfile = PersistenceLevel.quPersBeginning

kick object → persistence quPersBeginning (affected but persists). CoS=true, IT=false, DE=false → qualitatively changed.

source

theorem Semantics.Events.AgentivityLattice.build_object_persistence :

PersistenceLevel.fromPatientProfile ProtoRoles.buildObjectProfile = PersistenceLevel.exPersEnd

build object → persistence exPersEnd (entity created).

source

theorem Semantics.Events.AgentivityLattice.die_subject_persistence :

PersistenceLevel.fromPatientProfile ProtoRoles.dieSubjectProfile = PersistenceLevel.exPersBeginning

die subject → persistence exPersBeginning (entity ceases to exist). DE=true, IT=false → entity is destroyed.

source

theorem Semantics.Events.AgentivityLattice.run_subject_agentivity :

AgentivityNode.fromEntailmentProfile ProtoRoles.runSubjectProfile = { volition := true, sentience := true, instigation := false, motion := true }

run subject → agentivity {V,S,M} (no instigation).

source

theorem Semantics.Events.AgentivityLattice.arrive_subject_agentivity :

AgentivityNode.fromEntailmentProfile ProtoRoles.arriveSubjectProfile = { volition := false, sentience := false, instigation := false, motion := true }

arrive subject → agentivity {M} (motion only).

source

theorem Semantics.Events.AgentivityLattice.see_subject_agentivity :

AgentivityNode.fromEntailmentProfile ProtoRoles.seeSubjectProfile = { volition := false, sentience := true, instigation := false, motion := false }

see subject → agentivity {S} (sentience only).

source

theorem Semantics.Events.AgentivityLattice.sweep_basic_agentivity :

AgentivityNode.fromEntailmentProfile ProtoRoles.sweepBasicSubjectProfile = { volition := false, sentience := false, instigation := false, motion := true }

sweep basic subject → agentivity {M} (motion only, variable agentivity).

source

theorem Semantics.Events.AgentivityLattice.sweep_broom_agentivity :

AgentivityNode.fromEntailmentProfile ProtoRoles.sweepBroomSubjectProfile = { volition := true, sentience := true, instigation := true, motion := true }

sweep broom subject → agentivity {V,S,I,M} (instrument lexicalization adds full agentivity, @cite{rappaport-hovav-levin-2024}).

source

theorem Semantics.Events.AgentivityLattice.sweep_lexicalization_increases :

AgentivityNode.fromEntailmentProfile ProtoRoles.sweepBasicSubjectProfile < AgentivityNode.fromEntailmentProfile ProtoRoles.sweepBroomSubjectProfile

Instrument lexicalization strictly increases agentivity on the lattice: sweep basic {M} < sweep broom {V,S,I,M}.

source

theorem Semantics.Events.AgentivityLattice.grimm_agentivity_consistent_with_dowty (p q : ProtoRoles.EntailmentProfile) (h : AgentivityNode.fromEntailmentProfile p ≤ AgentivityNode.fromEntailmentProfile q) :

(!p.volition || q.volition) = true ∧ (!p.sentience || q.sentience) = true ∧ (!p.causation || q.causation) = true ∧ (!p.movement || q.movement) = true

Grimm's agentivity lattice ordering is consistent with Dowty's pAgentDominates: if Grimm a ≤ Grimm b on agentivity, then Dowty a dominates Dowty b on P-Agent features.

This holds because the feature-to-feature mapping is a bijection on the first 4 P-Agent features (volition, sentience, causation=instigation, movement=motion).

source

theorem Semantics.Events.AgentivityLattice.fromEntailmentProfile_monotone (p q : ProtoRoles.EntailmentProfile) (hv : p.volition = true → q.volition = true) (hs : p.sentience = true → q.sentience = true) (hc : p.causation = true → q.causation = true) (hm : p.movement = true → q.movement = true) :

AgentivityNode.fromEntailmentProfile p ≤ AgentivityNode.fromEntailmentProfile q

The Dowty→Grimm bridge is monotone: if one EntailmentProfile dominates another on P-Agent features, the corresponding AgentivityNodes are ordered.

source

theorem Semantics.Events.AgentivityLattice.dative_unifies_recipient_experiencer :

recipientNode.toCaseRegion = CaseRegion.dative ∧ experiencerNode.toCaseRegion = CaseRegion.dative

The dative region unifies recipients, experiencers, and second arguments of communication/service verbs — they all share the semantic properties of sentience and qualitative persistence (beginning) (@cite{grimm-2011} Fig. 7, p.536).

This explains dative "polysemy": the diverse uses of the dative share a connected region on the lattice, not a single function.

source

theorem Semantics.Events.AgentivityLattice.dative_experiencer_eq_recipient :

experiencerNode = recipientNode

The dative experiencer subject (@cite{grimm-2011} §5.1.1) has the same lattice position as the dative recipient — sentience + qualitative persistence. This explains why languages cross-linguistically use the same case (dative) for both.

source

structure Semantics.Events.AgentivityLattice.GenAccAlternation :

Type

The Russian genitive/accusative alternation arises when the object of an intensional verb (want, seek, await) falls in a region covered by two cases. The accusative covers existential persistence (beginning); the genitive covers total non-persistence (@cite{grimm-2011} Fig. 8).

Accusative (specific reading): the object is referential → exists → existential persistence (beginning) → ACC region.
Genitive (non-specific reading): the object need not exist → total non-persistence → GEN region.

The alternation is limited to verbs whose objects have no persistence entailments — only intensional verbs like want, seek, await license the genitive (@cite{grimm-2011} p.541).

specificReading : GrimmNode
The object node under the specific/referential reading.
nonSpecificReading : GrimmNode
The object node under the non-specific reading.
specific_more_persistent : self.nonSpecificReading.persistence ≤ self.specificReading.persistence
The specific reading has more persistence features.

Instances For

source

def Semantics.Events.AgentivityLattice.russianGenAcc :

GenAccAlternation

The canonical Russian gen/acc alternation for intensional verbs: ACC (specific) ↔ GEN (non-specific).

Equations

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

Instances For

source

theorem Semantics.Events.AgentivityLattice.genAcc_specific_is_acc :

russianGenAcc.specificReading.toCaseRegion = CaseRegion.accAbs

The specific reading maps to the ACC/ABS region.

source

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

minReq ≤ b

Agents are upwards closed in the agentivity dimension (@cite{grimm-2011} 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.

source

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

q ≤ maxPers

Patients are downwards closed in the persistence dimension (@cite{grimm-2011} 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.

source

def Semantics.Events.AgentivityLattice.semanticOpposition (agent patient : GrimmNode) :

ℤ

Semantic opposition between two GrimmNodes. Transitivity increases with the distance between agent and patient on the lattice. We measure this as the difference in total feature counts — higher opposition means more prototypically transitive.

Equations

Semantics.Events.AgentivityLattice.semanticOpposition agent patient = ↑agent.featureCount - ↑patient.featureCount

Instances For

source

theorem Semantics.Events.AgentivityLattice.maximal_opposition :

semanticOpposition maximalAgent maximalPatient = 6

Maximal agent vs maximal patient has the highest opposition (8 - 2 = 6).

source

theorem Semantics.Events.AgentivityLattice.classI_more_opposition_than_classII :

semanticOpposition effectorAgent TransitivityClass.resultativeEffective.patientNode > semanticOpposition effectorAgent TransitivityClass.contact.patientNode

Class I (break) has more opposition than Class II (shoot): the patient is more affected (fewer persistence features).

source

theorem Semantics.Events.AgentivityLattice.kick_subject_to_nom :

(GrimmNode.fromSubjectProfile ProtoRoles.kickSubjectProfile).toCaseRegion.toAccusativeCase = Core.Case.nom

Full pipeline: kick subject → GrimmNode → NOM/ERG → NOM (accusative).

source

theorem Semantics.Events.AgentivityLattice.kick_object_to_acc :

(GrimmNode.fromObjectProfile ProtoRoles.kickObjectProfile).toCaseRegion.toAccusativeCase = Core.Case.acc

Full pipeline: kick object → GrimmNode → ACC/ABS → ACC (accusative).

source

theorem Semantics.Events.AgentivityLattice.build_subject_to_nom :

(GrimmNode.fromSubjectProfile ProtoRoles.buildSubjectProfile).toCaseRegion.toAccusativeCase = Core.Case.nom

Build subject → NOM (full agent, total persistence).

source

theorem Semantics.Events.AgentivityLattice.build_object_outside_acc :

(GrimmNode.fromObjectProfile ProtoRoles.buildObjectProfile).toCaseRegion ≠ CaseRegion.accAbs

Build object → OBLIQUE (not ACC). The object of build maps to exPersEnd (entity comes into existence), which falls OUTSIDE the transitivity region (@cite{grimm-2011} p.529–530). Creation verbs are non-prototypically transitive — the object does not exist at the beginning of the event to "undergo its effects." This is a correct prediction: creation verb objects cross-linguistically show atypical case marking (e.g., pseudo-cleft asymmetry).

source

theorem Semantics.Events.AgentivityLattice.see_subject_not_nomErg :

(GrimmNode.fromSubjectProfile ProtoRoles.seeSubjectProfile).toCaseRegion ≠ CaseRegion.nomErg

Full pipeline: see subject → OBLIQUE (not NOM/ERG). The see-subject has sentience but no instigation, so it falls outside the NOM/ERG region. Grimm's system predicts non-canonical case for perception verb subjects cross-linguistically.

source

theorem Semantics.Events.AgentivityLattice.die_subject_to_abs :

(GrimmNode.fromObjectProfile ProtoRoles.dieSubjectProfile).toCaseRegion.toErgativeCase = Core.Case.abs

Full pipeline: die subject (unaccusative) → ACC/ABS. The sole argument of die maps to the patient region (no agentivity, exPersBeginning). In an ergative system this → ABS (= intransitive subject).

@cite{grimm-2011} illustrates the agentivity lattice with a chain of canonical verbs, each adding one feature. This demonstrates that the lattice directly formalizes "degree of agentivity" — higher on the lattice means more agentive.

source

def Semantics.Events.AgentivityLattice.sitAgentivity :

AgentivityNode

sit/stand subject: ⊥ (no agentivity). @cite{grimm-2011} p.523.

Equations

Semantics.Events.AgentivityLattice.sitAgentivity = ⊥

Instances For

source

def Semantics.Events.AgentivityLattice.knowAgentivity :

AgentivityNode

know/see subject: sentience only. @cite{grimm-2011} p.524.

Equations

Semantics.Events.AgentivityLattice.knowAgentivity = { volition := false, sentience := true, instigation := false, motion := false }

Instances For

source

def Semantics.Events.AgentivityLattice.discoverAgentivity :

AgentivityNode

discover subject: sentience + instigation. @cite{grimm-2011} p.524.

Equations

Semantics.Events.AgentivityLattice.discoverAgentivity = { volition := false, sentience := true, instigation := true, motion := false }

Instances For

source

def Semantics.Events.AgentivityLattice.lookAtAgentivity :

AgentivityNode

look at subject: sentience + instigation + motion. @cite{grimm-2011} p.524.

Equations

Semantics.Events.AgentivityLattice.lookAtAgentivity = { volition := false, sentience := true, instigation := true, motion := true }

Instances For

source

def Semantics.Events.AgentivityLattice.assassinateAgentivity :

AgentivityNode

assassinate subject: all four features. @cite{grimm-2011} p.524.

Equations

Semantics.Events.AgentivityLattice.assassinateAgentivity = ⊤

Instances For

source

theorem Semantics.Events.AgentivityLattice.canonical_verb_chain :

sitAgentivity < knowAgentivity ∧ knowAgentivity < discoverAgentivity ∧ discoverAgentivity < lookAtAgentivity ∧ lookAtAgentivity < assassinateAgentivity

The canonical verb chain is totally ordered and forms a maximal chain from ⊥ to ⊤ in the agentivity lattice.

source

All canonical verb positions satisfy volition → sentience.

source

theorem Semantics.Events.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 → ⊤

source

theorem Semantics.Events.AgentivityLattice.persistence_chain :

PersistenceLevel.exPersBeginning ≤ PersistenceLevel.quPersBeginning ∧ PersistenceLevel.quPersBeginning ≤ PersistenceLevel.totalPersistence

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

@cite{grimm-2011} (p.534): "it is a combination of verbal and nominal properties which trigger DOM." The lattice provides a formal account:

1. The case regions defined in §6 (`toCaseRegion`) map lattice positions
   to cases — ACC/ABS for ⊥-agentivity objects with existential
   persistence, DATIVE for sentient non-instigators with qualitative
   persistence (Fig. 7).

2. When we map nominal animacy to baseline agentive capacity and
   combine it with the verb's persistence profile, animate/human
   objects shift from ACC/ABS into the DATIVE region.

3. This is NOT a DOM-specific definition — it reuses `toCaseRegion`
   (§6) and `inTransitiveRegion` (§5), both defined for general
   case theory. The DOM prediction is a CONSEQUENCE of case theory.

The verb class effect (@cite{von-heusinger-2008}) also falls out:
verbs whose subjects map to NOM/ERG provide maximal contrast with
the object — DOM can regularize. Verbs whose subjects fall outside
NOM/ERG provide less contrast — DOM remains sensitive to nominal
properties.

source

def Semantics.Events.AgentivityLattice.animacyToAgentivity :

Core.Prominence.AnimacyLevel → AgentivityNode

Map nominal animacy to baseline agentive capacity on the lattice.

Only inherent referent properties are mapped — not event-specific ones like instigation or motion:

Human: volition + sentience (capacity for intentional action)
Animate: sentience (conscious but non-volitional)
Inanimate: ⊥ (no inherent agentive capacity)

The exclusion of instigation and motion is principled: these are event properties (did the participant instigate THIS event? move during THIS event?), not referent properties. Volition and sentience are inherent capacities of the referent type.

Equations

Semantics.Events.AgentivityLattice.animacyToAgentivity Core.Prominence.AnimacyLevel.human = { volition := true, sentience := true, instigation := false, motion := false }
Semantics.Events.AgentivityLattice.animacyToAgentivity Core.Prominence.AnimacyLevel.animate = { volition := false, sentience := true, instigation := false, motion := false }
Semantics.Events.AgentivityLattice.animacyToAgentivity Core.Prominence.AnimacyLevel.inanimate = ⊥

Instances For

source

theorem Semantics.Events.AgentivityLattice.animacy_all_valid (a : Core.Prominence.AnimacyLevel) :

(animacyToAgentivity a).valid = true

All animacy-derived nodes satisfy volition → sentience.

source

theorem Semantics.Events.AgentivityLattice.animacy_agentivity_monotone :

animacyToAgentivity Core.Prominence.AnimacyLevel.inanimate ≤ animacyToAgentivity Core.Prominence.AnimacyLevel.animate ∧ animacyToAgentivity Core.Prominence.AnimacyLevel.animate ≤ animacyToAgentivity Core.Prominence.AnimacyLevel.human

The mapping is monotone: higher animacy → higher agentivity. This is a structural property of the feature-subset ordering, not a stipulation.

source

def Semantics.Events.AgentivityLattice.objectNodeWithAnimacy (animacy : Core.Prominence.AnimacyLevel) (verbPersistence : PersistenceLevel) :

GrimmNode

Combine a referent's nominal agentivity (from animacy) with the verb's persistence profile for the object.

Equations

Semantics.Events.AgentivityLattice.objectNodeWithAnimacy animacy verbPersistence = { agentivity := Semantics.Events.AgentivityLattice.animacyToAgentivity animacy, persistence := verbPersistence }

Instances For

source

theorem Semantics.Events.AgentivityLattice.inanimate_object_in_accAbs :

(objectNodeWithAnimacy Core.Prominence.AnimacyLevel.inanimate PersistenceLevel.quPersBeginning).toCaseRegion = CaseRegion.accAbs

The key non-circular derivation. For canonical transitive objects (quPersBeginning = contact verbs like kick, hit, push):

Inanimate: ⟨⊥, qPB⟩ → toCaseRegion = accAbs (prototypical patient, no DOM needed)
Animate: ⟨{S}, qPB⟩ → toCaseRegion = dative (sentience shifts it into the dative region, Fig. 7)
Human: ⟨{V,S}, qPB⟩ → toCaseRegion = dative (volition + sentience, also in dative region)

toCaseRegion was defined in §6 for general case theory, not for DOM. That it automatically separates inanimate objects (accAbs) from animate/human objects (dative) is the lattice's genuine prediction.

source

theorem Semantics.Events.AgentivityLattice.animate_object_in_dative :

(objectNodeWithAnimacy Core.Prominence.AnimacyLevel.animate PersistenceLevel.quPersBeginning).toCaseRegion = CaseRegion.dative

source

theorem Semantics.Events.AgentivityLattice.human_object_in_dative :

(objectNodeWithAnimacy Core.Prominence.AnimacyLevel.human PersistenceLevel.quPersBeginning).toCaseRegion = CaseRegion.dative

source

def Semantics.Events.AgentivityLattice.domPredictedByLattice (animacy : Core.Prominence.AnimacyLevel) (verbPersistence : PersistenceLevel) :

Bool

DOM is predicted when the object is in the transitivity region but its nominal agentivity pushes it outside the ACC/ABS case region. Both conditions use infrastructure defined for general case theory (§5, §6), not for DOM.

Equations

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

Instances For

source

theorem Semantics.Events.AgentivityLattice.inanimate_canonical_no_dom :

domPredictedByLattice Core.Prominence.AnimacyLevel.inanimate PersistenceLevel.quPersBeginning = false

Inanimate objects of canonical transitives: in ACC/ABS, no DOM.

source

theorem Semantics.Events.AgentivityLattice.animate_canonical_dom :

domPredictedByLattice Core.Prominence.AnimacyLevel.animate PersistenceLevel.quPersBeginning = true

Animate objects of canonical transitives: outside ACC/ABS, DOM predicted. The lattice reason: sentience pushes the object into the dative region (@cite{grimm-2011} Fig. 7).

source

theorem Semantics.Events.AgentivityLattice.human_canonical_dom :

domPredictedByLattice Core.Prominence.AnimacyLevel.human PersistenceLevel.quPersBeginning = true

Human objects: also outside ACC/ABS, DOM predicted.

source

theorem Semantics.Events.AgentivityLattice.inanimate_resultative_no_dom :

domPredictedByLattice Core.Prominence.AnimacyLevel.inanimate PersistenceLevel.exPersBeginning = false

The same pattern holds for resultative verbs (break, destroy): inanimate objects stay in ACC/ABS, animate/human objects do not.

source

theorem Semantics.Events.AgentivityLattice.animate_resultative_dom :

domPredictedByLattice Core.Prominence.AnimacyLevel.animate PersistenceLevel.exPersBeginning = true ∧ domPredictedByLattice Core.Prominence.AnimacyLevel.human PersistenceLevel.exPersBeginning = true

source

theorem Semantics.Events.AgentivityLattice.creation_outside_transitivity (a : Core.Prominence.AnimacyLevel) :

(objectNodeWithAnimacy a PersistenceLevel.exPersEnd).inTransitiveRegion = false

Creation verb objects (build, invent — exPersEnd) are outside the transitivity region at ALL animacy levels. The object does not exist at event start, so it cannot "intrude" on the agent's role. DOM is inapplicable, not merely unnecessary.

source

def Semantics.Events.AgentivityLattice.subjectInAgentRegion (subjProfile : ProtoRoles.EntailmentProfile) :

Bool

Whether the subject maps to the NOM/ERG case region. When true, the verbal semantics alone provides maximal contrast between subject (NOM/ERG) and object (ACC/ABS or below), and DOM can regularize — it is redundant for disambiguation.

@cite{von-heusinger-2008}: matar 'kill' (Class 1, subject → NOM/ERG) regularized DOM centuries before ver 'see' (Class 2, subject → oblique).

Equations

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

Instances For

source

theorem Semantics.Events.AgentivityLattice.kick_subject_in_agent_region :

subjectInAgentRegion ProtoRoles.kickSubjectProfile = true

Kick subject → NOM/ERG: maximal verbal contrast. Corresponds to matar 'kill' — DOM regularized early.

source

theorem Semantics.Events.AgentivityLattice.see_subject_not_in_agent_region :

subjectInAgentRegion ProtoRoles.seeSubjectProfile = false

See subject → NOT NOM/ERG: insufficient verbal contrast. Corresponds to ver 'see' — DOM remained variable.

source

theorem Semantics.Events.AgentivityLattice.build_subject_in_agent_region :

subjectInAgentRegion ProtoRoles.buildSubjectProfile = true

Build subject → NOM/ERG: high verbal contrast, but moot because the object is outside the transitivity region (§21.5).

source

theorem Semantics.Events.AgentivityLattice.dom_monotone_inanimate_animate (p : PersistenceLevel) :

domPredictedByLattice Core.Prominence.AnimacyLevel.inanimate p = true → domPredictedByLattice Core.Prominence.AnimacyLevel.animate p = true

The lattice reproduces @cite{aissen-2003}'s monotonicity prediction: if DOM is predicted for a lower animacy level, it is also predicted for all higher levels. Universally quantified over persistence.

This is NOT stipulated — it follows from:

animacyToAgentivity is monotone (higher animacy → more features)
toCaseRegion maps ⊥ agentivity to accAbs, non-⊥ to dative/oblique
Once agentivity is non-⊥, adding features keeps it non-⊥

source

theorem Semantics.Events.AgentivityLattice.dom_monotone_animate_human (p : PersistenceLevel) :

domPredictedByLattice Core.Prominence.AnimacyLevel.animate p = true → domPredictedByLattice Core.Prominence.AnimacyLevel.human p = true

For totalPersistence objects (perception verbs: see, hear, know), toCaseRegion maps ⟨⊥, totalPersistence⟩ to oblique, not accAbs, because totalPersistence is not in {exPersBeginning, quPersBeginning}. This means domPredictedByLattice returns true for ALL animacy levels, including inanimate — overpredicting DOM for perception verb objects.

This reflects a genuine theoretical point: Grimm's system treats
perception verb objects as non-prototypical patients (they are not
affected or changed). But it means `domPredictedByLattice` is most
informative for verbs in the transitivity region's core: contact
(quPersBeginning) and resultative effective (exPersBeginning) verbs.

source

theorem Semantics.Events.AgentivityLattice.totalPersistence_all_outside_accAbs (a : Core.Prominence.AnimacyLevel) :

(objectNodeWithAnimacy a PersistenceLevel.totalPersistence).toCaseRegion ≠ CaseRegion.accAbs

Documentation

Linglib.Theories.Semantics.Events.AgentivityLattice

The Agentivity Lattice @cite{grimm-2011} #

Mathlib integration #

Bridges #