Clusivity systems — typology of inclusive/exclusive distinctions

[Cys09]

System-level typology of how a language encodes the inclusive/exclusive distinction in 1pl pronouns. Per-referent person categories (s1, minIncl, augIncl, excl, ...) live in Features/Person.lean::Category; this file classifies systems by which of those categories they grammatically distinguish.

The substrate cut is intentionally finer than WALS Ch 39 (which collapses plain inclExcl with minimal-augmented into a single "inclusive/exclusive" value). The minimal-augmented type — which licenses a 1-dual-inclusive form in addition to a 1pl-inclusive — is the typologically distinctive property of Tagalog (kata / tayo), several other Philippine languages, and many Australian languages.

Scope: pronominal clusivity (independent personal pronouns). Verbal clusivity (WALS Ch 40, Pronoun.InclusiveExclusiveVerbal) is a separately-marked phenomenon that may dissociate from pronominal clusivity (e.g. some Athabaskan languages). The five-value enum here is a first-cut typology; [Cys09] discusses additional minor types (degenerate-minimal-augmented, composite-unit-augmented) that this substrate does not currently distinguish.

inductive Features.Clusivity.System : Type

The five common marking types of the first person complex ([Cys09] Table 3.2; the attested-and-common five of the fifteen possible patterns, his Fig 3.1–3.2). Classified by which of the categories 1+2, 1+2+3, 1+3 receive specialized morphemes. The five rare attested patterns ((Pf)–(Pj), his §3.6.6) are not represented.

• noWe : System

  (Pb) No-we: none of 1+2, 1+2+3, 1+3 marked by a specialized morpheme (English verbal inflection; Pirahã, which lacks group marking altogether).

• unifiedWe : System

  (Pa) Unified-we: all three categories marked by the same specialized morpheme (English we, German wir).

• onlyInclusive : System

  (Pc) Only-inclusive: 1+2 and 1+2+3 share a specialized inclusive morpheme; 1+3 is marked by the first-person singular morpheme, not a specialized one (Maká).

• inclusiveExclusive : System

  (Pd) Inclusive/exclusive: inclusive (1+2, 1+2+3) and exclusive (1+3) each get a specialized morpheme (Apalai; Indonesian kita/kami).

• minimalAugmented : System

  (Pe) Minimal/augmented: all three categories get separate specialized morphemes (Tagalog kata/tayo/kami per [SO72] Chart 7; Ilocano ta/tayo/mi, his Fig 3.5–3.6).

@[implicit_reducible]

instance Features.Clusivity.instDecidableEqSystem : DecidableEq System

Equations

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

def Features.Clusivity.instReprSystem.repr : System → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Features.Clusivity.instReprSystem : Repr System

Equations

• Features.Clusivity.instReprSystem = { reprPrec := Features.Clusivity.instReprSystem.repr }

@[implicit_reducible]

instance Features.Clusivity.instFintypeSystem : Fintype System

Equations

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

Fig 3.10's nested questions: each type answers one more question positively than its predecessor, which is exactly why the types form the First Person Hierarchy (3.26).

def Features.Clusivity.System.specializedWe : System → Bool

Some specialized 'we' morpheme exists.

Equations

• Features.Clusivity.System.noWe.specializedWe = false
• x✝.specializedWe = true

def Features.Clusivity.System.specializedInclusive : System → Bool

The inclusive (1+2, 1+2+3) has marking distinct from the exclusive.

Equations

• Features.Clusivity.System.noWe.specializedInclusive = false
• Features.Clusivity.System.unifiedWe.specializedInclusive = false
• x✝.specializedInclusive = true

def Features.Clusivity.System.specializedExclusive : System → Bool

The exclusive (1+3) has its own specialized morpheme.

Equations

• Features.Clusivity.System.inclusiveExclusive.specializedExclusive = true
• Features.Clusivity.System.minimalAugmented.specializedExclusive = true
• x✝.specializedExclusive = false

def Features.Clusivity.System.splitInclusive : System → Bool

The inclusive is split: separate morphemes for 1+2 and 1+2+3.

Equations

• Features.Clusivity.System.minimalAugmented.splitInclusive = true
• x✝.splitInclusive = false

@[reducible, inline]

abbrev Features.Clusivity.System.hasInclExcl (s : System) : Bool

A system grammatically distinguishes inclusive from exclusive.

Equations

• s.hasInclExcl = s.specializedExclusive

@[reducible, inline]

abbrev Features.Clusivity.System.hasMinimalAugmented (s : System) : Bool

A system distinguishes minimal from augmented inclusive.

Equations

• s.hasMinimalAugmented = s.splitInclusive

theorem Features.Clusivity.System.exclusive_implies_inclusive (s : System) : s.specializedExclusive = true → s.specializedInclusive = true

Addressee inclusion implication I ([Cys09] (3.23), Fig 3.8): a specialized exclusive requires a specialized inclusive. The converse fails — only-inclusive systems are the witness. (Over the common types; the rare Binandere pattern, his (3.22)/(Pj), is the noted incidental exception.)

theorem Features.Clusivity.System.not_inclusive_implies_exclusive : ¬∀ (s : System), s.specializedInclusive = true → s.specializedExclusive = true

theorem Features.Clusivity.System.splitInclusive_implies_exclusive (s : System) : s.splitInclusive = true → s.specializedExclusive = true

Addressee inclusion implication II ([Cys09] (3.24), Fig 3.9): a split inclusive requires a specialized exclusive (disregarding the rare (Pf)/(Pg) patterns, his §3.6.6).

def Features.Clusivity.System.hierarchyRank : System → ℕ

Position in the First Person Hierarchy ([Cys09] (3.26)): no-we > unified-we > only-inclusive > inclusive/exclusive > minimal/augmented (rank counts the Fig 3.10 questions answered positively).

Equations

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

theorem Features.Clusivity.System.hierarchy_is_question_nesting (s t : System) : s.hierarchyRank ≤ t.hierarchyRank → (s.specializedWe = true → t.specializedWe = true) ∧ (s.specializedInclusive = true → t.specializedInclusive = true) ∧ (s.specializedExclusive = true → t.specializedExclusive = true) ∧ (s.splitInclusive = true → t.splitInclusive = true)

The hierarchy is exactly the nesting of Fig 3.10's questions: each of the four predicates is monotone in hierarchy rank, so each type's profile extends its predecessor's by one positive answer.

The per-referent clusivity Value (inclusive/exclusive) and the categoryOf bridge were dissolved into the canonical person inventory: clusivity is a person-value distinction (Person.firstInclusive / Person.firstExclusive, Features/Person/Basic.lean), and the category bridge is Person.Category.ofPersonNumber (Features/Person/Decomposition.lean). This file keeps the paradigm-level System typology, which classifies how a language's pronoun paradigm carves the person–number space.