Case as a region of the agentivity lattice

Grimm's central claim is that a core case marker corresponds to a connected region of the agentivity lattice, spreading outwards from the maximal agent and maximal patient nodes. Each participant type is assigned a case region, and regions are mapped to morphological cases under accusative and ergative alignment. Each core region is an order interval anchored at its pole, so connectedness is mathlib's Set.OrdConnected, inherited from Set.Ici and Set.Icc; the residual oblique region is not connected.

Main definitions

• CaseRegion: the nominative or ergative, accusative or absolutive, dative and oblique regions.
• ParticipantType.toCaseRegion: the region of a participant type.

Main results

• ParticipantType.toCaseRegion_eq_nomErg_iff: the nominative or ergative region is the up-set of the minimal instigator; the accusative and dative regions are intervals likewise.
• ordConnected_nomErg, ordConnected_accAbs, ordConnected_dative: the core regions are connected, and not_ordConnected_oblique the oblique region is not.

References

• [Gri11]

Case regions

inductive ArgumentStructure.CaseRegion : Type

The case regions of the agentivity lattice, three core regions, which are intervals anchored at the poles, and the residual oblique region ([Gri11] pp.532–533).

• nomErg : CaseRegion

  Nominative in accusative systems and ergative in ergative ones, the region spreading from the maximal agent, marking subjects.

• accAbs : CaseRegion

  Accusative in accusative systems and absolutive in ergative ones, the region spreading from the maximal patient and existential persistence (beginning), marking objects.

• dative : CaseRegion

  The dative, around sentience at qualitative persistence (beginning), marking recipients, experiencers and the second arguments of two-place communication and service verbs.

• oblique : CaseRegion

  The middle region between the core cases.

@[instance_reducible]

instance ArgumentStructure.instDecidableEqCaseRegion : DecidableEq CaseRegion

Equations

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

def ArgumentStructure.instReprCaseRegion.repr : CaseRegion → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance ArgumentStructure.instReprCaseRegion : Repr CaseRegion

Equations

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

def ArgumentStructure.ParticipantType.toCaseRegion (n : ParticipantType) : CaseRegion

A participant type is in the nominative or ergative region with instigation at total persistence, in the accusative or absolutive region with no agentivity at existential or qualitative persistence (beginning), in the dative region with sentience but no instigation at qualitative persistence (beginning), and otherwise in the oblique region.

Equations

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

def ArgumentStructure.CaseRegion.toAccusativeCase : CaseRegion → Case

The canonical case of a region under accusative alignment.

Equations

• ArgumentStructure.CaseRegion.nomErg.toAccusativeCase = Case.nom
• ArgumentStructure.CaseRegion.accAbs.toAccusativeCase = Case.acc
• ArgumentStructure.CaseRegion.dative.toAccusativeCase = Case.dat
• ArgumentStructure.CaseRegion.oblique.toAccusativeCase = Case.inst

def ArgumentStructure.CaseRegion.toErgativeCase : CaseRegion → Case

The canonical case of a region under ergative alignment.

Equations

• ArgumentStructure.CaseRegion.nomErg.toErgativeCase = Case.erg
• ArgumentStructure.CaseRegion.accAbs.toErgativeCase = Case.abs
• ArgumentStructure.CaseRegion.dative.toErgativeCase = Case.dat
• ArgumentStructure.CaseRegion.oblique.toErgativeCase = Case.inst

The core regions are intervals

def ArgumentStructure.minimalInstigator : ParticipantType

Instigation alone at total persistence is the bottom of the nominative or ergative region, the minimal acceptable agent of kill, a natural force such as electricity or the explosion ([Gri11] §2.3).

Equations

• ArgumentStructure.minimalInstigator = ({ArgumentStructure.Agentivity.Feature.instigation}, ⊤)

theorem ArgumentStructure.ParticipantType.toCaseRegion_eq_nomErg_iff (n : ParticipantType) : n.toCaseRegion = CaseRegion.nomErg ↔ minimalInstigator ≤ n

The nominative or ergative region is the up-set of the minimal instigator.

theorem ArgumentStructure.ParticipantType.toCaseRegion_eq_accAbs_iff (n : ParticipantType) : n.toCaseRegion = CaseRegion.accAbs ↔ maximalPatient ≤ n ∧ n ≤ TransitivityRank.contact.patientType

The accusative or absolutive region runs from the maximal patient to the patient of a contact verb.

theorem ArgumentStructure.ParticipantType.toCaseRegion_eq_dative_iff (n : ParticipantType) : n.toCaseRegion = CaseRegion.dative ↔ sentientNonInstigator ≤ n ∧ n ≤ ({Agentivity.Feature.volition, Agentivity.Feature.sentience, Agentivity.Feature.motion}, PersistenceLevel.quPersBeginning)

The dative region runs from sentience without instigation up to volition, sentience and motion, all at qualitative persistence (beginning).

theorem ArgumentStructure.setOf_nomErg_eq_Ici : {n : ParticipantType | n.toCaseRegion = CaseRegion.nomErg} = Set.Ici minimalInstigator

theorem ArgumentStructure.setOf_accAbs_eq_Icc : {n : ParticipantType | n.toCaseRegion = CaseRegion.accAbs} = Set.Icc maximalPatient TransitivityRank.contact.patientType

theorem ArgumentStructure.setOf_dative_eq_Icc : {n : ParticipantType | n.toCaseRegion = CaseRegion.dative} = Set.Icc sentientNonInstigator ({Agentivity.Feature.volition, Agentivity.Feature.sentience, Agentivity.Feature.motion}, PersistenceLevel.quPersBeginning)

Connectedness

theorem ArgumentStructure.ordConnected_nomErg : {n : ParticipantType | n.toCaseRegion = CaseRegion.nomErg}.OrdConnected

theorem ArgumentStructure.ordConnected_accAbs : {n : ParticipantType | n.toCaseRegion = CaseRegion.accAbs}.OrdConnected

theorem ArgumentStructure.ordConnected_dative : {n : ParticipantType | n.toCaseRegion = CaseRegion.dative}.OrdConnected

theorem ArgumentStructure.not_ordConnected_oblique : ¬{n : ParticipantType | n.toCaseRegion = CaseRegion.oblique}.OrdConnected

The oblique region is not connected: motion and motion with sentience and instigation, both at qualitative persistence (beginning), are oblique, while motion with sentience between them is dative.