@cite{konnelly-cowper-2020}

Konnelly, Lex and Elizabeth Cowper. 2020. Gender diversity and morphosyntax: An account of singular they. Glossa: a journal of general linguistics 5(1): 40. 1--19. DOI: https://doi.org/10.5334/gjgl.1000

Core Contribution

Variation in acceptance of singular they reflects speakers' position in a grammatical change in progress. The change has three stages, differing only in the contrastivity status of [MASC] and [FEM] on the gender features of the pronoun system. The pronoun Vocabulary Items themselves are constant across all three stages; what changes is which feature bundles nouns and names project.

Stage	[MASC]/[FEM] status	Singular they distribution
1	Contrastive	Quantified/generic epicene only
2	Contrastive, fewer nouns	Extends to ungendered names
3	Non-contrastive modifiers	Default for all singular animate

The key theorem: the VIs are constant across stages. At Stage 3, [MASC]/[FEM] are optional modifiers (non-contrastive in the sense of @cite{wiltschko-2008}), so their absence is the norm, and the Elsewhere Condition yields they as the default singular animate pronoun.

Connection to @cite{arnold-2026}

Arnold's pragmatic account (underspecified vs. personal singular they) complements K&C's grammatical account. At Stage 1, underspecified they is licensed only when discourse elaboration is thin (quantified/generic antecedents). At Stage 3, they is the grammatical default for any singular animate referent regardless of discourse elaboration, because the grammar itself no longer requires a contrastive gender feature.

Formalization

We define the pronoun VI rules using FeatureVI from Morphology.DM.VocabularyInsertion, parameterize the three stages via Contrastivity from Morphology.DM.Categorizer, and prove bridge theorems connecting to Arnold's discourse conditions.

inductive KonnellyCowper2020.PronFeature : Type

The morphosyntactic features relevant to English 3rd-person pronoun spellout (K&C §4, (11a--d)).

K&C place [MASC] and [FEM] on the φ head above Number (following @cite{kramer-2009}; @cite{kramer-2015}), [SG] on Num, and [INANIM] on n. For VI purposes, only the feature bundle at the pronoun terminal matters, not where in the tree it originates.

• sg : PronFeature
• masc : PronFeature
• fem : PronFeature
• inanim : PronFeature

@[implicit_reducible]

instance KonnellyCowper2020.instDecidableEqPronFeature : DecidableEq PronFeature

Equations

• KonnellyCowper2020.instDecidableEqPronFeature x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance KonnellyCowper2020.instReprPronFeature : Repr PronFeature

Equations

• KonnellyCowper2020.instReprPronFeature = { reprPrec := KonnellyCowper2020.instReprPronFeature.repr }

def KonnellyCowper2020.instReprPronFeature.repr : PronFeature → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance KonnellyCowper2020.instBEqPronFeature : BEq PronFeature

Equations

• KonnellyCowper2020.instBEqPronFeature = { beq := KonnellyCowper2020.instBEqPronFeature.beq }

def KonnellyCowper2020.instBEqPronFeature.beq : PronFeature → PronFeature → Bool

Equations

• KonnellyCowper2020.instBEqPronFeature.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def KonnellyCowper2020.vi_she : Morphology.DM.VI.FeatureVI PronFeature String

The four English 3rd-person pronoun VIs.

These are constant across all three stages — the change from Stage 1 to Stage 3 is in which feature bundles nouns project, not in the VI rules themselves.

(11) a. [SG] [FEM] ↔ she b. [SG] [MASC] ↔ he c. [SG, INANIM] ↔ it d. Elsewhere ↔ they

Equations

• KonnellyCowper2020.vi_she = { features := [KonnellyCowper2020.PronFeature.sg, KonnellyCowper2020.PronFeature.fem], exponent := "she" }

def KonnellyCowper2020.vi_he : Morphology.DM.VI.FeatureVI PronFeature String

Equations

• KonnellyCowper2020.vi_he = { features := [KonnellyCowper2020.PronFeature.sg, KonnellyCowper2020.PronFeature.masc], exponent := "he" }

def KonnellyCowper2020.vi_it : Morphology.DM.VI.FeatureVI PronFeature String

Equations

• KonnellyCowper2020.vi_it = { features := [KonnellyCowper2020.PronFeature.sg, KonnellyCowper2020.PronFeature.inanim], exponent := "it" }

def KonnellyCowper2020.vi_they : Morphology.DM.VI.FeatureVI PronFeature String

Equations

• KonnellyCowper2020.vi_they = { features := [], exponent := "they" }

def KonnellyCowper2020.pronounVIs : List (Morphology.DM.VI.FeatureVI PronFeature String)

The complete VI rule set for English 3rd-person pronouns. Order does not matter — the Subset Principle selects by specificity (feature-list length).

Equations

• KonnellyCowper2020.pronounVIs = [KonnellyCowper2020.vi_she, KonnellyCowper2020.vi_he, KonnellyCowper2020.vi_it, KonnellyCowper2020.vi_they]

theorem KonnellyCowper2020.plural_yields_they : Morphology.DM.VI.subsetPrinciple pronounVIs [] = some "they"

A plural bundle (no [SG]) → they (elsewhere).

theorem KonnellyCowper2020.masc_fem_overlap_resolves : (Morphology.DM.VI.subsetPrinciple pronounVIs [PronFeature.sg, PronFeature.masc, PronFeature.fem]).isSome = true

A singular bundle with both [MASC] and [FEM] → the VI system is well-defined even for this impossible configuration (no nominal bears both features). FEM wins by being listed first among equal-length matches.

inductive KonnellyCowper2020.Stage : Type

The three stages of grammatical change for singular they (K&C §4).

The stages differ only in the contrastivity status of [MASC] and [FEM]. The pronoun VIs (§2) are constant across stages.

• stage1 : Stage

  Stage 1 (pre-modern / conservative): [MASC] and [FEM] are fully contrastive. Absence of a gender feature on a singular animate nominal is possible only when the referent's gender is unknown (quantified/generic contexts).

• stage2 : Stage

  Stage 2 (innovative / current): [MASC] and [FEM] remain contrastive, but the inventory of nouns that obligatorily bear them shrinks. Ungendered proper names (Kelly, Morgan) may lack a gender feature even for referents of known gender.

• stage3 : Stage

  Stage 3 (most innovative): [MASC] and [FEM] become optional, non-contrastive modifiers. Their absence carries no semantic content — they is the default for any singular animate.

@[implicit_reducible]

instance KonnellyCowper2020.instDecidableEqStage : DecidableEq Stage

Equations

• KonnellyCowper2020.instDecidableEqStage x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def KonnellyCowper2020.instReprStage.repr : Stage → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance KonnellyCowper2020.instReprStage : Repr Stage

Equations

• KonnellyCowper2020.instReprStage = { reprPrec := KonnellyCowper2020.instReprStage.repr }

def KonnellyCowper2020.instBEqStage.beq : Stage → Stage → Bool

Equations

• KonnellyCowper2020.instBEqStage.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

@[implicit_reducible]

instance KonnellyCowper2020.instBEqStage : BEq Stage

Equations

• KonnellyCowper2020.instBEqStage = { beq := KonnellyCowper2020.instBEqStage.beq }

def KonnellyCowper2020.Stage.genderContrastivity : Stage → Morphology.DM.Contrastivity

The contrastivity status of [MASC]/[FEM] at each stage.

Equations

• KonnellyCowper2020.Stage.stage1.genderContrastivity = Morphology.DM.Contrastivity.contrastive
• KonnellyCowper2020.Stage.stage2.genderContrastivity = Morphology.DM.Contrastivity.contrastive
• KonnellyCowper2020.Stage.stage3.genderContrastivity = Morphology.DM.Contrastivity.nonContrastive

theorem KonnellyCowper2020.stage1_stage2_same_contrastivity : Stage.stage1.genderContrastivity = Stage.stage2.genderContrastivity

Stages 1 and 2 share contrastive gender features — they differ only in the inventory of nouns carrying them, not in the feature system itself.

theorem KonnellyCowper2020.stage1_stage3_different_contrastivity : Stage.stage1.genderContrastivity ≠ Stage.stage3.genderContrastivity

The Stage 1→3 transition is a change in the feature system itself (contrastive → non-contrastive), not just in lexical inventory.

def KonnellyCowper2020.Stage.genderObligatory : Stage → Bool

Whether a contrastive gender feature must be present on a singular animate nominal of known binary gender, at a given stage.

At Stage 1: always (contrastive features are obligatory for known gender). At Stage 2: depends on the noun (not modeled here — lexical variation). At Stage 3: never obligatory (non-contrastive = optional).

Equations

• KonnellyCowper2020.Stage.stage1.genderObligatory = true
• KonnellyCowper2020.Stage.stage2.genderObligatory = true
• KonnellyCowper2020.Stage.stage3.genderObligatory = false

theorem KonnellyCowper2020.genderObligatory_from_contrastivity (s : Stage) : s.genderObligatory = s.genderContrastivity.obligatory

Gender obligatoriness is DERIVED from the contrastivity status of [MASC]/[FEM], not stipulated independently. Contrastive features are obligatory (absence = ¬F); non-contrastive features are optional (absence = vacuous). This is the formal content of K&C's claim that the three stages differ only in feature system properties.

def KonnellyCowper2020.ungenderedBundle : List PronFeature

The feature bundle projected by a singular animate nominal with no gender specification — the critical case for singular they.

At all stages, this bundle is just [SG], with no [MASC], [FEM], or [INANIM]. The Elsewhere Condition yields they.

Equations

• KonnellyCowper2020.ungenderedBundle = [KonnellyCowper2020.PronFeature.sg]

def KonnellyCowper2020.feminineBundle : List PronFeature

The feature bundle projected by a singular animate feminine nominal.

Equations

• KonnellyCowper2020.feminineBundle = [KonnellyCowper2020.PronFeature.sg, KonnellyCowper2020.PronFeature.fem]

def KonnellyCowper2020.masculineBundle : List PronFeature

The feature bundle projected by a singular animate masculine nominal.

Equations

• KonnellyCowper2020.masculineBundle = [KonnellyCowper2020.PronFeature.sg, KonnellyCowper2020.PronFeature.masc]

def KonnellyCowper2020.inanimateBundle : List PronFeature

The feature bundle projected by a singular inanimate nominal.

Equations

• KonnellyCowper2020.inanimateBundle = [KonnellyCowper2020.PronFeature.sg, KonnellyCowper2020.PronFeature.inanim]

inductive KonnellyCowper2020.ReferentContext : Type

Classification of pronoun–antecedent configurations that differ in whether [MASC]/[FEM] is obligatorily projected at a given stage.

K&C §4.1: the three stages are distinguished by which referent contexts obligatorily project gender features.

• (12): "Every student brought {his/their} lunch" — quantifier-bound, gender optional at all stages.
• (13a): "Jess₁ said he₁ couldn't make it" — referential with known gendered name, gender obligatory at Stages 1--2.
• (13b): "Jess₁ said they₁ couldn't make it" — rejected at Stage 1 for a known-gender referent.
• Stage 2 innovation: ungendered proper names (Kelly, Morgan, Pat) may lack gender features even though the referent's gender is known.

• referentialKnownGender : ReferentContext

  Referential pronoun with a known-gender antecedent (e.g., "Jess said he couldn't make it").

• referentialUnknownGender : ReferentContext

  Referential pronoun with a gender-unknown/irrelevant antecedent (e.g., "the student said they would be late").

• quantifierBound : ReferentContext

  Quantifier-bound / generic pronoun (e.g., "every student brought their lunch").

• ungenderedProperName : ReferentContext

  Referential pronoun with an ungendered proper name antecedent (e.g., "Kelly said they would be late").

@[implicit_reducible]

instance KonnellyCowper2020.instDecidableEqReferentContext : DecidableEq ReferentContext

Equations

• KonnellyCowper2020.instDecidableEqReferentContext x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def KonnellyCowper2020.instReprReferentContext.repr : ReferentContext → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance KonnellyCowper2020.instReprReferentContext : Repr ReferentContext

Equations

• KonnellyCowper2020.instReprReferentContext = { reprPrec := KonnellyCowper2020.instReprReferentContext.repr }

def KonnellyCowper2020.instBEqReferentContext.beq : ReferentContext → ReferentContext → Bool

Equations

• KonnellyCowper2020.instBEqReferentContext.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

@[implicit_reducible]

instance KonnellyCowper2020.instBEqReferentContext : BEq ReferentContext

Equations

• KonnellyCowper2020.instBEqReferentContext = { beq := KonnellyCowper2020.instBEqReferentContext.beq }

def KonnellyCowper2020.genderObligatoryFor : ReferentContext → Stage → Bool

Whether [MASC]/[FEM] is obligatorily projected for a given referent context at a given stage.

This captures the full empirical landscape of K&C §4:

• Gender-unknown referents never project [MASC]/[FEM] (at any stage).
• Quantifier-bound pronouns optionally lack [MASC]/[FEM] at all stages.
• Known-gender referential pronouns require [MASC]/[FEM] at Stages 1--2.
• Ungendered names require [MASC]/[FEM] at Stage 1 but not Stage 2.
• At Stage 3, nothing is obligatory (non-contrastive).

Equations

• KonnellyCowper2020.genderObligatoryFor KonnellyCowper2020.ReferentContext.referentialUnknownGender x✝ = false
• KonnellyCowper2020.genderObligatoryFor KonnellyCowper2020.ReferentContext.quantifierBound x✝ = false
• KonnellyCowper2020.genderObligatoryFor KonnellyCowper2020.ReferentContext.referentialKnownGender KonnellyCowper2020.Stage.stage1 = true
• KonnellyCowper2020.genderObligatoryFor KonnellyCowper2020.ReferentContext.referentialKnownGender KonnellyCowper2020.Stage.stage2 = true
• KonnellyCowper2020.genderObligatoryFor KonnellyCowper2020.ReferentContext.referentialKnownGender KonnellyCowper2020.Stage.stage3 = false
• KonnellyCowper2020.genderObligatoryFor KonnellyCowper2020.ReferentContext.ungenderedProperName KonnellyCowper2020.Stage.stage1 = true
• KonnellyCowper2020.genderObligatoryFor KonnellyCowper2020.ReferentContext.ungenderedProperName KonnellyCowper2020.Stage.stage2 = false
• KonnellyCowper2020.genderObligatoryFor KonnellyCowper2020.ReferentContext.ungenderedProperName KonnellyCowper2020.Stage.stage3 = false

theorem KonnellyCowper2020.stage1_bound_variable_they : genderObligatoryFor ReferentContext.quantifierBound Stage.stage1 = false ∧ Morphology.DM.VI.subsetPrinciple pronounVIs ungenderedBundle = some "they"

K&C (12): At Stage 1, quantifier-bound pronouns can be they because [MASC]/[FEM] is optional in bound variable contexts. "Every student brought their lunch" is acceptable at Stage 1.

theorem KonnellyCowper2020.stage1_referential_requires_gender : genderObligatoryFor ReferentContext.referentialKnownGender Stage.stage1 = true

K&C (13): At Stage 1, referential pronouns with known-gender antecedents MUST project [MASC]/[FEM] — singular they is not available for a referent of known gender. "Jess₁ said they₁ couldn't make it" is rejected at Stage 1 (for a known-gender Jess).

theorem KonnellyCowper2020.stage2_ungendered_names : genderObligatoryFor ReferentContext.ungenderedProperName Stage.stage2 = false ∧ genderObligatoryFor ReferentContext.ungenderedProperName Stage.stage1 = true

The Stage 2 innovation: ungendered proper names (Kelly, Morgan, Pat) may lack [MASC]/[FEM] even though the referent's gender is known. This extends singular they beyond quantifier-bound contexts.

theorem KonnellyCowper2020.stage3_nothing_obligatory (ctx : ReferentContext) : genderObligatoryFor ctx Stage.stage3 = false

At Stage 3, no referent context obligatorily projects [MASC]/[FEM]. Singular they is available for all singular animate referents.

theorem KonnellyCowper2020.ungendered_always_they : Morphology.DM.VI.subsetPrinciple pronounVIs ungenderedBundle = some "they"

At all stages, ungendered singular animates get they. The stages differ only in how many nominals project ungendered bundles, not in what VI does with such a bundle.

theorem KonnellyCowper2020.feminine_always_she : Morphology.DM.VI.subsetPrinciple pronounVIs feminineBundle = some "she"

At all stages, feminine bundles still get she. Stage 3 speakers still have he/she available when the non-contrastive gender modifier is present.

theorem KonnellyCowper2020.masculine_always_he : Morphology.DM.VI.subsetPrinciple pronounVIs masculineBundle = some "he"

At all stages, masculine bundles still get he.

theorem KonnellyCowper2020.inanimate_always_it : Morphology.DM.VI.subsetPrinciple pronounVIs inanimateBundle = some "it"

At all stages, inanimate bundles still get it. The inanimate feature [INANIM] is not affected by the contrastivity change — it remains contrastive at all stages.

theorem KonnellyCowper2020.stage3_they_unrestricted : Stage.stage3.genderObligatory = false ∧ Morphology.DM.VI.subsetPrinciple pronounVIs ungenderedBundle = some "they"

At Stage 3, non-contrastive [MASC]/[FEM] means gender features are optional. For any singular animate referent — regardless of known gender — a speaker may omit the gender modifier, yielding they. This is the core K&C prediction: at Stage 3, singular they is unrestricted for animate referents.

theorem KonnellyCowper2020.stage1_they_restricted : Stage.stage1.genderObligatory = true ∧ Morphology.DM.VI.subsetPrinciple pronounVIs ungenderedBundle = some "they"

At Stage 1, gender features are obligatory for known-gender referents. Singular they arises only when gender is genuinely unknown.

theorem KonnellyCowper2020.stage1_aligns_with_underspecified_they : Arnold2026.licensesUnderspecified Features.DiscourseElaboration.underspecified = true ∧ Stage.stage1.genderObligatory = true

At Stage 1, singular they is restricted to contexts where discourse elaboration is underspecified — the grammatical obligation to project [MASC]/[FEM] for known-gender referents means they arises only when gender is unknown, which correlates with thin discourse models.

theorem KonnellyCowper2020.stage3_independent_of_discourse : Stage.stage3.genderObligatory = false

At Stage 3, singular they is the grammatical default — it does not require underspecified discourse elaboration. Arnold's personal they (elaborated discourse, known they/them pronouns) is naturally accommodated: the grammar produces they regardless of discourse state.

def KonnellyCowper2020.catHeadToPronFeatures (ch : Morphology.DM.CatHead) : List PronFeature

Project a DM n-head's phi-features into K&C's flat pronoun VI feature system.

This bridges @cite{kramer-2015}'s structured features on n (GenderFeature with dimension, polarity, interpretability) to K&C's flat feature system for VI competition.

The mapping for English (FEM dimension):

• i[+FEM] on n → [FEM] (K&C's feature that yields "she")
• i[−FEM] on n → [MASC] (K&C's feature that yields "he")
• i[−ANIM] on n → [INANIM] (yields "it")
• no gender on n → ∅ (elsewhere, yields "they")

Note: K&C adopt @cite{harley-ritter-2002}'s feature geometry with independent [MASC] and [FEM], while @cite{kramer-2015} uses [±FEM] with polarity. For English pronoun VI, these are equivalent: K&C's [FEM] = Kramer's [+FEM], K&C's [MASC] = Kramer's [−FEM].

Equations

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

theorem KonnellyCowper2020.iFem_singular_yields_she : Morphology.DM.VI.subsetPrinciple pronounVIs ([PronFeature.sg] ++ catHeadToPronFeatures Morphology.DM.CatHead.n_iFem) = some "she"

The end-to-end pipeline: DM n-head → projected features → VI → "she". A singular nominal categorized by n i[+FEM] gets "she" via the Elsewhere Condition.

theorem KonnellyCowper2020.iMasc_singular_yields_he : Morphology.DM.VI.subsetPrinciple pronounVIs ([PronFeature.sg] ++ catHeadToPronFeatures Morphology.DM.CatHead.n_iMasc) = some "he"

n i[−FEM] (masculine natural gender) → "he".

theorem KonnellyCowper2020.iInanim_singular_yields_it : Morphology.DM.VI.subsetPrinciple pronounVIs ([PronFeature.sg] ++ catHeadToPronFeatures Morphology.DM.CatHead.n_iInanim) = some "it"

n i[−ANIM] (inanimate) → "it".

theorem KonnellyCowper2020.plain_n_singular_yields_they : Morphology.DM.VI.subsetPrinciple pronounVIs ([PronFeature.sg] ++ catHeadToPronFeatures Morphology.DM.CatHead.n_plain) = some "they"

Plain n (no gender feature) → "they" (elsewhere). This is the structural correlate of K&C's core claim: they is what VI produces when the n-head lacks a gender feature.

structure KonnellyCowper2020.PronDP : Type

K&C's (14): the nominal structure relevant to pronoun feature projection.

DP
├── D (determiner/quantifier)
└── NumP
    ├── Num [SG]
    └── nP
        ├── n [gender, animacy]
        └── NP (root)

Features are distributed across heads: [SG] on Num, [MASC]/[FEM] on the φ head (which K&C identify with the n domain following @cite{kramer-2009}; @cite{kramer-2015}), and [INANIM] on n.

The DP is the maximal projection of the nominal extended projection n (F1) → Num (F3) → D (F4), a well-formed subsequence of @cite{borer-2005}'s full nominal spine N → n → Q → Num → D.

• nHead : Morphology.DM.CatHead

  The categorizing head n, bearing gender and animacy features.

• singular : Bool

  Whether the Num head bears [SG] (singular number).

• isQuantifier : Bool

  Whether D hosts a quantifier (relevant for bound-variable pronouns at Stage 1, where [MASC]/[FEM] are optional for quantifier-bound DPs).

def KonnellyCowper2020.instDecidableEqPronDP.decEq (x✝ x✝¹ : PronDP) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance KonnellyCowper2020.instDecidableEqPronDP : DecidableEq PronDP

Equations

• KonnellyCowper2020.instDecidableEqPronDP = KonnellyCowper2020.instDecidableEqPronDP.decEq

def KonnellyCowper2020.instReprPronDP.repr : PronDP → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance KonnellyCowper2020.instReprPronDP : Repr PronDP

Equations

• KonnellyCowper2020.instReprPronDP = { reprPrec := KonnellyCowper2020.instReprPronDP.repr }

def KonnellyCowper2020.PronDP.toPronBundle (ns : PronDP) : List PronFeature

Project the flat feature bundle for VI competition from the DP structure.

This composes features from their structural positions in K&C's (14):

• [SG] comes from the Num head
• Gender features ([MASC], [FEM]) come from n (via catHeadToPronFeatures)
• [INANIM] comes from n (also via catHeadToPronFeatures)

The resulting list is what the Subset Principle operates over.

Equations

• ns.toPronBundle = (if ns.singular = true then [KonnellyCowper2020.PronFeature.sg] else []) ++ KonnellyCowper2020.catHeadToPronFeatures ns.nHead

def KonnellyCowper2020.PronDP.spellout (ns : PronDP) : Option String

Spell out the pronoun for a nominal structure via VI competition.

This is the complete pipeline: DP structure → feature projection → Subset Principle → phonological exponent.

Equations

• ns.spellout = Morphology.DM.VI.subsetPrinciple KonnellyCowper2020.pronounVIs ns.toPronBundle

theorem KonnellyCowper2020.singular_feminine_spellout : { nHead := Morphology.DM.CatHead.n_iFem, singular := true }.spellout = some "she"

A singular feminine nominal (n i[+FEM], Num [SG]) → "she".

theorem KonnellyCowper2020.singular_masculine_spellout : { nHead := Morphology.DM.CatHead.n_iMasc, singular := true }.spellout = some "he"

A singular masculine nominal (n i[−FEM], Num [SG]) → "he".

theorem KonnellyCowper2020.singular_inanimate_spellout : { nHead := Morphology.DM.CatHead.n_iInanim, singular := true }.spellout = some "it"

A singular inanimate nominal (n i[−ANIM], Num [SG]) → "it".

theorem KonnellyCowper2020.singular_ungendered_spellout : { nHead := Morphology.DM.CatHead.n_plain, singular := true }.spellout = some "they"

A singular nominal with plain n (no gender, Num [SG]) → "they". The DP structure DETERMINES the elsewhere outcome — plain n projects no gender feature, so the Subset Principle selects the elsewhere VI.

theorem KonnellyCowper2020.plural_spellout : { nHead := Morphology.DM.CatHead.n_plain, singular := false }.spellout = some "they"

A plural nominal (no [SG]) → "they" (elsewhere).

theorem KonnellyCowper2020.quantifier_bound_spellout : { nHead := Morphology.DM.CatHead.n_plain, singular := true, isQuantifier := true }.spellout = some "they"

A quantifier-bound singular nominal with plain n → "they". The isQuantifier flag records the D-head status but does not affect VI: feature projection reads n and Num, not D content.

theorem KonnellyCowper2020.kc14_spine_consistent : Minimalist.allCategoryConsistent [Minimalist.Cat.n, Minimalist.Cat.Num, Minimalist.Cat.D] = true

K&C's (14) spine [n, Num, D] is a well-formed nominal extended projection: all heads share [-V, +N] features (category consistency).

theorem KonnellyCowper2020.kc14_spine_monotone : Minimalist.allFMonotone [Minimalist.Cat.n, Minimalist.Cat.Num, Minimalist.Cat.D] = true

K&C's (14) spine [n, Num, D] has monotonically increasing F-values: n (F1) ≤ Num (F3) ≤ D (F4). The gap between n (F1) and Num (F3) reflects K&C's omission of the Q (classifier) layer, which sits at F2 in @cite{borer-2005}'s full nominal spine.

theorem KonnellyCowper2020.kc14_fvalues_strict : Minimalist.fValue Minimalist.Cat.n < Minimalist.fValue Minimalist.Cat.Num ∧ Minimalist.fValue Minimalist.Cat.Num < Minimalist.fValue Minimalist.Cat.D

The F-values of K&C's (14) are strictly increasing: n (F1 = 1) < Num (F3 = 3) < D (F4 = 4).

theorem KonnellyCowper2020.kc14_spine_nominal : Minimalist.catFamily Minimalist.Cat.n = Minimalist.CatFamily.nominal ∧ Minimalist.catFamily Minimalist.Cat.Num = Minimalist.CatFamily.nominal ∧ Minimalist.catFamily Minimalist.Cat.D = Minimalist.CatFamily.nominal

K&C's (14) spine belongs to the nominal EP family.

theorem KonnellyCowper2020.stage3_they_from_structure (ctx : ReferentContext) : genderObligatoryFor ctx Stage.stage3 = false ∧ { nHead := Morphology.DM.CatHead.n_plain, singular := true }.spellout = some "they"

At Stage 3, every referent context permits an ungendered nominal structure (plain n), which produces "they". This composes two independent results:

• stage3_nothing_obligatory: no context requires gender features
• singular_ungendered_spellout: plain n → "they" via VI

The DP structure at all three stages is identical — K&C's (14). What changes across stages is which n-heads are available in which referent contexts, not the syntactic architecture itself.

theorem KonnellyCowper2020.elsewhere_is_epicene : Morphology.DM.VI.subsetPrinciple pronounVIs ungenderedBundle = some "they" ∧ Fragments.English.Pronouns.genderOf "they" = Fragments.English.Pronouns.GenderParadigm.epicene

The VI elsewhere exponent they corresponds to the Fragment's epicene gender paradigm. This makes explicit the connection that K&C's analysis reveals: epicene is not a positive gender class but the absence of a contrastive gender feature — the elsewhere case in VI competition.

theorem KonnellyCowper2020.vi_fragment_consistency : Fragments.English.Pronouns.genderOf "she" = Fragments.English.Pronouns.GenderParadigm.feminine ∧ Fragments.English.Pronouns.genderOf "he" = Fragments.English.Pronouns.GenderParadigm.masculine ∧ Fragments.English.Pronouns.genderOf "it" = Fragments.English.Pronouns.GenderParadigm.neuter ∧ Fragments.English.Pronouns.genderOf "they" = Fragments.English.Pronouns.GenderParadigm.epicene

The VI competition and the Fragment's gender paradigm are consistent across all four pronoun forms: each VI exponent maps to its expected gender paradigm class.

This is the bridge between the morphosyntactic mechanism (VI) and the descriptive grammar (GenderParadigm): VI derives which form is used, and the Fragment's paradigm classification records the result.

def KonnellyCowper2020.bjorkmanSubset (pronounFeatures antecedentFeatures : List PronFeature) : Bool

@cite{bjorkman-2017}'s dynamic discourse condition: a pronoun's gender features must be a subset of its antecedent's gender features. A pronoun that is "less specified" than its antecedent is acceptable; one that adds features the antecedent lacks is not.

K&C §5 argue this condition presupposes contrastive features and cannot extend to Stage 3, where features are non-contrastive.

Equations

• KonnellyCowper2020.bjorkmanSubset pronounFeatures antecedentFeatures = pronounFeatures.all fun (x : KonnellyCowper2020.PronFeature) => antecedentFeatures.contains x

theorem KonnellyCowper2020.they_always_bjorkman_ok (antecedent : List PronFeature) : bjorkmanSubset [] antecedent = true

Under Bjorkman's condition, they (no gender features) can always corefer with any antecedent, because ∅ ⊆ S for any set S.

theorem KonnellyCowper2020.he_blocked_for_ungendered_antecedent : bjorkmanSubset [PronFeature.masc] [] = false

Under Bjorkman's condition, he ([MASC]) cannot corefer with an antecedent that lacks [MASC] — the pronoun adds a feature the antecedent doesn't have. Example: "Every student₁ brought his₁ lunch" — his has [MASC] but every student has no gender feature → Bjorkman predicts this is blocked, matching Stage 1 speakers' judgments.

theorem KonnellyCowper2020.bjorkman_vacuous_at_stage3 : Stage.stage3.genderContrastivity = Morphology.DM.Contrastivity.nonContrastive ∧ bjorkmanSubset [] [] = true ∧ bjorkmanSubset [PronFeature.masc] [] = false ∧ Stage.stage3.genderObligatory = false

At Stage 3, K&C predict that antecedents' gender feature bundles are typically empty (non-contrastive features are optional modifiers whose absence is the norm). Bjorkman's condition is then vacuously satisfied for ALL pronouns, providing no constraint at all.

K&C argue this is a problem: Bjorkman's system gives no mechanism for why Stage 3 speakers would still optionally use "he"/"she" (which K&C handle via non-contrastive modifiers that are present but not obligatory).

theorem KonnellyCowper2020.bjorkman_blind_to_projection : genderObligatoryFor ReferentContext.ungenderedProperName Stage.stage1 = true ∧ genderObligatoryFor ReferentContext.ungenderedProperName Stage.stage2 = false

K&C §5.2: Bjorkman's condition also cannot explain the GRADUAL nature of the Stage 1→2 transition. If the change were simply learning that some names lack gender features (Bjorkman's account), it should be abrupt — once you learn "Kelly" has no [MASC], you accept they for Kelly. But K&C argue the change is gradual because it involves restructuring the feature system, not just updating lexical entries.

Formally: at Stage 1, ungendered names obligatorily project gender (so "Kelly₁ said they₁ couldn't make it" is rejected). The Stage 2 innovation is that certain names no longer project gender. This is NOT modeled by Bjorkman's condition, which only constrains pronoun selection given a fixed feature bundle — it doesn't address which bundles nominals project.

theorem KonnellyCowper2020.pets_pattern_with_animates : Morphology.DM.VI.subsetPrinciple pronounVIs ungenderedBundle = some "they" ∧ Morphology.DM.VI.subsetPrinciple pronounVIs inanimateBundle = some "it"

At Stage 3, animate non-human referents (pets) can also receive singular they — the ungendered bundle is available for all animate referents, not just humans.

theorem KonnellyCowper2020.inanimates_always_it : Morphology.DM.VI.subsetPrinciple pronounVIs inanimateBundle = some "it"

Inanimate singulars cannot receive they even at Stage 3: the [INANIM] feature remains contrastive, and it is the most specific match for [SG, INANIM].

K&C (10): "I put my favourite watch down somewhere, and now I can't find it / *them."