The containment order on Case

Caha takes the representation of a case to be a stack of nested feature shells, so that each case on a hierarchy of cases contains the cases before it. The hierarchy here is the list containment of the nominative, accusative, genitive, dative and locative, and one case is below another when it comes earlier in the list, [c₁, c₂] <+ containment. The cases off the list, such as the ergative, the absolutive and the instrumental, are comparable only to themselves. The order is a scoped instance (open scoped Case.Caha), since a theoretical order is an opt-in commitment and not an order on the inventory. McFadden's nonnominative cases, those containing the accusative, are the natural class whose shared feature conditions the stem allomorphy that sets the nominative apart, and the *ABA syncretism law over the order is the framework-neutral Morphology.IsContiguous.

The directional containment of spatial cases, Place ⊂ Goal ⊂ Source ⊂ Route, is Spatial.Path.Direction, and the decomposition of spatial cases into localization and direction is in Syntax/Case/Spatial.lean.

Main definitions

• Case.containment: the containment hierarchy.
• The scoped PartialOrder Case instance in Case.Caha: the containment order.
• Case.IsNonnominative: the cases containing the accusative.

Main results

• Case.IsNonnominative.mem_containment: every nonnominative case is on the hierarchy.

Implementation notes

The list is the start of Blake's hierarchy, nominative, accusative or ergative, genitive, dative, locative, ablative or instrumental, along its accusative alignment and cut before the ablative and instrumental, which share a position. McFadden takes Blake's hierarchy as Caha updates it, and Aitha caps it with the postpositions, which the locative stands for here. Caha's own sequences differ: his Universal Case sequence is nominative, accusative, genitive, dative, instrumental, comitative, and his Russian order puts the prepositional between the genitive and the dative. They are stated in Studies/Caha2009.lean.

References

• [Cah09]
• [Bla94b]
• [McF18]
• [Ait26]

def Case.containment : List Case

The containment hierarchy is the nominative, accusative, genitive, dative and locative, each containing the cases before it.

Equations

• Case.containment = [Case.nom, Case.acc, Case.gen, Case.dat, Case.loc]

theorem Case.nodup_containment : containment.Nodup

@[instance_reducible]

def Case.Caha.instPartialOrder : PartialOrder Case

In the containment order a case is below another when it comes earlier in containment, and a case off the hierarchy is comparable only to itself.

Equations

• Case.Caha.instPartialOrder = partialOrderOfSO fun (c₁ c₂ : Case) => [c₁, c₂].Sublist Case.containment

@[instance_reducible]

def Case.Caha.instDecidableLE : DecidableLE Case

Equations

• Case.Caha.instDecidableLE c₁ c₂ = { decide := decide (c₁ = c₂) || decide ([c₁, c₂].Sublist Case.containment), reflects_decide := ⋯ }

@[instance_reducible]

def Case.Caha.instDecidableLT : DecidableLT Case

Equations

• Case.Caha.instDecidableLT c₁ c₂ = { decide := decide ([c₁, c₂].isSublist Case.containment = true), reflects_decide := ⋯ }

def Case.IsNonnominative (c : Case) : Prop

A case is nonnominative when its representation contains the accusative's, .acc ≤ c in the containment order.

Equations

• c.IsNonnominative = (Case.acc ≤ c)

@[instance_reducible]

instance Case.instDecidableIsNonnominative (c : Case) : Decidable c.IsNonnominative

Equations

• c.instDecidableIsNonnominative = { decide := decide (Case.acc = c) || decide ([Case.acc, c].Sublist Case.containment), reflects_decide := ⋯ }

theorem Case.IsNonnominative.mem_containment {c : Case} (h : c.IsNonnominative) : c ∈ containment

A nonnominative case is on the containment hierarchy, so that the ergative, the absolutive and the oblique of a direct–oblique system are not nonnominative.