Cysouw, The Paradigmatic Structure of Person Marking (2003)

A person paradigm is a closed set of markers filling one syntagmatic slot, and its paradigmatic structure is which of its cells share a morpheme. Cysouw replaces the person × number grid by eight referential categories, the three singular participants and the five attested groups 1+2, 1+2+3, 1+3, 2+3 and 3+3, and reads a paradigm's structure off three kinds of homophony among them: singular, horizontal (a singular with a group) and vertical (two groups). The three 'we' categories admit fifteen patterns of specialized marking, of which ten are attested, five common and five rare; the common five obey the addressee inclusion implications (3.23) and (3.24), which, read as conditions, nest along the four questions of his Fig. 3.10 into the First Person Hierarchy (3.26). Chapter 4 surveys the structures of the whole grid, names the common and semi-common ones after exemplar languages, and states two generalizations over them: horizontal homophony spreads along the person hierarchy from the third person upwards, the Horizontal Homophony Hierarchies (4.106) and (4.107), and a paradigm gives up its oppositions in a fixed order, the first person complex first and singular person last, the Explicitness Hierarchy (4.108).

A paradigmatic structure is a setoid on the eight categories, the syncretism of a paradigm's cell-to-form map. The kinds of homophony, the 'we' pattern and both hierarchies are properties of that setoid, and every paradigm printed in chapters 3 and 4 is checked against the book's own classification and generalizations, with the exceptions the book names: Binandere against (3.23), the rare 'we' patterns against (3.24), the English pronouns and a few others against the horizontal hierarchy, and the European singular homophonies and the paradigms with vertical homophony under an inclusive/exclusive opposition against the explicitness hierarchy.

Implementation notes

• Cells the book draws as one block carry the same form string, so the syncretism of the forms is the book's block notation; fillers such as "(demonstratives)" are kept as printed.
• The named structures are kernels of labellings, the book's letter notation, of which only the kernel matters (his fn. 1, p. 40).
• Table 10.3 prints the descriptions of unified-we and only-inclusive swapped; Table 3.2 is followed.

TODO

• Chapter 7's dual paradigms, the Dual Explicitness Hierarchy (10.8) and the Dual Homophony Implication (10.3) need cells for restricted groups.
• The zero implications (10.5) and (10.6) need zero marking read off the forms.

References

• [M. Cysouw, The Paradigmatic Structure of Person Marking (2003)][cysouw-2003]

Kinds of homophony (§2.2, §4.2, §10.1.3)

def Cysouw2003.SingularHomophony (s : Setoid Person.Category) : Prop

Two singular categories share a morpheme (Fig. 2.1).

Equations

• Cysouw2003.SingularHomophony s = ∃ (a : Person.Category) (b : Person.Category), a.IsSingular ∧ b.IsSingular ∧ a ≠ b ∧ s a b

def Cysouw2003.HorizontalHomophony (s : Setoid Person.Category) : Prop

A singular category shares a morpheme with a group (Fig. 4.3).

Equations

• Cysouw2003.HorizontalHomophony s = ∃ (a : Person.Category) (b : Person.Category), a.IsSingular ∧ b.IsGroup ∧ s a b

def Cysouw2003.HorizontalHomophonyAt (s : Setoid Person.Category) (a : Person.Category) : Prop

The singular a shares its morpheme with a group of its own person: the first person with the exclusive or the inclusive, the second with 2+3, the third with 3+3 (§10.1.4).

Equations

• Cysouw2003.HorizontalHomophonyAt s a = ∃ (b : Person.Category), b.IsGroup ∧ b.person.coarsen = a.person ∧ s a b

def Cysouw2003.DiagonalHomophony (s : Setoid Person.Category) : Prop

A singular category shares a morpheme with a group of another person (§4.3.6).

Equations

• Cysouw2003.DiagonalHomophony s = ∃ (a : Person.Category) (b : Person.Category), a.IsSingular ∧ b.IsGroup ∧ b.person.coarsen ≠ a.person ∧ s a b

def Cysouw2003.VerticalHomophony (s : Setoid Person.Category) : Prop

Two groups share a morpheme, homophony inside the first person complex not counted (§10.1.6).

Equations

• Cysouw2003.VerticalHomophony s = ∃ (a : Person.Category) (b : Person.Category), a.IsGroup ∧ b.IsGroup ∧ a ≠ b ∧ ¬(a.IsFirstPersonComplex ∧ b.IsFirstPersonComplex) ∧ s a b

theorem Cysouw2003.DiagonalHomophony.horizontalHomophony {s : Setoid Person.Category} (h : DiagonalHomophony s) : HorizontalHomophony s

Diagonal homophony is horizontal.

The first person complex (§3.5–3.7)

def Cysouw2003.Specialized (s : Setoid Person.Category) (c : Person.Category) : Prop

A category is specialized when it shares no morpheme with a singular category (Fig. 3.1's letters against its dashes).

Equations

• Cysouw2003.Specialized s c = ∀ (x : Person.Category), x.IsSingular → ¬s c x

def Cysouw2003.WeRel (s : Setoid Person.Category) (a b : Person.Clusivity.Cell) : Prop

Fig. 3.1's reading of two speaker cells as alike: both specialized and syncretic, or neither specialized.

Equations

• Cysouw2003.WeRel s a b = (Cysouw2003.Specialized s ↑a ∧ Cysouw2003.Specialized s ↑b ∧ s ↑a ↑b ∨ ¬Cysouw2003.Specialized s ↑a ∧ ¬Cysouw2003.Specialized s ↑b)

@[instance_reducible]

def Cysouw2003.wePattern (s : Setoid Person.Category) : Person.Clusivity.Pattern

Fig. 3.1's pattern of a structure, its speaker cells grouped by WeRel; the dash class is the speaker's.

Equations

• Cysouw2003.wePattern s = { r := Cysouw2003.WeRel s, iseqv := ⋯ }

@[reducible, inline]

abbrev Cysouw2003.HasClusivity (s : Setoid Person.Category) (t : Person.Clusivity) : Prop

The structure is of the common type t.

Equations

• Cysouw2003.HasClusivity s t = (Cysouw2003.wePattern s = t.toPattern)

The Horizontal Homophony Hierarchy (§4.7, §10.1.4)

def Cysouw2003.RespectsHorizontalHierarchy (s : Setoid Person.Category) : Prop

Horizontal homophony holds within a person and, in one person, entails it in every less prominent person, so it appears first in the third person, then the second, then the first ((4.106), (4.107)); diagonal homophony is among the exceptions (§4.7).

Equations

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

theorem Cysouw2003.HasClusivity.unique {s : Setoid Person.Category} {t t' : Person.Clusivity} (h : HasClusivity s t) (h' : HasClusivity s t') : t = t'

@[instance_reducible]

instance Cysouw2003.instDecidableSingularHomophony (s : Setoid Person.Category) [DecidableRel ⇑s] : Decidable (SingularHomophony s)

Equations

• Cysouw2003.instDecidableSingularHomophony s = id inferInstance

@[instance_reducible]

instance Cysouw2003.instDecidableHorizontalHomophony (s : Setoid Person.Category) [DecidableRel ⇑s] : Decidable (HorizontalHomophony s)

Equations

• Cysouw2003.instDecidableHorizontalHomophony s = id inferInstance

@[instance_reducible]

instance Cysouw2003.instDecidableHorizontalHomophonyAt (s : Setoid Person.Category) [DecidableRel ⇑s] (a : Person.Category) : Decidable (HorizontalHomophonyAt s a)

Equations

• Cysouw2003.instDecidableHorizontalHomophonyAt s a = id inferInstance

@[instance_reducible]

instance Cysouw2003.instDecidableDiagonalHomophony (s : Setoid Person.Category) [DecidableRel ⇑s] : Decidable (DiagonalHomophony s)

Equations

• Cysouw2003.instDecidableDiagonalHomophony s = id inferInstance

@[instance_reducible]

instance Cysouw2003.instDecidableVerticalHomophony (s : Setoid Person.Category) [DecidableRel ⇑s] : Decidable (VerticalHomophony s)

Equations

• Cysouw2003.instDecidableVerticalHomophony s = id inferInstance

@[instance_reducible]

instance Cysouw2003.instDecidableSpecialized (s : Setoid Person.Category) [DecidableRel ⇑s] (c : Person.Category) : Decidable (Specialized s c)

Equations

• Cysouw2003.instDecidableSpecialized s c = id inferInstance

@[instance_reducible]

instance Cysouw2003.instDecidableRelCellWeRel (s : Setoid Person.Category) [DecidableRel ⇑s] : DecidableRel (WeRel s)

Equations

• Cysouw2003.instDecidableRelCellWeRel s x✝¹ x✝ = id inferInstance

@[instance_reducible]

instance Cysouw2003.instDecidableRelCellR (s : Setoid Person.Category) [DecidableRel ⇑s] : DecidableRel ⇑(wePattern s)

Equations

• Cysouw2003.instDecidableRelCellR s a b = Cysouw2003.instDecidableRelCellWeRel s a b

@[instance_reducible]

instance Cysouw2003.instDecidableRespectsHorizontalHierarchy (s : Setoid Person.Category) [DecidableRel ⇑s] : Decidable (RespectsHorizontalHierarchy s)

Equations

• Cysouw2003.instDecidableRespectsHorizontalHierarchy s = id inferInstance

def Cysouw2003.horizontalSingulars (s : Setoid Person.Category) [DecidableRel ⇑s] : Finset Person.Category

The singular categories showing horizontal homophony.

Equations

• Cysouw2003.horizontalSingulars s = {a : Person.Category | a.IsSingular ∧ Cysouw2003.HorizontalHomophonyAt s a}

The Explicitness Hierarchy (§4.7, §10.1.7)

inductive Cysouw2003.WeMarking : Type

The marking of 'we', Table 4.2's columns: minimal against augmented inclusive, inclusive against exclusive, or one form.

• minimalAugmented : WeMarking
• inclusiveExclusive : WeMarking
• unified : WeMarking

@[instance_reducible]

instance Cysouw2003.instDecidableEqWeMarking : DecidableEq WeMarking

Equations

• Cysouw2003.instDecidableEqWeMarking x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Cysouw2003.instReprWeMarking : Repr WeMarking

Equations

• Cysouw2003.instReprWeMarking = { reprPrec := Cysouw2003.instReprWeMarking.repr }

def Cysouw2003.instReprWeMarking.repr : WeMarking → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Cysouw2003.instFintypeWeMarking : Fintype WeMarking

Equations

• Cysouw2003.instFintypeWeMarking = { elems := { val := ↑Cysouw2003.WeMarking.enumList, nodup := Cysouw2003.WeMarking.enumList_nodup }, complete := Cysouw2003.instFintypeWeMarking._proof_1 }

def Cysouw2003.weMarking (s : Setoid Person.Category) [DecidableRel ⇑s] : WeMarking

The marking of 'we' in a structure, by whether the cells differ, as chapter 4's division into paradigms with and without an inclusive/exclusive opposition goes (§4.5–4.6 file the Ojibwe and Huave prefixes, whose inclusive is a singular morpheme, under the opposition), and as §4.7 counts any 1+2 against 1+2+3 difference as a minimal/augmented inclusive.

Equations

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

def Cysouw2003.RespectsExplicitnessHierarchy (s : Setoid Person.Category) [DecidableRel ⇑s] : Prop

The hierarchy (4.108), (10.7) as a constraint on which oppositions a paradigm may give up: singulars merge only where groups already merge, and groups merge only once 'we' is one form.

Equations

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

@[instance_reducible]

instance Cysouw2003.instDecidableRespectsExplicitnessHierarchy (s : Setoid Person.Category) [DecidableRel ⇑s] : Decidable (RespectsExplicitnessHierarchy s)

Equations

• Cysouw2003.instDecidableRespectsExplicitnessHierarchy s = id inferInstance

inductive Cysouw2003.Explicitness : Type

The rungs of the hierarchy, Fig. 10.9's stages of person differentiation P0–P4: singular homophony, vertical homophony, and the three markings of 'we'.

• singularHomophony : Explicitness
• verticalHomophony : Explicitness
• we (m : WeMarking) : Explicitness

def Cysouw2003.instDecidableEqExplicitness.decEq (x✝ x✝¹ : Explicitness) : Decidable (x✝ = x✝¹)

Equations

• Cysouw2003.instDecidableEqExplicitness.decEq Cysouw2003.Explicitness.singularHomophony Cysouw2003.Explicitness.singularHomophony = isTrue ⋯
• Cysouw2003.instDecidableEqExplicitness.decEq Cysouw2003.Explicitness.singularHomophony Cysouw2003.Explicitness.verticalHomophony = isFalse Cysouw2003.instDecidableEqExplicitness.decEq._proof_1
• Cysouw2003.instDecidableEqExplicitness.decEq Cysouw2003.Explicitness.singularHomophony (Cysouw2003.Explicitness.we m) = isFalse ⋯
• Cysouw2003.instDecidableEqExplicitness.decEq Cysouw2003.Explicitness.verticalHomophony Cysouw2003.Explicitness.singularHomophony = isFalse Cysouw2003.instDecidableEqExplicitness.decEq._proof_3
• Cysouw2003.instDecidableEqExplicitness.decEq Cysouw2003.Explicitness.verticalHomophony Cysouw2003.Explicitness.verticalHomophony = isTrue ⋯
• Cysouw2003.instDecidableEqExplicitness.decEq Cysouw2003.Explicitness.verticalHomophony (Cysouw2003.Explicitness.we m) = isFalse ⋯
• Cysouw2003.instDecidableEqExplicitness.decEq (Cysouw2003.Explicitness.we m) Cysouw2003.Explicitness.singularHomophony = isFalse ⋯
• Cysouw2003.instDecidableEqExplicitness.decEq (Cysouw2003.Explicitness.we m) Cysouw2003.Explicitness.verticalHomophony = isFalse ⋯
• Cysouw2003.instDecidableEqExplicitness.decEq (Cysouw2003.Explicitness.we a) (Cysouw2003.Explicitness.we b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Cysouw2003.instDecidableEqExplicitness : DecidableEq Explicitness

Equations

• Cysouw2003.instDecidableEqExplicitness = Cysouw2003.instDecidableEqExplicitness.decEq

@[instance_reducible]

instance Cysouw2003.instReprExplicitness : Repr Explicitness

Equations

• Cysouw2003.instReprExplicitness = { reprPrec := Cysouw2003.instReprExplicitness.repr }

def Cysouw2003.instReprExplicitness.repr : Explicitness → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Cysouw2003.instFintypeExplicitness : Fintype Explicitness

Equations

• Cysouw2003.instFintypeExplicitness = Fintype.ofEquiv (Unit ⊕ Unit ⊕ Cysouw2003.WeMarking) Cysouw2003.Explicitness.proxyTypeEquiv

def Cysouw2003.Explicitness.toNat : Explicitness → ℕ

Numeric embedding into ℕ preserving the order.

Equations

• Cysouw2003.Explicitness.singularHomophony.toNat = 0
• Cysouw2003.Explicitness.verticalHomophony.toNat = 1
• (Cysouw2003.Explicitness.we Cysouw2003.WeMarking.unified).toNat = 2
• (Cysouw2003.Explicitness.we Cysouw2003.WeMarking.inclusiveExclusive).toNat = 3
• (Cysouw2003.Explicitness.we Cysouw2003.WeMarking.minimalAugmented).toNat = 4

@[instance_reducible]

instance Cysouw2003.Explicitness.instLinearOrder : LinearOrder Explicitness

Equations

• Cysouw2003.Explicitness.instLinearOrder = LinearOrder.lift' Cysouw2003.Explicitness.toNat Cysouw2003.Explicitness.instLinearOrder._proof_1

theorem Cysouw2003.Explicitness.hierarchy : singularHomophony < verticalHomophony ∧ verticalHomophony < we WeMarking.unified ∧ we WeMarking.unified < we WeMarking.inclusiveExclusive ∧ we WeMarking.inclusiveExclusive < we WeMarking.minimalAugmented

The order of the rungs ((10.7), Fig. 10.4).

def Cysouw2003.explicitness (s : Setoid Person.Category) [DecidableRel ⇑s] : Option Explicitness

The rung of a structure on the hierarchy, the lowest opposition it has given up, for a structure respecting the hierarchy; the others do not fit it (Table 10.4).

Equations

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

def Cysouw2003.numberStage (s : Setoid Person.Category) [DecidableRel ⇑s] : Option Number.Stage

Fig. 10.8's number stages a paradigm without restricted groups can occupy (§10.2): no singular/group opposition at all (N1), a consistent one (N2), and neither on the intermediate rungs of the horizontal hierarchy.

Equations

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

inductive Cysouw2003.RarePattern : Type

The five rare attested patterns of the first person complex (Fig. 3.7).

• pf : RarePattern

  A morpheme for 1+2 and another for 1+2+3 and 1+3 together (Bardi, Kunimaipa, Tiwi).

• pg : RarePattern

  A morpheme for 1+2+3 and another for 1+2 and 1+3 together (Yaouré, Gooniyandi).

• ph : RarePattern

  Minimal and augmented inclusive marked apart, the exclusive by a singular morpheme (Tiwi).

• pi : RarePattern

  1+2 marked by a singular morpheme, 1+2+3 and 1+3 together (Kunimaipa).

• pj : RarePattern

  The inclusive marked by a singular morpheme, the exclusive by its own (Binandere).

@[instance_reducible]

instance Cysouw2003.instDecidableEqRarePattern : DecidableEq RarePattern

Equations

• Cysouw2003.instDecidableEqRarePattern x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Cysouw2003.instReprRarePattern.repr : RarePattern → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Cysouw2003.instReprRarePattern : Repr RarePattern

Equations

• Cysouw2003.instReprRarePattern = { reprPrec := Cysouw2003.instReprRarePattern.repr }

@[instance_reducible]

instance Cysouw2003.instFintypeRarePattern : Fintype RarePattern

Equations

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

def Cysouw2003.RarePattern.labels : RarePattern → Person.Category → ℕ

Fig. 3.7's letters as morpheme classes, 0 the singular class.

Equations

• Cysouw2003.RarePattern.pf.labels Person.Category.minIncl = 1
• Cysouw2003.RarePattern.pf.labels Person.Category.augIncl = 2
• Cysouw2003.RarePattern.pf.labels Person.Category.excl = 2
• Cysouw2003.RarePattern.pg.labels Person.Category.minIncl = 1
• Cysouw2003.RarePattern.pg.labels Person.Category.augIncl = 2
• Cysouw2003.RarePattern.pg.labels Person.Category.excl = 1
• Cysouw2003.RarePattern.ph.labels Person.Category.minIncl = 1
• Cysouw2003.RarePattern.ph.labels Person.Category.augIncl = 2
• Cysouw2003.RarePattern.pi.labels Person.Category.augIncl = 1
• Cysouw2003.RarePattern.pi.labels Person.Category.excl = 1
• Cysouw2003.RarePattern.pj.labels Person.Category.excl = 1
• x✝¹.labels x✝ = 0

@[reducible, inline]

abbrev Cysouw2003.RarePattern.pattern (q : RarePattern) : Person.Clusivity.Pattern

The rare pattern as a setoid on the four cells.

Equations

• q.pattern = Setoid.ker (q.labels ∘ Subtype.val)

theorem Cysouw2003.RarePattern.pattern_injective : Function.Injective pattern

The rare patterns are distinct from each other.

theorem Cysouw2003.RarePattern.pattern_ne (q : RarePattern) (t : Person.Clusivity) : q.pattern ≠ t.toPattern

The rare patterns are distinct from the common types, so ten of the fifteen patterns are attested (Figs. 3.1–3.2).

The named structures of chapter 4

inductive Cysouw2003.Kind : Type

The structures chapter 4 names after an exemplar: eight common (§4.3.2–5, §4.5.2–4, §4.5.6) and five semi-common (§4.4.2–4, §4.5.5).

• latin : Kind
• sinhalese : Kind
• berik : Kind
• maricopa : Kind
• maranao : Kind
• mandara : Kind
• tupiGuarani : Kind
• kwakiutl : Kind
• sierraPopoluca : Kind
• slave : Kind
• nezPerce : Kind
• kombai : Kind
• omie : Kind

@[instance_reducible]

instance Cysouw2003.instDecidableEqKind : DecidableEq Kind

Equations

• Cysouw2003.instDecidableEqKind x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Cysouw2003.instReprKind.repr : Kind → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Cysouw2003.instReprKind.repr Cysouw2003.Kind.latin prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Cysouw2003.Kind.latin")).group prec✝
• Cysouw2003.instReprKind.repr Cysouw2003.Kind.sinhalese prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Cysouw2003.Kind.sinhalese")).group prec✝
• Cysouw2003.instReprKind.repr Cysouw2003.Kind.berik prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Cysouw2003.Kind.berik")).group prec✝
• Cysouw2003.instReprKind.repr Cysouw2003.Kind.maricopa prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Cysouw2003.Kind.maricopa")).group prec✝
• Cysouw2003.instReprKind.repr Cysouw2003.Kind.maranao prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Cysouw2003.Kind.maranao")).group prec✝
• Cysouw2003.instReprKind.repr Cysouw2003.Kind.mandara prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Cysouw2003.Kind.mandara")).group prec✝
• Cysouw2003.instReprKind.repr Cysouw2003.Kind.tupiGuarani prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Cysouw2003.Kind.tupiGuarani")).group prec✝
• Cysouw2003.instReprKind.repr Cysouw2003.Kind.kwakiutl prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Cysouw2003.Kind.kwakiutl")).group prec✝
• Cysouw2003.instReprKind.repr Cysouw2003.Kind.slave prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Cysouw2003.Kind.slave")).group prec✝
• Cysouw2003.instReprKind.repr Cysouw2003.Kind.nezPerce prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Cysouw2003.Kind.nezPerce")).group prec✝
• Cysouw2003.instReprKind.repr Cysouw2003.Kind.kombai prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Cysouw2003.Kind.kombai")).group prec✝
• Cysouw2003.instReprKind.repr Cysouw2003.Kind.omie prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Cysouw2003.Kind.omie")).group prec✝

@[instance_reducible]

instance Cysouw2003.instReprKind : Repr Kind

Equations

• Cysouw2003.instReprKind = { reprPrec := Cysouw2003.instReprKind.repr }

@[instance_reducible]

instance Cysouw2003.instFintypeKind : Fintype Kind

Equations

• Cysouw2003.instFintypeKind = { elems := { val := ↑Cysouw2003.Kind.enumList, nodup := Cysouw2003.Kind.enumList_nodup }, complete := Cysouw2003.instFintypeKind._proof_1 }

def Cysouw2003.Kind.labels : Kind → Person.Category → ℕ

Morpheme classes of each named structure (Figs. 4.9–4.11); the wildcard covers the three 'we' cells.

Equations

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

def Cysouw2003.Kind.names : List (String × Kind)

The names the rows use.

Equations

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

@[reducible, inline]

abbrev Cysouw2003.Kind.pattern (k : Kind) : Setoid Person.Category

The paradigmatic structure of the named kind (Figs. 4.9–4.11).

Equations

• k.pattern = Morphology.syncretism k.labels

theorem Cysouw2003.Kind.pattern_injective : Function.Injective pattern

The named structures are distinct.

theorem Cysouw2003.Kind.hasClusivity_pattern : HasClusivity maricopa.pattern Person.Clusivity.noWe ∧ HasClusivity sierraPopoluca.pattern Person.Clusivity.onlyInclusive ∧ HasClusivity maranao.pattern Person.Clusivity.minimalAugmented ∧ (∀ k ∈ [mandara, tupiGuarani, kwakiutl], HasClusivity k.pattern Person.Clusivity.inclusiveExclusive) ∧ ∀ k ∈ [latin, sinhalese, berik, slave, nezPerce, kombai, omie], HasClusivity k.pattern Person.Clusivity.unifiedWe

Their first person complexes (Fig. 4.4): the Maricopa type has no 'we', the Sierra Popoluca type only an inclusive, the Maranao type a minimal/augmented one, the other types with an inclusive/exclusive opposition are inclusive/exclusive and the rest unified.

theorem Cysouw2003.Kind.respectsHorizontalHierarchy_pattern (k : Kind) : RespectsHorizontalHierarchy k.pattern

Every named structure respects the horizontal hierarchy.

theorem Cysouw2003.Kind.horizontalSingulars_inclusiveExclusive : horizontalSingulars mandara.pattern ⊂ horizontalSingulars tupiGuarani.pattern ∧ horizontalSingulars tupiGuarani.pattern ⊂ horizontalSingulars kwakiutl.pattern ∧ horizontalSingulars kwakiutl.pattern ⊂ horizontalSingulars sierraPopoluca.pattern

Hierarchy I, with an inclusive/exclusive opposition (Fig. 10.2): Mandara < Tupí-Guaraní < Kwakiutl < Sierra Popoluca, the last rung the exclusive marked like the speaker.

theorem Cysouw2003.Kind.horizontalSingulars_unified : horizontalSingulars latin.pattern ⊂ horizontalSingulars sinhalese.pattern ∧ horizontalSingulars sinhalese.pattern ⊂ horizontalSingulars berik.pattern ∧ horizontalSingulars berik.pattern ⊂ horizontalSingulars maricopa.pattern

Hierarchy II, without (Fig. 10.3): Latin < Sinhalese < Berik < Maricopa.

theorem Cysouw2003.Kind.respectsExplicitnessHierarchy_pattern (k : Kind) : RespectsExplicitnessHierarchy k.pattern

Every named structure respects the explicitness hierarchy.

theorem Cysouw2003.Kind.explicitness_pattern : explicitness slave.pattern = some Explicitness.verticalHomophony ∧ explicitness latin.pattern = some (Explicitness.we WeMarking.unified) ∧ explicitness maricopa.pattern = some (Explicitness.we WeMarking.unified) ∧ explicitness mandara.pattern = some (Explicitness.we WeMarking.inclusiveExclusive) ∧ explicitness sierraPopoluca.pattern = some (Explicitness.we WeMarking.inclusiveExclusive) ∧ explicitness maranao.pattern = some (Explicitness.we WeMarking.minimalAugmented)

Fig. 10.7's columns: vertical homophony (the Slave type) at P1, unified-we and no-we at P2, inclusive/exclusive and only-inclusive at P3, minimal/augmented at P4.

theorem Cysouw2003.Kind.numberStage_pattern : numberStage maricopa.pattern = some Number.Stage.N1 ∧ numberStage sierraPopoluca.pattern = some Number.Stage.N1 ∧ (∀ k ∈ [slave, latin, mandara, maranao], numberStage k.pattern = some Number.Stage.N2) ∧ numberStage sinhalese.pattern = none

Fig. 10.7's rows: no-we and only-inclusive at N1, the Slave, Latin, Mandara and Maranao types at N2, and the Sinhalese type between the two.

The paradigms of chapters 3 and 4

inductive Cysouw2003.Marking : Type

Morphological status of a paradigm (§1.2.4).

• independent : Marking
• inflectional : Marking

@[instance_reducible]

instance Cysouw2003.instDecidableEqMarking : DecidableEq Marking

Equations

• Cysouw2003.instDecidableEqMarking x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Cysouw2003.instReprMarking.repr : Marking → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Cysouw2003.instReprMarking : Repr Marking

Equations

• Cysouw2003.instReprMarking = { reprPrec := Cysouw2003.instReprMarking.repr }

inductive Cysouw2003.Ubiquity : Type

§4.2's frequency classes.

• common : Ubiquity
• semiCommon : Ubiquity
• rare : Ubiquity

@[instance_reducible]

instance Cysouw2003.instDecidableEqUbiquity : DecidableEq Ubiquity

Equations

• Cysouw2003.instDecidableEqUbiquity x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Cysouw2003.instReprUbiquity : Repr Ubiquity

Equations

• Cysouw2003.instReprUbiquity = { reprPrec := Cysouw2003.instReprUbiquity.repr }

def Cysouw2003.instReprUbiquity.repr : Ubiquity → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Cysouw2003.instReprUbiquity.repr Cysouw2003.Ubiquity.common prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Cysouw2003.Ubiquity.common")).group prec✝
• Cysouw2003.instReprUbiquity.repr Cysouw2003.Ubiquity.rare prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Cysouw2003.Ubiquity.rare")).group prec✝

structure Cysouw2003.Row : Type

A paradigm the book prints, its eight forms and the book's classification of it.

• id : String

  The example id.

• forms : Person.Category → String

  The form of each cell, block by block.

• chapter : ℕ

  The chapter printing it.

• marking : Option Marking

  Independent or inflectional, where the caption says.

• kind : Option Kind

  The named type the book files it under.

• ubiquity : Ubiquity

  Common, semi-common or rare.

• rare : Option RarePattern

  The rare 'we' pattern it illustrates (§3.6.6).

@[reducible, inline]

abbrev Cysouw2003.Row.syncretism (r : Row) : Setoid Person.Category

The paradigmatic structure of the row.

Equations

• r.syncretism = Morphology.syncretism r.forms

@[reducible, inline]

abbrev Cysouw2003.Row.wePattern (r : Row) : Person.Clusivity.Pattern

The row's pattern of the first person complex.

Equations

• r.wePattern = Cysouw2003.wePattern r.syncretism

def Cysouw2003.Row.ofExample? (e : Data.Examples.LinguisticExample) : Option Row

The row of an example.

Equations

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

theorem Cysouw2003.Row.isSome_ofExample (e : Data.Examples.LinguisticExample) : e ∈ Examples.all → (ofExample? e).isSome = true

def Cysouw2003.rows : List Row

The printed paradigms.

Equations

• Cysouw2003.rows = List.filterMap Cysouw2003.Row.ofExample? Cysouw2003.Examples.all

theorem Cysouw2003.rows_kind (r : Row) : r ∈ rows → ∀ (k : Kind), r.kind = some k → r.syncretism = k.pattern

Every paradigm the book files under a named type has that type's structure.

theorem Cysouw2003.rows_rare (r : Row) : r ∈ rows → ∀ (q : RarePattern), r.rare = some q → r.wePattern = q.pattern

Every paradigm of §3.6.6 has the rare pattern it illustrates.

theorem Cysouw2003.rows_hasClusivity (r : Row) : r ∈ rows → r.chapter = 4 → ∃ (t : Person.Clusivity), HasClusivity r.syncretism t

Every chapter-4 paradigm has one of the five common types, §4.2 having set the rare patterns aside.

theorem Cysouw2003.rows_specializedInclusive_of_specializedExclusive (r : Row) : r ∈ rows → r.rare ≠ some RarePattern.pj → r.wePattern.SpecializedExclusive → r.wePattern.SpecializedInclusive

Addressee inclusion implication I (3.23) over the printed paradigms, Binandere the one exception.

theorem Cysouw2003.binandere : ∃ r ∈ rows, r.rare = some RarePattern.pj ∧ r.wePattern.SpecializedExclusive ∧ ¬r.wePattern.SpecializedInclusive

theorem Cysouw2003.rows_specializedExclusive_of_splitInclusive (r : Row) : r ∈ rows → r.rare = none ∨ r.rare = some RarePattern.pi ∨ r.rare = some RarePattern.pj → r.wePattern.SplitInclusive → r.wePattern.SpecializedExclusive

Addressee inclusion implication II (3.24) over the printed paradigms. Its exceptions are the rare patterns that mark the two inclusives apart: (Pf) and (Pg), which the book names, and (Ph), whose paradigm (3.20) the book's list overlooks.

theorem Cysouw2003.rows_splitInclusive_not_specializedExclusive (r : Row) : r ∈ rows → r.rare = some RarePattern.pf ∨ r.rare = some RarePattern.pg ∨ r.rare = some RarePattern.ph → r.wePattern.SplitInclusive ∧ ¬r.wePattern.SpecializedExclusive

theorem Cysouw2003.english_inflection_noWe : ∃ r ∈ rows, r.id = "cysouw2003_4.68" ∧ HasClusivity r.syncretism Person.Clusivity.noWe

The strong universal 'we' (3.7) fails: the English inflection (4.68) has no 'we'.

theorem Cysouw2003.rows_inflectional_of_singularHomophony (r : Row) : r ∈ rows → SingularHomophony r.syncretism → r.marking = some Marking.inflectional

The Homophony Implication (2.14), (10.4) over the printed paradigms: singular homophony only in inflectional paradigms. The two independent-pronoun exceptions the book reports, Qawesqar and Winnebago, are described in chapter 2 without a printed paradigm.

theorem Cysouw2003.rows_rare_of_not_respectsHorizontalHierarchy (r : Row) : r ∈ rows → ¬RespectsHorizontalHierarchy r.syncretism → r.ubiquity = Ubiquity.rare

The Horizontal Homophony Hierarchy holds of every common and semi-common paradigm; its exceptions, the diagonal cases among them, are rare (§4.3.6, §4.5.7).

theorem Cysouw2003.rows_respectsHorizontalHierarchy_of_minimalAugmented (r : Row) : r ∈ rows → r.chapter = 4 → weMarking r.syncretism = WeMarking.minimalAugmented → RespectsHorizontalHierarchy r.syncretism

Table 4.2's first "nonesuch": under a minimal/augmented inclusive no chapter-4 paradigm breaks the horizontal hierarchy.

theorem Cysouw2003.rows_unified_of_singularHomophony (r : Row) : r ∈ rows → r.chapter = 4 → SingularHomophony r.syncretism → weMarking r.syncretism = WeMarking.unified

Table 4.2's second "nonesuch": no singular homophony under any inclusive/exclusive opposition.

theorem Cysouw2003.rows_rare_of_not_respectsExplicitnessHierarchy (r : Row) : r ∈ rows → ¬RespectsExplicitnessHierarchy r.syncretism → r.ubiquity = Ubiquity.rare

The Explicitness Hierarchy holds of every common and semi-common paradigm.

theorem Cysouw2003.rows_rare_of_singularHomophony_without_vertical (r : Row) : r ∈ rows → SingularHomophony r.syncretism → ¬VerticalHomophony r.syncretism → r.ubiquity = Ubiquity.rare

Singular homophony without vertical homophony is rare, the European paradigms of §4.3.6 (§4.7).

theorem Cysouw2003.rows_rare_of_verticalHomophony_inclusiveExclusive (r : Row) : r ∈ rows → VerticalHomophony r.syncretism → weMarking r.syncretism ≠ WeMarking.unified → r.ubiquity = Ubiquity.rare

Vertical homophony under an inclusive/exclusive opposition is rare (§4.6, Table 4.2).

theorem Cysouw2003.explicitness_fig10_4 : ∃ waskia ∈ rows, ∃ una ∈ rows, waskia.id = "cysouw2003_4.66" ∧ una.id = "cysouw2003_4.64" ∧ explicitness waskia.syncretism = some Explicitness.singularHomophony ∧ explicitness una.syncretism = some Explicitness.verticalHomophony ∧ explicitness Kind.latin.pattern = some (Explicitness.we WeMarking.unified) ∧ explicitness Kind.mandara.pattern = some (Explicitness.we WeMarking.inclusiveExclusive) ∧ explicitness Kind.maranao.pattern = some (Explicitness.we WeMarking.minimalAugmented)

Fig. 10.4's exemplars occupy the five rungs: the Waskia present (4.66), the Una undergoer suffixes (4.64), then the Latin, Mandara and Maranao types.

Two paradigms from the Fragments

def Cysouw2003.englishSubject (c : Person.Category) : Option String

The English subject pronouns by referential category: the form of the fragment's non-accusative entry with the category's person, clusivity collapsed, and number.

Equations

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

theorem Cysouw2003.english_pronouns : ∃ r ∈ rows, r.id = "cysouw2003_4.19" ∧ Morphology.syncretism englishSubject = r.syncretism

The English pronouns have the structure of (4.19).

theorem Cysouw2003.english_not_respectsHorizontalHierarchy : ¬RespectsHorizontalHierarchy (Morphology.syncretism englishSubject)

Horizontal homophony in the second person only: the English pronouns break the horizontal hierarchy (§4.3.6).

def Cysouw2003.tagalogAng (c : Person.Category) : Option String

The Tagalog ang series by referential category.

Equations

• Cysouw2003.tagalogAng c = Option.map (fun (x : PersonalPronoun) => x.form) (List.find? (fun (e : PersonalPronoun) => decide (e.category = some c)) Tagalog.angSeries)

theorem Cysouw2003.tagalog_maranao : Morphology.syncretism tagalogAng = Kind.maranao.pattern

The Tagalog ang series is a Maranao-type paradigm (§4.5.2).