Person and number in pronouns: a feature-geometric analysis

[HR02]: the person and number features of pronouns form a dependency geometry — Participant with Speaker and Addressee, Individuation with Group, Minimal, and its dependent Augmented — and a pronoun's content is a subtree containing the root, so that a complex geometry implies its simpler subgeometries. The active inventories of Daga, Kalihna, Tonkawa, Chinook, Yimas, and Boumaa Fijian (§2.3–2.8) give every attested person–number cell a distinct geometry within the inventory, and the person-only languages Pirahã, Maxakalí, and Kwakiutl (§4) realize exactly the geometries their inventories license — at most four first- and second-person pronouns. Pruning a dependent from a licensed geometry leaves a licensed geometry, whence no dual without plural, no paucal without dual, no inclusive without second person ((18)), and no gender in the plural without gender in the singular (Greenberg's Universals 37 and 45, §6.3); Universal 36, gender implies number, is the dependency of Class on Individuation. Markedness is node count: third person is least marked and the Fijian first inclusive paucal uses all eight nodes. Acquisition builds structure top-down, so first person precedes second and singular precedes plural ((20)).

Main definitions

• Lang, Lang.active: the nine languages and the nodes each activates.
• Row, rows: the pronoun tables, from the paper's example pool.

Main results

• active_of_rows: each inventory is read off its paradigm's contrasts.
• licenses_rows, cell_nodup: every attested cell is licensed by its language's inventory, distinct cells by distinct geometries.
• person_only_exhaust, card_participant_geometries: Pirahã, Maxakalí, and Kwakiutl realize exactly the licensed geometries; the Participant node yields four.
• dual_needs_plural, paucal_needs_dual, inclusive_needs_second: (18).
• gender_needs_number, gendered_plural_needs_gendered_singular, no_gender_only_in_plural: Universals 36, 37, and 45.
• third_least_marked, fijian_inclusive_paucal: node-count markedness.
• first_before_second, singular_before_plural: the acquisition order (20a).
• maxakali_coopts: bare Participant and Participant with Speaker fill to the same content yet are distinct geometries (§4.1).

References

• J. H. Greenberg, Some universals of grammar
• [F. Plank and W. Schellinger, The uneven distribution of genders over numbers][plank-schellinger-1997]

Languages and their inventories

inductive HarleyRitter2002.Lang : Type

The languages of §2.3–2.8 and §4.

• daga : Lang
• kalihna : Lang
• tonkawa : Lang
• chinook : Lang
• yimas : Lang
• fijian : Lang
• piraha : Lang
• maxakali : Lang
• kwakiutl : Lang

@[instance_reducible]

instance HarleyRitter2002.instDecidableEqLang : DecidableEq Lang

Equations

• HarleyRitter2002.instDecidableEqLang x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def HarleyRitter2002.instReprLang.repr : Lang → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance HarleyRitter2002.instReprLang : Repr Lang

Equations

• HarleyRitter2002.instReprLang = { reprPrec := HarleyRitter2002.instReprLang.repr }

@[instance_reducible]

instance HarleyRitter2002.instFintypeLang : Fintype Lang

Equations

• HarleyRitter2002.instFintypeLang = { elems := { val := ↑HarleyRitter2002.Lang.enumList, nodup := HarleyRitter2002.Lang.enumList_nodup }, complete := HarleyRitter2002.instFintypeLang._proof_1 }

def HarleyRitter2002.Lang.ofGlottocode : String → Option Lang

The language of a pool row, by Glottocode.

Equations

• HarleyRitter2002.Lang.ofGlottocode "daga1275" = some HarleyRitter2002.Lang.daga
• HarleyRitter2002.Lang.ofGlottocode "gali1262" = some HarleyRitter2002.Lang.kalihna
• HarleyRitter2002.Lang.ofGlottocode "tonk1249" = some HarleyRitter2002.Lang.tonkawa
• HarleyRitter2002.Lang.ofGlottocode "chin1286" = some HarleyRitter2002.Lang.chinook
• HarleyRitter2002.Lang.ofGlottocode "yima1243" = some HarleyRitter2002.Lang.yimas
• HarleyRitter2002.Lang.ofGlottocode "fiji1243" = some HarleyRitter2002.Lang.fijian
• HarleyRitter2002.Lang.ofGlottocode "pira1253" = some HarleyRitter2002.Lang.piraha
• HarleyRitter2002.Lang.ofGlottocode "maxa1247" = some HarleyRitter2002.Lang.maxakali
• HarleyRitter2002.Lang.ofGlottocode "kwak1269" = some HarleyRitter2002.Lang.kwakiutl
• HarleyRitter2002.Lang.ofGlottocode x✝ = none

def HarleyRitter2002.Lang.active : Lang → Finset Phi.Geometry.Node

The nodes each language activates ((12)–(17), (25), (27)): Speaker is contrastive where there is an inclusive, Minimal where there is a dual, Augmented where there is a paucal; the person-only languages activate no Individuation.

Equations

• One or more equations did not get rendered due to their size.
• HarleyRitter2002.Lang.daga.active = {Phi.Geometry.Node.referringExpression, Phi.Geometry.Node.participant, Phi.Geometry.Node.addressee, Phi.Geometry.Node.individuation, Phi.Geometry.Node.group}
• HarleyRitter2002.Lang.piraha.active = {Phi.Geometry.Node.referringExpression, Phi.Geometry.Node.participant, Phi.Geometry.Node.addressee}
• HarleyRitter2002.Lang.maxakali.active = {Phi.Geometry.Node.referringExpression, Phi.Geometry.Node.participant, Phi.Geometry.Node.speaker, Phi.Geometry.Node.addressee}
• HarleyRitter2002.Lang.kwakiutl.active = {Phi.Geometry.Node.referringExpression, Phi.Geometry.Node.participant, Phi.Geometry.Node.speaker, Phi.Geometry.Node.addressee}

theorem HarleyRitter2002.active_isLowerSet (l : Lang) : IsLowerSet ↑l.active

The pronoun tables

structure HarleyRitter2002.Row : Type

A pronoun of the tables: its language, cell, and form.

• lang : Lang
• person : Person
• number : Number
• form : String

def HarleyRitter2002.instDecidableEqRow.decEq (x✝ x✝¹ : Row) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance HarleyRitter2002.instDecidableEqRow : DecidableEq Row

Equations

• HarleyRitter2002.instDecidableEqRow = HarleyRitter2002.instDecidableEqRow.decEq

@[instance_reducible]

instance HarleyRitter2002.instReprRow : Repr Row

Equations

• HarleyRitter2002.instReprRow = { reprPrec := HarleyRitter2002.instReprRow.repr }

def HarleyRitter2002.instReprRow.repr : Row → ℕ → Std.Format

Equations

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

def HarleyRitter2002.personOfLabel : String → Option Person

The person of a pool row, by the tables' labels.

Equations

• HarleyRitter2002.personOfLabel "1" = some Person.first
• HarleyRitter2002.personOfLabel "1ex" = some Person.firstExclusive
• HarleyRitter2002.personOfLabel "1in" = some Person.firstInclusive
• HarleyRitter2002.personOfLabel "2" = some Person.second
• HarleyRitter2002.personOfLabel "3" = some Person.third
• HarleyRitter2002.personOfLabel x✝ = none

def HarleyRitter2002.numberOfLabel : String → Option Number

The number of a pool row, by the tables' labels; none is number-neutral.

Equations

• HarleyRitter2002.numberOfLabel "sg" = some Number.singular
• HarleyRitter2002.numberOfLabel "du" = some Number.dual
• HarleyRitter2002.numberOfLabel "pc" = some Number.paucal
• HarleyRitter2002.numberOfLabel "pl" = some Number.plural
• HarleyRitter2002.numberOfLabel "none" = some Number.general
• HarleyRitter2002.numberOfLabel x✝ = none

def HarleyRitter2002.Row.ofExample (ex : Data.Examples.LinguisticExample) : Option Row

Read a row off a pool example.

Equations

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

theorem HarleyRitter2002.row_ofExample_isSome (ex : Data.Examples.LinguisticExample) : ex ∈ Examples.all → (Row.ofExample ex).isSome = true

def HarleyRitter2002.rows : List Row

The pronouns of Tables 3–8 and 13–15.

Equations

• HarleyRitter2002.rows = List.filterMap HarleyRitter2002.Row.ofExample HarleyRitter2002.Examples.all

def HarleyRitter2002.Lang.rows (l : Lang) : List Row

A language's pronouns.

Equations

• l.rows = List.filter (fun (x : HarleyRitter2002.Row) => decide (x.lang = l)) HarleyRitter2002.rows

def HarleyRitter2002.Row.cell (r : Row) : Option (Finset Phi.Geometry.Node)

The geometry of a row's cell in its language.

Equations

• r.cell = Phi.Geometry.cell r.lang.active r.person r.number

theorem HarleyRitter2002.licenses_rows (r : Row) : r ∈ rows → Phi.Geometry.Licenses r.lang.active r.person r.number

Every attested cell is licensed by its language's inventory.

theorem HarleyRitter2002.active_of_rows (l : Lang) : (Phi.Geometry.Node.addressee ∈ l.active ↔ ∃ r ∈ l.rows, r.person = Person.second) ∧ (Phi.Geometry.Node.speaker ∈ l.active ↔ ∃ r ∈ l.rows, r.person = Person.firstInclusive) ∧ (Phi.Geometry.Node.minimal ∈ l.active ↔ ∃ r ∈ l.rows, r.number = Number.dual) ∧ (Phi.Geometry.Node.augmented ∈ l.active ↔ ∃ r ∈ l.rows, r.number = Number.paucal) ∧ (Phi.Geometry.Node.individuation ∈ l.active ↔ ∃ r ∈ l.rows, ∃ s ∈ l.rows, r.person = s.person ∧ r.number ≠ s.number)

The inventory is read off the paradigm (§2.4, §3): Addressee is active iff there is a second person, Speaker iff an inclusive, Minimal iff a dual, Augmented iff a paucal, and Individuation iff some person distinguishes numbers — which the person-only languages do not.

theorem HarleyRitter2002.cell_nodup (l : Lang) : (List.map Row.cell l.rows).Nodup

Within a language, distinct cells receive distinct geometries.

theorem HarleyRitter2002.person_only_exhaust (l : Lang) : l ∈ [Lang.piraha, Lang.maxakali, Lang.kwakiutl] → (List.filterMap Row.cell l.rows).toFinset = l.active.lowerSubsets.erase ∅

The person-only languages realize every nonempty lower subset of their inventory and nothing else (§4, (25), (27)).

theorem HarleyRitter2002.card_participant_geometries : {x ∈ Lang.maxakali.active.lowerSubsets | Phi.Geometry.Node.participant ∈ x}.card = 4

A language using only the Participant node has four geometries with it ((26)): no such language has more than four first- and second-person pronouns.

Complex geometries imply simpler ones (§2.10, §6.1)

theorem HarleyRitter2002.cell_plural_eq (A : Finset Phi.Geometry.Node) (p : Person) : Phi.Geometry.cell A p Number.plural = Option.map (fun (x : Finset Phi.Geometry.Node) => {b ∈ x | ¬Phi.Geometry.Node.minimal ≤ b}) (Phi.Geometry.cell A p Number.dual)

Plural is dual with Minimal pruned ((32a)).

theorem HarleyRitter2002.cell_singular_eq {A : Finset Phi.Geometry.Node} (h : Phi.Geometry.Node.minimal ∈ A) (p : Person) : Phi.Geometry.cell A p Number.singular = Option.map (fun (x : Finset Phi.Geometry.Node) => {b ∈ x | ¬Phi.Geometry.Node.group ≤ b}) (Phi.Geometry.cell A p Number.dual)

Singular is dual with Group pruned, in an inventory with a contrastive Minimal ((32a)).

theorem HarleyRitter2002.cell_dual_eq (A : Finset Phi.Geometry.Node) (p : Person) : Phi.Geometry.cell A p Number.dual = Option.map (fun (x : Finset Phi.Geometry.Node) => {b ∈ x | ¬Phi.Geometry.Node.augmented ≤ b}) (Phi.Geometry.cell A p Number.paucal)

Dual is paucal with Augmented pruned.

theorem HarleyRitter2002.cell_second_eq (A : Finset Phi.Geometry.Node) (n : Number) : Phi.Geometry.cell A Person.second n = Option.map (fun (x : Finset Phi.Geometry.Node) => {b ∈ x | ¬Phi.Geometry.Node.speaker ≤ b}) (Phi.Geometry.cell A Person.firstInclusive n) ∧ Phi.Geometry.cell A Person.firstExclusive n = Option.map (fun (x : Finset Phi.Geometry.Node) => {b ∈ x | ¬Phi.Geometry.Node.addressee ≤ b}) (Phi.Geometry.cell A Person.firstInclusive n)

Second person is inclusive with Speaker pruned, exclusive inclusive with Addressee pruned ((32b)).

theorem HarleyRitter2002.licenses_of_map_filter {A : Finset Phi.Geometry.Node} {p : Person} {n n' : Number} {p' : Person} {a : Phi.Geometry.Node} (h : Phi.Geometry.cell A p' n' = Option.map (fun (x : Finset Phi.Geometry.Node) => {b ∈ x | ¬a ≤ b}) (Phi.Geometry.cell A p n)) (hl : Phi.Geometry.Licenses A p n) : Phi.Geometry.Licenses A p' n'

theorem HarleyRitter2002.dual_needs_plural {A : Finset Phi.Geometry.Node} {p : Person} (h : Phi.Geometry.Licenses A p Number.dual) : Phi.Geometry.Licenses A p Number.plural

(18a) No dual without plural.

theorem HarleyRitter2002.paucal_needs_dual {A : Finset Phi.Geometry.Node} {p : Person} (h : Phi.Geometry.Licenses A p Number.paucal) : Phi.Geometry.Licenses A p Number.dual

(18b) No paucal without dual.

theorem HarleyRitter2002.inclusive_needs_second {A : Finset Phi.Geometry.Node} {n : Number} (h : Phi.Geometry.Licenses A Person.firstInclusive n) : Phi.Geometry.Licenses A Person.second n ∧ Phi.Geometry.Licenses A Person.firstExclusive n

(18c) No inclusive without second person — nor without exclusive.

Gender (§6.3)

theorem HarleyRitter2002.gender_needs_number {A : Finset Phi.Geometry.Node} (hA : IsLowerSet ↑A) (h : Phi.Geometry.Node.nounClass ∈ A) : Phi.Geometry.Node.individuation ∈ A

Universal 36: gender implies number — Class depends on Individuation.

theorem HarleyRitter2002.gendered_plural_needs_gendered_singular {A g : Finset Phi.Geometry.Node} (hg : g ∈ A.lowerSubsets) (hc : Phi.Geometry.Node.nounClass ∈ g) : {b ∈ g | ¬Phi.Geometry.Node.group ≤ b} ∈ A.lowerSubsets ∧ Phi.Geometry.Node.nounClass ∈ {b ∈ g | ¬Phi.Geometry.Node.group ≤ b} ∧ Phi.Geometry.Node.group ∉ {b ∈ g | ¬Phi.Geometry.Node.group ≤ b}

Universals 37 and 45: a gendered geometry with Group prunes to a gendered one without, so gender in the plural implies gender in the singular.

theorem HarleyRitter2002.no_gender_only_in_plural {A : Finset Phi.Geometry.Node} (hall : ∀ g ∈ A.lowerSubsets, Phi.Geometry.Node.nounClass ∈ g → Phi.Geometry.Node.group ∈ g) (g : Finset Phi.Geometry.Node) : g ∈ A.lowerSubsets → Phi.Geometry.Node.nounClass ∉ g

The system (45) — gender only in nonsingular numbers — is impossible: an inventory whose every gendered geometry has Group has no gendered geometry.

Markedness (§1.3, §2.3)

theorem HarleyRitter2002.third_least_marked {A : Finset Phi.Geometry.Node} {p : Person} {n : Number} {g g' : Finset Phi.Geometry.Node} (h : Phi.Geometry.cell A Person.third n = some g) (h' : Phi.Geometry.cell A p n = some g') : g ⊆ g'

Third person is the least marked: its geometry lies within every other person's in the same number.

theorem HarleyRitter2002.daga_first_singular_lt_plural (g : Finset Phi.Geometry.Node) : g ∈ Phi.Geometry.cell Lang.daga.active Person.first Number.singular → ∀ g' ∈ Phi.Geometry.cell Lang.daga.active Person.first Number.plural, g.card < g'.card

In Daga, the first singular is less marked than the first plural — the default Speaker and Minimal nodes are not counted (§2.3).

theorem HarleyRitter2002.fijian_inclusive_paucal : Phi.Geometry.cell Lang.fijian.active Person.firstInclusive Number.paucal = some Lang.fijian.active ∧ Lang.fijian.active.card = 8

The most marked pronoun, the Fijian first inclusive paucal, uses all eight person–number nodes (§2.8).

Acquisition (§3)

theorem HarleyRitter2002.first_before_second {A : Finset Phi.Geometry.Node} {n : Number} (g : Finset Phi.Geometry.Node) : g ∈ Phi.Geometry.cell A Person.first n → ∀ g' ∈ Phi.Geometry.cell A Person.second n, g ⊂ g'

First person is acquired before second: its geometry is a proper part ((20a-ii)).

theorem HarleyRitter2002.singular_before_plural {A : Finset Phi.Geometry.Node} {p : Person} (hm : Phi.Geometry.Node.minimal ∉ A) (hi : Phi.Geometry.Node.individuation ∈ A) (g : Finset Phi.Geometry.Node) : g ∈ Phi.Geometry.cell A p Number.singular → ∀ g' ∈ Phi.Geometry.cell A p Number.plural, g ⊂ g'

Singular is acquired before plural where Minimal is a default ((20a-iii)).

theorem HarleyRitter2002.second_third_plural_incomparable (g : Finset Phi.Geometry.Node) : g ∈ Phi.Geometry.cell Lang.daga.active Person.second Number.singular → ∀ g' ∈ Phi.Geometry.cell Lang.daga.active Person.third Number.plural, ¬g ⊆ g' ∧ ¬g' ⊆ g

Second person and third plural are incomparable, so their order varies ((20b)).

Empty paradigm space (§4.1)

theorem HarleyRitter2002.maxakali_coopts (g : Finset Phi.Geometry.Node) : g ∈ Phi.Geometry.cell Lang.maxakali.active Person.first Number.singular → ∀ g' ∈ Phi.Geometry.cell Lang.maxakali.active Person.firstExclusive Number.plural, g ≠ g' ∧ Phi.Geometry.fillDefaults g = Phi.Geometry.fillDefaults g'

Maxakalí's first singular, the bare Participant node, and its first exclusive plural, Participant with Speaker, fill to the same content by the Speaker default yet are distinct geometries — the exclusive plural co-opts the representation the contrastive Speaker makes available ((27)).