Konnelly and Cowper (2020): Gender Diversity and Morphosyntax

This file formalizes [KC20]'s account of singular they as a grammatical change in three stages. A third-person pronoun spells out a bundle of privative features by the Elsewhere Principle, the vocabulary items of (11) being she for [sg][fem], he for [sg][masc], it for [sg, inanim] and they elsewhere (items, spellout); the items are constant across the stages, and what changes is which features a pronoun's antecedent projects. On the structure (14), [sg] and [inanim] sit on Num and are always copied to the pronoun, while the gender feature on n is copied only optionally under a quantifier, which is why (12) every girl … their is fine and (13) every book … their is not (quantified). At Stage 1, [masc] and [fem] are contrastive and a noun referring to a person of known gender obligatorily bears one, so they needs an antecedent of unknown gender or a quantifier, (5). At Stage 2 the features are still contrastive but the insertion rule is optional, so an ungendered name like Kelly antecedes they, (6), while a lexically gendered noun does not, (15) and (21). At Stage 3 the features are the non-contrastive modifiers of [Wil08b] (Contrastivity), so they is the default for any singular animate antecedent, (7) and (25), with he and she still available, (8), and it still forced for inanimates, (10) (Stage.genders, forms, stage3_they, it_of_inanimate). Against [Bjo17]'s dynamic condition, which asks a pronoun's features to include its antecedent's, (24) the women said that she was leaving is wrongly licensed, whereas the number contrast excludes it here (bjorkman_overgenerates, women_not_she).

Implementation notes

• An antecedent records what the pronoun sees: the Num features, the gender feature n bears lexically, the referent's known binary gender that the insertion rule may add, and whether D hosts a quantifier. Stage 3's modifier, when present, is the referent's gender, as in (26).

References

• [KC20]
• [Bjo17]
• [Wil08b]

inductive KonnellyCowper2020.Feature : Type

The third-person pronoun has the privative features of (11), [sg] and [inanim] on Num and [masc] and [fem] on n, (14).

• sg : Feature
• inanim : Feature
• masc : Feature
• fem : Feature

@[instance_reducible]

instance KonnellyCowper2020.instDecidableEqFeature : DecidableEq Feature

Equations

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

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

Equations

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

@[instance_reducible]

instance KonnellyCowper2020.instReprFeature : Repr Feature

Equations

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

inductive KonnellyCowper2020.Gender : Type

The binary gender feature n may bear.

• masc : Gender
• fem : Gender

@[instance_reducible]

instance KonnellyCowper2020.instDecidableEqGender : DecidableEq Gender

Equations

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

@[instance_reducible]

instance KonnellyCowper2020.instReprGender : Repr Gender

Equations

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

def KonnellyCowper2020.instReprGender.repr : Gender → ℕ → Std.Format

Equations

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

def KonnellyCowper2020.Gender.feature : Gender → Feature

Equations

• KonnellyCowper2020.Gender.masc.feature = KonnellyCowper2020.Feature.masc
• KonnellyCowper2020.Gender.fem.feature = KonnellyCowper2020.Feature.fem

inductive KonnellyCowper2020.Class : Type

The class feature a nominal bears lexically, a gender on n or [inanim] on Num, §4.1.

• gender (g : Gender) : Class
• inanim : Class

def KonnellyCowper2020.instDecidableEqClass.decEq (x✝ x✝¹ : Class) : Decidable (x✝ = x✝¹)

Equations

• KonnellyCowper2020.instDecidableEqClass.decEq (KonnellyCowper2020.Class.gender a) (KonnellyCowper2020.Class.gender b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• KonnellyCowper2020.instDecidableEqClass.decEq (KonnellyCowper2020.Class.gender g) KonnellyCowper2020.Class.inanim = isFalse ⋯
• KonnellyCowper2020.instDecidableEqClass.decEq KonnellyCowper2020.Class.inanim (KonnellyCowper2020.Class.gender g) = isFalse ⋯
• KonnellyCowper2020.instDecidableEqClass.decEq KonnellyCowper2020.Class.inanim KonnellyCowper2020.Class.inanim = isTrue ⋯

@[instance_reducible]

instance KonnellyCowper2020.instDecidableEqClass : DecidableEq Class

Equations

• KonnellyCowper2020.instDecidableEqClass = KonnellyCowper2020.instDecidableEqClass.decEq

def KonnellyCowper2020.instReprClass.repr : Class → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance KonnellyCowper2020.instReprClass : Repr Class

Equations

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

def KonnellyCowper2020.items : List (DistributedMorphology.VocabularyItem Feature String)

The vocabulary items (11), constant across the stages.

Equations

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

def KonnellyCowper2020.spellout (b : List Feature) : Option String

The exponent of a feature bundle under the Subset Principle.

Equations

• KonnellyCowper2020.spellout b = DistributedMorphology.subsetPrinciple KonnellyCowper2020.items ↑b

theorem KonnellyCowper2020.spellout_items : spellout [Feature.sg, Feature.fem] = some "she" ∧ spellout [Feature.sg, Feature.masc] = some "he" ∧ spellout [Feature.sg, Feature.inanim] = some "it" ∧ spellout [Feature.sg] = some "they" ∧ spellout [] = some "they"

inductive KonnellyCowper2020.Contrastivity : Type

A feature is contrastive when its absence conveys its negation, and a non-contrastive modifier when its absence conveys nothing ([Wil08b]).

• contrastive : Contrastivity
• nonContrastive : Contrastivity

@[instance_reducible]

instance KonnellyCowper2020.instDecidableEqContrastivity : DecidableEq Contrastivity

Equations

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

@[instance_reducible]

instance KonnellyCowper2020.instReprContrastivity : Repr Contrastivity

Equations

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

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

Equations

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

inductive KonnellyCowper2020.Stage : Type

The three stages of the change, §4.

• one : Stage
• two : Stage
• three : Stage

@[instance_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.

@[instance_reducible]

instance KonnellyCowper2020.instReprStage : Repr Stage

Equations

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

def KonnellyCowper2020.Stage.genderContrastivity : Stage → Contrastivity

[masc] and [fem] are contrastive at Stages 1 and 2 and non-contrastive modifiers at Stage 3, §4.2.

Equations

• KonnellyCowper2020.Stage.one.genderContrastivity = KonnellyCowper2020.Contrastivity.contrastive
• KonnellyCowper2020.Stage.two.genderContrastivity = KonnellyCowper2020.Contrastivity.contrastive
• KonnellyCowper2020.Stage.three.genderContrastivity = KonnellyCowper2020.Contrastivity.nonContrastive

def KonnellyCowper2020.Stage.insertionObligatory : Stage → Bool

The rule inserting a known referent's gender on an ungendered noun is obligatory at Stage 1 and optional at Stage 2, §4.1 and §4.2.

Equations

• KonnellyCowper2020.Stage.one.insertionObligatory = true
• KonnellyCowper2020.Stage.two.insertionObligatory = false
• KonnellyCowper2020.Stage.three.insertionObligatory = false

structure KonnellyCowper2020.Antecedent : Type

An antecedent as the pronoun sees it, (14).

• singular : Bool
• lexical : Option Class

  The class feature the nominal bears lexically, as for mother, Susan or watch.

• known : Option Gender

  The referent's known binary gender, which the insertion rule may place on n.

• quantified : Bool

  Whether D hosts a quantifier.

def KonnellyCowper2020.instDecidableEqAntecedent.decEq (x✝ x✝¹ : Antecedent) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance KonnellyCowper2020.instDecidableEqAntecedent : DecidableEq Antecedent

Equations

• KonnellyCowper2020.instDecidableEqAntecedent = KonnellyCowper2020.instDecidableEqAntecedent.decEq

@[instance_reducible]

instance KonnellyCowper2020.instReprAntecedent : Repr Antecedent

Equations

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

def KonnellyCowper2020.instReprAntecedent.repr : Antecedent → ℕ → Std.Format

Equations

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

def KonnellyCowper2020.Antecedent.inanimate (a : Antecedent) : Bool

Equations

• a.inanimate = decide (a.lexical = some KonnellyCowper2020.Class.inanim)

def KonnellyCowper2020.Antecedent.lexicalGender (a : Antecedent) : Option Gender

The gender feature n bears lexically.

Equations

• a.lexicalGender = match a.lexical with | some (KonnellyCowper2020.Class.gender g) => some g | x => none

def KonnellyCowper2020.Antecedent.numFeatures (a : Antecedent) : List Feature

The features of Num, copied to the pronoun in every case.

Equations

• a.numFeatures = (if a.singular = true then [KonnellyCowper2020.Feature.sg] else []) ++ if a.inanimate = true then [KonnellyCowper2020.Feature.inanim] else []

def KonnellyCowper2020.Stage.genders (s : Stage) (a : Antecedent) : List (Option Gender)

The gender features n may bear at a stage. Without a lexical gender, n bears the referent's known gender obligatorily at Stage 1, optionally at Stage 2, and as a modifier at Stage 3.

Equations

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

def KonnellyCowper2020.bundles (s : Stage) (a : Antecedent) : List (List Feature)

The bundles a pronoun with antecedent a may spell out at stage s.

Equations

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

def KonnellyCowper2020.forms (s : Stage) (a : Antecedent) : List String

The pronoun forms available for an antecedent at a stage.

Equations

• KonnellyCowper2020.forms s a = List.filterMap KonnellyCowper2020.spellout (KonnellyCowper2020.bundles s a)

The stages in general

theorem KonnellyCowper2020.lexical_forces_gender {s : Stage} {a : Antecedent} {g : Gender} (h : s.genderContrastivity = Contrastivity.contrastive) (hl : a.lexical = some (Class.gender g)) : s.genders a = [some g]

A contrastive lexical gender feature is the only option, the source of (15) and (21) at Stages 1 and 2.

theorem KonnellyCowper2020.they_mem_forms {s : Stage} {a : Antecedent} (h : none ∈ s.genders a ∨ a.quantified = true) (hi : a.inanimate = false) : "they" ∈ forms s a

They is available whenever the pronoun may omit the gender feature and the antecedent is not inanimate.

theorem KonnellyCowper2020.stage3_they {a : Antecedent} (hi : a.inanimate = false) : "they" ∈ forms Stage.three a

At Stage 3 they is the default for every animate antecedent, (7) and (25).

theorem KonnellyCowper2020.it_of_inanimate {s : Stage} {a : Antecedent} (hs : a.singular = true) (hi : a.inanimate = true) (f : String) : f ∈ forms s a → f = "it"

A singular inanimate antecedent is it at every stage, (10) and (13), since [inanim] sits on Num and is always copied.

The paper's antecedents

def KonnellyCowper2020.anyone : Antecedent

(5a) anyone, a quantified antecedent of unknown gender.

Equations

• KonnellyCowper2020.anyone = { singular := true, lexical := none, known := none, quantified := true }

def KonnellyCowper2020.thePerson : Antecedent

(5b) the person at the door, a referential antecedent of unknown gender.

Equations

• KonnellyCowper2020.thePerson = { singular := true, lexical := none, known := none, quantified := false }

def KonnellyCowper2020.kelly : Antecedent

(6a) Kelly, an ungendered name for a referent of known gender.

Equations

• KonnellyCowper2020.kelly = { singular := true, lexical := none, known := some KonnellyCowper2020.Gender.fem, quantified := false }

def KonnellyCowper2020.maria : Antecedent

(7a) Maria, a lexically gendered name.

Equations

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

def KonnellyCowper2020.yourBrother : Antecedent

(7d) your brother, a lexically gendered noun.

Equations

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

def KonnellyCowper2020.theWatch : Antecedent

(10) my favourite watch, an inanimate antecedent.

Equations

• KonnellyCowper2020.theWatch = { singular := true, lexical := some KonnellyCowper2020.Class.inanim, known := none, quantified := false }

def KonnellyCowper2020.everyGirl : Antecedent

(12b) every girl, a quantified and lexically gendered antecedent.

Equations

• KonnellyCowper2020.everyGirl = { singular := true, lexical := some (KonnellyCowper2020.Class.gender KonnellyCowper2020.Gender.fem), known := none, quantified := true }

def KonnellyCowper2020.everyBook : Antecedent

(13) every book, a quantified inanimate antecedent.

Equations

• KonnellyCowper2020.everyBook = { singular := true, lexical := some KonnellyCowper2020.Class.inanim, known := none, quantified := true }

def KonnellyCowper2020.theWomen : Antecedent

the women of (23) and (24), a plural and lexically gendered antecedent.

Equations

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

theorem KonnellyCowper2020.stage1 : "they" ∈ forms Stage.one anyone ∧ "they" ∈ forms Stage.one thePerson ∧ "they" ∉ forms Stage.one kelly ∧ "they" ∉ forms Stage.one maria

At Stage 1, (5) against (6) and (7), they takes only a quantified or gender-unknown antecedent.

theorem KonnellyCowper2020.stage2 : "they" ∈ forms Stage.two kelly ∧ "they" ∉ forms Stage.two maria

At Stage 2, (6) against (15) and (21), an ungendered name antecedes they and a lexically gendered one does not.

theorem KonnellyCowper2020.stage3 : (∀ a ∈ [anyone, thePerson, kelly, maria, yourBrother], "they" ∈ forms Stage.three a) ∧ "she" ∈ forms Stage.three kelly ∧ forms Stage.three theWatch = ["it"]

At Stage 3, (7), (8) and (10), every animate antecedent takes they, she is still available, and the watch takes it alone.

theorem KonnellyCowper2020.quantified : "they" ∈ forms Stage.one everyGirl ∧ "she" ∈ forms Stage.one everyGirl ∧ forms Stage.one everyBook = ["it", "it"]

Under a quantifier, (12) and (13), the gender feature on n is optional while [inanim] on Num is not.

Bjorkman's dynamic condition, §5

@[reducible, inline]

abbrev KonnellyCowper2020.BjorkmanCondition (pronoun antecedent : List Feature) : Prop

[Bjo17]'s condition requires a referential pronoun's features to include those already associated with its referent.

Equations

• KonnellyCowper2020.BjorkmanCondition pronoun antecedent = (antecedent ⊆ pronoun)

theorem KonnellyCowper2020.bjorkman_women_they : BjorkmanCondition [Feature.fem] [Feature.fem] ∧ spellout [Feature.fem] = some "they"

In (23) the pronoun of the women bears <fem> without [sg], and no item spells that out but they.

theorem KonnellyCowper2020.bjorkman_overgenerates : BjorkmanCondition [Feature.sg, Feature.fem] [Feature.fem] ∧ spellout [Feature.sg, Feature.fem] = some "she"

In (24) a pronoun bearing <fem> and [sg] satisfies the condition for the women and spells out as she, which the condition therefore wrongly licenses.

theorem KonnellyCowper2020.women_not_she (s : Stage) : "she" ∉ forms s theWomen

On the present account the number feature on Num is copied, so a plural antecedent never yields she.