Cysouw (2003): The paradigmatic structure of person marking

The paradigmatic structures of [Cys03]. A person paradigm fills one slot with a closed set of markers over eight referential categories, the three singular participants and the five attested groups, and its structure is which categories share a morpheme: a setoid on Person.Category, the syncretism of the paradigm's cell-to-form map. The book's kinds of homophony, its types of the first person complex and its named structures are properties of that setoid.

Two of the book's generalizations are implicational hierarchies, and each is a lower set of a chain: horizontal homophony reaches the singular persons from the third upwards, and a paradigm gives up its oppositions from the first person complex outwards. The order of asking about the first person complex is the order of implication among the five types, and the order of giving up oppositions the order of implication among the common paradigms the book prints. Every paradigm the book prints is checked against its classification and against the hierarchies, with the exceptions the book names.

Main definitions

• Cysouw2003.Clusivity: the five common marking types of the first person complex, with their patterns Clusivity.toPattern, setoids on the four speaker-including cells.
• Clusivity.Question, Pattern.profile, Pattern.RespectsHierarchy: the four questions that tell the types apart, a pattern's positive answers, and the First Person Hierarchy.
• Cysouw2003.Structure: a paradigmatic structure, a setoid on Person.Category.

Main results

• Clusivity.ofAttribute_profile_le_iff: the order of asking is the order of implication among the five types' answers.
• Clusivity.rung_bijective: the types are exactly the lower sets of the questions.
• Clusivity.le_iff_profile_subset: the hierarchy is the order of the profiles.
• ofAttribute_givenUp_le_iff: the Explicitness Hierarchy is the order of implication among the common and semi-common paradigms the book prints.

Implementation notes

• The typology of the first person complex is finer than the WALS chapter on clusivity [Cys13], which collapses minimal/augmented into inclusive/exclusive and whose "no 'we'" value is the absence of any first-person non-singular, not noWe.

• 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 the book's letter labellings, of which only the kernel matters.

• The book's 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 and the Dual Homophony Implication need cells for restricted groups.
• The zero implications of chapter 10 need zero marking read off the forms.

References

• M. Cysouw, The Paradigmatic Structure of Person Marking (2003)
• M. Cysouw, Inclusive/Exclusive Distinction in Independent Pronouns (2013)

Marking types of the first person complex

inductive Cysouw2003.Clusivity : Type

The five common marking types of the first person complex, the common five of the fifteen possible patterns.

• noWe : Clusivity

  No 'we' category has a specialized morpheme, as in the English inflection (Pb).

• unifiedWe : Clusivity

  All three 'we' categories share one specialized morpheme, as English we (Pa).

• onlyInclusive : Clusivity

  1+2 and 1+2+3 share a specialized morpheme and 1+3 has none, as in Maká (Pc).

• inclusiveExclusive : Clusivity

  1+2 and 1+2+3 share one specialized morpheme and 1+3 has another, as in Apalai (Pd).

• minimalAugmented : Clusivity

  All three 'we' categories have separate specialized morphemes, as Ilocano ta tayo mi (Pe).

@[instance_reducible]

instance Cysouw2003.instDecidableEqClusivity : DecidableEq Clusivity

Equations

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

@[instance_reducible]

instance Cysouw2003.instReprClusivity : Repr Clusivity

Equations

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

def Cysouw2003.instReprClusivity.repr : Clusivity → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Cysouw2003.instFintypeClusivity : Fintype Clusivity

Equations

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

@[reducible, inline]

abbrev Cysouw2003.Clusivity.Cell : Type

The four cells of a pattern, the categories that include the speaker. The singular speaker stands for every singular morpheme.

Equations

• Cysouw2003.Clusivity.Cell = { c : Person.Category // c.IncludesSpeaker }

def Cysouw2003.Clusivity.Cell.speaker : Cell

The singular speaker.

Equations

• Cysouw2003.Clusivity.Cell.speaker = ⟨Person.Category.speaker, Cysouw2003.Clusivity.Cell.speaker._proof_1⟩

def Cysouw2003.Clusivity.Cell.speakerAddressee : Cell

The minimal inclusive 1+2.

Equations

• Cysouw2003.Clusivity.Cell.speakerAddressee = ⟨Person.Category.speakerAddressee, Cysouw2003.Clusivity.Cell.speakerAddressee._proof_1⟩

def Cysouw2003.Clusivity.Cell.speakerAddresseeOthers : Cell

The augmented inclusive 1+2+3.

Equations

• Cysouw2003.Clusivity.Cell.speakerAddresseeOthers = ⟨Person.Category.speakerAddresseeOthers, Cysouw2003.Clusivity.Cell.speakerAddresseeOthers._proof_1⟩

def Cysouw2003.Clusivity.Cell.speakerOthers : Cell

The exclusive 1+3.

Equations

• Cysouw2003.Clusivity.Cell.speakerOthers = ⟨Person.Category.speakerOthers, Cysouw2003.Clusivity.Cell.speakerOthers._proof_1⟩

@[reducible, inline]

abbrev Cysouw2003.Clusivity.Pattern : Type

A marking pattern of the first person complex, the letter notation as a setoid on the four cells.

Equations

• Cysouw2003.Clusivity.Pattern = Setoid Cysouw2003.Clusivity.Cell

inductive Cysouw2003.Clusivity.Question : Type

The four questions that classify the patterns, in the order the hierarchy asks them.

• specializedWe : Question

  Is there any specialized form for 'we'?

• specializedInclusive : Question

  Is the inclusive specialized?

• specializedExclusive : Question

  Is the exclusive specialized?

• splitInclusive : Question

  Is the inclusive split?

@[instance_reducible]

instance Cysouw2003.Clusivity.instDecidableEqQuestion : DecidableEq Question

Equations

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

@[instance_reducible]

instance Cysouw2003.Clusivity.instReprQuestion : Repr Question

Equations

• Cysouw2003.Clusivity.instReprQuestion = { reprPrec := Cysouw2003.Clusivity.instReprQuestion.repr }

def Cysouw2003.Clusivity.instReprQuestion.repr : Question → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Cysouw2003.Clusivity.instFintypeQuestion : Fintype Question

Equations

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

def Cysouw2003.Clusivity.Question.rank : Question → Fin 4

Position in the order of asking.

Equations

• Cysouw2003.Clusivity.Question.specializedWe.rank = 0
• Cysouw2003.Clusivity.Question.specializedInclusive.rank = 1
• Cysouw2003.Clusivity.Question.specializedExclusive.rank = 2
• Cysouw2003.Clusivity.Question.splitInclusive.rank = 3

@[instance_reducible]

instance Cysouw2003.Clusivity.Question.instLinearOrder : LinearOrder Question

Equations

• Cysouw2003.Clusivity.Question.instLinearOrder = LinearOrder.lift' Cysouw2003.Clusivity.Question.rank Cysouw2003.Clusivity.Question.instLinearOrder._proof_1

def Cysouw2003.Clusivity.Pattern.SpecializedWe (r : Pattern) : Prop

Some 'we' cell is not marked like the speaker.

Equations

• r.SpecializedWe = ∃ (c : Cysouw2003.Clusivity.Cell), (↑c).IsFirstPersonComplex ∧ ¬r c Cysouw2003.Clusivity.Cell.speaker

def Cysouw2003.Clusivity.Pattern.SpecializedInclusive (r : Pattern) : Prop

Both inclusive cells are marked neither like the speaker nor like the exclusive.

Equations

• r.SpecializedInclusive = ∀ (c : Cysouw2003.Clusivity.Cell), (↑c).IsInclusive → ¬r c Cysouw2003.Clusivity.Cell.speaker ∧ ¬r c Cysouw2003.Clusivity.Cell.speakerOthers

def Cysouw2003.Clusivity.Pattern.SpecializedExclusive (r : Pattern) : Prop

The exclusive is marked neither like the speaker nor like an inclusive cell.

Equations

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

def Cysouw2003.Clusivity.Pattern.SplitInclusive (r : Pattern) : Prop

Minimal and augmented inclusive are marked apart and neither like the speaker.

Equations

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

def Cysouw2003.Clusivity.Pattern.Answers (r : Pattern) : Question → Prop

The pattern answers the question positively.

Equations

• r.Answers Cysouw2003.Clusivity.Question.specializedWe = r.SpecializedWe
• r.Answers Cysouw2003.Clusivity.Question.specializedInclusive = r.SpecializedInclusive
• r.Answers Cysouw2003.Clusivity.Question.specializedExclusive = r.SpecializedExclusive
• r.Answers Cysouw2003.Clusivity.Question.splitInclusive = r.SplitInclusive

@[instance_reducible]

instance Cysouw2003.Clusivity.Pattern.instDecidableSpecializedWe (r : Pattern) [DecidableRel ⇑r] : Decidable r.SpecializedWe

Equations

• r.instDecidableSpecializedWe = id inferInstance

@[instance_reducible]

instance Cysouw2003.Clusivity.Pattern.instDecidableSpecializedInclusive (r : Pattern) [DecidableRel ⇑r] : Decidable r.SpecializedInclusive

Equations

• r.instDecidableSpecializedInclusive = id inferInstance

@[instance_reducible]

instance Cysouw2003.Clusivity.Pattern.instDecidableSpecializedExclusive (r : Pattern) [DecidableRel ⇑r] : Decidable r.SpecializedExclusive

Equations

• r.instDecidableSpecializedExclusive = id inferInstance

@[instance_reducible]

instance Cysouw2003.Clusivity.Pattern.instDecidableSplitInclusive (r : Pattern) [DecidableRel ⇑r] : Decidable r.SplitInclusive

Equations

• r.instDecidableSplitInclusive = id inferInstance

@[instance_reducible]

instance Cysouw2003.Clusivity.Pattern.instDecidablePredQuestionAnswers (r : Pattern) [DecidableRel ⇑r] : DecidablePred r.Answers

Equations

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

def Cysouw2003.Clusivity.Pattern.profile (r : Pattern) [DecidableRel ⇑r] : Finset Question

The questions the pattern answers positively.

Equations

• r.profile = Finset.filter r.Answers Finset.univ

def Cysouw2003.Clusivity.Pattern.RespectsHierarchy (r : Pattern) [DecidableRel ⇑r] : Prop

The pattern fits the hierarchy when, read as conditions, each positive answer requires the ones before it, so that the profile is an initial segment of the questions.

Equations

• r.RespectsHierarchy = IsLowerSet ↑r.profile

@[instance_reducible]

instance Cysouw2003.Clusivity.Pattern.instDecidableRespectsHierarchy (r : Pattern) [DecidableRel ⇑r] : Decidable r.RespectsHierarchy

Equations

• r.instDecidableRespectsHierarchy = { decide := decide (∀ a ∈ r.profile, ∀ b ≤ a, b ∈ r.profile), reflects_decide := ⋯ }

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

The letters as morpheme classes, 0 being the class of the singular speaker, the dash, in which every category outside the first person complex is placed.

Equations

• Cysouw2003.Clusivity.unifiedWe.labels Person.Category.speakerAddressee = 1
• Cysouw2003.Clusivity.unifiedWe.labels Person.Category.speakerAddresseeOthers = 1
• Cysouw2003.Clusivity.unifiedWe.labels Person.Category.speakerOthers = 1
• Cysouw2003.Clusivity.onlyInclusive.labels Person.Category.speakerAddressee = 1
• Cysouw2003.Clusivity.onlyInclusive.labels Person.Category.speakerAddresseeOthers = 1
• Cysouw2003.Clusivity.inclusiveExclusive.labels Person.Category.speakerAddressee = 1
• Cysouw2003.Clusivity.inclusiveExclusive.labels Person.Category.speakerAddresseeOthers = 1
• Cysouw2003.Clusivity.inclusiveExclusive.labels Person.Category.speakerOthers = 2
• Cysouw2003.Clusivity.minimalAugmented.labels Person.Category.speakerAddressee = 1
• Cysouw2003.Clusivity.minimalAugmented.labels Person.Category.speakerAddresseeOthers = 2
• Cysouw2003.Clusivity.minimalAugmented.labels Person.Category.speakerOthers = 3
• x✝¹.labels x✝ = 0

@[reducible, inline]

abbrev Cysouw2003.Clusivity.toPattern (t : Clusivity) : Pattern

The type's pattern, its column of letters as a setoid on the four cells.

Equations

• t.toPattern = Setoid.ker (t.labels ∘ Subtype.val)

theorem Cysouw2003.Clusivity.toPattern_injective : Function.Injective toPattern

The five patterns are distinct.

@[reducible, inline]

abbrev Cysouw2003.Clusivity.profile (t : Clusivity) : Finset Question

The questions a type answers positively.

Equations

• t.profile = t.toPattern.profile

theorem Cysouw2003.Clusivity.ofAttribute_profile_le_iff {q q' : Question} : Concept.ofAttribute (fun (t : Clusivity) (q : Question) => q ∈ t.profile) q' ≤ Concept.ofAttribute (fun (t : Clusivity) (q : Question) => q ∈ t.profile) q ↔ q ≤ q'

The order of asking is the order of implication among the five types, one question coming before another exactly when every type that answers the second positively answers the first so.

theorem Cysouw2003.Clusivity.profile_isLowerSet (t : Clusivity) : IsLowerSet ↑t.profile

Every common type fits the hierarchy, since a specialized exclusive requires a specialized inclusive and a split inclusive a specialized exclusive, the two addressee inclusion implications.

def Cysouw2003.Clusivity.rung (t : Clusivity) : { S : Finset Question // IsLowerSet ↑S }

The rung of a type is its profile, a lower set of the questions.

Equations

• t.rung = ⟨t.profile, ⋯⟩

theorem Cysouw2003.Clusivity.rung_bijective : Function.Bijective rung

The common types are exactly the rungs of the hierarchy, one for each lower set of the questions.

@[instance_reducible]

instance Cysouw2003.Clusivity.instLinearOrder : LinearOrder Clusivity

In the First Person Hierarchy a type precedes another when it answers fewer of the questions, ordering no-we, unified-we, only-inclusive, inclusive/exclusive and minimal/augmented.

Equations

• Cysouw2003.Clusivity.instLinearOrder = LinearOrder.lift' (fun (t : Cysouw2003.Clusivity) => t.profile.card) Cysouw2003.Clusivity.instLinearOrder._proof_2

theorem Cysouw2003.Clusivity.le_iff_profile_subset {s t : Clusivity} : s ≤ t ↔ s.profile ⊆ t.profile

Along the hierarchy each type's profile extends its predecessor's.

theorem Cysouw2003.Clusivity.profile_monotone : Monotone profile

theorem Cysouw2003.Clusivity.onlyInclusive_profile : onlyInclusive.profile = {Question.specializedWe, Question.specializedInclusive}

The converse of the first addressee inclusion implication fails at only-inclusive.

Paradigmatic structures

@[reducible, inline]

abbrev Cysouw2003.Structure : Type

A paradigmatic structure records which of the eight referential categories share a morpheme.

Equations

• Cysouw2003.Structure = Setoid Person.Category

@[reducible, inline]

abbrev Cysouw2003.Singular : Type

The singular categories are ordered by person prominence, the order in which horizontal homophony reaches them, the third person first and the first person last.

Equations

• Cysouw2003.Singular = { c : Person.Category // c.IsSingular }

@[instance_reducible]

instance Cysouw2003.instLinearOrderSingular : LinearOrder Singular

Equations

• Cysouw2003.instLinearOrderSingular = LinearOrder.lift' (fun (a : Cysouw2003.Singular) => (↑a).person.prominence) Cysouw2003.instLinearOrderSingular._proof_1

inductive Cysouw2003.WeMarking : Type

The marking of 'we', the columns of the book's Table 4.2, opposes minimal to augmented inclusive, or inclusive to exclusive, or has 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 }

inductive Cysouw2003.Opposition : Type

The oppositions a paradigm gives up, in the order the Explicitness Hierarchy says it gives them up, are the two inside the first person complex, then one between groups, then one between singulars.

• minimalAugmented : Opposition
• inclusiveExclusive : Opposition
• group : Opposition
• singular : Opposition

@[instance_reducible]

instance Cysouw2003.instDecidableEqOpposition : DecidableEq Opposition

Equations

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

def Cysouw2003.instReprOpposition.repr : Opposition → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Cysouw2003.instReprOpposition : Repr Opposition

Equations

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

@[instance_reducible]

instance Cysouw2003.instFintypeOpposition : Fintype Opposition

Equations

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

def Cysouw2003.Opposition.rank : Opposition → Fin 4

Position in the order of giving up.

Equations

• Cysouw2003.Opposition.minimalAugmented.rank = 0
• Cysouw2003.Opposition.inclusiveExclusive.rank = 1
• Cysouw2003.Opposition.group.rank = 2
• Cysouw2003.Opposition.singular.rank = 3

@[instance_reducible]

instance Cysouw2003.Opposition.instLinearOrder : LinearOrder Opposition

Equations

• Cysouw2003.Opposition.instLinearOrder = LinearOrder.lift' Cysouw2003.Opposition.rank Cysouw2003.Opposition.instLinearOrder._proof_1

inductive Cysouw2003.NumberStage : Type

The rows of the cognitive map, the stages of the hierarchical tree of number oppositions (Figure 10.8).

• N1 : NumberStage

  N1 paradigms do not distinguish number.

• N2 : NumberStage

  N2 paradigms consistently oppose singular to group marking.

• N3 : NumberStage

  N3 paradigms also mark a restricted group, the dual or the inclusive trial of the unit-augmented paradigm.

• N4 : NumberStage

  N4 paradigms also mark a small group, the paucal.

@[instance_reducible]

instance Cysouw2003.instDecidableEqNumberStage : DecidableEq NumberStage

Equations

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

def Cysouw2003.instReprNumberStage.repr : NumberStage → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Cysouw2003.instReprNumberStage : Repr NumberStage

Equations

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

Kinds of homophony

def Cysouw2003.Structure.SingularHomophony (s : Structure) : Prop

Two singular categories share a morpheme.

Equations

• s.SingularHomophony = ∃ (a : Cysouw2003.Singular) (b : Cysouw2003.Singular), a ≠ b ∧ s ↑a ↑b

def Cysouw2003.Structure.HorizontalHomophony (s : Structure) : Prop

A singular category shares a morpheme with a group.

Equations

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

def Cysouw2003.Structure.HorizontalHomophonyAt (s : Structure) (a : Singular) : 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.

Equations

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

def Cysouw2003.Structure.DiagonalHomophony (s : Structure) : Prop

A singular category shares a morpheme with a group of another person.

Equations

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

def Cysouw2003.Structure.VerticalHomophony (s : Structure) : Prop

Two groups share a morpheme, homophony inside the first person complex not counted.

Equations

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

theorem Cysouw2003.Structure.DiagonalHomophony.horizontalHomophony {s : Structure} (h : s.DiagonalHomophony) : s.HorizontalHomophony

Diagonal homophony is horizontal.

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

A category is specialized when it shares no morpheme with a singular one.

Equations

• s.Specialized c = ∀ (x : Cysouw2003.Singular), ¬s c ↑x

@[instance_reducible]

instance Cysouw2003.Structure.instDecidableSingularHomophony (s : Structure) [DecidableRel ⇑s] : Decidable s.SingularHomophony

Equations

• s.instDecidableSingularHomophony = id inferInstance

@[instance_reducible]

instance Cysouw2003.Structure.instDecidableHorizontalHomophony (s : Structure) [DecidableRel ⇑s] : Decidable s.HorizontalHomophony

Equations

• s.instDecidableHorizontalHomophony = id inferInstance

@[instance_reducible]

instance Cysouw2003.Structure.instDecidableHorizontalHomophonyAt (s : Structure) [DecidableRel ⇑s] (a : Singular) : Decidable (s.HorizontalHomophonyAt a)

Equations

• s.instDecidableHorizontalHomophonyAt a = id inferInstance

@[instance_reducible]

instance Cysouw2003.Structure.instDecidableDiagonalHomophony (s : Structure) [DecidableRel ⇑s] : Decidable s.DiagonalHomophony

Equations

• s.instDecidableDiagonalHomophony = id inferInstance

@[instance_reducible]

instance Cysouw2003.Structure.instDecidableVerticalHomophony (s : Structure) [DecidableRel ⇑s] : Decidable s.VerticalHomophony

Equations

• s.instDecidableVerticalHomophony = id inferInstance

@[instance_reducible]

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

Equations

• s.instDecidableSpecialized c = id inferInstance

The first person complex

def Cysouw2003.Structure.letter (s : Structure) [DecidableRel ⇑s] (a : Clusivity.Cell) : Option (Quotient s)

The book's letter for a speaker cell is its morpheme class when it is specialized, and the dash, one for every singular morpheme, when it is not.

Equations

• s.letter a = if s.Specialized ↑a then some ⟦↑a⟧ else none

@[reducible, inline]

abbrev Cysouw2003.Structure.wePattern (s : Structure) [DecidableRel ⇑s] : Clusivity.Pattern

The pattern of the first person complex, the kernel of the letters.

Equations

• s.wePattern = Setoid.ker s.letter

@[reducible, inline]

abbrev Cysouw2003.Structure.HasClusivity (s : Structure) [DecidableRel ⇑s] (t : Clusivity) : Prop

The structure is of the common type t.

Equations

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

theorem Cysouw2003.Structure.HasClusivity.unique {s : Structure} [DecidableRel ⇑s] {t t' : Clusivity} (h : s.HasClusivity t) (h' : s.HasClusivity t') : t = t'

The Horizontal Homophony Hierarchy

def Cysouw2003.Structure.horizontalSingulars (s : Structure) [DecidableRel ⇑s] : Finset Singular

The singular categories showing horizontal homophony.

Equations

• s.horizontalSingulars = Finset.filter s.HorizontalHomophonyAt Finset.univ

def Cysouw2003.Structure.RespectsHorizontalHierarchy (s : Structure) [DecidableRel ⇑s] : Prop

Horizontal homophony in one person entails it in every less prominent person, so it appears first in the third person, then the second, then the first; diagonal homophony is among the exceptions.

Equations

• s.RespectsHorizontalHierarchy = (¬s.DiagonalHomophony ∧ IsLowerSet ↑s.horizontalSingulars)

@[instance_reducible]

instance Cysouw2003.Structure.instDecidableRespectsHorizontalHierarchy (s : Structure) [DecidableRel ⇑s] : Decidable s.RespectsHorizontalHierarchy

Equations

• s.instDecidableRespectsHorizontalHierarchy = id inferInstance

theorem Cysouw2003.Structure.mem_horizontalSingulars_iff {s : Structure} [DecidableRel ⇑s] (h : s.RespectsHorizontalHierarchy) {a : Singular} : a ∈ s.horizontalSingulars ↔ ↑a ≤ s.horizontalSingulars.max

A structure respecting the hierarchy shows horizontal homophony exactly up to its rung.

def Cysouw2003.Structure.numberStage (s : Structure) [DecidableRel ⇑s] : Option NumberStage

A paradigm without restricted groups is at N1 with no singular/group opposition at all, at N2 with a consistent one, and at neither on the intermediate rungs of the horizontal hierarchy.

Equations

• s.numberStage = if ∀ (a : Cysouw2003.Singular), s.HorizontalHomophonyAt a then some Cysouw2003.NumberStage.N1 else if ¬s.HorizontalHomophony then some Cysouw2003.NumberStage.N2 else none

The Explicitness Hierarchy

def Cysouw2003.Structure.weMarking (s : Structure) [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 (the Ojibwe and Huave prefixes, whose inclusive is a singular morpheme, are filed under the opposition), and as any 1+2 against 1+2+3 difference counts as a minimal/augmented inclusive.

Equations

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

def Cysouw2003.Structure.GivesUp (s : Structure) [DecidableRel ⇑s] : Opposition → Prop

The structure has given up the opposition of minimal to augmented inclusive unless 'we' is marked so, of inclusive to exclusive when 'we' is one form, one between groups when two groups share a morpheme, and one between singulars when two singulars do.

Equations

• s.GivesUp Cysouw2003.Opposition.minimalAugmented = (s.weMarking ≠ Cysouw2003.WeMarking.minimalAugmented)
• s.GivesUp Cysouw2003.Opposition.inclusiveExclusive = (s.weMarking = Cysouw2003.WeMarking.unified)
• s.GivesUp Cysouw2003.Opposition.group = s.VerticalHomophony
• s.GivesUp Cysouw2003.Opposition.singular = s.SingularHomophony

@[instance_reducible]

instance Cysouw2003.Structure.instDecidablePredOppositionGivesUp (s : Structure) [DecidableRel ⇑s] : DecidablePred s.GivesUp

Equations

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

def Cysouw2003.Structure.givenUp (s : Structure) [DecidableRel ⇑s] : Finset Opposition

The oppositions the structure has given up.

Equations

• s.givenUp = Finset.filter s.GivesUp Finset.univ

def Cysouw2003.Structure.RespectsExplicitnessHierarchy (s : Structure) [DecidableRel ⇑s] : Prop

As a constraint on which oppositions a paradigm may give up, the hierarchy requires those given up to form an initial segment of the order, so singulars merge only where groups already merge, and groups only once 'we' is one form.

Equations

• s.RespectsExplicitnessHierarchy = IsLowerSet ↑s.givenUp

@[instance_reducible]

instance Cysouw2003.Structure.instDecidableRespectsExplicitnessHierarchy (s : Structure) [DecidableRel ⇑s] : Decidable s.RespectsExplicitnessHierarchy

Equations

• s.instDecidableRespectsExplicitnessHierarchy = { decide := decide (∀ a ∈ s.givenUp, ∀ b ≤ a, b ∈ s.givenUp), reflects_decide := ⋯ }

def Cysouw2003.Structure.explicitness (s : Structure) [DecidableRel ⇑s] : WithBot Opposition

The rung of a structure on the hierarchy is the last opposition it has given up, the book's stages of person differentiation P4 (none given up), P3, P2, P1 and P0 (a singular one).

Equations

• s.explicitness = s.givenUp.max

theorem Cysouw2003.Structure.mem_givenUp_iff {s : Structure} [DecidableRel ⇑s] (h : s.RespectsExplicitnessHierarchy) {o : Opposition} : o ∈ s.givenUp ↔ ↑o ≤ s.explicitness

A structure respecting the hierarchy has given up exactly the oppositions up to its rung.

The rare patterns of the first person complex

inductive Cysouw2003.RarePattern : Type

The five rare attested patterns of the first person complex.

• 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 → ℕ

The book's letters as morpheme classes, 0 the singular class.

Equations

• Cysouw2003.RarePattern.pf.labels Person.Category.speakerAddressee = 1
• Cysouw2003.RarePattern.pf.labels Person.Category.speakerAddresseeOthers = 2
• Cysouw2003.RarePattern.pf.labels Person.Category.speakerOthers = 2
• Cysouw2003.RarePattern.pg.labels Person.Category.speakerAddressee = 1
• Cysouw2003.RarePattern.pg.labels Person.Category.speakerAddresseeOthers = 2
• Cysouw2003.RarePattern.pg.labels Person.Category.speakerOthers = 1
• Cysouw2003.RarePattern.ph.labels Person.Category.speakerAddressee = 1
• Cysouw2003.RarePattern.ph.labels Person.Category.speakerAddresseeOthers = 2
• Cysouw2003.RarePattern.pi.labels Person.Category.speakerAddresseeOthers = 1
• Cysouw2003.RarePattern.pi.labels Person.Category.speakerOthers = 1
• Cysouw2003.RarePattern.pj.labels Person.Category.speakerOthers = 1
• x✝¹.labels x✝ = 0

@[reducible, inline]

abbrev Cysouw2003.RarePattern.pattern (q : RarePattern) : 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 : Clusivity) : q.pattern ≠ t.toPattern

The rare patterns are distinct from the common types, so ten of the fifteen patterns are attested.

The named structures of chapter 4

inductive Cysouw2003.Kind : Type

Chapter 4 names eight common and five semi-common structures after an exemplar.

• 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 ⋯

@[instance_reducible]

instance Cysouw2003.instReprKind : Repr Kind

Equations

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

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.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; 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) : Structure

The paradigmatic structure of the named kind.

Equations

• k.pattern = Setoid.ker k.labels

def Cysouw2003.Kind.clusivity : Kind → Clusivity

The book files each named structure's first person complex by type; 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.

Equations

• Cysouw2003.Kind.maricopa.clusivity = Cysouw2003.Clusivity.noWe
• Cysouw2003.Kind.sierraPopoluca.clusivity = Cysouw2003.Clusivity.onlyInclusive
• Cysouw2003.Kind.maranao.clusivity = Cysouw2003.Clusivity.minimalAugmented
• Cysouw2003.Kind.mandara.clusivity = Cysouw2003.Clusivity.inclusiveExclusive
• Cysouw2003.Kind.tupiGuarani.clusivity = Cysouw2003.Clusivity.inclusiveExclusive
• Cysouw2003.Kind.kwakiutl.clusivity = Cysouw2003.Clusivity.inclusiveExclusive
• Cysouw2003.Kind.latin.clusivity = Cysouw2003.Clusivity.unifiedWe
• Cysouw2003.Kind.sinhalese.clusivity = Cysouw2003.Clusivity.unifiedWe
• Cysouw2003.Kind.berik.clusivity = Cysouw2003.Clusivity.unifiedWe
• Cysouw2003.Kind.slave.clusivity = Cysouw2003.Clusivity.unifiedWe
• Cysouw2003.Kind.nezPerce.clusivity = Cysouw2003.Clusivity.unifiedWe
• Cysouw2003.Kind.kombai.clusivity = Cysouw2003.Clusivity.unifiedWe
• Cysouw2003.Kind.omie.clusivity = Cysouw2003.Clusivity.unifiedWe

theorem Cysouw2003.Kind.pattern_injective : Function.Injective pattern

The named structures are distinct.

theorem Cysouw2003.Kind.hasClusivity_pattern (k : Kind) : k.pattern.HasClusivity k.clusivity

Each named structure has the first person complex the book files it under.

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

Every named structure respects the horizontal hierarchy.

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

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

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

Hierarchy II, without one, runs Latin < Sinhalese < Berik < Maricopa.

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

Every named structure respects the explicitness hierarchy.

theorem Cysouw2003.Kind.explicitness_pattern : slave.pattern.explicitness = ↑Opposition.group ∧ latin.pattern.explicitness = ↑Opposition.inclusiveExclusive ∧ maricopa.pattern.explicitness = ↑Opposition.inclusiveExclusive ∧ mandara.pattern.explicitness = ↑Opposition.minimalAugmented ∧ sierraPopoluca.pattern.explicitness = ↑Opposition.minimalAugmented ∧ maranao.pattern.explicitness = ⊥

The columns of the book's cognitive map put vertical homophony (the Slave type) at P1, unified-we and no-we at P2, inclusive/exclusive and only-inclusive at P3, and minimal/augmented at P4.

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

The rows of the cognitive map put 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.

• 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 ⋯

@[instance_reducible]

instance Cysouw2003.instReprMarking : Repr Marking

Equations

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

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

Equations

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

inductive Cysouw2003.Ubiquity : Type

Chapter 4'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.

@[reducible, inline]

abbrev Cysouw2003.Row.syncretism (r : Row) : Structure

The paradigmatic structure of the row.

Equations

• r.syncretism = Setoid.ker r.forms

@[reducible, inline]

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

The row's pattern of the first person complex.

Equations

• r.wePattern = r.syncretism.wePattern

def Cysouw2003.Row.optional? {α : Type u_1} (e : Datum) (key : String) (table : List (String × α)) : Option (Option α)

A feature that may be absent but, when present, must parse.

Equations

• Cysouw2003.Row.optional? e key table = match e.feature? key with | none => some none | some s => Option.map some (List.lookup s table)

def Cysouw2003.Row.ofDatum? (e : Datum) : Option Row

The row of an example.

Equations

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

theorem Cysouw2003.Row.isSome_ofDatum (e : Datum) : e ∈ Examples.all → (ofDatum? e).isSome = true

def Cysouw2003.rows : List Row

The printed paradigms.

Equations

• Cysouw2003.rows = List.filterMap Cysouw2003.Row.ofDatum? 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 illustrating a rare pattern has it.

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

Every chapter-4 paradigm has one of the five common types, chapter 4 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 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 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 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" ∧ r.syncretism.HasClusivity Clusivity.noWe

The strong universal 'we' fails, since the English inflection has no 'we'.

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

Over the printed paradigms, the Homophony Implication holds, singular homophony occurring 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 → ¬r.syncretism.RespectsHorizontalHierarchy → 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.

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

By 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 → r.syncretism.SingularHomophony → r.syncretism.weMarking = WeMarking.unified

By Table 4.2's second "nonesuch", there is no singular homophony under any inclusive/exclusive opposition.

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

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

theorem Cysouw2003.ofAttribute_givenUp_le_iff {o o' : Opposition} : Concept.ofAttribute (fun (r : { r : Row // r ∈ List.filter (fun (x : Row) => decide (x.ubiquity ≠ Ubiquity.rare)) rows }) => (↑r).syncretism.GivesUp) o' ≤ Concept.ofAttribute (fun (r : { r : Row // r ∈ List.filter (fun (x : Row) => decide (x.ubiquity ≠ Ubiquity.rare)) rows }) => (↑r).syncretism.GivesUp) o ↔ o ≤ o'

The Explicitness Hierarchy is the order of implication among the common and semi-common printed paradigms, one opposition being given up before another exactly when every such paradigm that gives up the second gives up the first. With the rare paradigms included, three of its steps fail.

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

Singular homophony without vertical homophony is rare, the European paradigms.

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

Vertical homophony under an inclusive/exclusive opposition is rare.

theorem Cysouw2003.explicitness_rungs : ∃ waskia ∈ rows, ∃ una ∈ rows, waskia.id = "cysouw2003_4_66" ∧ una.id = "cysouw2003_4_64" ∧ waskia.syncretism.explicitness = ↑Opposition.singular ∧ una.syncretism.explicitness = ↑Opposition.group ∧ Kind.latin.pattern.explicitness = ↑Opposition.inclusiveExclusive ∧ Kind.mandara.pattern.explicitness = ↑Opposition.minimalAugmented ∧ Kind.maranao.pattern.explicitness = ⊥

Among the book's exemplars of the five rungs, the Waskia present and the Una undergoer suffixes have given up a singular and a group opposition, then come the Latin, Mandara and Maranao types.

Two paradigms from the Fragments

def Cysouw2003.englishSubject : Person.Category → Finset String

The English subject forms by referential category are the paradigm of the fragment's non-accusative pronouns.

Equations

• Cysouw2003.englishSubject = PersonalPronoun.paradigm ({x ∈ English.Pronouns.pronouns | x.case_ ≠ some Case.acc})

theorem Cysouw2003.english_pronouns : ∃ r ∈ rows, r.id = "cysouw2003_4_19" ∧ Setoid.ker englishSubject = r.syncretism

The English pronouns have the structure of the paradigm the book prints for them.

theorem Cysouw2003.english_not_respectsHorizontalHierarchy : ¬Structure.RespectsHorizontalHierarchy (Setoid.ker englishSubject)

With horizontal homophony in the second person only, the English pronouns break the horizontal hierarchy.

theorem Cysouw2003.tagalog_maranao : Setoid.ker Tagalog.ang = Kind.maranao.pattern

The Tagalog ang series is a Maranao-type paradigm.

theorem Cysouw2003.tagalog_minimalAugmented : Structure.HasClusivity (Setoid.ker Tagalog.ang) Clusivity.minimalAugmented

The Tagalog ang series is of the minimal-augmented type.