Person — the canonical inventory

[Cys09] [Har16a] [Sie04]

The root-namespace Person type is the canonical, analytical person inventory: the values languages' person systems distinguish, with clusivity folded in as person values. [Har16a]'s quadripartition (first exclusive / first inclusive / second / third) and the plain tripartition (first / second / third) coexist as inventory values — plain first is the tripartition cell (English we), related to the clusivity-marked cells by coarsen, exactly as Number.dual relates to Number.plural under coarsening. zero is the impersonal person (UD Person=0; Finnish-type impersonals).

UD.Person (Data/UD/Basic.lean) is the realization vocabulary — what corpora annotate — reachable by toUD/fromUD. UD has no clusivity, so toUD collapses the quadripartition cells to .first (ud_conflates_clusivity); the analytical values are not recoverable from UD alone.

This mirrors the Number API (Features/Number/Basic.lean): canonical analytical inventory at root namespace, UD demoted to realization, capability mixin (Features/Person/Capabilities.lean), unified resolution (Features/Person/Resolve.lean), feature decomposition and the Cysouw categories (Features/Person/Decomposition.lean).

The prominence scale over this inventory (Person.prominence, the dissolved Person's role) lives in Features/Prominence.lean.

inductive Person : Type

Grammatical person — the canonical analytical inventory. Clusivity is a person-value distinction ([Cys09]; [Har16a]'s quadripartition), not an orthogonal feature: firstInclusive and firstExclusive sit alongside the tripartition cell first.

• first : Person

  First person, clusivity-unmarked: the tripartition cell (English we).

• firstInclusive : Person

  First person inclusive: includes the addressee (Indonesian kita).

• firstExclusive : Person

  First person exclusive: excludes the addressee (Indonesian kami).

• second : Person

  Second person: addressee, not speaker.

• third : Person

  Third person: neither speaker nor addressee.

• zero : Person

  Impersonal/generic person (UD Person=0; Finnish-type impersonals).

@[implicit_reducible]

instance instDecidableEqPerson : DecidableEq Person

Equations

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

def instReprPerson.repr : Person → ℕ → Std.Format

Equations

• instReprPerson.repr Person.first prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Person.first")).group prec✝
• instReprPerson.repr Person.firstInclusive prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Person.firstInclusive")).group prec✝
• instReprPerson.repr Person.firstExclusive prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Person.firstExclusive")).group prec✝
• instReprPerson.repr Person.second prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Person.second")).group prec✝
• instReprPerson.repr Person.third prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Person.third")).group prec✝
• instReprPerson.repr Person.zero prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Person.zero")).group prec✝

@[implicit_reducible]

instance instReprPerson : Repr Person

Equations

• instReprPerson = { reprPrec := instReprPerson.repr }

@[implicit_reducible]

instance instFintypePerson : Fintype Person

Equations

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

Predicates

def Person.IncludesSpeaker : Person → Prop

The referent includes the speaker.

Equations

• Person.first.IncludesSpeaker = True
• Person.firstInclusive.IncludesSpeaker = True
• Person.firstExclusive.IncludesSpeaker = True
• x✝.IncludesSpeaker = False

@[implicit_reducible]

instance Person.instDecidablePredIncludesSpeaker : DecidablePred IncludesSpeaker

Equations

• Person.first.instDecidablePredIncludesSpeaker = isTrue trivial
• Person.firstInclusive.instDecidablePredIncludesSpeaker = isTrue trivial
• Person.firstExclusive.instDecidablePredIncludesSpeaker = isTrue trivial
• Person.second.instDecidablePredIncludesSpeaker = isFalse ⋯
• Person.third.instDecidablePredIncludesSpeaker = isFalse ⋯
• Person.zero.instDecidablePredIncludesSpeaker = isFalse ⋯

def Person.MarksClusivity : Person → Prop

The value marks clusivity (a quadripartition cell).

Equations

• Person.firstInclusive.MarksClusivity = True
• Person.firstExclusive.MarksClusivity = True
• x✝.MarksClusivity = False

@[implicit_reducible]

instance Person.instDecidablePredMarksClusivity : DecidablePred MarksClusivity

Equations

• Person.firstInclusive.instDecidablePredMarksClusivity = isTrue trivial
• Person.firstExclusive.instDecidablePredMarksClusivity = isTrue trivial
• Person.first.instDecidablePredMarksClusivity = isFalse ⋯
• Person.second.instDecidablePredMarksClusivity = isFalse ⋯
• Person.third.instDecidablePredMarksClusivity = isFalse ⋯
• Person.zero.instDecidablePredMarksClusivity = isFalse ⋯

def Person.IsSAP : Person → Prop

Speech-act participant: speaker or addressee included. zero is not a participant value.

Equations

• Person.third.IsSAP = False
• Person.zero.IsSAP = False
• x✝.IsSAP = True

@[implicit_reducible]

instance Person.instDecidablePredIsSAP : DecidablePred IsSAP

Equations

• Person.first.instDecidablePredIsSAP = isTrue trivial
• Person.firstInclusive.instDecidablePredIsSAP = isTrue trivial
• Person.firstExclusive.instDecidablePredIsSAP = isTrue trivial
• Person.second.instDecidablePredIsSAP = isTrue trivial
• Person.third.instDecidablePredIsSAP = isFalse ⋯
• Person.zero.instDecidablePredIsSAP = isFalse ⋯

Coarsening

The quadripartition cells coarsen to the tripartition cell, as Number.dual coarsens to Number.plural: a clusivity-less system realizes both inclusive and exclusive referents as plain first.

def Person.coarsen : Person → Person

Collapse clusivity: the tripartition image of each value.

Equations

• Person.firstInclusive.coarsen = Person.first
• Person.firstExclusive.coarsen = Person.first
• x✝.coarsen = x✝

@[simp]

theorem Person.coarsen_idempotent (p : Person) : p.coarsen.coarsen = p.coarsen

theorem Person.coarsen_eq_self_iff (p : Person) : p.coarsen = p ↔ ¬p.MarksClusivity

Coarsening erases exactly the clusivity marking.

UD realization vocabulary

def Person.toUD : Person → UD.Person

Realize as UD annotation: clusivity collapses to Person=1.

Equations

• Person.first.toUD = UD.Person.first
• Person.firstInclusive.toUD = UD.Person.first
• Person.firstExclusive.toUD = UD.Person.first
• Person.second.toUD = UD.Person.second
• Person.third.toUD = UD.Person.third
• Person.zero.toUD = UD.Person.zero

def Person.fromUD : UD.Person → Person

Analytical value of a UD annotation. Total: UD's vocabulary is a coarsening of the analytical inventory.

Equations

• Person.fromUD UD.Person.first = Person.first
• Person.fromUD UD.Person.second = Person.second
• Person.fromUD UD.Person.third = Person.third
• Person.fromUD UD.Person.zero = Person.zero

@[simp]

theorem Person.toUD_fromUD (u : UD.Person) : (fromUD u).toUD = u

UD round-trips on its own image.

theorem Person.fromUD_toUD (p : Person) : fromUD p.toUD = p.coarsen

The analytical inventory does not round-trip through UD: clusivity has no UD image. fromUD ∘ toUD is coarsen.

theorem Person.ud_conflates_clusivity : firstInclusive.toUD = firstExclusive.toUD

UD conflates the clusivity values under Person=1.

def Person.hierarchyRank : Person → ℕ

The person hierarchy 1 < 2 < 3 ([Zwi77]; resolution in coordination, [Cor06]). Clusivity-marked firsts share rank 0 with first; zero sits outside the hierarchy (sentinel rank 3).

Equations

• Person.first.hierarchyRank = 0
• Person.firstInclusive.hierarchyRank = 0
• Person.firstExclusive.hierarchyRank = 0
• Person.second.hierarchyRank = 1
• Person.third.hierarchyRank = 2
• Person.zero.hierarchyRank = 3

Person systems

structure Person.System : Type

A language's person system: the analytical values its paradigms distinguish ([Cys09]; the paradigm-level marking typology is Features.Clusivity.System, his Table 3.2).

• values : List Person

  The person values the system distinguishes.

@[implicit_reducible]

instance Person.instDecidableEqSystem : DecidableEq System

Equations

• Person.instDecidableEqSystem = Person.instDecidableEqSystem.decEq

def Person.instDecidableEqSystem.decEq (x✝ x✝¹ : System) : Decidable (x✝ = x✝¹)

Equations

• Person.instDecidableEqSystem.decEq { values := a } { values := b } = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Person.instReprSystem : Repr System

Equations

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

def Person.instReprSystem.repr : System → ℕ → Std.Format

Equations

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

def Person.System.HasClusivity (ns : System) : Prop

The system marks clusivity.

Equations

• ns.HasClusivity = (Person.firstInclusive ∈ ns.values ∨ Person.firstExclusive ∈ ns.values)

@[implicit_reducible]

instance Person.System.instDecidablePredHasClusivity : DecidablePred HasClusivity

Equations

• ns.instDecidablePredHasClusivity = id inferInstance

def Person.System.tripartition : System

The English-type tripartition.

Equations

• Person.System.tripartition = { values := [Person.first, Person.second, Person.third] }

def Person.System.quadripartition : System

The Indonesian/Tagalog-type quadripartition ([Har16a]).

Equations

• Person.System.quadripartition = { values := [Person.firstInclusive, Person.firstExclusive, Person.second, Person.third] }

theorem Person.System.tripartition_no_clusivity : ¬tripartition.HasClusivity

theorem Person.System.quadripartition_clusivity : quadripartition.HasClusivity

def Person.System.ExclusiveImpliesInclusive (ns : System) : Prop

Addressee inclusion implication I at the value level ([Cys09] (3.23), Fig 3.8): a distinguished exclusive requires a distinguished inclusive. The converse fails — only-inclusive systems (his (Pc), Maká) have an inclusive value whose exclusive is covered by the singular morpheme. (Over the common paradigm types; the rare Binandere pattern, his (3.22)/(Pj), is the noted incidental exception.)

Equations

• ns.ExclusiveImpliesInclusive = (Person.firstExclusive ∈ ns.values → Person.firstInclusive ∈ ns.values)

@[implicit_reducible]

instance Person.System.instDecidablePredExclusiveImpliesInclusive : DecidablePred ExclusiveImpliesInclusive

Equations

• ns.instDecidablePredExclusiveImpliesInclusive = id inferInstance

theorem Person.System.tripartition_exclImpliesIncl : tripartition.ExclusiveImpliesInclusive

theorem Person.System.quadripartition_exclImpliesIncl : quadripartition.ExclusiveImpliesInclusive