Paradigmatic Structure of Person Marking

[Cys09] [Gre63]

Formalizes the typological framework from:

Cysouw, M. (2009). The Paradigmatic Structure of Person Marking. Oxford Studies in Typology and Linguistic Theory. Oxford University Press.

Core Ideas

Person marking is analyzed not via traditional "person × number" grids but via participant groups: sets of speech act participants that are marked by a single morpheme. "Plural" is reanalyzed as qualitative group composition (who is included?) rather than quantitative number (how many?).

The 8-cell paradigmatic scheme (Fig 10.1) comprises:

• 3 singular categories: speaker (1), addressee (2), other (3)
• 5 group categories: 1+2 (minimal inclusive), 1+2+3 (augmented inclusive), 1+3 (exclusive), 2+3 (second person group), 3+3 (third person group)

A paradigmatic structure assigns each category to a morpheme class: categories sharing a class are homophonous (marked by the same form).

Key Results Formalized

• Singular homophony types (Sa–Se): 5 patterns from Chapter 2
• First person complex types (Pa–Pe): 5 common patterns from Chapter 3
• Explicitness Hierarchy (10.7): ordering of paradigmatic explicitness
• Horizontal Homophony Hierarchy (10.1–10.2): ordering of horizontal mergers
• Implicational universals: exclusive → inclusive (3.23), split inclusive → exclusive (3.24)
• Homophony Implication (10.4): singular homophony → inflectional paradigm

structure Cysouw2009.ParadigmaticStructure : Type

A paradigmatic structure assigns each of the 8 person categories to a morpheme class. Categories assigned the same natural number are realized by the same morpheme (homophonous).

This is the central representational device: all of Cysouw's typological classifications are computable from this function.

• name : String

  Language or paradigm name

• isoCode : String

  ISO 639-3 code (if applicable)

• morphClass : Person.Category → ℕ

  Maps each person category to a morpheme class index. Same index = same morpheme (homophony).

• isInflectional : Bool

  Whether this is an inflectional (true) or independent (false) paradigm

@[implicit_reducible]

instance Cysouw2009.instBEqParadigmaticStructure : BEq ParadigmaticStructure

Equations

• Cysouw2009.instBEqParadigmaticStructure = { beq := fun (a b : Cysouw2009.ParadigmaticStructure) => a.name == b.name }

def Cysouw2009.ParadigmaticStructure.homophonous (s : ParadigmaticStructure) (c1 c2 : Person.Category) : Bool

Two categories are homophonous in a paradigm iff they share morphClass.

Equations

• s.homophonous c1 c2 = (s.morphClass c1 == s.morphClass c2)

def Cysouw2009.ParadigmaticStructure.distinctForms (s : ParadigmaticStructure) : ℕ

Number of distinct morphemes in the paradigm.

Equations

• s.distinctForms = (List.map s.morphClass Person.Category.all).eraseDups.length

inductive Cysouw2009.SingularType : Type

The 5 singular homophony types ([Cys09], §2.1–2.5).

Classifies how the three singular categories (1, 2, 3) pattern with respect to homophony within a paradigm.

• Sa : SingularType
• Sb : SingularType
• Sc : SingularType
• Sd : SingularType
• Se : SingularType

@[implicit_reducible]

instance Cysouw2009.instDecidableEqSingularType : DecidableEq SingularType

Equations

• Cysouw2009.instDecidableEqSingularType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Cysouw2009.instReprSingularType : Repr SingularType

Equations

• Cysouw2009.instReprSingularType = { reprPrec := Cysouw2009.instReprSingularType.repr }

def Cysouw2009.instReprSingularType.repr : SingularType → ℕ → Std.Format

Equations

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

def Cysouw2009.ParadigmaticStructure.singularType (s : ParadigmaticStructure) : SingularType

Compute the singular homophony type from a paradigmatic structure.

Equations

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

inductive Cysouw2009.FirstPersonComplexType : Type

The 5 common types of marking for 'we' ([Cys09], Table 3.2/10.3).

Classifies how the three first-person-complex categories (1+2, 1+2+3, 1+3) pattern in the paradigm relative to singular 1.

• Pa : FirstPersonComplexType
• Pb : FirstPersonComplexType
• Pc : FirstPersonComplexType
• Pd : FirstPersonComplexType
• Pe : FirstPersonComplexType

@[implicit_reducible]

instance Cysouw2009.instDecidableEqFirstPersonComplexType : DecidableEq FirstPersonComplexType

Equations

• Cysouw2009.instDecidableEqFirstPersonComplexType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Cysouw2009.instReprFirstPersonComplexType : Repr FirstPersonComplexType

Equations

• Cysouw2009.instReprFirstPersonComplexType = { reprPrec := Cysouw2009.instReprFirstPersonComplexType.repr }

def Cysouw2009.instReprFirstPersonComplexType.repr : FirstPersonComplexType → ℕ → Std.Format

Equations

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

def Cysouw2009.ParadigmaticStructure.firstPersonComplexType (s : ParadigmaticStructure) : FirstPersonComplexType

Compute the first person complex type from a paradigmatic structure.

Follows the decision tree in Figure 3.10:

1. Any specialized 'we'? (No → Pb)
2. Inclusive distinguished from exclusive? (No → Pa unified-we)
3. Exclusive specialized (≠ 1sg)? (No → Pc only-inclusive)
4. Inclusive split (min ≠ aug)? (No → Pd, Yes → Pe)

Equations

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

def Cysouw2009.ParadigmaticStructure.hasHorizontalHomophony (s : ParadigmaticStructure) : Bool

Whether a paradigm has horizontal homophony (singular = non-singular).

Equations

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

def Cysouw2009.ParadigmaticStructure.hasSingularHomophony (s : ParadigmaticStructure) : Bool

Whether a paradigm has singular homophony (between singular categories).

Equations

• s.hasSingularHomophony = (s.homophonous Person.Category.s1 Person.Category.s2 || s.homophonous Person.Category.s1 Person.Category.s3 || s.homophonous Person.Category.s2 Person.Category.s3)

def Cysouw2009.ParadigmaticStructure.hasVerticalHomophony (s : ParadigmaticStructure) : Bool

Whether a paradigm has vertical homophony (between non-singular categories, excluding the first person complex internal structure).

Cysouw §10.1.6: "the various kinds of homophony between the categories of the first person complex are not included under this heading." So we only check mergers between the first person complex and {2+3, 3+3}, or between 2+3 and 3+3.

Equations

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

inductive Cysouw2009.ExplicitnessLevel : Type

Explicitness level of a paradigm.

Measures how many person oppositions are grammaticalized in the paradigm. Higher = more explicit (more distinct morphemes).

• singularHomophony : ExplicitnessLevel
• verticalHomophony : ExplicitnessLevel
• unifiedWe : ExplicitnessLevel
• inclusiveExclusive : ExplicitnessLevel
• minimalAugmented : ExplicitnessLevel

@[implicit_reducible]

instance Cysouw2009.instDecidableEqExplicitnessLevel : DecidableEq ExplicitnessLevel

Equations

• Cysouw2009.instDecidableEqExplicitnessLevel x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Cysouw2009.instReprExplicitnessLevel : Repr ExplicitnessLevel

Equations

• Cysouw2009.instReprExplicitnessLevel = { reprPrec := Cysouw2009.instReprExplicitnessLevel.repr }

def Cysouw2009.instReprExplicitnessLevel.repr : ExplicitnessLevel → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Cysouw2009.instOrdExplicitnessLevel : Ord ExplicitnessLevel

Equations

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

def Cysouw2009.ParadigmaticStructure.explicitnessLevel (s : ParadigmaticStructure) : ExplicitnessLevel

Compute the explicitness level of a paradigmatic structure.

Equations

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

inductive Cysouw2009.HorizHomophonyLevel : Type

Horizontal Homophony Hierarchy.

If horizontal homophony occurs, it follows the person hierarchy 1 > 2 > 3: first attested in 3rd person, then 2nd, then 1st (exclusive).

• none_ : HorizHomophonyLevel
• third : HorizHomophonyLevel
• second : HorizHomophonyLevel
• exclusive : HorizHomophonyLevel
• first : HorizHomophonyLevel

@[implicit_reducible]

instance Cysouw2009.instDecidableEqHorizHomophonyLevel : DecidableEq HorizHomophonyLevel

Equations

• Cysouw2009.instDecidableEqHorizHomophonyLevel x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Cysouw2009.instReprHorizHomophonyLevel : Repr HorizHomophonyLevel

Equations

• Cysouw2009.instReprHorizHomophonyLevel = { reprPrec := Cysouw2009.instReprHorizHomophonyLevel.repr }

def Cysouw2009.instReprHorizHomophonyLevel.repr : HorizHomophonyLevel → ℕ → Std.Format

Equations

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

def Cysouw2009.addresseeInclusionImplication (s : ParadigmaticStructure) : Prop

Addressee Inclusion Implication I: Exclusive → Inclusive. If there is a specialized exclusive morpheme, there is also a specialized inclusive morpheme.

Equations

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

def Cysouw2009.splitInclusiveImplication (s : ParadigmaticStructure) : Prop

Split Inclusive Implication: Split inclusive → Exclusive. If the inclusive is split into minimal and augmented, then the exclusive is specialized.

Equations

• Cysouw2009.splitInclusiveImplication s = (s.morphClass Person.Category.minIncl ≠ s.morphClass Person.Category.augIncl → s.morphClass Person.Category.excl ≠ s.morphClass Person.Category.s1)

def Cysouw2009.homophonyImplication (s : ParadigmaticStructure) : Prop

Homophony Implication: Singular homophony → inflectional paradigm.

Equations

• Cysouw2009.homophonyImplication s = (s.hasSingularHomophony = true → s.isInflectional = true)

def Cysouw2009.latin : ParadigmaticStructure

Latin (Sa, Pd): all singular distinct, inclusive/exclusive. 1sg -ō, 2sg -s, 3sg -t, 1+2/1+2+3 -mus, 1+3 -mus, 2+3 -tis, 3+3 -nt Note: Latin has no incl/excl distinction, unified 'we' = 1pl -mus.

Equations

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

def Cysouw2009.englishPronouns : ParadigmaticStructure

English verbal inflection (Sb, Pb): 2=3 homophony in present tense, no specialized 'we' (English has -s for 3sg, zero elsewhere → 1=2 in terms of overt marking, but the paradigm structure is actually Sb-type when we consider the pronoun paradigm: I/you/he-she-it). Actually in the verbal inflection: walk/walk/walks → 1=2 vs 3 = Sd type. For the independent pronouns: I ≠ you ≠ he/she → Sa, unified-we.

Equations

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

def Cysouw2009.englishInflection : ParadigmaticStructure

English verbal inflection (Sd type): walk/walk/walks → 1=2 vs 3.

Equations

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

def Cysouw2009.dutchInflection : ParadigmaticStructure

Dutch verbal inflection (Sb type): loop/loopt/loopt → 1 vs 2=3. No incl/excl distinction, unified plural -en.

Equations

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

def Cysouw2009.spanishSubjunctive : ParadigmaticStructure

Spanish verbal inflection (Sc type): hablo/hablas/habla → 1=3 homophony in subjunctive (hable/hables/hable). Indicative present = Sa. Using the subjunctive as the classic Sc example.

Equations

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

def Cysouw2009.frenchInflection : ParadigmaticStructure

French verbal inflection (Se type): parle/parles/parle → 1=2=3 (phonologically identical in spoken French for -er verbs).

Equations

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

def Cysouw2009.mandara : ParadigmaticStructure

Mandara (Chadic): independent pronouns with inclusive/exclusive (Pd). yá/ká/á (1/2/3), má (1+2/1+2+3), ŋá (1+3), kwá (2+3), tá (3+3).

Equations

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

def Cysouw2009.ilocano : ParadigmaticStructure

Ilocano: minimal/augmented system (Pe). co (1sg), ta (1+2 minimal), tayo (1+2+3 augmented), mi (1+3 exclusive), mo (2sg), yo (2+3), na (3sg), da (3+3).

Equations

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

def Cysouw2009.maka : ParadigmaticStructure

Maká (Mataco-Guaicuruan, Paraguay): only-inclusive (Pc). hoy- (1sg/1+3), xi(t)- (1+2/1+2+3), other forms for 2, 3, 2+3, 3+3.

Equations

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

def Cysouw2009.piraha : ParadigmaticStructure

Mura Pirahã: no-we (Pb). Only 3 singular pronouns, no group marking.

Equations

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

def Cysouw2009.toda : ParadigmaticStructure

Toda (Dravidian): Tupí-Guaraní-type with 3=3+3 horizontal homophony.

Equations

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

def Cysouw2009.czechPronouns : ParadigmaticStructure

Czech independent pronouns: Sa (all singular distinct), unified-we (Pa).

Equations

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

def Cysouw2009.finnishInflection : ParadigmaticStructure

Finnish verbal inflection (Sa type): puhun/puhut/puhuu — all singular distinct (suffixes: -n, -t, -V). No inclusive/exclusive distinction, unified 'we' (Pa): puhumme (-mme). Person marking is inflectional. Singular person distinction confirmed by the negative auxiliary paradigm from Finnish.Negation: en/et/ei are all distinct.

Equations

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

def Cysouw2009.allParadigms : List ParadigmaticStructure

All language data.

Equations

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

theorem Cysouw2009.allParadigms_count : allParadigms.length = 13

Singular homophony type verification

theorem Cysouw2009.latin_is_Sa : latin.singularType = SingularType.Sa

theorem Cysouw2009.dutch_is_Sb : dutchInflection.singularType = SingularType.Sb

theorem Cysouw2009.spanish_subj_is_Sc : spanishSubjunctive.singularType = SingularType.Sc

theorem Cysouw2009.english_infl_is_Sd : englishInflection.singularType = SingularType.Sd

theorem Cysouw2009.french_is_Se : frenchInflection.singularType = SingularType.Se

theorem Cysouw2009.finnish_is_Sa : finnishInflection.singularType = SingularType.Sa

First person complex type verification

theorem Cysouw2009.english_pronouns_Pa : englishPronouns.firstPersonComplexType = FirstPersonComplexType.Pa

theorem Cysouw2009.english_infl_Pb : englishInflection.firstPersonComplexType = FirstPersonComplexType.Pb

theorem Cysouw2009.maka_Pc : maka.firstPersonComplexType = FirstPersonComplexType.Pc

theorem Cysouw2009.mandara_Pd : mandara.firstPersonComplexType = FirstPersonComplexType.Pd

theorem Cysouw2009.ilocano_Pe : ilocano.firstPersonComplexType = FirstPersonComplexType.Pe

theorem Cysouw2009.piraha_Pb : piraha.firstPersonComplexType = FirstPersonComplexType.Pb

theorem Cysouw2009.finnish_Pa : finnishInflection.firstPersonComplexType = FirstPersonComplexType.Pa

Five singular types are exhaustive over our data

theorem Cysouw2009.all_singular_types_attested : (((((allParadigms.any fun (x : ParadigmaticStructure) => x.singularType == SingularType.Sa) && allParadigms.any fun (x : ParadigmaticStructure) => x.singularType == SingularType.Sb) && allParadigms.any fun (x : ParadigmaticStructure) => x.singularType == SingularType.Sc) && allParadigms.any fun (x : ParadigmaticStructure) => x.singularType == SingularType.Sd) && decide ((allParadigms.any fun (x : ParadigmaticStructure) => x.singularType == SingularType.Se) = true)) = true

All five first-person complex types are attested

theorem Cysouw2009.all_fpc_types_attested : (((((allParadigms.any fun (x : ParadigmaticStructure) => x.firstPersonComplexType == FirstPersonComplexType.Pa) && allParadigms.any fun (x : ParadigmaticStructure) => x.firstPersonComplexType == FirstPersonComplexType.Pb) && allParadigms.any fun (x : ParadigmaticStructure) => x.firstPersonComplexType == FirstPersonComplexType.Pc) && allParadigms.any fun (x : ParadigmaticStructure) => x.firstPersonComplexType == FirstPersonComplexType.Pd) && decide ((allParadigms.any fun (x : ParadigmaticStructure) => x.firstPersonComplexType == FirstPersonComplexType.Pe) = true)) = true

theorem Cysouw2009.addressee_inclusion_holds : (allParadigms.all fun (s : ParadigmaticStructure) => if (s.morphClass Person.Category.excl != s.morphClass Person.Category.s1) = true then s.morphClass Person.Category.minIncl != s.morphClass Person.Category.s1 || s.morphClass Person.Category.augIncl != s.morphClass Person.Category.s1 else true) = true

Addressee Inclusion Implication holds for all paradigms: exclusive specialized → inclusive specialized. (Cysouw 3.23)

theorem Cysouw2009.split_inclusive_holds : (allParadigms.all fun (s : ParadigmaticStructure) => if (s.morphClass Person.Category.minIncl != s.morphClass Person.Category.augIncl) = true then s.morphClass Person.Category.excl != s.morphClass Person.Category.s1 else true) = true

Split Inclusive Implication holds for all paradigms: min.incl ≠ aug.incl → exclusive specialized. (Cysouw 3.24)

theorem Cysouw2009.homophony_implication_holds : (allParadigms.all fun (s : ParadigmaticStructure) => if s.hasSingularHomophony = true then s.isInflectional else true) = true

Homophony Implication holds for all paradigms: singular homophony → inflectional paradigm. (Cysouw 10.4)

theorem Cysouw2009.independent_no_singular_homophony : ((List.filter (fun (x : ParadigmaticStructure) => x.isInflectional == false) allParadigms).all fun (x : ParadigmaticStructure) => x.hasSingularHomophony == false) = true

Independent pronouns → no singular homophony (contrapositive of 10.4).

theorem Cysouw2009.ilocano_most_explicit : ilocano.explicitnessLevel = ExplicitnessLevel.minimalAugmented

Ilocano (Pe/minimal-augmented) is the most explicit.

theorem Cysouw2009.mandara_incl_excl : mandara.explicitnessLevel = ExplicitnessLevel.inclusiveExclusive

Mandara (Pd/inclusive-exclusive) is one step below.

theorem Cysouw2009.english_pronouns_unified : englishPronouns.explicitnessLevel = ExplicitnessLevel.unifiedWe

English pronouns (Pa/unified-we) are at unified-we level.

theorem Cysouw2009.french_least_explicit : frenchInflection.explicitnessLevel = ExplicitnessLevel.singularHomophony

French inflection (Se/singular homophony) is least explicit.

theorem Cysouw2009.explicitness_correlates_with_forms : ilocano.distinctForms > mandara.distinctForms ∧ mandara.distinctForms > englishPronouns.distinctForms ∧ englishPronouns.distinctForms > frenchInflection.distinctForms

The Explicitness Hierarchy is respected in our data: more explicit paradigms distinguish more categories.

theorem Cysouw2009.toda_horizontal_homophony : toda.hasHorizontalHomophony = true

Toda has horizontal homophony (3sg = 3+3).

theorem Cysouw2009.english_horizontal_homophony : englishPronouns.hasHorizontalHomophony = true

English pronouns have horizontal homophony (you.sg = you.pl).

theorem Cysouw2009.latin_no_horizontal_homophony : latin.hasHorizontalHomophony = false

Latin has no horizontal homophony.

theorem Cysouw2009.piraha_maximal_horizontal : piraha.hasHorizontalHomophony = true ∧ piraha.homophonous Person.Category.s1 Person.Category.excl = true ∧ piraha.homophonous Person.Category.s2 Person.Category.secondGrp = true ∧ piraha.homophonous Person.Category.s3 Person.Category.thirdGrp = true

Pirahã has maximal horizontal homophony (all singular = group).

def Cysouw2009.ParadigmaticStructure.weFormCount (s : ParadigmaticStructure) : ℕ

The First Person Hierarchy: no-we < unified-we < only-inclusive < inclusive/exclusive < minimal/augmented

Verified: the hierarchy corresponds to increasing number of forms for 'we'. We count the distinct morpheme classes among {1+2, 1+2+3, 1+3}.

Equations

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

theorem Cysouw2009.piraha_zero_we_forms : piraha.weFormCount = 0

theorem Cysouw2009.english_one_we_form : englishPronouns.weFormCount = 1

theorem Cysouw2009.maka_one_we_form : maka.weFormCount = 1

theorem Cysouw2009.mandara_two_we_forms : mandara.weFormCount = 2

theorem Cysouw2009.ilocano_three_we_forms : ilocano.weFormCount = 3

theorem Cysouw2009.first_person_hierarchy : piraha.weFormCount < englishPronouns.weFormCount ∧ englishPronouns.weFormCount ≤ maka.weFormCount ∧ maka.weFormCount < mandara.weFormCount ∧ mandara.weFormCount < ilocano.weFormCount

The First Person Hierarchy is respected: Pb (no-we) < Pa (unified) < Pd (incl/excl) < Pe (min/aug) measured by number of specialized 'we' forms.

Bridge 3: English Fragment Pronouns ↔ Paradigmatic Structure

Connect the English pronouns fragment (Fragments/English/Pronouns.lean) to Cysouw's classification. English independent pronouns are Sa (all singular distinct) with unified-we (Pa).

theorem Cysouw2009.english_fragment_sa : englishPronouns.singularType = SingularType.Sa

English pronoun paradigmatic structure is Sa (all distinct in singular).

theorem Cysouw2009.english_fragment_pa : englishPronouns.firstPersonComplexType = FirstPersonComplexType.Pa

English pronoun paradigmatic structure is Pa (unified 'we').

theorem Cysouw2009.english_you_horizontal : englishPronouns.homophonous Person.Category.s2 Person.Category.secondGrp = true

English has horizontal homophony: you.sg = you.pl (2 = 2+3). This is visible in the Fragment: English.Pronouns.you and you_pl share the same surface form "you".

Bridge 4: Czech Fragment ↔ Paradigmatic Structure

Czech pronouns (já/ty/on/my/vy/oni) are Sa with unified-we.

theorem Cysouw2009.czech_fragment_sa : czechPronouns.singularType = SingularType.Sa

theorem Cysouw2009.czech_fragment_pa : czechPronouns.firstPersonComplexType = FirstPersonComplexType.Pa

Bridge 5: Morphological status ↔ Explicitness

[Cys09] shows that inflectional paradigms correlate with lower explicitness. Our data confirms: all inflectional paradigms have explicitness ≤ unified-we (i.e., singular or vertical homophony, or unified-we).

theorem Cysouw2009.inflectional_less_explicit : ((List.filter (fun (x : ParadigmaticStructure) => x.isInflectional) allParadigms).all fun (s : ParadigmaticStructure) => s.explicitnessLevel == ExplicitnessLevel.singularHomophony || s.explicitnessLevel == ExplicitnessLevel.verticalHomophony || s.explicitnessLevel == ExplicitnessLevel.unifiedWe) = true

Inflectional paradigms in our data are all at or below unified-we on the Explicitness Hierarchy.

theorem Cysouw2009.independent_more_explicit : ((List.filter (fun (x : ParadigmaticStructure) => x.isInflectional == false) allParadigms).all fun (s : ParadigmaticStructure) => s.explicitnessLevel != ExplicitnessLevel.singularHomophony) = true

Independent pronoun paradigms show greater explicitness: none have singular homophony.

Number.Stage (Cysouw Fig 10.8) lives in Features/Number/Basic.lean — promoted to substrate because both [Cys09] and [Cor00] consume it.

def Cysouw2009.ParadigmaticStructure.numberStage (s : ParadigmaticStructure) : Number.Stage

Classify a paradigm's number stage by checking singular/group opposition.

Equations

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

inductive Cysouw2009.PersonStage : Type

Person differentiation stages ([Cys09], Fig 10.9).

Measures how finely person is distinguished in non-singular categories.

• P0 : PersonStage
• P1 : PersonStage
• P2 : PersonStage
• P3 : PersonStage
• P4 : PersonStage

@[implicit_reducible]

instance Cysouw2009.instDecidableEqPersonStage : DecidableEq PersonStage

Equations

• Cysouw2009.instDecidableEqPersonStage x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Cysouw2009.instReprPersonStage.repr : PersonStage → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Cysouw2009.instReprPersonStage : Repr PersonStage

Equations

• Cysouw2009.instReprPersonStage = { reprPrec := Cysouw2009.instReprPersonStage.repr }

def Cysouw2009.ParadigmaticStructure.personStage (s : ParadigmaticStructure) : PersonStage

Classify a paradigm's person differentiation stage, per the Fig 10.9 tree as instantiated by Fig 10.7's columns: the only-inclusive and inclusive/exclusive types both sit at P3 (an inclusive–exclusive opposition is present either way); paradigms with an undifferentiated first person complex (no-we, unified-we) are P2 when the non-first non-singulars are differentiated and P1 under vertical homophony (P0 when the singulars are undifferentiated too). (Corrected against the source: a previous revision placed unified-we at P1 and only-inclusive at P2, one stage below Fig 10.7's columns.)

Equations

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

theorem Cysouw2009.ilocano_P4 : ilocano.personStage = PersonStage.P4

theorem Cysouw2009.mandara_P3 : mandara.personStage = PersonStage.P3

theorem Cysouw2009.english_pron_P2 : englishPronouns.personStage = PersonStage.P2

English pronouns are unified-we with differentiated you/they: column P2 of Fig 10.7.

theorem Cysouw2009.piraha_P2 : piraha.personStage = PersonStage.P2

Pirahã is no-we with non-singular reference via the (distinct) singular forms: P2, with Fig 10.7's no-we column.

structure Cysouw2009.CognitiveMapPosition : Type

Position in Cysouw's cognitive map (Fig 10.6), combining the number-of-forms-for-'we' with the paradigm type.

• numberStage : Number.Stage
• personStage : PersonStage
• singularType : SingularType
• firstPersonComplexType : FirstPersonComplexType
• weFormCount : ℕ

def Cysouw2009.instReprCognitiveMapPosition.repr : CognitiveMapPosition → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Cysouw2009.instReprCognitiveMapPosition : Repr CognitiveMapPosition

Equations

• Cysouw2009.instReprCognitiveMapPosition = { reprPrec := Cysouw2009.instReprCognitiveMapPosition.repr }

def Cysouw2009.instBEqCognitiveMapPosition.beq : CognitiveMapPosition → CognitiveMapPosition → Bool

Equations

• One or more equations did not get rendered due to their size.
• Cysouw2009.instBEqCognitiveMapPosition.beq x✝¹ x✝ = false

@[implicit_reducible]

instance Cysouw2009.instBEqCognitiveMapPosition : BEq CognitiveMapPosition

Equations

• Cysouw2009.instBEqCognitiveMapPosition = { beq := Cysouw2009.instBEqCognitiveMapPosition.beq }

def Cysouw2009.ParadigmaticStructure.cognitiveMapPosition (s : ParadigmaticStructure) : CognitiveMapPosition

Compute the full cognitive map position of a paradigm.

Equations

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

theorem Cysouw2009.finnish_singular_distinct_from_fragment : have sg := List.map (fun (x : Finnish.Negation.NegForm) => x.form) (List.filter (fun (x : Finnish.Negation.NegForm) => x.number == "sg") Finnish.Negation.negParadigm); sg.eraseDups.length = 3

Finnish singular person distinction confirmed by the Fragment's negative auxiliary paradigm: the three singular forms (en/et/ei) are all distinct.

The Category × Number junction (ch. 6: cardinality as restriction)

Ch. 6 redefines pronominal number: the eight referential categories are unmarked for number — a group is defined by the KIND of its participants, not their quantity (Figs 6.1–6.2) — so a group's number coordinate in the canonical inventory is Number.general. Number marking proper is restriction of group reference: restricted 1+3 is the traditional dual, and restricted 1+2+3 is the traditional "trial" = McKay's unit augmented (§6.2 with its footnote on the etic/emic split; our Number.unitAugmented). Higher restricted numbers grammaticalize from numerals and become paucals (§6.4: true trials are extremely rare, true quadrals unattested — Sursurunga's "quadral" is a greater paucal, our Number.greaterPaucal, following Corbett).

So Cysouw himself rejects factoring the categories through person × number — the junction below is our representational bridge between the two canonical inventories, not his analysis. It works because the inventories carry his distinctions natively: the group/ restricted contrast is general vs the restricted values, and the one genuinely ambiguous cell — 1+2, referentially identical to its own restriction (Fig 6.3), aligned three ways by attested paradigms (Figs 6.4–6.5: with the duals, Maori (6.1); with the inclusive group, Umpila (6.2); with the singulars as emically MINIMAL, Fig 6.5) — gets McKay's emic coordinate (firstInclusive, minimal), the analysis our API already assigns Tagalog kata.

def Cysouw2009.categoryToPersonNumber : Person.Category → Person × Number

The (person, number) coordinates of each referential category: singular participants are singular, groups are general (number-unmarked, ch. 6's central claim), and the inclusive cells carry the minimal/augmented coordinates (McKay's emic labels).

Equations

• Cysouw2009.categoryToPersonNumber Person.Category.s1 = (Person.first, Number.singular)
• Cysouw2009.categoryToPersonNumber Person.Category.s2 = (Person.second, Number.singular)
• Cysouw2009.categoryToPersonNumber Person.Category.s3 = (Person.third, Number.singular)
• Cysouw2009.categoryToPersonNumber Person.Category.minIncl = (Person.firstInclusive, Number.minimal)
• Cysouw2009.categoryToPersonNumber Person.Category.augIncl = (Person.firstInclusive, Number.augmented)
• Cysouw2009.categoryToPersonNumber Person.Category.excl = (Person.firstExclusive, Number.general)
• Cysouw2009.categoryToPersonNumber Person.Category.secondGrp = (Person.second, Number.general)
• Cysouw2009.categoryToPersonNumber Person.Category.thirdGrp = (Person.third, Number.general)

def Cysouw2009.compatiblePairs : List (Person × Number)

The compatible pairs: the image of the eight categories in Person × Number.

Equations

• Cysouw2009.compatiblePairs = List.map Cysouw2009.categoryToPersonNumber Person.Category.all

theorem Cysouw2009.categoryToPersonNumber_injective : compatiblePairs.Nodup

The junction: the coordinates are injective — the eight referential categories embed into Person × Number, so the two canonical inventories compose without loss.

theorem Cysouw2009.categoryToPersonNumber_fst (c : Person.Category) : (categoryToPersonNumber c).1 = c.person

The person coordinate is the established person projection.

theorem Cysouw2009.general_iff_nonInclusive_group (c : Person.Category) : (categoryToPersonNumber c).2 = Number.general ↔ c.IsGroup ∧ ¬c.IsInclusive

Exactly the group categories are number-unmarked (general): ch. 6's claim that groups are defined by kind, not quantity, holds of the coordinates by construction — except at the inclusive cells, where the 1+2 vs 1+2+3 contrast is itself quantificational (minimal vs augmented), which is why 1+2 is the ambiguous category.