Clusivity: marking types of the first person complex

A person paradigm marks the three 'we' categories 1+2, 1+2+3 and 1+3 either by a morpheme of their own or by one that also marks a singular category, and groups them in some way. [cysouw-2003]'s Fig. 3.1 writes such a pattern with a letter per specialized morpheme class and a dash where a singular morpheme is reused; of the fifteen possible patterns five are common (his Table 3.2) and form Clusivity. Each type's toPattern is that notation as a setoid on Clusivity.Cell, the four speaker-including categories, the singular speaker standing for any singular morpheme, and the four questions of his Fig. 3.10 are read off the setoid. The First Person Hierarchy (3.26) is the linear order on the types, along which each question's answer is monotone.

The five rare attested patterns ((Pf)–(Pj), his §3.6.6) are not types in this sense and live with the study. The typology is finer than [cysouw-2013]'s WALS chapter, which collapses minimal/augmented into inclusive/exclusive and whose "no 'we'" value is the absence of any first-person non-singular, not Clusivity.noWe.

References

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

inductive Person.Clusivity : Type

The five common marking types of the first person complex ([cysouw-2003] Table 3.2, the common five of the fifteen patterns of his Fig. 3.1).

• 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, his Fig. 3.6).

@[instance_reducible]

instance Person.instDecidableEqClusivity : DecidableEq Clusivity

Equations

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

@[instance_reducible]

instance Person.instReprClusivity : Repr Clusivity

Equations

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

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

Equations

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

@[instance_reducible]

instance Person.instFintypeClusivity : Fintype Clusivity

Equations

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

@[reducible, inline]

abbrev Person.Clusivity.Cell : Type

Fig. 3.1's four cells, the categories that include the speaker; the singular speaker stands for every singular morpheme.

Equations

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

def Person.Clusivity.Cell.s1 : Cell

The singular speaker.

Equations

• Person.Clusivity.Cell.s1 = ⟨Person.Category.s1, Person.Clusivity.Cell.s1._proof_1⟩

def Person.Clusivity.Cell.minIncl : Cell

The minimal inclusive 1+2.

Equations

• Person.Clusivity.Cell.minIncl = ⟨Person.Category.minIncl, Person.Clusivity.Cell.minIncl._proof_1⟩

def Person.Clusivity.Cell.augIncl : Cell

The augmented inclusive 1+2+3.

Equations

• Person.Clusivity.Cell.augIncl = ⟨Person.Category.augIncl, Person.Clusivity.Cell.augIncl._proof_1⟩

def Person.Clusivity.Cell.excl : Cell

The exclusive 1+3.

Equations

• Person.Clusivity.Cell.excl = ⟨Person.Category.excl, Person.Clusivity.Cell.excl._proof_1⟩

@[reducible, inline]

abbrev Person.Clusivity.Pattern : Type

A marking pattern of the first person complex, Fig. 3.1's notation as a setoid on the four cells.

Equations

• Person.Clusivity.Pattern = Setoid Person.Clusivity.Cell

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

Some 'we' cell is not marked like the speaker (Fig. 3.10's first question).

Equations

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

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

Both inclusive cells are marked neither like the speaker nor like the exclusive (Fig. 3.10's second question, read as his Fig. 3.8 reads it for the common types).

Equations

• r.SpecializedInclusive = ∀ (c : Person.Clusivity.Cell), (↑c).IsInclusive → ¬r c Person.Clusivity.Cell.s1 ∧ ¬r c Person.Clusivity.Cell.excl

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

The exclusive is marked neither like the speaker nor like an inclusive cell (Fig. 3.10's third question).

Equations

• r.SpecializedExclusive = (¬r Person.Clusivity.Cell.excl Person.Clusivity.Cell.s1 ∧ ∀ (c : Person.Clusivity.Cell), (↑c).IsInclusive → ¬r Person.Clusivity.Cell.excl c)

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

Minimal and augmented inclusive are marked apart and neither like the speaker (Fig. 3.10's fourth question).

Equations

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

@[instance_reducible]

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

Equations

• r.instDecidableSpecializedWe = id inferInstance

@[instance_reducible]

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

Equations

• r.instDecidableSpecializedInclusive = id inferInstance

@[instance_reducible]

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

Equations

• r.instDecidableSpecializedExclusive = id inferInstance

@[instance_reducible]

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

Equations

• r.instDecidableSplitInclusive = id inferInstance

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

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

Equations

• Person.Clusivity.unifiedWe.labels Person.Category.minIncl = 1
• Person.Clusivity.unifiedWe.labels Person.Category.augIncl = 1
• Person.Clusivity.unifiedWe.labels Person.Category.excl = 1
• Person.Clusivity.onlyInclusive.labels Person.Category.minIncl = 1
• Person.Clusivity.onlyInclusive.labels Person.Category.augIncl = 1
• Person.Clusivity.inclusiveExclusive.labels Person.Category.minIncl = 1
• Person.Clusivity.inclusiveExclusive.labels Person.Category.augIncl = 1
• Person.Clusivity.inclusiveExclusive.labels Person.Category.excl = 2
• Person.Clusivity.minimalAugmented.labels Person.Category.minIncl = 1
• Person.Clusivity.minimalAugmented.labels Person.Category.augIncl = 2
• Person.Clusivity.minimalAugmented.labels Person.Category.excl = 3
• x✝¹.labels x✝ = 0

@[reducible, inline]

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

The type's pattern, Fig. 3.2's column as a setoid on the four cells.

Equations

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

theorem Person.Clusivity.toPattern_injective : Function.Injective toPattern

The five patterns are distinct.

theorem Person.Clusivity.specializedInclusive_of_specializedExclusive {t : Clusivity} (h : t.toPattern.SpecializedExclusive) : t.toPattern.SpecializedInclusive

A specialized exclusive requires a specialized inclusive ((3.23), Fig. 3.8).

theorem Person.Clusivity.onlyInclusive_specializedInclusive : onlyInclusive.toPattern.SpecializedInclusive

The converse of (3.23) fails at only-inclusive.

theorem Person.Clusivity.onlyInclusive_not_specializedExclusive : ¬onlyInclusive.toPattern.SpecializedExclusive

theorem Person.Clusivity.specializedExclusive_of_splitInclusive {t : Clusivity} (h : t.toPattern.SplitInclusive) : t.toPattern.SpecializedExclusive

A split inclusive requires a specialized exclusive ((3.24), Fig. 3.9).

def Person.Clusivity.hierarchyRank : Clusivity → ℕ

Position on the First Person Hierarchy (3.26), the number of Fig. 3.10's questions answered positively: no-we, unified-we, only-inclusive, inclusive/exclusive, minimal/augmented.

Equations

• Person.Clusivity.noWe.hierarchyRank = 0
• Person.Clusivity.unifiedWe.hierarchyRank = 1
• Person.Clusivity.onlyInclusive.hierarchyRank = 2
• Person.Clusivity.inclusiveExclusive.hierarchyRank = 3
• Person.Clusivity.minimalAugmented.hierarchyRank = 4

@[instance_reducible]

instance Person.Clusivity.instLinearOrder : LinearOrder Clusivity

The First Person Hierarchy (3.26) as the order on the types.

Equations

• Person.Clusivity.instLinearOrder = LinearOrder.lift' Person.Clusivity.hierarchyRank Person.Clusivity.instLinearOrder._proof_1

theorem Person.Clusivity.specializedWe_of_le {s t : Clusivity} (h : s ≤ t) (hs : s.toPattern.SpecializedWe) : t.toPattern.SpecializedWe

Each of Fig. 3.10's answers is monotone along the hierarchy, so each type's profile extends its predecessor's by one positive answer.

theorem Person.Clusivity.specializedInclusive_of_le {s t : Clusivity} (h : s ≤ t) (hs : s.toPattern.SpecializedInclusive) : t.toPattern.SpecializedInclusive

theorem Person.Clusivity.specializedExclusive_of_le {s t : Clusivity} (h : s ≤ t) (hs : s.toPattern.SpecializedExclusive) : t.toPattern.SpecializedExclusive

theorem Person.Clusivity.splitInclusive_of_le {s t : Clusivity} (h : s ≤ t) (hs : s.toPattern.SplitInclusive) : t.toPattern.SplitInclusive