Person

@cite{cysouw-2009} @cite{siewierska-2004}

Two components of the person API:

§ 1–4: Person Features (@cite{cysouw-2009}, @cite{siewierska-2004}). Framework-neutral decomposition of person into binary features:

• [±participant]: whether the referent includes a speech-act participant (speaker or addressee). 1st and 2nd person are [+participant]; 3rd person is [−participant].
• [±author]: whether the referent includes the speaker. 1st person is [+author]; 2nd and 3rd are [−author].

These features form a containment hierarchy: [+author] → [+participant]. An author (speaker) is necessarily a participant.

This decomposition is shared across theoretical frameworks:

• Minimalism: @cite{preminger-2014}, @cite{bejar-rezac-2009}
• Distributed Morphology: @cite{munoz-perez-2026} (Fission)
• Typology: @cite{cysouw-2009}, @cite{siewierska-2004}

The Minimalist-specific extension [±proximate] (@cite{pancheva-zubizarreta-2018}) is added in Theories/Syntax/Minimalism/PersonGeometry.lean.

§ 5–9: Person Categories (@cite{cysouw-2009}). The 8 referential person categories from Cysouw's paradigmatic framework. Three singular categories (individual speech act roles) and five group categories (attested combinations of participants).

The full paradigmatic structure machinery (morpheme classes, homophony types, language data) remains in Phenomena/Agreement/PersonMarkingTypology.lean.

structure Features.Person.Features : Type

Binary person features: [±participant, ±author].

These two features suffice for the three-way person distinction:

• 1st person: [+participant, +author]
• 2nd person: [+participant, −author]
• 3rd person: [−participant, −author]

The fourth combination [−participant, +author] is ill-formed: an author (speaker) is necessarily a speech-act participant.

• hasParticipant : Bool

  [+participant]: referent includes a speech-act participant (1P or 2P).

• hasAuthor : Bool

  [+author]: referent includes the speaker (1P only for singulars).

@[implicit_reducible]

instance Features.Person.instDecidableEqFeatures : DecidableEq Features

Equations

• Features.Person.instDecidableEqFeatures = Features.Person.instDecidableEqFeatures.decEq

def Features.Person.instDecidableEqFeatures.decEq (x✝ x✝¹ : Features) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance Features.Person.instReprFeatures : Repr Features

Equations

• Features.Person.instReprFeatures = { reprPrec := Features.Person.instReprFeatures.repr }

def Features.Person.instReprFeatures.repr : Features → ℕ → Std.Format

Equations

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

def Features.Person.Features.wellFormed (pf : Features) : Bool

Well-formedness: [+author] → [+participant]. An author (speaker) is necessarily a participant.

Equations

• pf.wellFormed = (!pf.hasAuthor || pf.hasParticipant)

def Features.Person.first : Features

1st person features: [+participant, +author].

Equations

• Features.Person.first = { hasParticipant := true, hasAuthor := true }

def Features.Person.second : Features

2nd person features: [+participant, −author].

Equations

• Features.Person.second = { hasParticipant := true, hasAuthor := false }

def Features.Person.third : Features

3rd person features: [−participant, −author].

Equations

• Features.Person.third = { hasParticipant := false, hasAuthor := false }

def Features.Prominence.PersonLevel.toFeatures : PersonLevel → Person.Features

Decompose PersonLevel into binary person features.

Equations

• Features.Prominence.PersonLevel.first.toFeatures = Features.Person.first
• Features.Prominence.PersonLevel.second.toFeatures = Features.Person.second
• Features.Prominence.PersonLevel.third.toFeatures = Features.Person.third

def Features.Prominence.PersonLevel.ofUDPerson : UD.Person → Option PersonLevel

Convert UD.Person to PersonLevel. The UD .zero (impersonal) case has no PersonLevel analogue; everything else is direct.

Equations

• Features.Prominence.PersonLevel.ofUDPerson UD.Person.first = some Features.Prominence.PersonLevel.first
• Features.Prominence.PersonLevel.ofUDPerson UD.Person.second = some Features.Prominence.PersonLevel.second
• Features.Prominence.PersonLevel.ofUDPerson UD.Person.third = some Features.Prominence.PersonLevel.third
• Features.Prominence.PersonLevel.ofUDPerson UD.Person.zero = none

@[simp]

theorem Features.Person.first_wellFormed : first.wellFormed = true

@[simp]

theorem Features.Person.second_wellFormed : second.wellFormed = true

@[simp]

theorem Features.Person.third_wellFormed : third.wellFormed = true

theorem Features.Person.illFormed_only : { hasParticipant := false, hasAuthor := true }.wellFormed = false

The ill-formed combination [−participant, +author] is the only combination that violates well-formedness.

theorem Features.Person.exactly_three_wellFormed : (List.filter Features.wellFormed [{ hasParticipant := true, hasAuthor := true }, { hasParticipant := true, hasAuthor := false }, { hasParticipant := false, hasAuthor := true }, { hasParticipant := false, hasAuthor := false }]).length = 3

There are exactly 3 well-formed feature combinations (= 3 persons).

theorem Features.Person.PersonLevel.toFeatures_wellFormed (p : Prominence.PersonLevel) : p.toFeatures.wellFormed = true

All person levels yield well-formed features.

theorem Features.Person.PersonLevel.isSAP_eq_participant (p : Prominence.PersonLevel) : p.isSAP = p.toFeatures.hasParticipant

PersonLevel.isSAP = Features.hasParticipant.

@[implicit_reducible]

instance Features.Person.instPhiFeaturesFeatures : PhiFeatures Features

Person features are a PhiFeatures instance: outer = hasParticipant, inner = hasAuthor.

All shared properties (no_four_way, specLevel, wellFormed, injective) are inherited by construction.

Equations

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

@[simp]

theorem Features.Person.first_is_maximal : PhiFeatures.toPair first = PrivativePair.maximal

The three canonical person values map to the three PrivativePair cells.

@[simp]

theorem Features.Person.second_is_intermediate : PhiFeatures.toPair second = PrivativePair.intermediate

@[simp]

theorem Features.Person.third_is_minimal : PhiFeatures.toPair third = PrivativePair.minimal

theorem Features.Person.no_fourth_person (a b c d : Features) : a.wellFormed = true → b.wellFormed = true → c.wellFormed = true → d.wellFormed = true → a ≠ b → a ≠ c → a ≠ d → b ≠ c → b ≠ d → c ≠ d → False

No 4-way singular person distinction (inherited from PhiFeatures).

inductive Features.Person.Category : Type

The 8 referential person categories (@cite{cysouw-2009}, Fig 10.1).

Three singular categories (individual speech act roles) and five group categories (attested combinations of participants).

• s1 : Category
• s2 : Category
• s3 : Category
• minIncl : Category
• augIncl : Category
• excl : Category
• secondGrp : Category
• thirdGrp : Category

@[implicit_reducible]

instance Features.Person.instDecidableEqCategory : DecidableEq Category

Equations

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

@[implicit_reducible]

instance Features.Person.instReprCategory : Repr Category

Equations

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

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

Equations

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

@[implicit_reducible]

instance Features.Person.instInhabitedCategory : Inhabited Category

Equations

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

def Features.Person.instInhabitedCategory.default : Category

Equations

• Features.Person.instInhabitedCategory.default = Features.Person.Category.s1

def Features.Person.Category.all : List Category

All 8 categories in canonical order (singular, then group).

Equations

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

theorem Features.Person.Category.all_length : all.length = 8

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

Is this a singular (individual) category?

Equations

• c.IsSingular = (c = Features.Person.Category.s1 ∨ c = Features.Person.Category.s2 ∨ c = Features.Person.Category.s3)

@[implicit_reducible]

instance Features.Person.Category.instDecidablePredIsSingular : DecidablePred IsSingular

Equations

• x✝.instDecidablePredIsSingular = Features.Person.Category.instDecidablePredIsSingular._aux_1 x✝

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

Is this a group (non-singular) category?

Equations

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

@[implicit_reducible]

instance Features.Person.Category.instDecidablePredIsGroup : DecidablePred IsGroup

Equations

• x✝.instDecidablePredIsGroup = Features.Person.Category.instDecidablePredIsGroup._aux_1 x✝

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

Is this part of the first person complex (contains speaker as part of a group)?

Equations

• c.IsFirstPersonComplex = (c = Features.Person.Category.minIncl ∨ c = Features.Person.Category.augIncl ∨ c = Features.Person.Category.excl)

@[implicit_reducible]

instance Features.Person.Category.instDecidablePredIsFirstPersonComplex : DecidablePred IsFirstPersonComplex

Equations

• x✝.instDecidablePredIsFirstPersonComplex = Features.Person.Category.instDecidablePredIsFirstPersonComplex._aux_1 x✝

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

Is this an inclusive category (contains both speaker and addressee)?

Equations

• c.IsInclusive = (c = Features.Person.Category.minIncl ∨ c = Features.Person.Category.augIncl)

@[implicit_reducible]

instance Features.Person.Category.instDecidablePredIsInclusive : DecidablePred IsInclusive

Equations

• x✝.instDecidablePredIsInclusive = Features.Person.Category.instDecidablePredIsInclusive._aux_1 x✝

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

Does this category include the speaker?

Equations

• c.IncludesSpeaker = (c = Features.Person.Category.s1 ∨ c = Features.Person.Category.minIncl ∨ c = Features.Person.Category.augIncl ∨ c = Features.Person.Category.excl)

@[implicit_reducible]

instance Features.Person.Category.instDecidablePredIncludesSpeaker : DecidablePred IncludesSpeaker

Equations

• x✝.instDecidablePredIncludesSpeaker = Features.Person.Category.instDecidablePredIncludesSpeaker._aux_1 x✝

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

Does this category include the addressee?

Equations

• c.IncludesAddressee = (c = Features.Person.Category.s2 ∨ c = Features.Person.Category.minIncl ∨ c = Features.Person.Category.augIncl ∨ c = Features.Person.Category.secondGrp)

@[implicit_reducible]

instance Features.Person.Category.instDecidablePredIncludesAddressee : DecidablePred IncludesAddressee

Equations

• x✝.instDecidablePredIncludesAddressee = Features.Person.Category.instDecidablePredIncludesAddressee._aux_1 x✝

def Features.Person.Category.toUDPerson : Category → Option UD.Person

Map singular Category to UD.Person.

Equations

• Features.Person.Category.s1.toUDPerson = some UD.Person.first
• Features.Person.Category.s2.toUDPerson = some UD.Person.second
• Features.Person.Category.s3.toUDPerson = some UD.Person.third
• x✝.toUDPerson = none

def Features.Person.Category.fromUDPerson : UD.Person → Option Category

Map UD.Person to singular Category.

Equations

• Features.Person.Category.fromUDPerson UD.Person.first = some Features.Person.Category.s1
• Features.Person.Category.fromUDPerson UD.Person.second = some Features.Person.Category.s2
• Features.Person.Category.fromUDPerson UD.Person.third = some Features.Person.Category.s3
• Features.Person.Category.fromUDPerson UD.Person.zero = none

theorem Features.Person.ud_person_roundtrip : (Category.fromUDPerson UD.Person.first).bind Category.toUDPerson = some UD.Person.first ∧ (Category.fromUDPerson UD.Person.second).bind Category.toUDPerson = some UD.Person.second ∧ (Category.fromUDPerson UD.Person.third).bind Category.toUDPerson = some UD.Person.third

Round-trip: UD.Person → Category → UD.Person is identity.

def Features.Person.Category.toUDPersonNumber : Category → Option (UD.Person × UD.Number)

Map Category to traditional person × number pair.

Equations

• Features.Person.Category.s1.toUDPersonNumber = some (UD.Person.first, UD.Number.Sing)
• Features.Person.Category.s2.toUDPersonNumber = some (UD.Person.second, UD.Number.Sing)
• Features.Person.Category.s3.toUDPersonNumber = some (UD.Person.third, UD.Number.Sing)
• Features.Person.Category.minIncl.toUDPersonNumber = some (UD.Person.first, UD.Number.Dual)
• Features.Person.Category.augIncl.toUDPersonNumber = some (UD.Person.first, UD.Number.Plur)
• Features.Person.Category.excl.toUDPersonNumber = some (UD.Person.first, UD.Number.Plur)
• Features.Person.Category.secondGrp.toUDPersonNumber = some (UD.Person.second, UD.Number.Plur)
• Features.Person.Category.thirdGrp.toUDPersonNumber = some (UD.Person.third, UD.Number.Plur)

theorem Features.Person.ud_conflates_incl_excl : Category.augIncl.toUDPersonNumber = Category.excl.toUDPersonNumber

UD conflates inclusive and exclusive under first person plural.

def Features.Person.Category.toFeatures : Category → Features

Decompose any Category into binary person features.

• hasAuthor = includesSpeaker: the referent contains the speaker.
• hasParticipant = includesSpeaker ∨ includesAddressee: the referent contains at least one speech-act participant.

Features underdetermine group categories: excl, minIncl, and augIncl all map to ⟨true, true⟩. The full Category type is needed for number and inclusivity distinctions.

Equations

• Features.Person.Category.s1.toFeatures = { hasParticipant := true, hasAuthor := true }
• Features.Person.Category.s2.toFeatures = { hasParticipant := true, hasAuthor := false }
• Features.Person.Category.s3.toFeatures = { hasParticipant := false, hasAuthor := false }
• Features.Person.Category.minIncl.toFeatures = { hasParticipant := true, hasAuthor := true }
• Features.Person.Category.augIncl.toFeatures = { hasParticipant := true, hasAuthor := true }
• Features.Person.Category.excl.toFeatures = { hasParticipant := true, hasAuthor := true }
• Features.Person.Category.secondGrp.toFeatures = { hasParticipant := true, hasAuthor := false }
• Features.Person.Category.thirdGrp.toFeatures = { hasParticipant := false, hasAuthor := false }

theorem Features.Person.toFeatures_author_iff_speaker (p : Category) : p.toFeatures.hasAuthor = true ↔ p.IncludesSpeaker

hasAuthor ↔ IncludesSpeaker for all categories.

theorem Features.Person.toFeatures_participant_iff_sap (p : Category) : p.toFeatures.hasParticipant = true ↔ p.IncludesSpeaker ∨ p.IncludesAddressee

hasParticipant ↔ IncludesSpeaker ∨ IncludesAddressee for all categories.

theorem Features.Person.toFeatures_wellFormed (p : Category) : p.toFeatures.wellFormed = true

All 8 categories yield well-formed features.

def Features.Person.Category.toPersonLevel : Category → Option Prominence.PersonLevel

Map singular Category to PersonLevel (the canonical three-way person distinction used by PersonGeometry, DifferentialIndexing, etc.). Group categories map to none — they encode number distinctions that PersonLevel does not capture.

Equations

• Features.Person.Category.s1.toPersonLevel = some Features.Prominence.PersonLevel.first
• Features.Person.Category.s2.toPersonLevel = some Features.Prominence.PersonLevel.second
• Features.Person.Category.s3.toPersonLevel = some Features.Prominence.PersonLevel.third
• x✝.toPersonLevel = none

def Features.Person.Category.fromPersonLevel : Prominence.PersonLevel → Category

Map PersonLevel to singular Category.

Equations

• Features.Person.Category.fromPersonLevel Features.Prominence.PersonLevel.first = Features.Person.Category.s1
• Features.Person.Category.fromPersonLevel Features.Prominence.PersonLevel.second = Features.Person.Category.s2
• Features.Person.Category.fromPersonLevel Features.Prominence.PersonLevel.third = Features.Person.Category.s3

theorem Features.Person.personLevel_roundtrip (p : Prominence.PersonLevel) : (Category.fromPersonLevel p).toPersonLevel = some p

Round-trip: PersonLevel → Category → PersonLevel is identity.

theorem Features.Person.includesSpeaker_iff_author : Category.s1.IncludesSpeaker ∧ ¬Category.s2.IncludesSpeaker ∧ ¬Category.s3.IncludesSpeaker

includesSpeaker on Category = hasParticipant ∧ hasAuthor on PersonLevel for singular categories: speaker (s1) = [+participant, +author], addressee (s2) = [+participant, −author], other (s3) = [−participant, −author]. This unifies the Category decomposition in Spanish/PersonFeatures.lean with PersonGeometry.decomposePerson.

theorem Features.Person.includesAddressee_iff_participant_not_author : ¬Category.s1.IncludesAddressee ∧ Category.s2.IncludesAddressee ∧ ¬Category.s3.IncludesAddressee

theorem Features.Person.singular_sap_match : (Category.s1.IncludesSpeaker ∨ Category.s1.IncludesAddressee) ∧ (Category.s2.IncludesSpeaker ∨ Category.s2.IncludesAddressee) ∧ ¬(Category.s3.IncludesSpeaker ∨ Category.s3.IncludesAddressee)

SAP (speech-act participant) = IncludesSpeaker ∨ IncludesAddressee for singular categories. This matches PersonLevel.isSAP.

theorem Features.Person.s1_features_match : Category.s1.toFeatures = Prominence.PersonLevel.first.toFeatures

Singular categories: Category.toFeatures agrees with PersonLevel.toFeatures via the PersonLevel bridge.

theorem Features.Person.s2_features_match : Category.s2.toFeatures = Prominence.PersonLevel.second.toFeatures

theorem Features.Person.s3_features_match : Category.s3.toFeatures = Prominence.PersonLevel.third.toFeatures

inductive Features.Person.EpistemicAuthority : Type

Epistemic authority marking on verb agreement. @cite{bickel-nichols-2001}

Some languages (Akhvakh, Kathmandu Newari, Tibetan) mark whether the speaker has direct epistemic authority over the event. The morphological distinction cross-cuts person but correlates with it:

• conjunct: speaker has authority (1st person declarative, 2nd person interrogative)
• disjunct: speaker lacks authority (2nd/3rd declarative, 1st/3rd interrogative)

• conjunct : EpistemicAuthority
• disjunct : EpistemicAuthority

@[implicit_reducible]

instance Features.Person.instDecidableEqEpistemicAuthority : DecidableEq EpistemicAuthority

Equations

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

@[implicit_reducible]

instance Features.Person.instReprEpistemicAuthority : Repr EpistemicAuthority

Equations

• Features.Person.instReprEpistemicAuthority = { reprPrec := Features.Person.instReprEpistemicAuthority.repr }

def Features.Person.instReprEpistemicAuthority.repr : EpistemicAuthority → ℕ → Std.Format

Equations

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