Grammatical person

Person is the inventory of values that languages' person systems distinguish, clusivity among them. Harbour's quadripartition, first exclusive, first inclusive, second and third, sits beside the tripartition's first, the first person unmarked for clusivity (English we), to which coarsen sends both clusivity values as coarsening sends Number.dual to Number.plural. The impersonal is not a value but the absence of one, Option Person, as the Universal Dependencies tag Person=0 is ingested (Morphology/Word/UD.lean). A value means the participant sets its referents can have (Person.participantSets), and whether it includes the speaker, is a speech-act participant, or marks clusivity is read off them.

The person hierarchy 1 > 2 > 3, the hierarchy of reference and coordination of Zwicky, Corbett, and Dalrymple and Kaplan, is Person.prominence, the top of a value's feature bundle (Syntax/Person/Features.lean). It is not the only person scale: Zwicky distinguishes morphosyntactic hierarchies that order the participants otherwise, as Algonquian ranks the second person above the first, and for argument coding splits Haspelmath's person scale is the binary cut between participants and the rest (Person.Class).

Main definitions

• Person: the inventory.
• Person.participantSets: the participant sets a value covers.
• Person.ofParticipants: the value covering exactly one participant set.
• Person.IncludesSpeaker, Person.IsSAP, Person.MarksClusivity: predicates read off the participant sets.
• Person.coarsen: the value without its clusivity.

References

• [Cys03]
• [Har16a]
• [Sie04]
• [Zwi77a]
• [Cor06]
• [DK00a]
• [Has21c]

inductive Person : Type

Grammatical person, clusivity being a distinction among person values rather than an orthogonal feature: firstInclusive and firstExclusive sit beside the tripartition's first.

• first : Person

  first is the first person unmarked for clusivity, the tripartition's (English we).

• firstInclusive : Person

  firstInclusive is the first person including the addressee (Indonesian kita).

• firstExclusive : Person

  firstExclusive is the first person excluding the addressee (Indonesian kami).

• second : Person

  second refers to the addressee and not the speaker.

• third : Person

  third refers to neither the speaker nor the addressee.

@[instance_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✝

@[instance_reducible]

instance instReprPerson : Repr Person

Equations

• instReprPerson = { reprPrec := instReprPerson.repr }

@[instance_reducible]

instance instFintypePerson : Fintype Person

Equations

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

Participant sets

A person value covers the referents whose participants, the speaker and the addressee among them, form one of its participant sets: {speaker} or {speaker, addressee} for the first person unmarked for clusivity and a single set for each value of the quadripartition. The predicates on values read these sets off.

def Person.participantSets : Person → Finset (Finset Discourse.Role)

p.participantSets is the family of participant sets of the referents p covers.

Equations

• Person.first.participantSets = {{Discourse.Role.speaker}, {Discourse.Role.speaker, Discourse.Role.addressee}}
• Person.firstInclusive.participantSets = {{Discourse.Role.speaker, Discourse.Role.addressee}}
• Person.firstExclusive.participantSets = {{Discourse.Role.speaker}}
• Person.second.participantSets = {{Discourse.Role.addressee}}
• Person.third.participantSets = {∅}

theorem Person.participantSets_injective : Function.Injective participantSets

@[simp]

theorem Person.participantSets_inj {p q : Person} : p.participantSets = q.participantSets ↔ p = q

theorem Person.participantSets_nonempty (p : Person) : p.participantSets.Nonempty

def Person.ofParticipants (s : Finset Discourse.Role) : Person

The person of a referent whose participants are s is first inclusive with both, first exclusive with the speaker alone, second with the addressee alone, and third with neither.

Equations

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

@[simp]

theorem Person.participantSets_ofParticipants (s : Finset Discourse.Role) : (ofParticipants s).participantSets = {s}

theorem Person.participantSets_eq_singleton_iff {p : Person} {s : Finset Discourse.Role} : p.participantSets = {s} ↔ p = ofParticipants s

The values of the quadripartition are exactly those covering a single participant set.

theorem Person.ofParticipants_injective : Function.Injective ofParticipants

Predicates

def Person.IncludesSpeaker (p : Person) : Prop

The value includes the speaker when each of its participant sets contains the speaker.

Equations

• p.IncludesSpeaker = ∀ s ∈ p.participantSets, Discourse.Role.speaker ∈ s

@[instance_reducible]

instance Person.instDecidablePredIncludesSpeaker : DecidablePred IncludesSpeaker

Equations

• x✝.instDecidablePredIncludesSpeaker = id inferInstance

def Person.IsSAP (p : Person) : Prop

A speech-act participant value has only nonempty participant sets.

Equations

• p.IsSAP = ∀ s ∈ p.participantSets, s.Nonempty

@[instance_reducible]

instance Person.instDecidablePredIsSAP : DecidablePred IsSAP

Equations

• x✝.instDecidablePredIsSAP = id inferInstance

def Person.MarksClusivity (p : Person) : Prop

The value marks clusivity when it includes the speaker and covers a single participant set, fixing whether the addressee is included.

Equations

• p.MarksClusivity = (p.IncludesSpeaker ∧ p.participantSets.card = 1)

@[instance_reducible]

instance Person.instDecidablePredMarksClusivity : DecidablePred MarksClusivity

Equations

• x✝.instDecidablePredMarksClusivity = id inferInstance

Coarsening

The clusivity values coarsen to the tripartition's first, as Number.dual coarsens to Number.plural, so a system without clusivity realizes inclusive and exclusive referents alike.

def Person.coarsen (p : Person) : Person

coarsen collapses clusivity, sending a value marking clusivity to the first person and keeping every other value.

Equations

• p.coarsen = if p.MarksClusivity then Person.first else p

@[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.