Gender on the nominal categorizer

The nominal categorizer is the locus of grammatical gender: an n may carry a valued gender feature (Gender.Signed), interpretable (natural) or uninterpretable (arbitrary), and Vocabulary Insertion realizes the result in the language's own gender system (Gender.System), falling back to the system's morphosyntactic default. The attested realization patterns — Set 1, Set 2, three-gender, animacy-based — differ only in their system, and PF is blind to interpretability. DM features are the non-hybrid fragment of Gender.SplitFeature, and the FEM slice of the head inventory is Gender.KramerN.

Main definitions

• GenderFeature, Interpretability, Contrastivity — gender features on n and their LF status
• Categorizer.Head — a categorizer with phi-features and the selectional feature {D}; Categorizer.Head.gendered builds the canonical inventory n_iFem … n_uMasc
• Categorizer.Head.realizeGender — Vocabulary Insertion into a Gender.System; IsSet1 … IsAnimacyBased — the attested patterns
• Categorizer.Head.LicensesIntrusion — gender-conditioned templatic t-intrusion

Main statements

• toSplitFeature_not_isHybrid — the DM calculus generates no hybrid features
• realizeGender_congr — PF is blind to interpretability
• not_isSet1_and_isSet2 — the Set 1 vs Set 2 parameter is exclusive

References

• R. Kramer, The morphosyntax of gender
• L. J. Adamson, Gender assignment is local
• L. Konnelly and E. Cowper, Gender diversity and morphosyntax
• P. W. Smith, Feature mismatches

Phi-features on categorizing heads

Grammatical gender lives on n, as an interpretable (natural) or uninterpretable (arbitrary) feature over a language-particular dimension ([Kra15]; [Ada24] for MASC and Teop).

inductive DistributedMorphology.Interpretability : Type

Whether a gender feature is legible at LF ([Kra15] §3.4.2). Interpretable gender is natural gender, restricting the denotation and licensed through the Encyclopedia, while uninterpretable gender is arbitrary, visible only at PF through Vocabulary Insertion.

• i : Interpretability
• u : Interpretability

@[instance_reducible]

instance DistributedMorphology.instDecidableEqInterpretability : DecidableEq Interpretability

Equations

• DistributedMorphology.instDecidableEqInterpretability x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance DistributedMorphology.instReprInterpretability : Repr Interpretability

Equations

• DistributedMorphology.instReprInterpretability = { reprPrec := DistributedMorphology.instReprInterpretability.repr }

def DistributedMorphology.instReprInterpretability.repr : Interpretability → ℕ → Std.Format

Equations

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

inductive DistributedMorphology.Contrastivity : Type

Whether the absence of a feature is itself meaningful ([Wil08b]; applied to gender by [KC20] §4). A contrastive feature's absence conveys ¬F, while a non-contrastive feature is a modifier whose absence is vacuous. Orthogonal to Interpretability — an interpretable feature can be non-contrastive.

• contrastive : Contrastivity
• nonContrastive : Contrastivity

@[instance_reducible]

instance DistributedMorphology.instDecidableEqContrastivity : DecidableEq Contrastivity

Equations

• DistributedMorphology.instDecidableEqContrastivity x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance DistributedMorphology.instReprContrastivity : Repr Contrastivity

Equations

• DistributedMorphology.instReprContrastivity = { reprPrec := DistributedMorphology.instReprContrastivity.repr }

def DistributedMorphology.instReprContrastivity.repr : Contrastivity → ℕ → Std.Format

Equations

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

def DistributedMorphology.Contrastivity.obligatory : Contrastivity → Bool

A contrastive feature must be present when the referent's value is known, since its absence would wrongly convey ¬F — a non-contrastive feature need not be.

Equations

• DistributedMorphology.Contrastivity.contrastive.obligatory = true
• DistributedMorphology.Contrastivity.nonContrastive.obligatory = false

structure DistributedMorphology.GenderFeature : Type

A valued gender feature (Gender.Signed) annotated for interpretability. Per dimension this yields the four attested gendered ns of [Kra15] Ch 3 — i[+VAL], i[−VAL], u[+VAL], u[−VAL] — beside plain n with no feature.

• interp : Interpretability
• val : Gender.Signed

@[instance_reducible]

instance DistributedMorphology.instDecidableEqGenderFeature : DecidableEq GenderFeature

Equations

• DistributedMorphology.instDecidableEqGenderFeature = DistributedMorphology.instDecidableEqGenderFeature.decEq

def DistributedMorphology.instDecidableEqGenderFeature.decEq (x✝ x✝¹ : GenderFeature) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance DistributedMorphology.instReprGenderFeature : Repr GenderFeature

Equations

• DistributedMorphology.instReprGenderFeature = { reprPrec := DistributedMorphology.instReprGenderFeature.repr }

def DistributedMorphology.instReprGenderFeature.repr : GenderFeature → ℕ → Std.Format

Equations

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

def DistributedMorphology.GenderFeature.IsNatural (g : GenderFeature) : Prop

Whether a gender feature is interpretable (natural).

Equations

• g.IsNatural = (g.interp = DistributedMorphology.Interpretability.i)

@[instance_reducible]

instance DistributedMorphology.instDecidablePredGenderFeatureIsNatural : DecidablePred GenderFeature.IsNatural

Equations

• DistributedMorphology.instDecidablePredGenderFeatureIsNatural x✝ = DistributedMorphology.instDecidablePredGenderFeatureIsNatural._aux_1 x✝

def DistributedMorphology.GenderFeature.IsArbitrary (g : GenderFeature) : Prop

Whether a gender feature is uninterpretable (arbitrary).

Equations

• g.IsArbitrary = (g.interp = DistributedMorphology.Interpretability.u)

@[instance_reducible]

instance DistributedMorphology.instDecidablePredGenderFeatureIsArbitrary : DecidablePred GenderFeature.IsArbitrary

Equations

• DistributedMorphology.instDecidablePredGenderFeatureIsArbitrary x✝ = DistributedMorphology.instDecidablePredGenderFeatureIsArbitrary._aux_1 x✝

inductive DistributedMorphology.NumberOnN : Type

Number on the n head. Irregular plurals such as Amharic broken plurals are marked on n inside the categorization domain, while the regular plural -otʃtʃ realizes Num outside nP ([Kra15] §3.3, Ch 8).

• sg : NumberOnN
• pl : NumberOnN

@[instance_reducible]

instance DistributedMorphology.instDecidableEqNumberOnN : DecidableEq NumberOnN

Equations

• DistributedMorphology.instDecidableEqNumberOnN x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def DistributedMorphology.instReprNumberOnN.repr : NumberOnN → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance DistributedMorphology.instReprNumberOnN : Repr NumberOnN

Equations

• DistributedMorphology.instReprNumberOnN = { reprPrec := DistributedMorphology.instReprNumberOnN.repr }

structure DistributedMorphology.PhiBundle : Type

The phi-features a categorizing head hosts — gender and, for irregular nouns, number on n, while v and a carry none ([Kra15] Ch 3).

• gender : Option GenderFeature
• number : Option NumberOnN

def DistributedMorphology.instDecidableEqPhiBundle.decEq (x✝ x✝¹ : PhiBundle) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance DistributedMorphology.instDecidableEqPhiBundle : DecidableEq PhiBundle

Equations

• DistributedMorphology.instDecidableEqPhiBundle = DistributedMorphology.instDecidableEqPhiBundle.decEq

def DistributedMorphology.instReprPhiBundle.repr : PhiBundle → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance DistributedMorphology.instReprPhiBundle : Repr PhiBundle

Equations

• DistributedMorphology.instReprPhiBundle = { reprPrec := DistributedMorphology.instReprPhiBundle.repr }

@[instance_reducible]

instance DistributedMorphology.instInhabitedPhiBundle : Inhabited PhiBundle

Equations

• DistributedMorphology.instInhabitedPhiBundle = { default := { } }

structure DistributedMorphology.Categorizer.Head : Type

A categorizing head with its phi-features and the selectional feature {D}, which creates a specifier position for an iPossessor DP in Spec,nP ([Ada24], following [Myl16]'s convention). A functional morpheme is a feature bundle: Categorizer.Head is the head-leaf label of WordStructure Categorizer.Head, the φ-enriched instance of word-internal structure.

• categorizer : Categorizer

  The categorizer n, v, or a.

• phi : PhiBundle

  The gender and number content ([Kra15]).

• selectsD : Bool

  The selectional feature {D} licensing an iPossessor.

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

Equations

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

@[instance_reducible]

instance DistributedMorphology.Categorizer.instDecidableEqHead : DecidableEq Head

Equations

• DistributedMorphology.Categorizer.instDecidableEqHead = DistributedMorphology.Categorizer.instDecidableEqHead.decEq

@[instance_reducible]

instance DistributedMorphology.Categorizer.instReprHead : Repr Head

Equations

• DistributedMorphology.Categorizer.instReprHead = { reprPrec := DistributedMorphology.Categorizer.instReprHead.repr }

def DistributedMorphology.Categorizer.instReprHead.repr : Head → ℕ → Std.Format

Equations

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

def DistributedMorphology.Categorizer.Head.toCategory (ch : Head) : Minimalist.Cat

The syntactic category of a phi-enriched categorizer head.

Equations

• ch.toCategory = ch.categorizer.toCategory

def DistributedMorphology.Categorizer.Head.iPoss (phi : PhiBundle := { }) : Head

An iPossessable n head — {D} by construction, with the phi-bundle supplying any gender (Teop's body-part n carries u[+ANIM], Jarawara's is bare).

Equations

• DistributedMorphology.Categorizer.Head.iPoss phi = { categorizer := DistributedMorphology.Categorizer.n, phi := phi, selectsD := true }

theorem DistributedMorphology.Categorizer.Head.iPoss_selectsD (phi : PhiBundle) : (iPoss phi).selectsD = true

iPossessable n-heads always have selectsD = true, by construction.

The canonical head inventory ([Kra15] Ch 3)

FEM dimension: Amharic, Spanish, Romance ([Kra15] Chs 3, 6). ANIM: Teop, Algonquian, Lealao Chinantec (Chs 5–6; [Ada24] §3.1). MASC: Jarawara only ([Ada24] §3.2) — Maa's arbitrary masculine is negative-polarity FEM, not MASC.

def DistributedMorphology.Categorizer.Head.gendered (interp : Interpretability) (v : Gender.Signed) : Head

The gendered nominal categorizer: n bearing the valued feature v with interpretability interp.

Equations

• DistributedMorphology.Categorizer.Head.gendered interp v = { categorizer := DistributedMorphology.Categorizer.n, phi := { gender := some { interp := interp, val := v } } }

theorem DistributedMorphology.Categorizer.Head.gendered_inj {i₁ i₂ : Interpretability} {v₁ v₂ : Gender.Signed} : gendered i₁ v₁ = gendered i₂ v₂ ↔ i₁ = i₂ ∧ v₁ = v₂

Distinct feature content gives distinct heads — every pairwise contrast in the inventory below, in one statement.

def DistributedMorphology.Categorizer.Head.n_iFem : Head

The n bearing interpretable [+FEM] — female natural gender. In Amharic the female member of a same-root pair can carry the suffix -it ([Kra15] (10)).

Equations

• DistributedMorphology.Categorizer.Head.n_iFem = DistributedMorphology.Categorizer.Head.gendered DistributedMorphology.Interpretability.i { dim := Gender.Dimension.fem, pole := Gender.Pole.pos }

def DistributedMorphology.Categorizer.Head.n_iMasc : Head

The n bearing interpretable [−FEM] — male natural gender. The name gives the resulting gender: the feature is negative-polarity FEM, not the MASC dimension of Jarawara (n_uMasc).

Equations

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

def DistributedMorphology.Categorizer.Head.n_plain : Head

The plain n with no gender feature — the default nominal categorizer.

Equations

• DistributedMorphology.Categorizer.Head.n_plain = { categorizer := DistributedMorphology.Categorizer.n }

theorem DistributedMorphology.Categorizer.Head.gendered_ne_n_plain (interp : Interpretability) (v : Gender.Signed) : gendered interp v ≠ n_plain

A gendered head is never the plain n.

def DistributedMorphology.Categorizer.Head.n_uFem : Head

The n bearing uninterpretable [+FEM] — the arbitrary feminine of Set 1 languages (Amharic, Spanish), leaving masculine as the default. Amharic assigns it to a handful of inanimates such as car, earth, sun, and church ([Kra15] (9), Ch 6).

Equations

• DistributedMorphology.Categorizer.Head.n_uFem = DistributedMorphology.Categorizer.Head.gendered DistributedMorphology.Interpretability.u { dim := Gender.Dimension.fem, pole := Gender.Pole.pos }

def DistributedMorphology.Categorizer.Head.n_uNegFem : Head

The n bearing uninterpretable [−FEM] — the arbitrary masculine of Set 2, leaving feminine as the default (Maa, [Kra15] §6.3).

Equations

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

def DistributedMorphology.Categorizer.Head.n_iAnim : Head

The n bearing interpretable [+ANIM] — Teop gender I nouns, taking the article a.

Equations

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

def DistributedMorphology.Categorizer.Head.n_iInanim : Head

The n bearing interpretable [−ANIM] — Teop gender II nouns, taking the article o.

Equations

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

def DistributedMorphology.Categorizer.Head.n_uAnim : Head

The n bearing uninterpretable [+ANIM] — Teop's body-part n when iPossessed ([Ada24] §3.1).

Equations

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

def DistributedMorphology.Categorizer.Head.n_uMasc : Head

The n bearing uninterpretable [+MASC] — Jarawara's marked masculine, with feminine as the unmarked plain n. [Ada24] (58) also allows the interpretable variant, not modeled here.

Equations

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

def DistributedMorphology.Categorizer.Head.v_plain : Head

The verbal categorizer, with no phi-features.

Equations

• DistributedMorphology.Categorizer.Head.v_plain = { categorizer := DistributedMorphology.Categorizer.v }

def DistributedMorphology.Categorizer.Head.a_plain : Head

The adjectival categorizer, with no phi-features.

Equations

• DistributedMorphology.Categorizer.Head.a_plain = { categorizer := DistributedMorphology.Categorizer.a }

theorem DistributedMorphology.heads_roots_categorize_ofRoot (ch : Categorizer.Head) (r : Root) : heads (categorize ch (ofRoot r)) = {ch} ∧ roots (categorize ch (ofRoot r)) = {r}

In the categorization configuration [n √], all φ-content sits on the single head leaf and the single root leaf carries none: gender enters nominal structure only through n ([Kra15]).

Licensing Conditions ([Kra15] §3.4)

inductive DistributedMorphology.LicensingType : Type

How a root–n combination is licensed ([Kra15] §3.4.1). Semantic licensing restricts interpretation — the Encyclopedia entry is defined only under the matching n — while arbitrary licensing lists the root in a Vocabulary Item's context at PF.

• semantic : LicensingType
• arbitrary : LicensingType

@[instance_reducible]

instance DistributedMorphology.instDecidableEqLicensingType : DecidableEq LicensingType

Equations

• DistributedMorphology.instDecidableEqLicensingType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance DistributedMorphology.instReprLicensingType : Repr LicensingType

Equations

• DistributedMorphology.instReprLicensingType = { reprPrec := DistributedMorphology.instReprLicensingType.repr }

def DistributedMorphology.instReprLicensingType.repr : LicensingType → ℕ → Std.Format

Equations

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

def DistributedMorphology.Categorizer.Head.LicensesIntrusion (ch : Head) : Prop

The head licenses templatic [t]-intrusion: it is a nominal categorizer bearing a gender feature, whose exponent the bound root hosts ([Fau26] (11), [Low14]) — canonically Set 1 feminine, the Hebrew /t/ of taQTiL nouns and the Amharic /t/ of gerunds and infinitives. Verbal stems are blocked because gender is realized on the higher Agr head ([Kra20]).

Equations

• ch.LicensesIntrusion = (ch.categorizer = DistributedMorphology.Categorizer.n ∧ ch.phi.gender.isSome = true)

@[instance_reducible]

instance DistributedMorphology.instDecidablePredHeadLicensesIntrusion : DecidablePred Categorizer.Head.LicensesIntrusion

Equations

• DistributedMorphology.instDecidablePredHeadLicensesIntrusion x✝ = DistributedMorphology.instDecidablePredHeadLicensesIntrusion._aux_1 x✝

theorem DistributedMorphology.GenderFeature.isArbitrary_iff_not_isNatural (gf : GenderFeature) : gf.IsArbitrary ↔ ¬gf.IsNatural

Arbitrary gender is exactly the failure of natural gender: the two interpretability classes partition the features.

def DistributedMorphology.GenderFeature.licensingType : GenderFeature → LicensingType

Interpretable gender is semantically licensed and uninterpretable gender arbitrarily ([Kra15] §3.4.1).

Equations

• { interp := DistributedMorphology.Interpretability.i, val := val }.licensingType = DistributedMorphology.LicensingType.semantic
• { interp := DistributedMorphology.Interpretability.u, val := val }.licensingType = DistributedMorphology.LicensingType.arbitrary

@[simp]

theorem DistributedMorphology.GenderFeature.licensingType_i (v : Gender.Signed) : { interp := Interpretability.i, val := v }.licensingType = LicensingType.semantic

@[simp]

theorem DistributedMorphology.GenderFeature.licensingType_u (v : Gender.Signed) : { interp := Interpretability.u, val := v }.licensingType = LicensingType.arbitrary

The split-feature reading

DM's gender features are the non-hybrid fragment of the split-feature architecture of Features/Gender/Decomposition.lean: interpretable gender values both halves of a Gender.SplitFeature, uninterpretable gender only the morphological one. The FEM slice of the head inventory is [Kra15]'s calculus Gender.KramerN.

def DistributedMorphology.GenderFeature.toSplitFeature (gf : GenderFeature) : Gender.SplitFeature Gender.Signed

A DM gender feature as a split feature ([Smi15] via Gender.SplitFeature) — interpretable gender values both halves, uninterpretable gender only the morphological one.

Equations

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

def DistributedMorphology.PhiBundle.genderSplit (phi : PhiBundle) : Gender.SplitFeature Gender.Signed

The gender half of a phi-bundle as a split feature, absent for plain heads.

Equations

• phi.genderSplit = (Option.map DistributedMorphology.GenderFeature.toSplitFeature phi.gender).getD { uF := none, iF := none }

theorem DistributedMorphology.toSplitFeature_isNatural_iff (gf : GenderFeature) : gf.toSplitFeature.IsNatural ↔ gf.IsNatural

Natural gender in the DM sense is natural gender in the split-feature sense.

theorem DistributedMorphology.toSplitFeature_isArbitrary_iff (gf : GenderFeature) : gf.toSplitFeature.IsArbitrary ↔ gf.IsArbitrary

Arbitrary gender in the DM sense is arbitrary gender in the split-feature sense.

theorem DistributedMorphology.toSplitFeature_not_isHybrid (gf : GenderFeature) : ¬gf.toSplitFeature.IsHybrid

The DM calculus generates no hybrids — the mismatch zoo of [Smi15] lies outside it (cf. Gender.KramerN.toSplitFeature_not_isHybrid for the FEM slice).

theorem DistributedMorphology.genderSplit_isAbsent_iff (phi : PhiBundle) : phi.genderSplit.IsAbsent ↔ phi.gender = none

A phi-bundle's split feature is absent exactly when the head is plain.

def DistributedMorphology.Categorizer.Head.ofKramerN : Gender.KramerN → Head

[Kra15]'s FEM-dimension calculus embeds into the head inventory.

Equations

• DistributedMorphology.Categorizer.Head.ofKramerN Gender.KramerN.plain = DistributedMorphology.Categorizer.Head.n_plain
• DistributedMorphology.Categorizer.Head.ofKramerN Gender.KramerN.iFem = DistributedMorphology.Categorizer.Head.n_iFem
• DistributedMorphology.Categorizer.Head.ofKramerN Gender.KramerN.iMasc = DistributedMorphology.Categorizer.Head.n_iMasc
• DistributedMorphology.Categorizer.Head.ofKramerN Gender.KramerN.uFem = DistributedMorphology.Categorizer.Head.n_uFem
• DistributedMorphology.Categorizer.Head.ofKramerN Gender.KramerN.uMasc = DistributedMorphology.Categorizer.Head.n_uNegFem

DM Gender → Minimalist Feature System

def DistributedMorphology.GenderFeature.toPhiFeature (gf : GenderFeature) : Minimalist.PhiFeature

A DM gender feature as a Minimalist phi-feature.

Equations

• gf.toPhiFeature = Minimalist.PhiFeature.gender gf.val.toNat

def DistributedMorphology.GenderFeature.toGramFeature (gf : GenderFeature) : Minimalist.GramFeature

A DM gender feature as a grammatical feature — valued when interpretable, unvalued (a probe) when uninterpretable.

Equations

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

theorem DistributedMorphology.interpretable_gender_valued (gf : GenderFeature) (h : gf.interp = Interpretability.i) : gf.toGramFeature = Minimalist.GramFeature.valued (Minimalist.FeatureVal.phi (Minimalist.PhiFeature.gender gf.val.toNat))

Interpretable gender maps to a valued feature.

theorem DistributedMorphology.uninterpretable_gender_unvalued (gf : GenderFeature) (h : gf.interp = Interpretability.u) : gf.toGramFeature = Minimalist.GramFeature.unvalued (Minimalist.FeatureVal.phi (Minimalist.PhiFeature.gender gf.val.toNat))

Uninterpretable gender maps to an unvalued feature.

Vocabulary Insertion into a gender system

The bridge from features on n to a language's genders is Vocabulary Insertion into that language's own Gender.System — the carrier discipline of Features/Gender/Basic.lean. One map covers the attested patterns of [Kra15] Chs 5–7, which differ only in their system: the valued feature is realized by value, and a bare n falls back to the system's morphosyntactic default.

def DistributedMorphology.Categorizer.Head.realizeGender {G : Type u_1} (sys : Gender.System G) (value : Gender.Signed → G) (ch : Head) : G

Vocabulary Insertion of gender: realize the head's valued feature in the language's own system, falling back to the system's default.

Equations

• DistributedMorphology.Categorizer.Head.realizeGender sys value ch = (Option.map (fun (gf : DistributedMorphology.GenderFeature) => value gf.val) ch.phi.gender).getD sys.default

@[simp]

theorem DistributedMorphology.realizeGender_gendered {G : Type u_1} (sys : Gender.System G) (value : Gender.Signed → G) (interp : Interpretability) (v : Gender.Signed) : Categorizer.Head.realizeGender sys value (Categorizer.Head.gendered interp v) = value v

@[simp]

theorem DistributedMorphology.realizeGender_n_plain {G : Type u_1} (sys : Gender.System G) (value : Gender.Signed → G) : Categorizer.Head.realizeGender sys value Categorizer.Head.n_plain = sys.default

theorem DistributedMorphology.realizeGender_congr {G : Type u_1} (sys : Gender.System G) (value : Gender.Signed → G) {ch₁ ch₂ : Categorizer.Head} (h : Option.map (fun (x : GenderFeature) => x.val) ch₁.phi.gender = Option.map (fun (x : GenderFeature) => x.val) ch₂.phi.gender) : Categorizer.Head.realizeGender sys value ch₁ = Categorizer.Head.realizeGender sys value ch₂

PF is blind to interpretability: heads carrying the same valued feature realize alike, whatever their LF status — natural and arbitrary gender receive the same Vocabulary Item ([Kra15]).

theorem DistributedMorphology.realizeGender_ofKramerN {G : Type u_1} (sys : Gender.System G) (value : Gender.Signed → G) (k₁ k₂ : Gender.KramerN) (h : k₁.exponence = k₂.exponence) : Categorizer.Head.realizeGender sys value (Categorizer.Head.ofKramerN k₁) = Categorizer.Head.realizeGender sys value (Categorizer.Head.ofKramerN k₂)

Realization sees only what Gender.KramerN.exponence sees.

The attested realization patterns ([Kra15] Chs 5–7)

Each pattern is a constraint on the system's comparative labels: which label the valued feature realizes and which label the default carries. Set 1 and Set 2 share a feature inventory and differ only here.

def DistributedMorphology.IsSet1 {G : Type u_1} (sys : Gender.System G) (value : Gender.Signed → G) : Prop

A Set 1 system: [+FEM] realizes the feminine-labeled gender and the default is masculine-labeled (Amharic, Spanish; [Kra15] Ch 6).

Equations

• DistributedMorphology.IsSet1 sys value = (sys.label (value { dim := Gender.Dimension.fem, pole := Gender.Pole.pos }) = some Gender.feminine ∧ sys.label sys.default = some Gender.masculine)

def DistributedMorphology.IsSet2 {G : Type u_1} (sys : Gender.System G) (value : Gender.Signed → G) : Prop

A Set 2 system: [−FEM] realizes the masculine-labeled gender and the default is feminine-labeled (Maa; [Kra15] §6.3).

Equations

• DistributedMorphology.IsSet2 sys value = (sys.label (value { dim := Gender.Dimension.fem, pole := Gender.Pole.neg }) = some Gender.masculine ∧ sys.label sys.default = some Gender.feminine)

def DistributedMorphology.IsThreeGender {G : Type u_1} (sys : Gender.System G) (value : Gender.Signed → G) : Prop

A three-gender system: both FEM poles are realized and the default is neuter-labeled (Mangarayi; [Kra15] §7.2 — the other Ch 7 case studies add uninterpretable features to this inventory).

Equations

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

def DistributedMorphology.IsAnimacyBased {G : Type u_1} (sys : Gender.System G) (value : Gender.Signed → G) : Prop

An animacy system: [+ANIM] realizes the animate-labeled gender and the default is inanimate-labeled (Lealao Chinantec, [Kra15] §5.3; Algonquian, §6.4; Teop, [Ada24]).

Equations

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

theorem DistributedMorphology.not_isSet1_and_isSet2 {G : Type u_1} (sys : Gender.System G) (value : Gender.Signed → G) : ¬(IsSet1 sys value ∧ IsSet2 sys value)

The Set 1 vs Set 2 parameter is exclusive: their defaults carry different labels.

theorem DistributedMorphology.IsSet1.realize_labels {G : Type u_1} {sys : Gender.System G} {value : Gender.Signed → G} (h : IsSet1 sys value) : sys.label (Categorizer.Head.realizeGender sys value Categorizer.Head.n_uFem) = some Gender.feminine ∧ sys.label (Categorizer.Head.realizeGender sys value Categorizer.Head.n_plain) = some Gender.masculine

In a Set 1 system, arbitrary-feminine n realizes the feminine-labeled gender and plain n the masculine-labeled default.

theorem DistributedMorphology.IsSet2.realize_labels {G : Type u_1} {sys : Gender.System G} {value : Gender.Signed → G} (h : IsSet2 sys value) : sys.label (Categorizer.Head.realizeGender sys value Categorizer.Head.n_uNegFem) = some Gender.masculine ∧ sys.label (Categorizer.Head.realizeGender sys value Categorizer.Head.n_plain) = some Gender.feminine

In a Set 2 system, arbitrary-masculine n realizes the masculine-labeled gender and plain n the feminine-labeled default.

Discourse-level gender

def DistributedMorphology.Categorizer.Head.genderInfo {G : Type u_1} (sys : Gender.System G) (value : Gender.Signed → G) (ch : Head) : GenderInfo

The discourse-level gender information a head determines: the comparative label of its realized gender, unspecified where the system leaves the class unlabeled.

Equations

• DistributedMorphology.Categorizer.Head.genderInfo sys value ch = (sys.label (DistributedMorphology.Categorizer.Head.realizeGender sys value ch)).elim GenderInfo.unspecified GenderInfo.known

theorem DistributedMorphology.genderInfo_known {G : Type u_1} (sys : Gender.System G) (value : Gender.Signed → G) (hlab : ∀ (g : G), (sys.label g).isSome = true) (ch : Categorizer.Head) : ∃ (g : Gender), Categorizer.Head.genderInfo sys value ch = GenderInfo.known g

In a fully labeled system the grammar always determines a concrete discourse gender: underspecification ([Arn26]) arises from the discourse, not from a resolved morphosyntax.