Paradigmatic Structure of Person Marking

@cite{cysouw-2009} @cite{greenberg-1963}

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 Phenomena.Agreement.Typology.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 : Core.Person.Category → Nat

  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

instance Phenomena.Agreement.Typology.instBEqParadigmaticStructure : BEq ParadigmaticStructure

Equations

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

def Phenomena.Agreement.Typology.ParadigmaticStructure.homophonous (s : ParadigmaticStructure) (c1 c2 : Core.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 Phenomena.Agreement.Typology.ParadigmaticStructure.distinctForms (s : ParadigmaticStructure) : Nat

Number of distinct morphemes in the paradigm.

Equations

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

inductive Phenomena.Agreement.Typology.SingularType : Type

The 5 singular homophony types (@cite{cysouw-2009}, §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

instance Phenomena.Agreement.Typology.instDecidableEqSingularType : DecidableEq SingularType

Equations

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

def Phenomena.Agreement.Typology.instBEqSingularType.beq : SingularType → SingularType → Bool

Equations

• Phenomena.Agreement.Typology.instBEqSingularType.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Agreement.Typology.instBEqSingularType : BEq SingularType

Equations

• Phenomena.Agreement.Typology.instBEqSingularType = { beq := Phenomena.Agreement.Typology.instBEqSingularType.beq }

instance Phenomena.Agreement.Typology.instReprSingularType : Repr SingularType

Equations

• Phenomena.Agreement.Typology.instReprSingularType = { reprPrec := Phenomena.Agreement.Typology.instReprSingularType.repr }

def Phenomena.Agreement.Typology.instReprSingularType.repr : SingularType → Nat → Std.Format

Equations

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

def Phenomena.Agreement.Typology.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 Phenomena.Agreement.Typology.FirstPersonComplexType : Type

The 5 common types of marking for 'we' (@cite{cysouw-2009}, 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

instance Phenomena.Agreement.Typology.instDecidableEqFirstPersonComplexType : DecidableEq FirstPersonComplexType

Equations

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

def Phenomena.Agreement.Typology.instBEqFirstPersonComplexType.beq : FirstPersonComplexType → FirstPersonComplexType → Bool

Equations

• Phenomena.Agreement.Typology.instBEqFirstPersonComplexType.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Agreement.Typology.instBEqFirstPersonComplexType : BEq FirstPersonComplexType

Equations

• Phenomena.Agreement.Typology.instBEqFirstPersonComplexType = { beq := Phenomena.Agreement.Typology.instBEqFirstPersonComplexType.beq }

def Phenomena.Agreement.Typology.instReprFirstPersonComplexType.repr : FirstPersonComplexType → Nat → Std.Format

Equations

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

instance Phenomena.Agreement.Typology.instReprFirstPersonComplexType : Repr FirstPersonComplexType

Equations

• Phenomena.Agreement.Typology.instReprFirstPersonComplexType = { reprPrec := Phenomena.Agreement.Typology.instReprFirstPersonComplexType.repr }

def Phenomena.Agreement.Typology.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 Phenomena.Agreement.Typology.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 Phenomena.Agreement.Typology.ParadigmaticStructure.hasSingularHomophony (s : ParadigmaticStructure) : Bool

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

Equations

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

def Phenomena.Agreement.Typology.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 Phenomena.Agreement.Typology.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

instance Phenomena.Agreement.Typology.instDecidableEqExplicitnessLevel : DecidableEq ExplicitnessLevel

Equations

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

instance Phenomena.Agreement.Typology.instBEqExplicitnessLevel : BEq ExplicitnessLevel

Equations

• Phenomena.Agreement.Typology.instBEqExplicitnessLevel = { beq := Phenomena.Agreement.Typology.instBEqExplicitnessLevel.beq }

def Phenomena.Agreement.Typology.instBEqExplicitnessLevel.beq : ExplicitnessLevel → ExplicitnessLevel → Bool

Equations

• Phenomena.Agreement.Typology.instBEqExplicitnessLevel.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Phenomena.Agreement.Typology.instReprExplicitnessLevel.repr : ExplicitnessLevel → Nat → Std.Format

Equations

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

instance Phenomena.Agreement.Typology.instReprExplicitnessLevel : Repr ExplicitnessLevel

Equations

• Phenomena.Agreement.Typology.instReprExplicitnessLevel = { reprPrec := Phenomena.Agreement.Typology.instReprExplicitnessLevel.repr }

instance Phenomena.Agreement.Typology.instOrdExplicitnessLevel : Ord ExplicitnessLevel

Equations

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

def Phenomena.Agreement.Typology.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 Phenomena.Agreement.Typology.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

instance Phenomena.Agreement.Typology.instDecidableEqHorizHomophonyLevel : DecidableEq HorizHomophonyLevel

Equations

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

instance Phenomena.Agreement.Typology.instBEqHorizHomophonyLevel : BEq HorizHomophonyLevel

Equations

• Phenomena.Agreement.Typology.instBEqHorizHomophonyLevel = { beq := Phenomena.Agreement.Typology.instBEqHorizHomophonyLevel.beq }

def Phenomena.Agreement.Typology.instBEqHorizHomophonyLevel.beq : HorizHomophonyLevel → HorizHomophonyLevel → Bool

Equations

• Phenomena.Agreement.Typology.instBEqHorizHomophonyLevel.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Agreement.Typology.instReprHorizHomophonyLevel : Repr HorizHomophonyLevel

Equations

• Phenomena.Agreement.Typology.instReprHorizHomophonyLevel = { reprPrec := Phenomena.Agreement.Typology.instReprHorizHomophonyLevel.repr }

def Phenomena.Agreement.Typology.instReprHorizHomophonyLevel.repr : HorizHomophonyLevel → Nat → Std.Format

Equations

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

def Phenomena.Agreement.Typology.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 Phenomena.Agreement.Typology.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

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

def Phenomena.Agreement.Typology.homophonyImplication (s : ParadigmaticStructure) : Prop

Homophony Implication: Singular homophony → inflectional paradigm.

Equations

• Phenomena.Agreement.Typology.homophonyImplication s = (s.hasSingularHomophony = true → s.isInflectional = true)

def Phenomena.Agreement.Typology.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 Phenomena.Agreement.Typology.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 Phenomena.Agreement.Typology.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 Phenomena.Agreement.Typology.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 Phenomena.Agreement.Typology.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 Phenomena.Agreement.Typology.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 Phenomena.Agreement.Typology.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 Phenomena.Agreement.Typology.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 Phenomena.Agreement.Typology.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 Phenomena.Agreement.Typology.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 Phenomena.Agreement.Typology.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 Phenomena.Agreement.Typology.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 Phenomena.Agreement.Typology.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 Fragments.Finnish.Negation: en/et/ei are all distinct.

Equations

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

def Phenomena.Agreement.Typology.allParadigms : List ParadigmaticStructure

All language data.

Equations

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

theorem Phenomena.Agreement.Typology.allParadigms_count : allParadigms.length = 13

Singular homophony type verification

theorem Phenomena.Agreement.Typology.latin_is_Sa : latin.singularType = SingularType.Sa

theorem Phenomena.Agreement.Typology.dutch_is_Sb : dutchInflection.singularType = SingularType.Sb

theorem Phenomena.Agreement.Typology.spanish_subj_is_Sc : spanishSubjunctive.singularType = SingularType.Sc

theorem Phenomena.Agreement.Typology.english_infl_is_Sd : englishInflection.singularType = SingularType.Sd

theorem Phenomena.Agreement.Typology.french_is_Se : frenchInflection.singularType = SingularType.Se

theorem Phenomena.Agreement.Typology.finnish_is_Sa : finnishInflection.singularType = SingularType.Sa

First person complex type verification

theorem Phenomena.Agreement.Typology.english_pronouns_Pa : englishPronouns.firstPersonComplexType = FirstPersonComplexType.Pa

theorem Phenomena.Agreement.Typology.english_infl_Pb : englishInflection.firstPersonComplexType = FirstPersonComplexType.Pb

theorem Phenomena.Agreement.Typology.maka_Pc : maka.firstPersonComplexType = FirstPersonComplexType.Pc

theorem Phenomena.Agreement.Typology.mandara_Pd : mandara.firstPersonComplexType = FirstPersonComplexType.Pd

theorem Phenomena.Agreement.Typology.ilocano_Pe : ilocano.firstPersonComplexType = FirstPersonComplexType.Pe

theorem Phenomena.Agreement.Typology.piraha_Pb : piraha.firstPersonComplexType = FirstPersonComplexType.Pb

theorem Phenomena.Agreement.Typology.finnish_Pa : finnishInflection.firstPersonComplexType = FirstPersonComplexType.Pa

Five singular types are exhaustive over our data

theorem Phenomena.Agreement.Typology.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 Phenomena.Agreement.Typology.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 Phenomena.Agreement.Typology.addressee_inclusion_holds : (allParadigms.all fun (s : ParadigmaticStructure) => if (s.morphClass Core.Person.Category.excl != s.morphClass Core.Person.Category.s1) = true then s.morphClass Core.Person.Category.minIncl != s.morphClass Core.Person.Category.s1 || s.morphClass Core.Person.Category.augIncl != s.morphClass Core.Person.Category.s1 else true) = true

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

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

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

theorem Phenomena.Agreement.Typology.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 Phenomena.Agreement.Typology.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 Phenomena.Agreement.Typology.ilocano_most_explicit : ilocano.explicitnessLevel = ExplicitnessLevel.minimalAugmented

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

theorem Phenomena.Agreement.Typology.mandara_incl_excl : mandara.explicitnessLevel = ExplicitnessLevel.inclusiveExclusive

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

theorem Phenomena.Agreement.Typology.english_pronouns_unified : englishPronouns.explicitnessLevel = ExplicitnessLevel.unifiedWe

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

theorem Phenomena.Agreement.Typology.french_least_explicit : frenchInflection.explicitnessLevel = ExplicitnessLevel.singularHomophony

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

theorem Phenomena.Agreement.Typology.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 Phenomena.Agreement.Typology.toda_horizontal_homophony : toda.hasHorizontalHomophony = true

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

theorem Phenomena.Agreement.Typology.english_horizontal_homophony : englishPronouns.hasHorizontalHomophony = true

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

theorem Phenomena.Agreement.Typology.latin_no_horizontal_homophony : latin.hasHorizontalHomophony = false

Latin has no horizontal homophony.

theorem Phenomena.Agreement.Typology.piraha_maximal_horizontal : piraha.hasHorizontalHomophony = true ∧ piraha.homophonous Core.Person.Category.s1 Core.Person.Category.excl = true ∧ piraha.homophonous Core.Person.Category.s2 Core.Person.Category.secondGrp = true ∧ piraha.homophonous Core.Person.Category.s3 Core.Person.Category.thirdGrp = true

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

def Phenomena.Agreement.Typology.ParadigmaticStructure.weFormCount (s : ParadigmaticStructure) : Nat

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 Phenomena.Agreement.Typology.piraha_zero_we_forms : piraha.weFormCount = 0

theorem Phenomena.Agreement.Typology.english_one_we_form : englishPronouns.weFormCount = 1

theorem Phenomena.Agreement.Typology.maka_one_we_form : maka.weFormCount = 1

theorem Phenomena.Agreement.Typology.mandara_two_we_forms : mandara.weFormCount = 2

theorem Phenomena.Agreement.Typology.ilocano_three_we_forms : ilocano.weFormCount = 3

theorem Phenomena.Agreement.Typology.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 Phenomena.Agreement.Typology.english_fragment_sa : englishPronouns.singularType = SingularType.Sa

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

theorem Phenomena.Agreement.Typology.english_fragment_pa : englishPronouns.firstPersonComplexType = FirstPersonComplexType.Pa

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

theorem Phenomena.Agreement.Typology.english_you_horizontal : englishPronouns.homophonous Core.Person.Category.s2 Core.Person.Category.secondGrp = true

English has horizontal homophony: you.sg = you.pl (2 = 2+3). This is visible in the Fragment: Fragments.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 Phenomena.Agreement.Typology.czech_fragment_sa : czechPronouns.singularType = SingularType.Sa

theorem Phenomena.Agreement.Typology.czech_fragment_pa : czechPronouns.firstPersonComplexType = FirstPersonComplexType.Pa

Bridge 5: Morphological status ↔ Explicitness

@cite{cysouw-2009} 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 Phenomena.Agreement.Typology.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 Phenomena.Agreement.Typology.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.

inductive Phenomena.Agreement.Typology.NumberStage : Type

Number opposition stages (@cite{cysouw-2009}, Fig 10.8).

Hierarchical tree of number oppositions, from no number marking (N₁) to full number marking with restricted groups (N₃/N₄).

• N1 : NumberStage
• N2 : NumberStage
• N3 : NumberStage
• N4 : NumberStage

instance Phenomena.Agreement.Typology.instDecidableEqNumberStage : DecidableEq NumberStage

Equations

• Phenomena.Agreement.Typology.instDecidableEqNumberStage x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Phenomena.Agreement.Typology.instBEqNumberStage : BEq NumberStage

Equations

• Phenomena.Agreement.Typology.instBEqNumberStage = { beq := Phenomena.Agreement.Typology.instBEqNumberStage.beq }

def Phenomena.Agreement.Typology.instBEqNumberStage.beq : NumberStage → NumberStage → Bool

Equations

• Phenomena.Agreement.Typology.instBEqNumberStage.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Agreement.Typology.instReprNumberStage : Repr NumberStage

Equations

• Phenomena.Agreement.Typology.instReprNumberStage = { reprPrec := Phenomena.Agreement.Typology.instReprNumberStage.repr }

def Phenomena.Agreement.Typology.instReprNumberStage.repr : NumberStage → Nat → Std.Format

Equations

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

def Phenomena.Agreement.Typology.ParadigmaticStructure.numberStage (s : ParadigmaticStructure) : NumberStage

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 Phenomena.Agreement.Typology.PersonStage : Type

Person differentiation stages (@cite{cysouw-2009}, Fig 10.9).

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

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

instance Phenomena.Agreement.Typology.instDecidableEqPersonStage : DecidableEq PersonStage

Equations

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

def Phenomena.Agreement.Typology.instBEqPersonStage.beq : PersonStage → PersonStage → Bool

Equations

• Phenomena.Agreement.Typology.instBEqPersonStage.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Agreement.Typology.instBEqPersonStage : BEq PersonStage

Equations

• Phenomena.Agreement.Typology.instBEqPersonStage = { beq := Phenomena.Agreement.Typology.instBEqPersonStage.beq }

instance Phenomena.Agreement.Typology.instReprPersonStage : Repr PersonStage

Equations

• Phenomena.Agreement.Typology.instReprPersonStage = { reprPrec := Phenomena.Agreement.Typology.instReprPersonStage.repr }

def Phenomena.Agreement.Typology.instReprPersonStage.repr : PersonStage → Nat → Std.Format

Equations

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

def Phenomena.Agreement.Typology.ParadigmaticStructure.personStage (s : ParadigmaticStructure) : PersonStage

Classify a paradigm's person differentiation stage.

Equations

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

theorem Phenomena.Agreement.Typology.ilocano_P4 : ilocano.personStage = PersonStage.P4

theorem Phenomena.Agreement.Typology.mandara_P3 : mandara.personStage = PersonStage.P3

theorem Phenomena.Agreement.Typology.english_pron_P1 : englishPronouns.personStage = PersonStage.P1

theorem Phenomena.Agreement.Typology.piraha_P1 : piraha.personStage = PersonStage.P1

structure Phenomena.Agreement.Typology.CognitiveMapPosition : Type

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

• numberStage : NumberStage
• personStage : PersonStage
• singularType : SingularType
• firstPersonComplexType : FirstPersonComplexType
• weFormCount : Nat

def Phenomena.Agreement.Typology.instReprCognitiveMapPosition.repr : CognitiveMapPosition → Nat → Std.Format

Equations

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

instance Phenomena.Agreement.Typology.instReprCognitiveMapPosition : Repr CognitiveMapPosition

Equations

• Phenomena.Agreement.Typology.instReprCognitiveMapPosition = { reprPrec := Phenomena.Agreement.Typology.instReprCognitiveMapPosition.repr }

def Phenomena.Agreement.Typology.instBEqCognitiveMapPosition.beq : CognitiveMapPosition → CognitiveMapPosition → Bool

Equations

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

instance Phenomena.Agreement.Typology.instBEqCognitiveMapPosition : BEq CognitiveMapPosition

Equations

• Phenomena.Agreement.Typology.instBEqCognitiveMapPosition = { beq := Phenomena.Agreement.Typology.instBEqCognitiveMapPosition.beq }

def Phenomena.Agreement.Typology.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 Phenomena.Agreement.Typology.finnish_singular_distinct_from_fragment : have sg := List.map (fun (x : Fragments.Finnish.Negation.NegForm) => x.form) (List.filter (fun (x : Fragments.Finnish.Negation.NegForm) => x.number == "sg") Fragments.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.