Documentation

Linglib.Fragments.Georgian.Agreement

Georgian Agreement Fragment [Jus24] #

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.

def Georgian.Agreement.objectAgr :

Agreement.Paradigm String

Object agreement prefixes, as a descriptive paradigm over canonical φ-cells (Agreement.Cell — the same φ a pronoun carries). SAP objects (1st/2nd person) receive an overt prefix; 3rd person objects have no entry (unmarked). A controller's Word.agrCell indexes it directly.

Equations

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

Instances For

def Georgian.Agreement.isIndexed (c : Agreement.Cell) :

Bool

A P/R argument is indexed iff the object paradigm realizes its φ-cell. Differential: SAP cells are present, 3rd person absent.

Equations

Georgian.Agreement.isIndexed c = (Georgian.Agreement.objectAgr.realize c).isSome

Instances For

def Georgian.Agreement.subjectIsIndexed :

Agreement.Cell → Bool

Subject agreement is always present (not differential).

Equations

Georgian.Agreement.subjectIsIndexed x✝ = true

Instances For

theorem Georgian.Agreement.sap_objects_indexed :

isIndexed (Agreement.Cell.pn UD.Person.first UD.Number.Sing) = true ∧ isIndexed (Agreement.Cell.pn UD.Person.second UD.Number.Sing) = true ∧ isIndexed (Agreement.Cell.pn UD.Person.first UD.Number.Plur) = true ∧ isIndexed (Agreement.Cell.pn UD.Person.second UD.Number.Plur) = true

SAP objects are indexed (receive an overt prefix).

theorem Georgian.Agreement.third_objects_not_indexed :

isIndexed (Agreement.Cell.pn UD.Person.third UD.Number.Sing) = false ∧ isIndexed (Agreement.Cell.pn UD.Person.third UD.Number.Plur) = false

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

theorem Georgian.Agreement.p_indexing_differential :

Agreement.Cell.pnCells.any isIndexed = true ∧ (!decide (Agreement.Cell.pnCells.all isIndexed = true)) = true

P indexing is differential.

theorem Georgian.Agreement.indexed_iff_sap :

(Agreement.Cell.pnCells.all fun (c : Agreement.Cell) => isIndexed c == c.isSAP) = true

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

inductive 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

@[implicit_reducible]

instance Georgian.Agreement.instDecidableEqTenseSeries :

DecidableEq TenseSeries

Equations

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

@[implicit_reducible]

instance Georgian.Agreement.instReprTenseSeries :

Repr TenseSeries

Equations

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

def Georgian.Agreement.instReprTenseSeries.repr :

TenseSeries → ℕ → Std.Format

Equations

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

Instances For

def Georgian.Agreement.georgianSplit :

Alignment.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 Alignment.SplitErgativity from [Bla94b]'s typology of tense/aspect-conditioned splits.

Equations

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

Instances For

theorem Georgian.Agreement.aorist_ergative :

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

Aorist triggers ergative alignment.

theorem Georgian.Agreement.present_accusative :

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

Present series is non-ergative.

theorem Georgian.Agreement.evidential_accusative :

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

Evidential series is non-ergative.

def Georgian.Agreement.subjectCase :

TenseSeries → Case

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

Equations

Instances For

def Georgian.Agreement.objectCase :

TenseSeries → Case

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

Equations

Instances For

def Georgian.Agreement.caseInventory :

Finset Case

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

Georgian.Agreement.caseInventory = {Case.nom, Case.erg, Case.dat}

Instances For

def Georgian.Agreement.allTenseSeries :

List TenseSeries

The inventory covers all tense-series case frames.

Equations

Georgian.Agreement.allTenseSeries = [Georgian.Agreement.TenseSeries.present, Georgian.Agreement.TenseSeries.aorist, Georgian.Agreement.TenseSeries.evidential]

Instances For

theorem Georgian.Agreement.inventory_covers_subjects (ts : TenseSeries) :

ts ∈ allTenseSeries → subjectCase ts ∈ caseInventory

theorem Georgian.Agreement.inventory_covers_objects (ts : TenseSeries) :

ts ∈ allTenseSeries → objectCase ts ∈ caseInventory

def Georgian.Agreement.fullCaseInventory :

Finset Case

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

Georgian.Agreement.fullCaseInventory = {Case.nom, Case.erg, Case.gen, Case.dat}

Instances For

inductive Georgian.Agreement.VerbClass :

Georgian verb classes ([Har81]).

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 [Mar91]'s Ergative generalization.

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

Instances For

@[implicit_reducible]

instance Georgian.Agreement.instDecidableEqVerbClass :

DecidableEq VerbClass

Equations

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

@[implicit_reducible]

instance Georgian.Agreement.instReprVerbClass :

Equations

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

def Georgian.Agreement.instReprVerbClass.repr :

VerbClass → ℕ → Std.Format

Equations

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

Instances For

def Georgian.Agreement.takesErgInAorist :

VerbClass → Bool

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

The Ergative generalization ([Mar91] 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 Georgian.Agreement.class1_takes_erg :

takesErgInAorist VerbClass.class1 = true

theorem Georgian.Agreement.class2_no_erg :

takesErgInAorist VerbClass.class2 = false

theorem Georgian.Agreement.class3_takes_erg :

takesErgInAorist VerbClass.class3 = true

theorem Georgian.Agreement.class4_no_erg :

takesErgInAorist VerbClass.class4 = false

def Georgian.Agreement.verbClassSubjectCase :

VerbClass → TenseSeries → Case

Subject case by verb class and tense series ([Mar91] ex. 1–3).

Present/aorist patterns from [Mar91]. Evidential follows the general inversion pattern: all subjects surface as DAT ([Har81]).

Equations

Instances For

def Georgian.Agreement.verbClassObjectCase :

VerbClass → TenseSeries → Option Case

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

Equations

Instances For

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

verbClassSubjectCase VerbClass.class1 ts = subjectCase ts

Class 1 patterns match the existing subjectCase/objectCase.

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

verbClassObjectCase VerbClass.class1 ts = some (objectCase ts)

theorem Georgian.Agreement.erg_iff_nonderived :

takesErgInAorist VerbClass.class1 = true ∧ takesErgInAorist VerbClass.class3 = true ∧ takesErgInAorist VerbClass.class2 = false ∧ takesErgInAorist VerbClass.class4 = false

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