Documentation

Linglib.Fragments.Georgian.Agreement

Georgian Agreement Fragment @cite{just-2024} #

@cite{harris-1981}

Georgian (Kartvelian) has a polypersonal agreement system where the finite verb indexes both subject and object. Object agreement is person-conditioned: indirect objects (dative-marked) are cross-referenced on the verb for 1st/2nd person but not for 3rd person.

This is differential P indexing conditioned by person prominence.

Agreement Paradigm Overview #

Georgian has two sets of verbal agreement markers:

Set	Position	Function
Subject markers	prefix/suffix	Always present
Object markers	prefix	SAP objects only (differential)

The object markers are prefixed to the verb stem:

m- 1sg object ("me")
g- 2sg object ("you")
No marker for 3rd person objects

Split-Ergative Case #

Georgian has a tense/aspect-conditioned split ergative system:

Present series: NOM-DAT alignment
Aorist series: ERG-NOM alignment
Evidential series: DAT-NOM (inversion)

The agreement split is orthogonal to the case split — object agreement is person-conditioned regardless of the case frame.

inductive Fragments.Georgian.Agreement.PersonNumber :

Person-number combinations in the Georgian agreement paradigm.

Instances For

instance Fragments.Georgian.Agreement.instDecidableEqPersonNumber :

DecidableEq PersonNumber

Equations

Fragments.Georgian.Agreement.instDecidableEqPersonNumber x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Fragments.Georgian.Agreement.instBEqPersonNumber.beq :

PersonNumber → PersonNumber → Bool

Equations

Fragments.Georgian.Agreement.instBEqPersonNumber.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

instance Fragments.Georgian.Agreement.instBEqPersonNumber :

BEq PersonNumber

Equations

Fragments.Georgian.Agreement.instBEqPersonNumber = { beq := Fragments.Georgian.Agreement.instBEqPersonNumber.beq }

instance Fragments.Georgian.Agreement.instReprPersonNumber :

Repr PersonNumber

Equations

Fragments.Georgian.Agreement.instReprPersonNumber = { reprPrec := Fragments.Georgian.Agreement.instReprPersonNumber.repr }

def Fragments.Georgian.Agreement.instReprPersonNumber.repr :

PersonNumber → Nat → Std.Format

Equations

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

Instances For

def Fragments.Georgian.Agreement.allPersonNumbers :

List PersonNumber

All person-number values.

Equations

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

Instances For

def Fragments.Georgian.Agreement.PersonNumber.isSAP (pn : PersonNumber) :

Is this a SAP (speech act participant)?

Equations

pn.isSAP = (pn.person == 1 || pn.person == 2)

Instances For

def Fragments.Georgian.Agreement.objectPrefix :

PersonNumber → Option String

Object agreement prefix on the verb. SAP objects receive an overt marker; 3rd person objects receive none.

Equations

Instances For

def Fragments.Georgian.Agreement.pIsIndexed (pn : PersonNumber) :

Whether a P/R argument at a given person-number is indexed (triggers an object prefix on the verb).

Derived from objectPrefix: a person-number is indexed iff it has a non-none object prefix.

Equations

Fragments.Georgian.Agreement.pIsIndexed pn = (Fragments.Georgian.Agreement.objectPrefix pn).isSome

Instances For

def Fragments.Georgian.Agreement.subjectIsIndexed :

PersonNumber → Bool

Subject agreement is always present (not differential).

Equations

Fragments.Georgian.Agreement.subjectIsIndexed x✝ = true

Instances For

SAP objects are indexed (receive an overt prefix).

theorem Fragments.Georgian.Agreement.third_objects_not_indexed :

pIsIndexed PersonNumber.p3sg = false ∧ pIsIndexed PersonNumber.p3pl = false

3rd person objects are NOT indexed (no prefix).

theorem Fragments.Georgian.Agreement.p_indexing_differential :

allPersonNumbers.any pIsIndexed = true ∧ (!decide (allPersonNumbers.all pIsIndexed = true)) = true

P indexing is differential.

theorem Fragments.Georgian.Agreement.indexed_iff_has_prefix :

(allPersonNumbers.all fun (pn : PersonNumber) => pIsIndexed pn == (objectPrefix pn).isSome) = true

P indexing is grounded in the presence of an object prefix: indexed ↔ has overt prefix.

theorem Fragments.Georgian.Agreement.indexed_iff_sap :

(allPersonNumbers.all fun (pn : PersonNumber) => pIsIndexed pn == pn.isSAP) = true

The indexed/not-indexed split aligns with SAP vs 3rd.

inductive Fragments.Georgian.Agreement.TenseSeries :

Georgian tense series. Case alignment varies by series:

Present: S/A = NOM, P/R = DAT (accusative-like framing)
Aorist: A = ERG, S/P = NOM (ergative framing)
Evidential: A = DAT, S/P = NOM ("inversion")

present : TenseSeries
aorist : TenseSeries
evidential : TenseSeries

Instances For

instance Fragments.Georgian.Agreement.instDecidableEqTenseSeries :

DecidableEq TenseSeries

Equations

Fragments.Georgian.Agreement.instDecidableEqTenseSeries x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Fragments.Georgian.Agreement.instBEqTenseSeries :

BEq TenseSeries

Equations

Fragments.Georgian.Agreement.instBEqTenseSeries = { beq := Fragments.Georgian.Agreement.instBEqTenseSeries.beq }

def Fragments.Georgian.Agreement.instBEqTenseSeries.beq :

TenseSeries → TenseSeries → Bool

Equations

Fragments.Georgian.Agreement.instBEqTenseSeries.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

instance Fragments.Georgian.Agreement.instReprTenseSeries :

Repr TenseSeries

Equations

Fragments.Georgian.Agreement.instReprTenseSeries = { reprPrec := Fragments.Georgian.Agreement.instReprTenseSeries.repr }

def Fragments.Georgian.Agreement.instReprTenseSeries.repr :

TenseSeries → Nat → Std.Format

Equations

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

Instances For

def Fragments.Georgian.Agreement.georgianSplit :

Core.SplitErgativity TenseSeries

Georgian split-ergative system: only the aorist series uses ergative alignment. Present uses NOM-DAT framing and evidential uses DAT-NOM "inversion" — both non-ergative.

This instantiates Core.SplitErgativity from @cite{blake-1994}'s typology of tense/aspect-conditioned splits.

Equations

Fragments.Georgian.Agreement.georgianSplit = { ergCondition := fun (ts : Fragments.Georgian.Agreement.TenseSeries) => ts == Fragments.Georgian.Agreement.TenseSeries.aorist }

Instances For

theorem Fragments.Georgian.Agreement.aorist_ergative :

georgianSplit.alignment TenseSeries.aorist = Core.AlignmentFamily.ergative

Aorist triggers ergative alignment.

theorem Fragments.Georgian.Agreement.present_accusative :

georgianSplit.alignment TenseSeries.present = Core.AlignmentFamily.accusative

Present series is non-ergative.

theorem Fragments.Georgian.Agreement.evidential_accusative :

georgianSplit.alignment TenseSeries.evidential = Core.AlignmentFamily.accusative

Evidential series is non-ergative.

def Fragments.Georgian.Agreement.subjectCase :

TenseSeries → Core.Case

Case frame for the subject (A/S) in each tense series.

Equations

Instances For

def Fragments.Georgian.Agreement.objectCase :

TenseSeries → Core.Case

Case frame for the object (P/R) in each tense series.

Equations

Instances For

def Fragments.Georgian.Agreement.caseInventory :

Georgian agreement-relevant case inventory: {NOM, ERG, DAT}.

Note: the full Georgian case system also includes GEN (possessive) and INST (instrumental), yielding {NOM, ERG, GEN, DAT, INST} which satisfies contiguity. Here we validate only the agreement-visible subset, which also satisfies contiguity (all rank ≥ 4).

Equations

Fragments.Georgian.Agreement.caseInventory = [Core.Case.nom , Core.Case.erg , Core.Case.dat ]

Instances For

def Fragments.Georgian.Agreement.allTenseSeries :

List TenseSeries

The inventory covers all tense-series case frames.

Equations

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

Instances For

theorem Fragments.Georgian.Agreement.inventory_covers_subjects :

(allTenseSeries.all fun (ts : TenseSeries) => caseInventory.any fun (x : Core.Case) => x == subjectCase ts) = true

theorem Fragments.Georgian.Agreement.inventory_covers_objects :

(allTenseSeries.all fun (ts : TenseSeries) => caseInventory.any fun (x : Core.Case) => x == objectCase ts) = true

def Fragments.Georgian.Agreement.fullCaseInventory :

The agreement-relevant inventory {NOM, ERG, DAT} is valid per Blake's hierarchy: NOM/ERG at rank 6, DAT at rank 4, GEN at rank 5 — but wait: GEN is rank 5 and is NOT in the inventory, so there IS a gap!

This actually fails strict contiguity (Blake's hierarchy says you "usually" need GEN before DAT). Georgian is a known exception: DAT is so prominent in the case system (present P, evidential A, plus indirect objects) that it exists without surface genitive case being part of the agreement system.

We validate the full case system instead.

Equations

Fragments.Georgian.Agreement.fullCaseInventory = [Core.Case.nom , Core.Case.erg , Core.Case.gen , Core.Case.dat ]

Instances For

theorem Fragments.Georgian.Agreement.full_inventory_valid :

Core.validInventory fullCaseInventory = true

inductive Fragments.Georgian.Agreement.VerbClass :

Georgian verb classes (@cite{harris-1981}).

The class determines unaccusativity, case frame, and agreement pattern. The key split for case theory: classes 1 and 3 (non-derived subjects) take ERG in the aorist, while class 2 (derived/unaccusative subject) does not — motivating @cite{marantz-1991}'s Ergative generalization.

class1 : VerbClass
class2 : VerbClass
class3 : VerbClass
class4 : VerbClass

Instances For

instance Fragments.Georgian.Agreement.instDecidableEqVerbClass :

DecidableEq VerbClass

Equations

Fragments.Georgian.Agreement.instDecidableEqVerbClass x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Fragments.Georgian.Agreement.instBEqVerbClass :

Equations

Fragments.Georgian.Agreement.instBEqVerbClass = { beq := Fragments.Georgian.Agreement.instBEqVerbClass.beq }

def Fragments.Georgian.Agreement.instBEqVerbClass.beq :

VerbClass → VerbClass → Bool

Equations

Fragments.Georgian.Agreement.instBEqVerbClass.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

instance Fragments.Georgian.Agreement.instReprVerbClass :

Equations

Fragments.Georgian.Agreement.instReprVerbClass = { reprPrec := Fragments.Georgian.Agreement.instReprVerbClass.repr }

def Fragments.Georgian.Agreement.instReprVerbClass.repr :

VerbClass → Nat → Std.Format

Equations

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

Instances For

def Fragments.Georgian.Agreement.takesErgInAorist :

VerbClass → Bool

Does the subject take ERG in the aorist (Series II)?

The Ergative generalization (@cite{marantz-1991} ex. 6): ERG tracks the thematic vs derived status of the subject. Class 2 (unaccusative) subjects are derived (raised from object position) → no ERG. Class 4 subjects have quirky DAT (lexical case) → not eligible for ERG.

Equations

Instances For

theorem Fragments.Georgian.Agreement.class1_takes_erg :

takesErgInAorist VerbClass.class1 = true

theorem Fragments.Georgian.Agreement.class2_no_erg :

takesErgInAorist VerbClass.class2 = false

theorem Fragments.Georgian.Agreement.class3_takes_erg :

takesErgInAorist VerbClass.class3 = true

theorem Fragments.Georgian.Agreement.class4_no_erg :

takesErgInAorist VerbClass.class4 = false

def Fragments.Georgian.Agreement.verbClassSubjectCase :

VerbClass → TenseSeries → Core.Case

Subject case by verb class and tense series (@cite{marantz-1991} ex. 1–3).

Present/aorist patterns from @cite{marantz-1991}. Evidential follows the general inversion pattern: all subjects surface as DAT (@cite{harris-1981}).

Equations

Instances For

def Fragments.Georgian.Agreement.verbClassObjectCase :

VerbClass → TenseSeries → Option Core.Case

Object case by verb class and tense series. Classes 2 and 3 are intransitive (no direct object).

Equations

Instances For

theorem Fragments.Georgian.Agreement.class1_matches_subjectCase (ts : TenseSeries) :

verbClassSubjectCase VerbClass.class1 ts = subjectCase ts

Class 1 patterns match the existing subjectCase/objectCase.

theorem Fragments.Georgian.Agreement.class1_matches_objectCase (ts : TenseSeries) :

verbClassObjectCase VerbClass.class1 ts = some (objectCase ts)

The Ergative generalization from verb classes: ERG in the aorist ↔ non-derived subject (classes 1, 3).