Feature decomposition of gender

This file defines the bivalent features [±feminine] and [±neuter] of a sex-based three-gender system. Neuter is the most specified gender and masculine the least, as in the person and number presentations.

Main definitions

• Gender.Features: the bivalent [±feminine, ±neuter] features as finsets over the chain feminine < neuter, whose well-formed cells are Features.neuter, Features.feminine and Features.masculine.

Implementation notes

• The bivalent presentation's three-cell bound Features.card_wellFormed is a claim about the presentation and not about gender systems: Fula has twenty controller genders.
• Smith's dual-feature system is Minimalist.Coordination.Bundle, and Kramer's gender features on the nominal categorizer are in Morphology/DistributedMorphology/Gender.lean.
• Hammerly's rejection of the presentation, with masculine a bare gender node and natural gender derived at LF, is a single-paper analysis for its study.

References

• [Sau03] — the markedness ordering the bivalent presentation reconstructs
• [Sau08b] — the Dominance test for markedness
• [Ham19]

The bivalent presentation: [±feminine, ±neuter]

[Sau03] derives Czech gender agreement under coordination from a markedness ordering on which masculine is semantically vacuous, feminine presupposes non-masculinity and neuter presupposes genderlessness (§6, (45)); [Sau08b]'s Dominance test, the gender a mixed coordination takes, likewise makes masculine less marked than feminine (pp. 63–65). The presentation here reconstructs the ordering as two binary features with the containment [+neuter] → [+feminine], so the three genders of a sex-based system are the initial segments of the chain feminine < neuter, neuter the most specified and masculine the least, as for person and number (Person.Features, Number.Features).

inductive Gender.Feature : Type

The two gender features, neuter depending on feminine.

• feminine : Feature

  [feminine] holds of non-masculine referents, those feminine and neuter share.

• neuter : Feature

  [neuter] holds of referents triggering neuter agreement.

@[instance_reducible]

instance Gender.instDecidableEqFeature : DecidableEq Feature

Equations

• Gender.instDecidableEqFeature x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Gender.instReprFeature.repr : Feature → ℕ → Std.Format

Equations

• Gender.instReprFeature.repr Gender.Feature.feminine prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Gender.Feature.feminine")).group prec✝
• Gender.instReprFeature.repr Gender.Feature.neuter prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Gender.Feature.neuter")).group prec✝

@[instance_reducible]

instance Gender.instReprFeature : Repr Feature

Equations

• Gender.instReprFeature = { reprPrec := Gender.instReprFeature.repr }

@[instance_reducible]

instance Gender.instFintypeFeature : Fintype Feature

Equations

• Gender.instFintypeFeature = { elems := { val := ↑Gender.Feature.enumList, nodup := Gender.Feature.enumList_nodup }, complete := Gender.instFintypeFeature._proof_1 }

def Gender.Feature.rank : Feature → Fin 2

Feature.rank places feminine below neuter on the dependency chain.

Equations

• Gender.Feature.feminine.rank = 0
• Gender.Feature.neuter.rank = 1

@[instance_reducible]

instance Gender.instLinearOrderFeature : LinearOrder Feature

Equations

• Gender.instLinearOrderFeature = LinearOrder.lift' Gender.Feature.rank Gender.instLinearOrderFeature._proof_1

@[instance_reducible]

instance Gender.instLocallyFiniteOrderBotFeature : LocallyFiniteOrderBot Feature

Equations

• Gender.instLocallyFiniteOrderBotFeature = Fintype.toLocallyFiniteOrderBot

@[reducible, inline]

abbrev Gender.Features : Type

A gender feature bundle is the set of its positive features.

Equations

• Gender.Features = Finset Gender.Feature

def Gender.Features.neuter : Features

The neuter is [+feminine, +neuter], the whole chain.

Equations

• Gender.Features.neuter = Finset.Iic Gender.Feature.neuter

def Gender.Features.feminine : Features

The feminine is [+feminine, −neuter], the chain below neuter.

Equations

• Gender.Features.feminine = Finset.Iic Gender.Feature.feminine

def Gender.Features.masculine : Features

The masculine is [−feminine, −neuter], the empty bundle.

Equations

• Gender.Features.masculine = ∅

theorem Gender.Features.neuter_eq : neuter = {Feature.feminine, Feature.neuter}

theorem Gender.Features.feminine_eq : feminine = {Feature.feminine}

theorem Gender.Features.not_wellFormed_singleton_neuter : ¬IsLowerSet ↑{Feature.neuter}

The bundle with the neuter feature alone violates containment.

theorem Gender.Features.card_wellFormed : Fintype.card { gf : Features // IsLowerSet ↑gf } = 3

Exactly three bundles pass the containment filter, the three genders. The bound is a claim about the presentation and not about gender systems.

def Gender.Features.toGender (f : Features) : Option Gender

Map gender features to the comparative labels.

Equations

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

def Gender.Features.fromGender : Gender → Option Features

Map comparative labels to gender features (partial — only sex-based labels have feature equivalents).

Equations

• Gender.Features.fromGender Gender.neuter = some Gender.Features.neuter
• Gender.Features.fromGender Gender.feminine = some Gender.Features.feminine
• Gender.Features.fromGender Gender.masculine = some Gender.Features.masculine
• Gender.Features.fromGender x✝ = none

theorem Gender.Features.fromGender_toGender {f : Features} (h : IsLowerSet ↑f) : f.toGender.bind fromGender = some f

A bundle passing the containment filter survives the round trip through its label.