Georgian case marking and verbal agreement

The Georgian verb agrees with its subject and its objects by means of two sets of affixes. Set A has v- for the first person, nothing for the second and a suffix for the third, and adds -t for a first or second person plural. Set B has m- for the first person singular, gv- for the first person plural and g- for the second person, with -t for its plural. A third person direct object has no Set B affix, while a third person indirect object has h- or s- before certain consonants.

Which set marks which argument, and in which case the arguments stand, depends on the class of the verb and on the series of its tense. The tenses fall into three series: the first contains the present and the future, the second the aorist, the third the perfect. Transitive verbs, and the medial verbs that pattern with them, such as tamaš 'play', have three patterns. In the first series the subject is nominative with Set A and the direct object dative with Set B. In the second the subject is ergative and the direct object nominative, with the same sets. In the third the subject is dative with Set B and the direct object nominative with Set A, and an indirect object loses its agreement and becomes the object of the postposition -tvis 'for'. Intransitive verbs have the first of these patterns in every series, and indirect verbs, such as c'on 'like', have the third in every series.

Main declarations

• Georgian.setA, Georgian.setB: the two sets of agreement affixes.
• Georgian.Series, Georgian.VerbClass: the series of the tenses and the classes of verbs.
• Georgian.Pattern: the case and the agreement set of the subject and the objects, with the three patterns Pattern.nominative, Pattern.ergative and Pattern.inverse.
• Georgian.pattern: the pattern of each class in each series.

Main results

• Georgian.hasObjectPrefix_iff_isSAP: the direct objects with a Set B prefix are the first and second persons.
• Georgian.subject_affixes_present_eq_aorist: the subject keeps its set of affixes from the first series to the second, whatever becomes of its case.
• Georgian.subject_case_ne_iff: the subject changes case from the first series to the second exactly in the transitive and medial classes.

Implementation notes

The third person suffixes of Set A are those of the present; other tenses have -a or -o in the singular and -es or -nen in the plural. The classes are the four of Harris, who numbers them 1 (transitive), 2 (intransitive), 3 (medial) and 4 (indirect); Hewitt adds a small class of stative verbs, which pattern with the intransitives.

References

• [Hew95]
• [Har81]

The agreement affixes

def Georgian.setA : Agreement.Paradigm (List Morphology.Morph)

The affixes of Set A, as they stand in the present.

Equations

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

def Georgian.setB : Agreement.Paradigm (List Morphology.Morph)

The affixes of Set B, as they mark a direct object.

Equations

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

def Georgian.thirdIndirect : Morphology.Morph

The Set B prefix of a third person indirect object. It stands before k, k', g, q' and p', becomes s- before c, c', j, č, č', ǰ, t, t' and d, and is dropped before other consonants and before vowels.

Equations

• Georgian.thirdIndirect = Morphology.Morph.pref "h"

def Georgian.HasObjectPrefix (c : Agreement.Bundle) : Prop

A direct object of the cell has a Set B prefix.

Equations

• Georgian.HasObjectPrefix c = ∃ ms ∈ Georgian.setB.realize c, ms ≠ []

@[instance_reducible]

instance Georgian.instDecidablePredBundleHasObjectPrefix : DecidablePred HasObjectPrefix

Equations

• Georgian.instDecidablePredBundleHasObjectPrefix x✝ = Georgian.instDecidablePredBundleHasObjectPrefix._aux_1 x✝

theorem Georgian.hasObjectPrefix_iff_isSAP (c : Agreement.Bundle) : c ∈ Agreement.Bundle.personNumberCells → (HasObjectPrefix c ↔ c.IsSAP)

The direct objects with a Set B prefix are the first and second persons.

Series and verb classes

inductive Georgian.Series : Type

The three series of tenses. The first contains the present, the imperfect, the future and the conditional, the second the aorist and the optative, the third the perfect and the pluperfect.

• present : Series
• aorist : Series
• perfect : Series

@[instance_reducible]

instance Georgian.instDecidableEqSeries : DecidableEq Series

Equations

• Georgian.instDecidableEqSeries x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Georgian.instReprSeries : Repr Series

Equations

• Georgian.instReprSeries = { reprPrec := Georgian.instReprSeries.repr }

def Georgian.instReprSeries.repr : Series → ℕ → Std.Format

Equations

• Georgian.instReprSeries.repr Georgian.Series.present prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Georgian.Series.present")).group prec✝
• Georgian.instReprSeries.repr Georgian.Series.aorist prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Georgian.Series.aorist")).group prec✝
• Georgian.instReprSeries.repr Georgian.Series.perfect prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Georgian.Series.perfect")).group prec✝

@[instance_reducible]

instance Georgian.instFintypeSeries : Fintype Series

Equations

• Georgian.instFintypeSeries = { elems := { val := ↑Georgian.Series.enumList, nodup := Georgian.Series.enumList_nodup }, complete := Georgian.instFintypeSeries._proof_1 }

inductive Georgian.VerbClass : Type

The classes of verbs, by their case marking and agreement.

• transitive : VerbClass

  Transitive verbs, as k'l 'kill'.

• intransitive : VerbClass

  Intransitive verbs, among them the passives, as i-k'vl-eb 'be killed'.

• medial : VerbClass

  Medial verbs, which usually have a subject alone and pattern with the transitives, as tamaš 'play'.

• indirect : VerbClass

  Indirect verbs, whose experiencer is dative in every series, as c'on 'like'.

@[instance_reducible]

instance Georgian.instDecidableEqVerbClass : DecidableEq VerbClass

Equations

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

def Georgian.instReprVerbClass.repr : VerbClass → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Georgian.instReprVerbClass.repr Georgian.VerbClass.medial prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Georgian.VerbClass.medial")).group prec✝

@[instance_reducible]

instance Georgian.instReprVerbClass : Repr VerbClass

Equations

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

@[instance_reducible]

instance Georgian.instFintypeVerbClass : Fintype VerbClass

Equations

• Georgian.instFintypeVerbClass = { elems := { val := ↑Georgian.VerbClass.enumList, nodup := Georgian.VerbClass.enumList_nodup }, complete := Georgian.instFintypeVerbClass._proof_1 }

inductive Georgian.AffixSet : Type

The two sets of agreement affixes.

• A : AffixSet
• B : AffixSet

@[instance_reducible]

instance Georgian.instDecidableEqAffixSet : DecidableEq AffixSet

Equations

• Georgian.instDecidableEqAffixSet x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Georgian.instReprAffixSet.repr : AffixSet → ℕ → Std.Format

Equations

• Georgian.instReprAffixSet.repr Georgian.AffixSet.A prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Georgian.AffixSet.A")).group prec✝
• Georgian.instReprAffixSet.repr Georgian.AffixSet.B prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Georgian.AffixSet.B")).group prec✝

@[instance_reducible]

instance Georgian.instReprAffixSet : Repr AffixSet

Equations

• Georgian.instReprAffixSet = { reprPrec := Georgian.instReprAffixSet.repr }

@[instance_reducible]

instance Georgian.instFintypeAffixSet : Fintype AffixSet

Equations

• Georgian.instFintypeAffixSet = { elems := { val := ↑Georgian.AffixSet.enumList, nodup := Georgian.AffixSet.enumList_nodup }, complete := Georgian.instFintypeAffixSet._proof_1 }

def Georgian.AffixSet.paradigm : AffixSet → Agreement.Paradigm (List Morphology.Morph)

The affixes of a set.

Equations

• Georgian.AffixSet.A.paradigm = Georgian.setA
• Georgian.AffixSet.B.paradigm = Georgian.setB

structure Georgian.Marking : Type

The marking of an argument, its case and the set of affixes it agrees by, if any.

• case : Case
• affixes : Option AffixSet

def Georgian.instDecidableEqMarking.decEq (x✝ x✝¹ : Marking) : Decidable (x✝ = x✝¹)

Equations

• Georgian.instDecidableEqMarking.decEq { case := a, affixes := a_1 } { case := b, affixes := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

@[instance_reducible]

instance Georgian.instDecidableEqMarking : DecidableEq Marking

Equations

• Georgian.instDecidableEqMarking = Georgian.instDecidableEqMarking.decEq

@[instance_reducible]

instance Georgian.instReprMarking : Repr Marking

Equations

• Georgian.instReprMarking = { reprPrec := Georgian.instReprMarking.repr }

def Georgian.instReprMarking.repr : Marking → ℕ → Std.Format

Equations

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

structure Georgian.Pattern : Type

A pattern of case marking and agreement for the subject and the two objects.

• subject : Marking
• directObject : Marking
• indirectObject : Marking

def Georgian.instDecidableEqPattern.decEq (x✝ x✝¹ : Pattern) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Georgian.instDecidableEqPattern : DecidableEq Pattern

Equations

• Georgian.instDecidableEqPattern = Georgian.instDecidableEqPattern.decEq

def Georgian.instReprPattern.repr : Pattern → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Georgian.instReprPattern : Repr Pattern

Equations

• Georgian.instReprPattern = { reprPrec := Georgian.instReprPattern.repr }

def Georgian.Pattern.nominative : Pattern

The subject is nominative with Set A, and both objects are dative with Set B.

Equations

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

def Georgian.Pattern.ergative : Pattern

The subject is ergative with Set A, the direct object nominative and the indirect object dative, both with Set B.

Equations

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

def Georgian.Pattern.inverse : Pattern

The subject is dative with Set B and the direct object nominative with Set A. The indirect object is a genitive governed by the postposition -tvis 'for', without agreement.

Equations

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

def Georgian.pattern : VerbClass → Series → Pattern

The pattern of each class of verbs in each series.

Equations

• Georgian.pattern Georgian.VerbClass.transitive Georgian.Series.present = Georgian.Pattern.nominative
• Georgian.pattern Georgian.VerbClass.medial Georgian.Series.present = Georgian.Pattern.nominative
• Georgian.pattern Georgian.VerbClass.transitive Georgian.Series.aorist = Georgian.Pattern.ergative
• Georgian.pattern Georgian.VerbClass.medial Georgian.Series.aorist = Georgian.Pattern.ergative
• Georgian.pattern Georgian.VerbClass.transitive Georgian.Series.perfect = Georgian.Pattern.inverse
• Georgian.pattern Georgian.VerbClass.medial Georgian.Series.perfect = Georgian.Pattern.inverse
• Georgian.pattern Georgian.VerbClass.intransitive x✝ = Georgian.Pattern.nominative
• Georgian.pattern Georgian.VerbClass.indirect x✝ = Georgian.Pattern.inverse

theorem Georgian.subject_affixes_present_eq_aorist (v : VerbClass) : (pattern v Series.present).subject.affixes = (pattern v Series.aorist).subject.affixes

The subject keeps its set of affixes from the first series to the second, whatever becomes of its case.

theorem Georgian.subject_case_ne_iff (v : VerbClass) : (pattern v Series.present).subject.case ≠ (pattern v Series.aorist).subject.case ↔ v = VerbClass.transitive ∨ v = VerbClass.medial

The subject changes case from the first series to the second exactly in the transitive and medial classes.

theorem Georgian.affixes_eq_A_iff (v : VerbClass) (s : Series) : ((pattern v s).subject.affixes = some AffixSet.A ↔ (pattern v s).subject.case ≠ Case.dat) ∧ ((pattern v s).directObject.affixes = some AffixSet.A ↔ (pattern v s).subject.case = Case.dat)

In every class and series the nominative argument is the one that agrees by Set A, unless the subject is ergative.