Kramer (2015): The Morphosyntax of Gender

This file formalizes chapter 10 of the book, on nominals with more than one n. Kramer's Highest Gender Hypothesis says that such a nominal agrees in the gender of its highest n, as that n would give over a bare root. She derives it from cyclicity: each n is a cyclic head that sends the nPs below it to spell-out, so agreement finds the last cycle alone. On a hierarchical alternative, agreement searches down for the highest n bearing a gender. The two differ only when a plain n tops a gendered one, where cyclicity predicts the default gender, and Amharic ɨnnat-ɨnnät 'motherhood' and German Städt-chen 'little town' bear it out, masculine and neuter. A diminutive that keeps the gender of its base is not an n.

Main results

• highestGender: a nominal agrees as its highest n would over a bare root.
• amharic_innat, german_chen: a plain n over a feminine n gives the default, where a search of every n would give the feminine.
• evaluative_transparent: an evaluative head that is not an n leaves the gender unchanged.

Implementation notes

• A head is a categorizer or an evaluative head that is not a categorizer; only categorizers are cyclic, and an evaluative head bears no gender.
• Genders are read off [±FEM], with the language's default for a plain n.

References

• [Kra15]

inductive Kramer2015.Head : Type

A head of a nominal, a categorizer or an evaluative head that is not one.

• cat (h : DistributedMorphology.Categorizer.Head) : Head
• eval : Head

def Kramer2015.instDecidableEqHead.decEq (x✝ x✝¹ : Head) : Decidable (x✝ = x✝¹)

Equations

• Kramer2015.instDecidableEqHead.decEq (Kramer2015.Head.cat a) (Kramer2015.Head.cat b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Kramer2015.instDecidableEqHead.decEq (Kramer2015.Head.cat h) Kramer2015.Head.eval = isFalse ⋯
• Kramer2015.instDecidableEqHead.decEq Kramer2015.Head.eval (Kramer2015.Head.cat h) = isFalse ⋯
• Kramer2015.instDecidableEqHead.decEq Kramer2015.Head.eval Kramer2015.Head.eval = isTrue ⋯

@[instance_reducible]

instance Kramer2015.instDecidableEqHead : DecidableEq Head

Equations

• Kramer2015.instDecidableEqHead = Kramer2015.instDecidableEqHead.decEq

def Kramer2015.Head.Cyclic : Head → Prop

Categorizers are cyclic and evaluative heads are not.

Equations

• (Kramer2015.Head.cat h).Cyclic = True
• Kramer2015.Head.eval.Cyclic = False

@[instance_reducible]

instance Kramer2015.instDecidablePredHeadCyclic : DecidablePred Head.Cyclic

Equations

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

def Kramer2015.Head.gender : Head → Option Gender

The gender a head's [±FEM] feature labels, if it bears one.

Equations

• One or more equations did not get rendered due to their size.
• Kramer2015.Head.eval.gender = none

def Kramer2015.agreeing (default : Gender) (r : DistributedMorphology.Root) (hs : List Head) : Gender

The agreeing gender of a nominal over the root r with the heads hs, innermost first, in a language whose default gender is default.

Equations

• Kramer2015.agreeing default r hs = DistributedMorphology.agreeingGender Kramer2015.Head.gender default ({ root := r, heads := hs }.lastCycle Kramer2015.Head.Cyclic)

theorem Kramer2015.highestGender (default : Gender) (r r' : DistributedMorphology.Root) (hs : List Head) (h : DistributedMorphology.Categorizer.Head) : agreeing default r (hs ++ [Head.cat h]) = agreeing default r' [Head.cat h]

The Highest Gender Hypothesis (32). A nominal agrees as its highest n would over a bare root.

theorem Kramer2015.amharic_innat (r : DistributedMorphology.Root) : agreeing Gender.masculine r [Head.cat DistributedMorphology.Categorizer.Head.n_iFem, Head.cat DistributedMorphology.Categorizer.Head.n_plain] = Gender.masculine ∧ DistributedMorphology.agreeingGender Head.gender Gender.masculine [Head.cat DistributedMorphology.Categorizer.Head.n_plain, Head.cat DistributedMorphology.Categorizer.Head.n_iFem] = Gender.feminine

In (22)–(26) ɨnnat-ɨnnät 'motherhood' is the plain n -ɨnnät over the female n of ɨnnat 'mother', and takes the masculine default; a search of every n would find the feminine.

theorem Kramer2015.german_chen (r : DistributedMorphology.Root) : agreeing Gender.neuter r [Head.cat DistributedMorphology.Categorizer.Head.n_uFem, Head.cat DistributedMorphology.Categorizer.Head.n_plain] = Gender.neuter ∧ DistributedMorphology.agreeingGender Head.gender Gender.neuter [Head.cat DistributedMorphology.Categorizer.Head.n_plain, Head.cat DistributedMorphology.Categorizer.Head.n_uFem] = Gender.feminine

In (29) and (31) Städt-chen 'little town' is the plain n -chen over the arbitrary feminine n of Stadt 'town', and is neuter; a search of every n would find the feminine.

theorem Kramer2015.evaluative_transparent (default : Gender) (r : DistributedMorphology.Root) (hs : List Head) (h : DistributedMorphology.Categorizer.Head) : agreeing default r (hs ++ [Head.cat h, Head.eval]) = agreeing default r (hs ++ [Head.cat h])

By (42) an evaluative head that is not an n leaves the nominal the gender of its highest n, as Russian l'es-ók 'little forest' stays masculine.