Referential person categories

The eight referential person categories. A category is a configuration of the speech-act participants a referent contains and of the others it contains, none, one or several: the three singular participants and the five attested groups. The two groups this excludes, several speakers and an audience with no one else, are the configurations Category.WellFormed rejects.

Main definitions

• Person.Category: the eight categories.
• Category.toConfig: the configuration of a category, a bijection onto the well-formed ones.
• Category.IsSingular, Category.IsGroup, Category.IsFirstPersonComplex, Category.IsInclusive: the classes of categories read off the configuration.
• Category.person: the person projection, keeping clusivity on the groups.
• Category.ofPersonNumber: the categories a (person, number) coordinate pair realizes.
• Category.sharedPerson, Category.sharedNumber: the coordinates a set of categories shares, neutral values where they differ.

Main results

• Category.toConfig_bijective: the categories are exactly the well-formed configurations.
• Category.ofPersonNumber_person: every category is recovered from its person at some number.

References

• M. Cysouw, The Paradigmatic Structure of Person Marking (2003)

inductive Person.Category : Type

The eight referential person categories, the three singular participants and the five attested groups.

• speaker : Category

  The speaker alone, Cysouw's 1.

• addressee : Category

  The addressee alone, Cysouw's 2.

• other : Category

  A single other, Cysouw's 3.

• speakerAddressee : Category

  The minimal inclusive, speaker and addressee only, Cysouw's 1+2.

• speakerAddresseeOthers : Category

  The augmented inclusive, speaker and addressee with others, Cysouw's 1+2+3.

• speakerOthers : Category

  The exclusive, speaker with others but not the addressee, Cysouw's 1+3.

• addresseeOthers : Category

  The addressee with others, Cysouw's 2+3.

• others : Category

  Several others, Cysouw's 3+3.

@[instance_reducible]

instance Person.instDecidableEqCategory : DecidableEq Category

Equations

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

@[instance_reducible]

instance Person.instReprCategory : Repr Category

Equations

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

def Person.instReprCategory.repr : Category → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Person.instReprCategory.repr Person.Category.speaker prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Person.Category.speaker")).group prec✝
• Person.instReprCategory.repr Person.Category.addressee prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Person.Category.addressee")).group prec✝
• Person.instReprCategory.repr Person.Category.other prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Person.Category.other")).group prec✝
• Person.instReprCategory.repr Person.Category.others prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Person.Category.others")).group prec✝

@[instance_reducible]

instance Person.instInhabitedCategory : Inhabited Category

Equations

• Person.instInhabitedCategory = { default := Person.instInhabitedCategory.default }

@[instance_reducible]

instance Person.instFintypeCategory : Fintype Category

Equations

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

Configurations

def Person.Category.participants : Category → Finset Discourse.Role

The speech-act participants a category contains.

Equations

• Person.Category.speaker.participants = {Discourse.Role.speaker}
• Person.Category.speakerOthers.participants = {Discourse.Role.speaker}
• Person.Category.addressee.participants = {Discourse.Role.addressee}
• Person.Category.addresseeOthers.participants = {Discourse.Role.addressee}
• Person.Category.speakerAddressee.participants = {Discourse.Role.speaker, Discourse.Role.addressee}
• Person.Category.speakerAddresseeOthers.participants = {Discourse.Role.speaker, Discourse.Role.addressee}
• Person.Category.other.participants = ∅
• Person.Category.others.participants = ∅

def Person.Category.otherCount : Category → Fin 3

A category contains no others, one, or several, several counting as two.

Equations

• Person.Category.speaker.otherCount = 0
• Person.Category.addressee.otherCount = 0
• Person.Category.speakerAddressee.otherCount = 0
• Person.Category.other.otherCount = 1
• Person.Category.speakerOthers.otherCount = 1
• Person.Category.addresseeOthers.otherCount = 1
• Person.Category.speakerAddresseeOthers.otherCount = 1
• Person.Category.others.otherCount = 2

def Person.Category.WellFormed (x : Finset Discourse.Role × Fin 3) : Prop

A configuration of participants and others is a category iff it is nonempty and has several others only on their own. The speaker and the addressee are unique individuals, so a group of speakers or of addressees does not arise, and a participant with one other or with several forms one group.

Equations

• Person.Category.WellFormed x = ((x.1.Nonempty ∨ x.2 ≠ 0) ∧ (x.2 = 2 → x.1 = ∅))

@[instance_reducible]

instance Person.Category.instDecidablePredProdFinsetRoleFinOfNatNatWellFormed : DecidablePred WellFormed

Equations

• Person.Category.instDecidablePredProdFinsetRoleFinOfNatNatWellFormed x✝ = id inferInstance

def Person.Category.toConfig (c : Category) : { x : Finset Discourse.Role × Fin 3 // WellFormed x }

The configuration of a category.

Equations

• c.toConfig = ⟨(c.participants, c.otherCount), ⋯⟩

theorem Person.Category.toConfig_bijective : Function.Bijective toConfig

The categories are exactly the well-formed configurations.

def Person.Category.all : List Category

All eight categories in canonical order, singular then group.

Equations

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

Predicates

def Person.Category.card (c : Category) : ℕ

The members of a category, several others counting as two.

Equations

• c.card = c.participants.card + ↑c.otherCount

def Person.Category.IsSingular (c : Category) : Prop

A singular category has one member.

Equations

• c.IsSingular = (c.card = 1)

def Person.Category.IsGroup (c : Category) : Prop

A group category has several members.

Equations

• c.IsGroup = (2 ≤ c.card)

def Person.Category.IncludesSpeaker (c : Category) : Prop

The category includes the speaker.

Equations

• c.IncludesSpeaker = (Discourse.Role.speaker ∈ c.participants)

def Person.Category.IncludesAddressee (c : Category) : Prop

The category includes the addressee.

Equations

• c.IncludesAddressee = (Discourse.Role.addressee ∈ c.participants)

def Person.Category.IsFirstPersonComplex (c : Category) : Prop

The first person complex consists of the groups including the speaker.

Equations

• c.IsFirstPersonComplex = (c.IncludesSpeaker ∧ c.IsGroup)

def Person.Category.IsInclusive (c : Category) : Prop

An inclusive category includes both the speaker and the addressee.

Equations

• c.IsInclusive = (c.IncludesSpeaker ∧ c.IncludesAddressee)

@[instance_reducible]

instance Person.Category.instDecidablePredIsSingular : DecidablePred IsSingular

Equations

• x✝.instDecidablePredIsSingular = id inferInstance

@[instance_reducible]

instance Person.Category.instDecidablePredIsGroup : DecidablePred IsGroup

Equations

• x✝.instDecidablePredIsGroup = id inferInstance

@[instance_reducible]

instance Person.Category.instDecidablePredIncludesSpeaker : DecidablePred IncludesSpeaker

Equations

• x✝.instDecidablePredIncludesSpeaker = id inferInstance

@[instance_reducible]

instance Person.Category.instDecidablePredIncludesAddressee : DecidablePred IncludesAddressee

Equations

• x✝.instDecidablePredIncludesAddressee = id inferInstance

@[instance_reducible]

instance Person.Category.instDecidablePredIsFirstPersonComplex : DecidablePred IsFirstPersonComplex

Equations

• x✝.instDecidablePredIsFirstPersonComplex = id inferInstance

@[instance_reducible]

instance Person.Category.instDecidablePredIsInclusive : DecidablePred IsInclusive

Equations

• x✝.instDecidablePredIsInclusive = id inferInstance

theorem Person.Category.isGroup_iff_not_isSingular {c : Category} : c.IsGroup ↔ ¬c.IsSingular

A category is a group iff it is not singular.

theorem Person.Category.IsInclusive.isFirstPersonComplex {c : Category} (h : c.IsInclusive) : c.IsFirstPersonComplex

theorem Person.Category.IsFirstPersonComplex.includesSpeaker {c : Category} (h : c.IsFirstPersonComplex) : c.IncludesSpeaker

theorem Person.Category.IsInclusive.includesSpeaker {c : Category} (h : c.IsInclusive) : c.IncludesSpeaker

The person projection

def Person.Category.person (c : Category) : Person

The person of a category is the person of its participants, clusivity being a property of groups.

Equations

• c.person = if c.IsGroup then Person.ofParticipants c.participants else (Person.ofParticipants c.participants).coarsen

theorem Person.Category.person_includesSpeaker_iff (c : Category) : c.person.IncludesSpeaker ↔ c.IncludesSpeaker

The person projection tracks speaker inclusion.

theorem Person.Category.participants_mem_participantSets_person (c : Category) : c.participants ∈ c.person.participantSets

The person of a category covers the category's participants.

theorem Person.Category.person_separates_clusivity : speakerAddresseeOthers.person ≠ speakerOthers.person

Unlike UD realization, the person projection separates inclusive from exclusive.

def Person.Category.ofPersonNumber : Person → Number → Finset Category

The categories a (person, number) coordinate pair can realize. Clusivity rides on the person value and the minimal/augmented coordinates give the minimal/augmented inclusives directly (Tagalog kata = (firstInclusive, minimal) ↦ {speakerAddressee}). A clusivity-unmarked non-singular first person is the syncretism {speakerAddressee, speakerAddresseeOthers, speakerOthers} (English we), general number is noncommittal between the singular and the group category ((second, general) ↦ {addressee, addresseeOthers}), and a singular bearing clusivity realizes nothing.

Equations

• Person.Category.ofPersonNumber Person.first Number.singular = {Person.Category.speaker}
• Person.Category.ofPersonNumber Person.first Number.minimal = {Person.Category.speaker}
• Person.Category.ofPersonNumber Person.first Number.dual = {Person.Category.speakerAddressee, Person.Category.speakerOthers}
• Person.Category.ofPersonNumber Person.first Number.general = {Person.Category.speaker, Person.Category.speakerAddressee, Person.Category.speakerAddresseeOthers, Person.Category.speakerOthers}
• Person.Category.ofPersonNumber Person.first x✝ = {Person.Category.speakerAddressee, Person.Category.speakerAddresseeOthers, Person.Category.speakerOthers}
• Person.Category.ofPersonNumber Person.firstInclusive Number.singular = ∅
• Person.Category.ofPersonNumber Person.firstInclusive Number.minimal = {Person.Category.speakerAddressee}
• Person.Category.ofPersonNumber Person.firstInclusive Number.dual = {Person.Category.speakerAddressee}
• Person.Category.ofPersonNumber Person.firstInclusive Number.general = {Person.Category.speakerAddressee, Person.Category.speakerAddresseeOthers}
• Person.Category.ofPersonNumber Person.firstInclusive x✝ = {Person.Category.speakerAddresseeOthers}
• Person.Category.ofPersonNumber Person.firstExclusive Number.singular = ∅
• Person.Category.ofPersonNumber Person.firstExclusive x✝ = {Person.Category.speakerOthers}
• Person.Category.ofPersonNumber Person.second Number.singular = {Person.Category.addressee}
• Person.Category.ofPersonNumber Person.second Number.minimal = {Person.Category.addressee}
• Person.Category.ofPersonNumber Person.second Number.general = {Person.Category.addressee, Person.Category.addresseeOthers}
• Person.Category.ofPersonNumber Person.second x✝ = {Person.Category.addresseeOthers}
• Person.Category.ofPersonNumber Person.third Number.singular = {Person.Category.other}
• Person.Category.ofPersonNumber Person.third Number.minimal = {Person.Category.other}
• Person.Category.ofPersonNumber Person.third Number.general = {Person.Category.other, Person.Category.others}
• Person.Category.ofPersonNumber Person.third x✝ = {Person.Category.others}

theorem Person.Category.ofPersonNumber_person (c : Category) : ∃ (n : Number), ofPersonNumber c.person n = {c}

ofPersonNumber inverts the person projection, recovering every category from its coordinates at some number value.

The person and number of a set of categories

A form that can denote several categories, the polite German Sie for an addressee or addressees or English we for any group containing the speaker, has a person and a number only up to the values neutral between them, the clusivity-unmarked first and the noncommittal general.

def Person.Category.sharedPerson (s : Finset Category) : Option Person

The person shared by a set of referential categories is the common value of person where there is one, first for categories differing only in clusivity, and none for the empty set and for categories disagreeing on the speech-act roles they include.

Equations

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

def Person.Category.sharedNumber (s : Finset Category) : Option Number

The number shared by a set of referential categories is singular or plural when the categories agree, general when they mix individuals and groups, and none for the empty set. Cysouw's categories do not separate dual from plural, so the projection is at that granularity.

Equations

• Person.Category.sharedNumber s = if s = ∅ then none else if ∀ c ∈ s, c.IsSingular then some Number.singular else if ∀ c ∈ s, c.IsGroup then some Number.plural else some Number.general

theorem Person.Category.sharedPerson_singleton (c : Category) : sharedPerson {c} = some c.person

A single category shares its own person.

theorem Person.Category.sharedPerson_ofPersonNumber (p : Person) (n : Number) (h : (ofPersonNumber p n).Nonempty) : sharedPerson (ofPersonNumber p n) = some p

The categories a coordinate pair realizes share that person, wherever there are any.

theorem Person.Category.sharedNumber_ofPersonNumber_eq_general (p : Person) (n : Number) (h : sharedNumber (ofPersonNumber p n) = some Number.general) : n = Number.general

The categories a coordinate pair realizes share the general number only at general number.