Person

[HR02] [AH08] [AN18] [Har16a] [Cys09] [Sie04]

Two components of the person API:

§ 1–4: Person Features ([HR02]'s dependency organization, in the bivalent presentation surveyed by [AH08]; with [AN18]'s function-valued alternative). The typological category inventory (§5+) is [Cys09]'s, derived from these features — not their source. Decomposition of person into two bivalent 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. The hierarchy is carried as the cooccurrence filter inherited from Features.ContainmentPair — the descriptive convention of the feature-geometric tradition. [Har16a] ch. 9 rejects the filter: in his calculus +author(−participant(π)) is the quadripartition exclusive, not ill-formed — see Features/ContainmentPair.lean and Studies/Harbour2016.lean.

This decomposition is shared across theoretical frameworks:

• Minimalism: [Pre14], [BR09]
• Distributed Morphology: [MP26] (Fission)
• Typology: [Cys09], [Sie04]

The Minimalist-specific extension [±proximate] ([PZ18]) is added in Syntax/Minimalist/Phi/Geometry.lean.

The canonical analytical inventory (root Person) lives in Features/Person/Basic.lean; this file is its feature decomposition and referential-category layer.

§ 5–9: Person Categories ([Cys09]). 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) lives in Studies/Cysouw2009.lean.

structure Person.Features : Type

Bivalent 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 cut by the containment filter (WellFormed): 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 Person.instDecidableEqFeatures : DecidableEq Features

Equations

• Person.instDecidableEqFeatures = Person.instDecidableEqFeatures.decEq

def 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 Person.instReprFeatures : Repr Features

Equations

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

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

Equations

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

@[implicit_reducible]

instance Person.instFintypeFeatures : Fintype Features

Equations

• Person.instFintypeFeatures = Fintype.ofEquiv ((_ : Bool) × Bool) Person.Features.proxyTypeEquiv

def Person.firstF : Features

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

Equations

• Person.firstF = { hasParticipant := true, hasAuthor := true }

def Person.secondF : Features

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

Equations

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

def Person.thirdF : Features

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

Equations

• Person.thirdF = { hasParticipant := false, hasAuthor := false }

def Person.toFeatures : Person → Option Features

Decompose a person value into the binary features. The quadripartition cells share firstF (the two-feature system underdetermines clusivity — see Category.toFeatures); the impersonal zero has no featural decomposition.

Equations

• Person.first.toFeatures = some Person.firstF
• Person.firstInclusive.toFeatures = some Person.firstF
• Person.firstExclusive.toFeatures = some Person.firstF
• Person.second.toFeatures = some Person.secondF
• Person.third.toFeatures = some Person.thirdF
• Person.zero.toFeatures = none

def Person.featuresEquiv : Features ≃ Features.ContainmentPair

The [±participant, ±author] decomposition is carrier-equivalent to the containment pair: outer = participant, inner = author. One edge of the φ-feature iso-web (phiKernelEquiv, Studies/Harbour2016.lean).

Equations

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

@[implicit_reducible]

instance Person.instContainmentPairLikeFeatures : Features.ContainmentPairLike Features

Equations

• Person.instContainmentPairLikeFeatures = Features.ContainmentPairLike.ofEquiv Person.featuresEquiv

@[simp]

theorem Person.firstF_is_maximal : Features.ContainmentPairLike.toPair firstF = Features.ContainmentPair.maximal

The three canonical person values land on the three well-formed cells.

@[simp]

theorem Person.secondF_is_intermediate : Features.ContainmentPairLike.toPair secondF = Features.ContainmentPair.intermediate

@[simp]

theorem Person.thirdF_is_minimal : Features.ContainmentPairLike.toPair thirdF = Features.ContainmentPair.minimal

@[reducible, inline]

abbrev Person.Features.WellFormed (pf : Features) : Prop

Well-formedness: [+author] → [+participant] — an author is necessarily a participant. The geometry-tradition containment filter, inherited from ContainmentPair.WellFormed through the presentation.

Equations

• pf.WellFormed = Features.ContainmentPairLike.WellFormed pf

@[simp]

theorem Person.firstF_wellFormed : firstF.WellFormed

@[simp]

theorem Person.secondF_wellFormed : secondF.WellFormed

@[simp]

theorem Person.thirdF_wellFormed : thirdF.WellFormed

theorem Person.illFormed_only : ¬{ hasParticipant := false, hasAuthor := true }.WellFormed

The filtered combination [−participant, +author] is the only one that violates containment.

theorem Person.card_wellFormed : Fintype.card { pf : Features // pf.WellFormed } = 3

Exactly 3 well-formed feature combinations (= 3 persons) — the carrier count of the containment chain (ContainmentPair.card_wellFormed).

theorem Person.toFeatures_wellFormed (p : Person) (f : Features) : p.toFeatures = some f → f.WellFormed

Every defined decomposition is well-formed.

theorem Person.isSAP_iff_participant (p : Person) (f : Features) : p.toFeatures = some f → (p.IsSAP ↔ f.hasParticipant = true)

IsSAP is featural participanthood.

theorem Person.no_fourth_person (a b c d : Features) : a.WellFormed → b.WellFormed → c.WellFormed → d.WellFormed → a ≠ b → a ≠ c → a ≠ d → b ≠ c → b ≠ d → c ≠ d → False

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

inductive Person.Category : Type

The 8 referential person categories ([Cys09] ch. 3: the three singular participants plus the five attested of the seven logical groups of Table 3.1 — 1+1 (mass speaking) and 2+2 (present-audience-only) are dismissed as not grammaticalized, his §3.4).

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

@[implicit_reducible]

instance Person.instDecidableEqCategory : DecidableEq Category

Equations

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

@[implicit_reducible]

instance Person.instReprCategory : Repr Category

Equations

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

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

Equations

• Person.instReprCategory.repr Person.Category.s1 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Person.Category.s1")).group prec✝
• Person.instReprCategory.repr Person.Category.s2 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Person.Category.s2")).group prec✝
• Person.instReprCategory.repr Person.Category.s3 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Person.Category.s3")).group prec✝
• Person.instReprCategory.repr Person.Category.minIncl prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Person.Category.minIncl")).group prec✝
• Person.instReprCategory.repr Person.Category.augIncl prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Person.Category.augIncl")).group prec✝
• Person.instReprCategory.repr Person.Category.excl prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Person.Category.excl")).group prec✝
• Person.instReprCategory.repr Person.Category.secondGrp prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Person.Category.secondGrp")).group prec✝
• Person.instReprCategory.repr Person.Category.thirdGrp prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Person.Category.thirdGrp")).group prec✝

@[implicit_reducible]

instance Person.instInhabitedCategory : Inhabited Category

Equations

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

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

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

Is this a singular (individual) category?

Equations

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

@[implicit_reducible]

instance Person.Category.instDecidablePredIsSingular : DecidablePred IsSingular

Equations

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

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

Is this a group (non-singular) category?

Equations

• c.IsGroup = (c = Person.Category.minIncl ∨ c = Person.Category.augIncl ∨ c = Person.Category.excl ∨ c = Person.Category.secondGrp ∨ c = Person.Category.thirdGrp)

@[implicit_reducible]

instance Person.Category.instDecidablePredIsGroup : DecidablePred IsGroup

Equations

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

def 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 = Person.Category.minIncl ∨ c = Person.Category.augIncl ∨ c = Person.Category.excl)

@[implicit_reducible]

instance Person.Category.instDecidablePredIsFirstPersonComplex : DecidablePred IsFirstPersonComplex

Equations

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

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

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

Equations

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

@[implicit_reducible]

instance Person.Category.instDecidablePredIsInclusive : DecidablePred IsInclusive

Equations

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

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

Does this category include the speaker?

Equations

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

@[implicit_reducible]

instance Person.Category.instDecidablePredIncludesSpeaker : DecidablePred IncludesSpeaker

Equations

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

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

Does this category include the addressee?

Equations

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

@[implicit_reducible]

instance Person.Category.instDecidablePredIncludesAddressee : DecidablePred IncludesAddressee

Equations

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

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

Map singular Category to UD.Person.

Equations

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

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

Map UD.Person to singular Category.

Equations

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

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

Map Category to traditional person × number pair.

Equations

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

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

UD conflates inclusive and exclusive under first person plural.

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

The [Cys09] category a (person, number) coordinate pair realizes, over the canonical inventories. Clusivity rides on the person value; the minimal/augmented coordinates give the minimal/augmented inclusives directly (Tagalog kata = (firstInclusive, minimal) ↦ minIncl, the junction coordinates of Studies/Cysouw2009.lean); the Maori-type dual alignment maps there too; plain first non-singulars are a syncretism (none).

Equations

• Person.Category.ofPersonNumber Person.first Number.singular = some Person.Category.s1
• Person.Category.ofPersonNumber Person.firstInclusive Number.singular = some Person.Category.s1
• Person.Category.ofPersonNumber Person.firstExclusive Number.singular = some Person.Category.s1
• Person.Category.ofPersonNumber Person.second Number.singular = some Person.Category.s2
• Person.Category.ofPersonNumber Person.third Number.singular = some Person.Category.s3
• Person.Category.ofPersonNumber Person.firstInclusive Number.minimal = some Person.Category.minIncl
• Person.Category.ofPersonNumber Person.firstInclusive Number.dual = some Person.Category.minIncl
• Person.Category.ofPersonNumber Person.firstInclusive Number.augmented = some Person.Category.augIncl
• Person.Category.ofPersonNumber Person.firstInclusive Number.plural = some Person.Category.augIncl
• Person.Category.ofPersonNumber Person.firstInclusive Number.general = some Person.Category.augIncl
• Person.Category.ofPersonNumber Person.firstExclusive Number.dual = some Person.Category.excl
• Person.Category.ofPersonNumber Person.firstExclusive Number.plural = some Person.Category.excl
• Person.Category.ofPersonNumber Person.firstExclusive Number.general = some Person.Category.excl
• Person.Category.ofPersonNumber Person.firstExclusive Number.augmented = some Person.Category.excl
• Person.Category.ofPersonNumber Person.second Number.dual = some Person.Category.secondGrp
• Person.Category.ofPersonNumber Person.second Number.plural = some Person.Category.secondGrp
• Person.Category.ofPersonNumber Person.second Number.general = some Person.Category.secondGrp
• Person.Category.ofPersonNumber Person.third Number.dual = some Person.Category.thirdGrp
• Person.Category.ofPersonNumber Person.third Number.plural = some Person.Category.thirdGrp
• Person.Category.ofPersonNumber Person.third Number.general = some Person.Category.thirdGrp
• Person.Category.ofPersonNumber x✝¹ x✝ = none

def Person.Category.person : Category → Person

The person coordinate of each referential category — the projection the canonical inventory recovers losslessly where UD cannot: minIncl/augIncl ↦ firstInclusive, excl ↦ firstExclusive. (The number coordinate is toUDPersonNumber's second component; the full Category ≃ compatible (Person × Number) junction is the planned phase-2 theorem.)

Equations

• Person.Category.s1.person = Person.first
• Person.Category.s2.person = Person.second
• Person.Category.s3.person = Person.third
• Person.Category.minIncl.person = Person.firstInclusive
• Person.Category.augIncl.person = Person.firstInclusive
• Person.Category.excl.person = Person.firstExclusive
• Person.Category.secondGrp.person = Person.second
• Person.Category.thirdGrp.person = Person.third

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

The person projection tracks speaker inclusion.

theorem Person.person_separates_clusivity : Category.augIncl.person ≠ Category.excl.person

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

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

ofPersonNumber inverts the person projection: every category is recovered from its coordinates at some number value.

def Person.Category.toFeatures : Category → Features

Decompose any Category into binary person features (the framework-neutral Cysouw/Siewierska [±participant, ±author] decomposition).

• 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⟩ — a genuine property of the descriptive two-feature system (the Category enum carries the clusivity distinction the features cannot). The theory-laden Harbour-sign decomposition that does distinguish the exclusive (+author −participant) lives in the theory layer (as Studies.Harbour2016.signOf, over Syntax.Minimalist.Phi.Lattice operators), not here.

Equations

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

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

hasAuthor ↔ IncludesSpeaker for all categories.

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

hasParticipant ↔ IncludesSpeaker ∨ IncludesAddressee for all categories.

theorem Person.Category.toFeatures_wellFormed (p : Category) : p.toFeatures.WellFormed

All 8 categories yield well-formed features.

def Person.Category.ofSingularPerson : Person → Option Category

The singular Category of a tripartition person value.

Equations

• Person.Category.ofSingularPerson Person.first = some Person.Category.s1
• Person.Category.ofSingularPerson Person.second = some Person.Category.s2
• Person.Category.ofSingularPerson Person.third = some Person.Category.s3
• Person.Category.ofSingularPerson x✝ = none

theorem Person.singular_category_roundtrip (c : Category) (h : c.IsSingular) : Category.ofSingularPerson c.person = some c

Round-trip: singular categories are recovered from their person projection.

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

includesSpeaker on Category = hasParticipant ∧ hasAuthor on Person 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 Phi.Geometry.decomposePerson.

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

theorem 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 Person.isSAP.

theorem Person.singular_features_match (c : Category) : c.IsSingular → some c.toFeatures = c.person.toFeatures

Singular categories: Category.toFeatures agrees with the person decomposition through the person projection.

inductive Person.EpistemicAuthority : Type

Epistemic authority marking on verb agreement. [BN07]

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 Person.instDecidableEqEpistemicAuthority : DecidableEq EpistemicAuthority

Equations

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

@[implicit_reducible]

instance Person.instReprEpistemicAuthority : Repr EpistemicAuthority

Equations

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

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

Equations

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