Blake (1994): Case

Blake surveys inflectional case systems from two members to a dozen and finds that they tend to be built up in one order: nominative, then accusative or ergative, genitive, dative, locative, ablative or instrumental, and then the rest. A language with a case at some position usually has a case at every position to its left. The vocative is set aside, since it marks no relation of a dependent to a head.

Blake stresses that this is a tendency and not an implicational universal. Bound pronouns and word order can do the work of a higher case, which leaves a gap, as with the Nanai genitive. And the lowest case of a small system is an elsewhere case of many functions, labelled by convention for the highest of them, which leaves an apparent gap where a lower function sits. The Latin ablative is such a case, merging an older ablative, instrumental and locative, and its label is in Blake's words somewhat arbitrary: the Latin labels skip the locative position, and the functions the Latin cases express fill it.

Main definitions

• Position, position: the positions of the hierarchy and the position of a case, with the vocative off the hierarchy.
• positions, gaps: the positions an inventory fills, and the unfilled ones to the left of a filled one.
• Conforms: an inventory fills every position to the left of each position it fills.

Main results

• Conforms.total: the position sets of two conforming inventories are nested, so that conforming systems lie along a single line of growth.
• gaps_subset_of_conforms: when the functions of a language's cases conform, a gap among its case labels is a position filled by a function some case is not labelled for.
• systems_conform, gaps_nanai, gaps_tarascan: the systems Blake cites at each stage conform, and his two gapped systems each miss one position.
• gaps_latin_labels, conforms_latin_functions: the Latin labels skip the locative and the Latin functions do not.
• latin_abl_functions_ancient_greek, latin_dat_functions_ssubset_ancient_greek: Greek has no ablative, its genitive and dative expressing the functions of the Latin one, and its dative is the more comprehensive case.
• gaps_finnish, gaps_hungarian, gaps_dargwa, gaps_mongolian, gaps_yakut, gaps_basel: the gaps among the fragment inventories.

Implementation notes

The absolutive is placed with the nominative, since Blake calls the unmarked case of an ergative system nominative. His systems with a purposive, Toda, Irula and Warndarang, are left out, the purposive not being a Case value. The text was checked in the second edition ([Bla01]).

References

• [Bla94b]
• [Bla01]
• [Sut92]

The hierarchy

inductive Blake1994.Position : Type

The positions of the hierarchy, from the nominative down. Accusative and ergative share a position, as do ablative and instrumental, and the cases past them all share the last.

• nom : Position
• accErg : Position
• gen : Position
• dat : Position
• loc : Position
• ablInst : Position
• other : Position

@[instance_reducible]

instance Blake1994.instDecidableEqPosition : DecidableEq Position

Equations

• Blake1994.instDecidableEqPosition x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Blake1994.instFintypePosition : Fintype Position

Equations

• Blake1994.instFintypePosition = { elems := { val := ↑Blake1994.Position.enumList, nodup := Blake1994.Position.enumList_nodup }, complete := Blake1994.instFintypePosition._proof_1 }

def Blake1994.instReprPosition.repr : Position → ℕ → Std.Format

Equations

• Blake1994.instReprPosition.repr Blake1994.Position.nom prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Blake1994.Position.nom")).group prec✝
• Blake1994.instReprPosition.repr Blake1994.Position.accErg prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Blake1994.Position.accErg")).group prec✝
• Blake1994.instReprPosition.repr Blake1994.Position.gen prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Blake1994.Position.gen")).group prec✝
• Blake1994.instReprPosition.repr Blake1994.Position.dat prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Blake1994.Position.dat")).group prec✝
• Blake1994.instReprPosition.repr Blake1994.Position.loc prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Blake1994.Position.loc")).group prec✝
• Blake1994.instReprPosition.repr Blake1994.Position.ablInst prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Blake1994.Position.ablInst")).group prec✝
• Blake1994.instReprPosition.repr Blake1994.Position.other prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Blake1994.Position.other")).group prec✝

@[instance_reducible]

instance Blake1994.instReprPosition : Repr Position

Equations

• Blake1994.instReprPosition = { reprPrec := Blake1994.instReprPosition.repr }

def Blake1994.Position.rank : Position → Fin 7

The place of a position in the sequence.

Equations

• Blake1994.Position.nom.rank = 0
• Blake1994.Position.accErg.rank = 1
• Blake1994.Position.gen.rank = 2
• Blake1994.Position.dat.rank = 3
• Blake1994.Position.loc.rank = 4
• Blake1994.Position.ablInst.rank = 5
• Blake1994.Position.other.rank = 6

theorem Blake1994.Position.rank_injective : Function.Injective rank

@[instance_reducible]

instance Blake1994.instLinearOrderPosition : LinearOrder Position

Equations

• Blake1994.instLinearOrderPosition = LinearOrder.lift' Blake1994.Position.rank Blake1994.Position.rank_injective

def Blake1994.position : Case → Option Position

The position of a case. A local case goes by its direction, a case of rest with the locative and a case of source with the ablative, and the vocative has no position. The oblique of a two-case system is at the second position, the case that is likely to cover P or A but for which Blake finds the label oblique more appropriate (p. 156).

Equations

• One or more equations did not get rendered due to their size.
• Blake1994.position Case.nom = some Blake1994.Position.nom
• Blake1994.position Case.abs = some Blake1994.Position.nom
• Blake1994.position Case.acc = some Blake1994.Position.accErg
• Blake1994.position Case.erg = some Blake1994.Position.accErg
• Blake1994.position Case.obl = some Blake1994.Position.accErg
• Blake1994.position Case.gen = some Blake1994.Position.gen
• Blake1994.position Case.dat = some Blake1994.Position.dat
• Blake1994.position Case.inst = some Blake1994.Position.ablInst
• Blake1994.position Case.voc = none

def Blake1994.positions (inv : Finset Case) : Finset Position

The positions an inventory fills.

Equations

• Blake1994.positions inv = inv.biUnion fun (c : Case) => (Blake1994.position c).toFinset

def Blake1994.Conforms (inv : Finset Case) : Prop

An inventory conforms to the hierarchy when it fills every position to the left of each position it fills.

Equations

• Blake1994.Conforms inv = IsLowerSet ↑(Blake1994.positions inv)

def Blake1994.gaps (inv : Finset Case) : Finset Position

The gaps of an inventory are the unfilled positions to the left of a filled one.

Equations

• Blake1994.gaps inv = {q : Blake1994.Position | q ∉ Blake1994.positions inv ∧ ∃ p ∈ Blake1994.positions inv, q < p}

theorem Blake1994.mem_positions {inv : Finset Case} {p : Position} : p ∈ positions inv ↔ ∃ c ∈ inv, position c = some p

theorem Blake1994.mem_gaps {inv : Finset Case} {q : Position} : q ∈ gaps inv ↔ q ∉ positions inv ∧ ∃ p ∈ positions inv, q < p

@[instance_reducible]

instance Blake1994.instDecidableConforms {inv : Finset Case} : Decidable (Conforms inv)

Equations

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

theorem Blake1994.conforms_iff {inv : Finset Case} : Conforms inv ↔ ∀ c ∈ inv, ∀ (p : Position), position c = some p → ∀ q < p, ∃ d ∈ inv, position d = some q

Conformity in Blake's own wording, that a language with a case at some position has a case at each position to its left.

theorem Blake1994.conforms_iff_gaps_eq_empty {inv : Finset Case} : Conforms inv ↔ gaps inv = ∅

theorem Blake1994.positions_mono {inv inv' : Finset Case} (h : inv ⊆ inv') : positions inv ⊆ positions inv'

theorem Blake1994.Conforms.total {inv inv' : Finset Case} (h : Conforms inv) (h' : Conforms inv') : positions inv ⊆ positions inv' ∨ positions inv' ⊆ positions inv

Conforming systems lie along one line of growth, since of any two one fills every position the other fills.

theorem Blake1994.positions_insert_voc {inv : Finset Case} : positions (insert Case.voc inv) = positions inv

The vocative is off the hierarchy, so adding it changes nothing.

theorem Blake1994.gaps_subset_of_conforms {inv inv' : Finset Case} (h : inv ⊆ inv') (h' : Conforms inv') : gaps inv ⊆ positions inv' \ positions inv

Labelling a case for the highest of its functions leaves only apparent gaps. When the case functions of a language conform, each gap among its case labels is a position that some case fills with a function it is not labelled for.

The systems Blake cites

def Blake1994.classicalArmenian : Finset Case

Classical Armenian, with the Proto-Indo-European system less the vocative.

Equations

• Blake1994.classicalArmenian = {Case.nom, Case.acc, Case.gen, Case.dat, Case.loc, Case.abl, Case.inst}

def Blake1994.nanai : Finset Case

Nanai, where a bound pronoun cross-references the possessor.

Equations

• Blake1994.nanai = {Case.nom, Case.acc, Case.dat, Case.loc, Case.abl, Case.inst, Case.all}

def Blake1994.tarascan : Finset Case

Tarascan, where recipients and beneficiaries take the accusative and the locative covers source and goal as well as location.

Equations

• Blake1994.tarascan = {Case.nom, Case.acc, Case.gen, Case.loc, Case.inst, Case.com}

def Blake1994.systems : List (Finset Case)

The systems Blake cites for the successive stages of the hierarchy, with the four cases of Ancient Greek (beside its vocative), German and Icelandic, the six of the Slavonic languages (beside the vocative of Polish, Czech and Serbo-Croat) and of Turkish, the seven of Classical Armenian and the eight of Tamil.

Equations

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

theorem Blake1994.systems_conform (inv : Finset Case) : inv ∈ systems → Conforms inv

theorem Blake1994.gaps_nanai : gaps nanai = {Position.gen}

Nanai has every position down to the last but the genitive.

theorem Blake1994.gaps_tarascan : gaps tarascan = {Position.dat}

Tarascan has every position down to the last but the dative.

Latin

Blake gives Latin as the five-case stage, nominative, accusative, genitive, dative and a last case of many functions whose label is somewhat arbitrary.

theorem Blake1994.gaps_latin_labels : gaps (Finset.image Latin.Case.label Finset.univ) = {Position.loc}

The Latin case labels skip the locative.

theorem Blake1994.positions_latin_functions : positions (Finset.univ.biUnion Latin.Case.functions) = Finset.univ

The functions the Latin cases express fill every position.

theorem Blake1994.conforms_latin_functions : Conforms (Finset.univ.biUnion Latin.Case.functions)

theorem Blake1994.gaps_latin_labels_subset : gaps (Finset.image Latin.Case.label Finset.univ) ⊆ positions (Finset.univ.biUnion Latin.Case.functions) \ positions (Finset.image Latin.Case.label Finset.univ)

The Latin gap is apparent, the locative being a function of a case labelled for another.

Ancient Greek

Blake sets the Ancient Greek dative beside the Latin one to show that cases are compared by the functions they cover and not by their labels. Greek has no ablative, and the functions of the Latin ablative fall to the Greek genitive, which expresses source, and to the Greek dative, which expresses location and instrument, so that the Greek dative is the more comprehensive case.

theorem Blake1994.latin_abl_functions_ancient_greek : Case.abl ∉ Finset.image Greek.Ancient.Case.label Finset.univ ∧ Latin.Case.abl.functions ⊆ Greek.Ancient.Case.gen.functions ∪ Greek.Ancient.Case.dat.functions

Greek has no ablative, and the functions of the Latin ablative fall to its genitive and dative.

theorem Blake1994.latin_dat_functions_ssubset_ancient_greek : Latin.Case.dat.functions ⊂ Greek.Ancient.Case.dat.functions

The Greek dative is a more comprehensive case than the Latin dative.

The other case inventories of the fragments

theorem Blake1994.fragments_conform (inv : Finset Case) : inv ∈ [Finset.image Greek.StandardModern.Case.label Finset.univ, Finset.image Arabic.ModernStandard.Case.label Finset.univ, Finset.image HindiUrdu.Case.label Finset.univ, Finset.image Telugu.Case.label Finset.univ, Finset.image Belarusian.Case.label Finset.univ, Finset.image Cassubian.Case.label Finset.univ, Finset.image Russian.Case.label Finset.univ, Finset.image Slovenian.Case.label Finset.univ, Finset.image Sorbian.Upper.Case.label Finset.univ, Finset.image Sorbian.Lower.Case.label Finset.univ, Finset.image Ukrainian.Case.label Finset.univ] → Conforms inv

Modern Greek, Modern Standard Arabic, Hindi, Telugu and the Slavic languages not among Blake's systems conform. Blake gives Modern Greek and Classical Arabic as three-case systems of nominative, accusative and genitive ([Bla01] p. 156), and the inflectional cases of Hindi–Urdu, leaving aside the vocative, as nominative and oblique (p. 10).

theorem Blake1994.gaps_finnish : gaps (Finset.image Finnish.Case.label Finset.univ) = {Position.dat}

Finnish has no dative, the allative marking the recipient.

theorem Blake1994.gaps_hungarian : gaps (Finset.image Hungarian.Case.label Finset.univ) = {Position.gen}

Hungarian has no genitive, the dative marking the possessor, as in the Pama-Nyungan languages Blake mentions.

theorem Blake1994.gaps_dargwa : gaps (Finset.image Dargwa.Case.label Finset.univ) = {Position.loc, Position.ablInst}

The grammatical cases of Dargwa skip the locative and the ablative, which belong to its separate series of local cases.

theorem Blake1994.gaps_mongolian : gaps (Finset.image Mongolian.Case.label Finset.univ) = {Position.loc}

Mongolian has no locative, which postpositions express.

theorem Blake1994.gaps_yakut : gaps (Finset.image Yakut.Case.label Finset.univ) = {Position.loc}

Yakut has no locative.

theorem Blake1994.gaps_basel : gaps (Finset.image German.Basel.Case.label Finset.univ) = {Position.gen}

Basel German has no genitive, its possessor a dative construction.