Gender assignment is local

Adamson's gender locality hypothesis says that the gender feature on a nominalizer n is valued within nP (GenderLocal), so an inalienable possessor in Spec,nP can bear on a noun's gender while an alienable possessor in Spec,PossP cannot (possession_asymmetry). Possession bears on gender in two ways. Under possessee gender the nominalizer that licenses a possessor carries a gender of its own: Teop body-part roots take a gender I nominalizer that introduces the body-part relation with or without the selectional feature licensing a possessor, and the possessor-less variant is renominalized by a gender II alienator that closes the possessor slot (Teop.relationalN, Teop.alienatorN, Teop.freeDenot_iff), so a bina-naa 'my spleen' is gender I and o bina 'the spleen' gender II (Teop.switch, Teop.rows_class). The alienator is a plain n over a gendered one, so the default gender II is what the cyclic explanation of Kramer's Highest Gender Hypothesis predicts and not the hierarchical one (Teop.free_cyclic). Mosel and Spriggs's gender I-E is gender I with a proprial feature. The article vocabulary derives the article of every class (Teop.article_eq_headArticle), and agreeing adjectives and numerals distinguish only gender (Teop.agreementClasses_targetArticle). Jarawara's possessed nouns are the unmarked feminine, and the mano ~ mani alternation is agreement with the possessor: gender impoverishment next to a plural or participant feature bleeds the masculine exponent (Jarawara.decl_masc_only, Jarawara.agreeingForm_eq_form), and a monomoraic possessor prefix forms one word with the noun it possesses and is invisible beyond it, so in o-mano baki the outer noun agrees with the possessed noun's own feminine (Jarawara.complex_match, Jarawara.complex_mismatch).

Under inherited gender the nominalizer is unvalued and probes its possessor (inheritedGender): Yanyuwa wini 'name' and Coastal Marind igih 'name' and nanVh 'face' take the gender of an inalienable possessor on their agreement targets and, for nanVh, in their own form (Yanyuwa.name_agreement, CoastalMarind.name_demonstrative, CoastalMarind.face_inherits), and an alienable possessor leaves them unvalued (Yanyuwa.name_alienable). The hypothesis extends beyond possession: Standard Italian plurals in -a carry number on n and change gender, regular plurals carry number on Num and do not (Italian.gender_change_iff_local).

Implementation notes

• An inalienable possessor sits in Spec,nP, following Myler; Alexiadou makes it the complement of the noun. Both places are within nP, which is all the locality hypothesis uses.
• A Teop nominal's class is the gender a probe finds in the last cycle of its spine, Kramer's derivation of the Highest Gender Hypothesis from cyclicity.

References

• [Ada24]
• [Kra15]
• [Ale03]
• [MS00]
• [Dix04]
• [Myl16]

The gender locality hypothesis

inductive Adamson2024.Layer : Type

The layers of the nominal projection, from the root up.

• root : Layer
• n : Layer
• poss : Layer
• num : Layer
• d : Layer

@[instance_reducible]

instance Adamson2024.instDecidableEqLayer : DecidableEq Layer

Equations

• Adamson2024.instDecidableEqLayer x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Adamson2024.instReprLayer.repr : Layer → ℕ → Std.Format

Equations

• Adamson2024.instReprLayer.repr Adamson2024.Layer.root prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Adamson2024.Layer.root")).group prec✝
• Adamson2024.instReprLayer.repr Adamson2024.Layer.n prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Adamson2024.Layer.n")).group prec✝
• Adamson2024.instReprLayer.repr Adamson2024.Layer.poss prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Adamson2024.Layer.poss")).group prec✝
• Adamson2024.instReprLayer.repr Adamson2024.Layer.num prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Adamson2024.Layer.num")).group prec✝
• Adamson2024.instReprLayer.repr Adamson2024.Layer.d prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Adamson2024.Layer.d")).group prec✝

@[instance_reducible]

instance Adamson2024.instReprLayer : Repr Layer

Equations

• Adamson2024.instReprLayer = { reprPrec := Adamson2024.instReprLayer.repr }

@[instance_reducible]

instance Adamson2024.instFintypeLayer : Fintype Layer

Equations

• Adamson2024.instFintypeLayer = { elems := { val := ↑Adamson2024.Layer.enumList, nodup := Adamson2024.Layer.enumList_nodup }, complete := Adamson2024.instFintypeLayer._proof_1 }

def Adamson2024.Layer.height : Layer → ℕ

The height of a layer.

Equations

• Adamson2024.Layer.root.height = 0
• Adamson2024.Layer.n.height = 1
• Adamson2024.Layer.poss.height = 2
• Adamson2024.Layer.num.height = 3
• Adamson2024.Layer.d.height = 4

@[instance_reducible]

instance Adamson2024.instLinearOrderLayer : LinearOrder Layer

Equations

• Adamson2024.instLinearOrderLayer = LinearOrder.lift' Adamson2024.Layer.height Adamson2024.instLinearOrderLayer._proof_1

inductive Adamson2024.Position : Type

The positions of a possessor or of a number feature.

• nHead : Position
• specN : Position
• specPoss : Position
• num : Position

@[instance_reducible]

instance Adamson2024.instDecidableEqPosition : DecidableEq Position

Equations

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

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

Equations

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

@[instance_reducible]

instance Adamson2024.instReprPosition : Repr Position

Equations

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

@[instance_reducible]

instance Adamson2024.instFintypePosition : Fintype Position

Equations

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

def Adamson2024.Position.layer : Position → Layer

The layer a position attaches at.

Equations

• Adamson2024.Position.nHead.layer = Adamson2024.Layer.n
• Adamson2024.Position.specN.layer = Adamson2024.Layer.n
• Adamson2024.Position.specPoss.layer = Adamson2024.Layer.poss
• Adamson2024.Position.num.layer = Adamson2024.Layer.num

def Adamson2024.GenderLocal (p : Position) : Prop

A position is local to gender when it attaches within nP. The gender locality hypothesis says that only local positions can value gender on n.

Equations

• Adamson2024.GenderLocal p = (p.layer ≤ Adamson2024.Layer.n)

@[instance_reducible]

instance Adamson2024.instDecidablePredPositionGenderLocal : DecidablePred GenderLocal

Equations

• Adamson2024.instDecidablePredPositionGenderLocal x✝ = { decide := x✝.layer.height.ble Adamson2024.Layer.n.height, reflects_decide := ⋯ }

inductive Adamson2024.PossessionType : Type

Inalienable and alienable possession.

• inalienable : PossessionType
• alienable : PossessionType

@[instance_reducible]

instance Adamson2024.instDecidableEqPossessionType : DecidableEq PossessionType

Equations

• Adamson2024.instDecidableEqPossessionType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Adamson2024.instReprPossessionType.repr : PossessionType → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Adamson2024.instReprPossessionType : Repr PossessionType

Equations

• Adamson2024.instReprPossessionType = { reprPrec := Adamson2024.instReprPossessionType.repr }

@[instance_reducible]

instance Adamson2024.instFintypePossessionType : Fintype PossessionType

Equations

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

def Adamson2024.PossessionType.possessorPosition : PossessionType → Position

An inalienable possessor sits in Spec,nP and an alienable one in Spec,PossP.

Equations

• Adamson2024.PossessionType.inalienable.possessorPosition = Adamson2024.Position.specN
• Adamson2024.PossessionType.alienable.possessorPosition = Adamson2024.Position.specPoss

theorem Adamson2024.possession_asymmetry : GenderLocal PossessionType.inalienable.possessorPosition ∧ ¬GenderLocal PossessionType.alienable.possessorPosition

An inalienable possessor can bear on gender, an alienable one cannot.

def Adamson2024.inheritedGender {G : Type u_1} (pos : Position) (g : G) : Option G

The gender an unvalued n acquires from a possessor of gender g at pos, when the possessor is local.

Equations

• Adamson2024.inheritedGender pos g = if Adamson2024.GenderLocal pos then some g else none

Teop: possessee gender

def Adamson2024.Teop.relationalN (selectsD : Bool) : DistributedMorphology.Categorizer.Head

The nominalizer of a body-part or kinship root, bearing u[animate] and, when selectsD, the feature {D} that licenses a possessor.

Equations

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

def Adamson2024.Teop.alienatorN : DistributedMorphology.Categorizer.Head

The alienator, a gender II n that closes the possessor slot.

Equations

• Adamson2024.Teop.alienatorN = DistributedMorphology.Categorizer.Head.n_plain

def Adamson2024.Teop.headClass (h : DistributedMorphology.Categorizer.Head) : Option Teop.NounClass

The class a head gives a nominal, the a-class for the gender I feature [+ANIM] and none otherwise.

Equations

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

def Adamson2024.Teop.ipossessed : List DistributedMorphology.Categorizer.Head

The n's of a possessed body-part noun, the {D} nominalizer.

Equations

• Adamson2024.Teop.ipossessed = [Adamson2024.Teop.relationalN true]

def Adamson2024.Teop.free : List DistributedMorphology.Categorizer.Head

The n's of an unpossessed body-part noun, the {D}-less nominalizer under the alienator, innermost first. Alienably possessed and compounded body-part nouns have the same n's.

Equations

• Adamson2024.Teop.free = [Adamson2024.Teop.relationalN false, Adamson2024.Teop.alienatorN]

def Adamson2024.Teop.classOf (r : DistributedMorphology.Root) (hs : List DistributedMorphology.Categorizer.Head) : Teop.NounClass

The class of a nominal over the root r with the n's hs, the gender a probe finds in its last cycle, which is the o-class (gender II) by default. Every categorizer is a cyclic head.

Equations

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

theorem Adamson2024.Teop.switch (r : DistributedMorphology.Root) : classOf r ipossessed = Teop.NounClass.a ∧ classOf r free = Teop.NounClass.o

a bina-naa 'my spleen' is a-class and o bina 'the spleen' is o-class, the o-class being gender II, the default.

theorem Adamson2024.Teop.free_cyclic (r : DistributedMorphology.Root) : classOf r free = Teop.NounClass.o ∧ DistributedMorphology.agreeingGender headClass Teop.NounClass.o free.reverse = Teop.NounClass.a

The plain alienator over the gender I nominalizer gives o bina the default o-class, as the Highest Gender Hypothesis predicts; a probe searching every n would find the lower one and give the a-class.

theorem Adamson2024.Teop.bodyPartTerms_free (r : DistributedMorphology.Root) (n : Teop.Noun) : n ∈ Teop.bodyPartTerms → n.gender = classOf r free

Every body-part term of the fragment has the class of the unpossessed noun.

def Adamson2024.Teop.possession : List (String × List DistributedMorphology.Categorizer.Head)

The n's of a body-part or kinship noun, by how it is possessed.

Equations

• Adamson2024.Teop.possession = [("inalienable", Adamson2024.Teop.ipossessed), ("alienable", Adamson2024.Teop.free), ("none", Adamson2024.Teop.free)]

theorem Adamson2024.Teop.rows_class (r : DistributedMorphology.Root) (e : Datum) : e ∈ Examples.all → e.language = "teop1238" → ∀ s ∈ e.parse? "possession" possession, ∀ c ∈ e.parse? "gender" [("I", Teop.NounClass.a), ("II", Teop.NounClass.o)], classOf r s = c

The analysis predicts the class of every attested body-part and kinship phrase from how its noun is possessed, (39), (40), (44), (45), (48) and (51).

inductive Adamson2024.Teop.ArticleFeature : Type

The features of the article, copied from DP by concord.

• animate : ArticleFeature
• pl : ArticleFeature
• proper : ArticleFeature

@[instance_reducible]

instance Adamson2024.Teop.instDecidableEqArticleFeature : DecidableEq ArticleFeature

Equations

• Adamson2024.Teop.instDecidableEqArticleFeature x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Adamson2024.Teop.instReprArticleFeature : Repr ArticleFeature

Equations

• Adamson2024.Teop.instReprArticleFeature = { reprPrec := Adamson2024.Teop.instReprArticleFeature.repr }

def Adamson2024.Teop.instReprArticleFeature.repr : ArticleFeature → ℕ → Std.Format

Equations

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

def Adamson2024.Teop.articles : List (DistributedMorphology.VocabularyItem ArticleFeature Teop.Article)

The article vocabulary (32).

Equations

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

def Adamson2024.Teop.classFeatures : Teop.NounClass → List ArticleFeature

The article features of each class. Gender I-E is gender I with [proper].

Equations

• Adamson2024.Teop.classFeatures Teop.NounClass.e = [Adamson2024.Teop.ArticleFeature.animate, Adamson2024.Teop.ArticleFeature.proper]
• Adamson2024.Teop.classFeatures Teop.NounClass.a = [Adamson2024.Teop.ArticleFeature.animate]
• Adamson2024.Teop.classFeatures Teop.NounClass.o = []

def Adamson2024.Teop.article (c : Teop.NounClass) (plural : Bool) : Option Teop.Article

The article inserted by the Subset Principle, by class and number.

Equations

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

theorem Adamson2024.Teop.article_eq_headArticle (c : Teop.NounClass) (pl : Bool) : article c pl = some (Teop.headArticle c pl)

The vocabulary derives the basic article of every class and number.

theorem Adamson2024.Teop.agreementClasses_targetArticle : Gender.agreementClasses Teop.targetArticle = Setoid.ker fun (c : Teop.NounClass) => (classFeatures c).contains ArticleFeature.animate

The agreement classes of adjectives and numerals are the fibres of [animate], so gender I-E is not a gender.

theorem Adamson2024.Teop.kinship (r : DistributedMorphology.Root) : DistributedMorphology.subsetPrinciple articles ↑(ArticleFeature.proper :: classFeatures (classOf r ipossessed)) = some Teop.Article.e ∧ DistributedMorphology.subsetPrinciple articles ↑(ArticleFeature.proper :: classFeatures (classOf r free)) = some Teop.Article.o

A possessed kinship term takes the proprial article e, (50), and one under the alienator takes o, (51).

def Adamson2024.Teop.ipossessedDenot {E : Type u_1} {S : Type u_2} (isSpleen : E → S → Prop) (bodyPartOf : E → E → S → Prop) : E → E → S → Prop

The possessed body-part noun, the root relationalized by the body-part-of relation.

Equations

• Adamson2024.Teop.ipossessedDenot isSpleen bodyPartOf = Possession.π isSpleen bodyPartOf

def Adamson2024.Teop.freeDenot {E : Type u_1} {S : Type u_2} (isSpleen : E → S → Prop) (bodyPartOf : E → E → S → Prop) : E → S → Prop

The unpossessed body-part noun, whose possessor slot the alienator closes.

Equations

• Adamson2024.Teop.freeDenot isSpleen bodyPartOf = ⨆ (x : E), Adamson2024.Teop.ipossessedDenot isSpleen bodyPartOf x

theorem Adamson2024.Teop.freeDenot_iff {E : Type u_1} {S : Type u_2} (isSpleen : E → S → Prop) (bodyPartOf : E → E → S → Prop) (y : E) (s : S) : freeDenot isSpleen bodyPartOf y s ↔ isSpleen y s ∧ ∃ (x : E), bodyPartOf x y s

The possessor slot is open under the {D} nominalizer and existentially closed under the alienator.

Jarawara: possessee gender and possessor agreement

inductive Adamson2024.Jarawara.Phi : Type

The privative φ-features are [masc], [pl], and [participant] for first and second person.

• masc : Phi
• pl : Phi
• participant : Phi

@[instance_reducible]

instance Adamson2024.Jarawara.instDecidableEqPhi : DecidableEq Phi

Equations

• Adamson2024.Jarawara.instDecidableEqPhi x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Adamson2024.Jarawara.instReprPhi : Repr Phi

Equations

• Adamson2024.Jarawara.instReprPhi = { reprPrec := Adamson2024.Jarawara.instReprPhi.repr }

def Adamson2024.Jarawara.instReprPhi.repr : Phi → ℕ → Std.Format

Equations

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

def Adamson2024.Jarawara.possessorPhi : Jarawara.Possessor → List Phi

The features a possessor contributes to agreement.

Equations

• Adamson2024.Jarawara.possessorPhi Jarawara.Possessor.sg1 = [Adamson2024.Jarawara.Phi.participant]
• Adamson2024.Jarawara.possessorPhi Jarawara.Possessor.sg2 = [Adamson2024.Jarawara.Phi.participant]
• Adamson2024.Jarawara.possessorPhi Jarawara.Possessor.incl = [Adamson2024.Jarawara.Phi.participant, Adamson2024.Jarawara.Phi.pl]
• Adamson2024.Jarawara.possessorPhi Jarawara.Possessor.excl = [Adamson2024.Jarawara.Phi.participant, Adamson2024.Jarawara.Phi.pl]
• Adamson2024.Jarawara.possessorPhi Jarawara.Possessor.nsg2 = [Adamson2024.Jarawara.Phi.participant, Adamson2024.Jarawara.Phi.pl]
• Adamson2024.Jarawara.possessorPhi (Jarawara.Possessor.sg3 g) = if g = Jarawara.Gender.masc then [Adamson2024.Jarawara.Phi.masc] else []
• Adamson2024.Jarawara.possessorPhi (Jarawara.Possessor.nsg3 g) = Adamson2024.Jarawara.Phi.pl :: if g = Jarawara.Gender.masc then [Adamson2024.Jarawara.Phi.masc] else []

def Adamson2024.Jarawara.impoverishment : List (DistributedMorphology.ImpoverishmentRule (List Phi) Phi)

Gender impoverishment deletes [masc] next to [pl] and next to [participant].

Equations

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

def Adamson2024.Jarawara.impoverish (φ : List Phi) : List Phi

The φ-bundle after impoverishment.

Equations

• Adamson2024.Jarawara.impoverish φ = DistributedMorphology.runChain (DistributedMorphology.ImpoverishmentRule.apply List.erase) Adamson2024.Jarawara.impoverishment ↑φ

def Adamson2024.Jarawara.declarative : List (DistributedMorphology.VocabularyItem Phi String)

The declarative marker is ka for [masc] and ke elsewhere.

Equations

• Adamson2024.Jarawara.declarative = [DistributedMorphology.VocabularyItem.ofFeatures [Adamson2024.Jarawara.Phi.masc] "ka", DistributedMorphology.VocabularyItem.ofFeatures [] "ke"]

def Adamson2024.Jarawara.decl (φ : List Phi) : Option String

The declarative marker agreeing with a nominal of features φ.

Equations

• Adamson2024.Jarawara.decl φ = DistributedMorphology.subsetPrinciple Adamson2024.Jarawara.declarative ↑(Adamson2024.Jarawara.impoverish φ)

theorem Adamson2024.Jarawara.decl_masc_only : decl [Phi.masc] = some "ka" ∧ decl [] = some "ke" ∧ decl [Phi.participant] = some "ke" ∧ decl [Phi.masc, Phi.pl] = some "ke"

Masculine singular takes ka and everything else ke, so impoverishment bleeds the specific exponent.

def Adamson2024.Jarawara.possessedItems (marked unmarked : String) : List (DistributedMorphology.VocabularyItem Phi String)

A possessed noun takes its marked form for [participant] or a surviving [masc] and its unmarked form elsewhere.

Equations

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

def Adamson2024.Jarawara.agreeingForm (n : Jarawara.PossessedNoun) (φ : List Phi) : Option String

The form of a possessed noun agreeing with a possessor of features φ.

Equations

• Adamson2024.Jarawara.agreeingForm n φ = DistributedMorphology.subsetPrinciple (Adamson2024.Jarawara.possessedItems n.mForm n.fForm) ↑(Adamson2024.Jarawara.impoverish φ)

theorem Adamson2024.Jarawara.agreeingForm_eq_form (n : Jarawara.PossessedNoun) : n ∈ Jarawara.possessedNouns → ∀ (p : Jarawara.Possessor), agreeingForm n (possessorPhi p) = some (n.form p)

Impoverishment then insertion derives the form of every possessed noun with every possessor; the third person masculine nonsingular, mee mani, is where impoverishment does the work.

def Adamson2024.Jarawara.visibleOutside (p : Jarawara.Possessor) : List Phi

A possessor makes its features visible outside the word of the noun it possesses unless it is a prefix, a pronoun below the two-mora minimal word that forms one word with that noun.

Equations

• Adamson2024.Jarawara.visibleOutside p = if p.IsPrefix then [] else Adamson2024.Jarawara.possessorPhi p

def Adamson2024.Jarawara.inside (p : Jarawara.Possessor) : Option String

bako 'inside' in [[p mano] bako], agreeing with the possessor when its features percolate and with the feminine possessed noun otherwise.

Equations

• Adamson2024.Jarawara.inside p = Adamson2024.Jarawara.agreeingForm Jarawara.bako (Adamson2024.Jarawara.visibleOutside p)

theorem Adamson2024.Jarawara.complex_match (p : Jarawara.Possessor) : ¬p.IsPrefix → inside p = some (Jarawara.bako.form p)

A possessor that is a separate word percolates, so the inner and outer nouns match.

theorem Adamson2024.Jarawara.complex_mismatch (p : Jarawara.Possessor) : p.IsPrefix → agreeingForm Jarawara.mano (possessorPhi p) = some "mano" ∧ inside p = some "baki"

The prefixes o- and ti- do not, as in o-mano baki and ti-mano baki.

Yanyuwa and Coastal Marind: inherited gender

theorem Adamson2024.Yanyuwa.name_agreement (s : Yanyuwa.Speaker) (g : Yanyuwa.Gender) : Option.map (Yanyuwa.agreementPrefix s) (inheritedGender PossessionType.inalienable.possessorPosition g) = some (Yanyuwa.agreementPrefix s g)

Quantifiers and demonstratives agreeing with wini 'name' take the prefix of an inalienable possessor's class.

theorem Adamson2024.Yanyuwa.classes_separated (s : Yanyuwa.Speaker) : ¬Function.Injective (Yanyuwa.agreementPrefix s) ∧ Function.Injective fun (g : Yanyuwa.Gender) => (Yanyuwa.agreementPrefix s g, decide g.HasNumber)

A prefix alone does not tell female from feminine, nor, in men's speech, male from masculine; with number, which only the female and male classes distinguish, every class is told apart.

theorem Adamson2024.Yanyuwa.name_alienable (g : Yanyuwa.Gender) : inheritedGender PossessionType.alienable.possessorPosition g = none

An alienable possessor is out of the probe's reach.

theorem Adamson2024.CoastalMarind.name_demonstrative (g : CoastalMarind.Gender) : Option.map (fun (x : CoastalMarind.Gender) => CoastalMarind.demonstrative x false) (inheritedGender PossessionType.inalienable.possessorPosition g) = some (CoastalMarind.demonstrative g false)

The demonstrative agreeing with igih 'name' takes the possessor's gender.

theorem Adamson2024.CoastalMarind.face_inherits : Option.map (fun (x : CoastalMarind.Gender) => CoastalMarind.face x false) (inheritedGender PossessionType.inalienable.possessorPosition CoastalMarind.Gender.gI) = some "nanih" ∧ Option.map (fun (x : CoastalMarind.Gender) => CoastalMarind.face x false) (inheritedGender PossessionType.inalienable.possessorPosition CoastalMarind.Gender.gII) = some "nanuh" ∧ CoastalMarind.similative CoastalMarind.Gender.gI false = "hi" ∧ CoastalMarind.similative CoastalMarind.Gender.gII false = "hu"

nanVh 'face' is nanih with a gender I possessor and nanuh with a gender II one, the similative agreeing alongside.

Number on n

def Adamson2024.Italian.numberPosition : Italian.NumberGender.PluralClass → Position

A plural class's number feature sits on n for the -a plurals and on Num for regular plurals.

Equations

• Adamson2024.Italian.numberPosition Italian.NumberGender.PluralClass.aPlural = Adamson2024.Position.nHead
• Adamson2024.Italian.numberPosition Italian.NumberGender.PluralClass.regular = Adamson2024.Position.num

theorem Adamson2024.Italian.gender_change_iff_local (n : Italian.NumberGender.Noun) : n ∈ Italian.NumberGender.aPlurals ++ Italian.NumberGender.regulars → (n.gender ≠ n.plGender ↔ GenderLocal (numberPosition n.pluralClass))

Gender changes between singular and plural exactly when number sits within the hypothesis's reach.