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/Core/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 Core.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).

instance Core.Person.instDecidableEqFeatures : DecidableEq Features

Equations

• Core.Person.instDecidableEqFeatures = Core.Person.instDecidableEqFeatures.decEq

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

Equations

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

instance Core.Person.instBEqFeatures : BEq Features

Equations

• Core.Person.instBEqFeatures = { beq := Core.Person.instBEqFeatures.beq }

def Core.Person.instBEqFeatures.beq : Features → Features → Bool

Equations

• Core.Person.instBEqFeatures.beq { hasParticipant := a, hasAuthor := a_1 } { hasParticipant := b, hasAuthor := b_1 } = (a == b && a_1 == b_1)
• Core.Person.instBEqFeatures.beq x✝¹ x✝ = false

instance Core.Person.instReprFeatures : Repr Features

Equations

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

def Core.Person.instReprFeatures.repr : Features → Nat → Std.Format

Equations

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

def Core.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 Core.Person.first : Features

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

Equations

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

def Core.Person.second : Features

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

Equations

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

def Core.Person.third : Features

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

Equations

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

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

Decompose PersonLevel into binary person features.

Equations

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

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

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

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

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

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

theorem Core.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 Core.Person.PersonLevel.toFeatures_wellFormed (p : Prominence.PersonLevel) : p.toFeatures.wellFormed = true

All person levels yield well-formed features.

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

PersonLevel.isSAP = Features.hasParticipant.

inductive Core.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

instance Core.Person.instDecidableEqCategory : DecidableEq Category

Equations

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

def Core.Person.instBEqCategory.beq : Category → Category → Bool

Equations

• Core.Person.instBEqCategory.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Core.Person.instBEqCategory : BEq Category

Equations

• Core.Person.instBEqCategory = { beq := Core.Person.instBEqCategory.beq }

def Core.Person.instReprCategory.repr : Category → Nat → Std.Format

Equations

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

instance Core.Person.instReprCategory : Repr Category

Equations

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

instance Core.Person.instInhabitedCategory : Inhabited Category

Equations

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

def Core.Person.instInhabitedCategory.default : Category

Equations

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

def Core.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 Core.Person.Category.all_length : all.length = 8

def Core.Person.Category.isSingular : Category → Bool

Is this a singular (individual) category?

Equations

• Core.Person.Category.s1.isSingular = true
• Core.Person.Category.s2.isSingular = true
• Core.Person.Category.s3.isSingular = true
• x✝.isSingular = false

def Core.Person.Category.isGroup : Category → Bool

Is this a group (non-singular) category?

Equations

• Core.Person.Category.minIncl.isGroup = true
• Core.Person.Category.augIncl.isGroup = true
• Core.Person.Category.excl.isGroup = true
• Core.Person.Category.secondGrp.isGroup = true
• Core.Person.Category.thirdGrp.isGroup = true
• x✝.isGroup = false

def Core.Person.Category.isFirstPersonComplex : Category → Bool

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

Equations

• Core.Person.Category.minIncl.isFirstPersonComplex = true
• Core.Person.Category.augIncl.isFirstPersonComplex = true
• Core.Person.Category.excl.isFirstPersonComplex = true
• x✝.isFirstPersonComplex = false

def Core.Person.Category.isInclusive : Category → Bool

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

Equations

• Core.Person.Category.minIncl.isInclusive = true
• Core.Person.Category.augIncl.isInclusive = true
• x✝.isInclusive = false

def Core.Person.Category.includesSpeaker : Category → Bool

Does this category include the speaker?

Equations

• Core.Person.Category.s1.includesSpeaker = true
• Core.Person.Category.minIncl.includesSpeaker = true
• Core.Person.Category.augIncl.includesSpeaker = true
• Core.Person.Category.excl.includesSpeaker = true
• x✝.includesSpeaker = false

def Core.Person.Category.includesAddressee : Category → Bool

Does this category include the addressee?

Equations

• Core.Person.Category.s2.includesAddressee = true
• Core.Person.Category.minIncl.includesAddressee = true
• Core.Person.Category.augIncl.includesAddressee = true
• Core.Person.Category.secondGrp.includesAddressee = true
• x✝.includesAddressee = false

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

Map singular Category to UD.Person.

Equations

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

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

Map UD.Person to singular Category.

Equations

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

theorem Core.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 Core.Person.Category.toUDPersonNumber : Category → Option (UD.Person × UD.Number)

Map Category to traditional person × number pair.

Equations

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

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

UD conflates inclusive and exclusive under first person plural.

def Core.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

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

theorem Core.Person.toFeatures_author_eq_speaker (p : Category) : p.toFeatures.hasAuthor = p.includesSpeaker

hasAuthor = includesSpeaker for all categories.

theorem Core.Person.toFeatures_participant_eq_sap (p : Category) : p.toFeatures.hasParticipant = (p.includesSpeaker || p.includesAddressee)

hasParticipant = includesSpeaker ∨ includesAddressee for all categories.

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

All 8 categories yield well-formed features.

def Core.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

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

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

Map PersonLevel to singular Category.

Equations

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

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

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

theorem Core.Person.includesSpeaker_iff_author : Category.s1.includesSpeaker = true ∧ Category.s2.includesSpeaker = false ∧ Category.s3.includesSpeaker = false

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 Core.Person.includesAddressee_iff_participant_not_author : Category.s1.includesAddressee = false ∧ Category.s2.includesAddressee = true ∧ Category.s3.includesAddressee = false

theorem Core.Person.singular_sap_match : (Category.s1.includesSpeaker || Category.s1.includesAddressee) = true ∧ (Category.s2.includesSpeaker || Category.s2.includesAddressee) = true ∧ (Category.s3.includesSpeaker || Category.s3.includesAddressee) = false

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

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

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

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

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