Harbour (2016): Impossible Persons

@cite{harbour-2016}

Formalizes the core results of:

Harbour, D. (2016). Impossible Persons. Linguistic Inquiry Monographs 74. MIT Press.

The Partition Problem

Person categories are not primitives — they are derived from two privative features [±author] and [±participant] operating on sets of discourse participants. These features have the containment relation [+author] ⊂ [+participant] (an author is necessarily a participant), making them an instance of the Features.PrivativePair abstraction.

The key insight: features evaluate over groups (non-empty sets of individuals), not just atomic referents. A group is [+author] iff it contains the speaker; [+participant] iff it contains any speech-act participant.

Results Formalized

1. Discourse groups derive the 8 person categories (Ch 4–5). Three discourse roles (speaker, addressee, other) × atomicity yield exactly the 8 categories from @cite{cysouw-2009}'s typological inventory. No more, no fewer.

2. Person–number isomorphism (Ch 9: "The Phi Kernel"). Person features [±participant, ±author] and number features [±minimal, ±atomic] instantiate the same PrivativePair skeleton via PhiFeatures.

3. Clusivity derived (Ch 5). Inclusive/exclusive is not a feature — it falls out of person × atomicity. A [+author] non-atomic group is inclusive iff it also contains the addressee; exclusive otherwise.

4. Impossibility results (Ch 4–5). No 4-way singular person; no person system with exclusive but not inclusive.

5. Containment hierarchy (Ch 9). The person hierarchy 1 > 2 > 3 and number hierarchy sg > du > pl both reduce to the specification ordering of PrivativePair. Bridge theorem specLevel_agrees_with_segments connects this to @cite{bejar-rezac-2009}'s articulated segments.

inductive Harbour2016.Clusivity : Type

Clusivity values for non-atomic [+author] groups.

@cite{harbour-2016} Ch 5: clusivity is derived from the interaction of person features and group composition, not from a stipulated [±inclusive] feature.

• inclusive : Clusivity
• exclusive : Clusivity

@[implicit_reducible]

instance Harbour2016.instDecidableEqClusivity : DecidableEq Clusivity

Equations

• Harbour2016.instDecidableEqClusivity x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Harbour2016.instReprClusivity.repr : Clusivity → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Harbour2016.instReprClusivity : Repr Clusivity

Equations

• Harbour2016.instReprClusivity = { reprPrec := Harbour2016.instReprClusivity.repr }

structure Harbour2016.DiscourseGroup : Type

A discourse group: a non-empty collection of discourse participants, described by which role types are present and whether the group is atomic.

Three role types: speaker, addressee, other (non-SAP). A group must contain at least one member (nonempty). An atomic group contains exactly one individual (atomic_exclusive).

Representational note: @cite{harbour-2016} uses actual sets of individuals, making atomicity a derived property (|group| = 1). The Boolean encoding here requires explicit constraints (atomic_exclusive, nonatomic_multiple) to maintain consistency between the role flags and the atomicity flag. These constraints are representational guards, not part of Harbour's theory.

• hasSpeaker : Bool

  The group contains the speaker.

• hasAddressee : Bool

  The group contains the addressee.

• hasOther : Bool

  The group contains at least one non-SAP individual.

• isAtomic : Bool

  The group is a singleton (one individual).

• nonempty : (self.hasSpeaker || self.hasAddressee || decide (self.hasOther = true)) = true

  Non-empty: at least one role present.

• atomic_exclusive : self.isAtomic = true → (self.hasSpeaker && self.hasAddressee) = false ∧ (self.hasSpeaker && self.hasOther) = false ∧ (self.hasAddressee && self.hasOther) = false

  Atomic groups have at most one role type (no pair is both true). Combined with nonempty, this gives exactly one.

• nonatomic_multiple : self.isAtomic = false → (self.hasSpeaker && self.hasAddressee) = true ∨ (self.hasSpeaker && self.hasOther) = true ∨ (self.hasAddressee && self.hasOther) = true ∨ self.hasOther = true

  Non-atomic groups require multiple individuals. In the Boolean encoding, this means either ≥ 2 role types are present, or the "other" slot represents multiple individuals (as in thirdGrp = {3, 3}).

def Harbour2016.instDecidableEqDiscourseGroup.decEq (x✝ x✝¹ : DiscourseGroup) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance Harbour2016.instDecidableEqDiscourseGroup : DecidableEq DiscourseGroup

Equations

• Harbour2016.instDecidableEqDiscourseGroup = Harbour2016.instDecidableEqDiscourseGroup.decEq

def Harbour2016.DiscourseGroup.author (g : DiscourseGroup) : Bool

[+author]: the group contains the speaker. @cite{harbour-2016} Ch 4: features evaluate over sets, not atoms.

Equations

• g.author = g.hasSpeaker

def Harbour2016.DiscourseGroup.participant (g : DiscourseGroup) : Bool

[+participant]: the group contains at least one SAP.

Equations

• g.participant = (g.hasSpeaker || g.hasAddressee)

def Harbour2016.DiscourseGroup.toPrivativePair (g : DiscourseGroup) : Features.PrivativePair

Extract the PrivativePair: outer = participant, inner = author.

Equations

• g.toPrivativePair = { outer := g.participant, inner := g.author }

theorem Harbour2016.DiscourseGroup.wellFormed (g : DiscourseGroup) : g.toPrivativePair.wellFormed = true

Person features on groups are always well-formed: [+author] → [+participant] because the speaker is a participant.

theorem Harbour2016.DiscourseGroup.agrees_with_core (g : DiscourseGroup) : g.toPrivativePair = Features.PhiFeatures.toPair { hasParticipant := g.participant, hasAuthor := g.author }

Group-level person features agree with Features.Person.Features on the atomic (singular) cases.

def Harbour2016.DiscourseGroup.toCategory (g : DiscourseGroup) : Features.Person.Category

Map a DiscourseGroup to the corresponding Cysouw Category.

Equations

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

theorem Harbour2016.all_categories_reachable (c : Features.Person.Category) : ∃ (g : DiscourseGroup), g.toCategory = c

All 8 Cysouw categories are reachable from discourse groups.

theorem Harbour2016.group_features_match_category (c : Features.Person.Category) : ∃ (g : DiscourseGroup), g.toCategory = c ∧ g.toPrivativePair = Features.PhiFeatures.toPair c.toFeatures

Group-level person features agree with Category.toFeatures: the PrivativePair extracted from a group matches the one extracted from its Cysouw category.

This is the key consistency result: the set-level feature evaluation (@cite{harbour-2016}) and the individual-level feature assignment (Core) agree on the person feature values for each category.

theorem Harbour2016.person_number_isomorphism : Features.PhiFeatures.toPair Features.Number.singularF = Features.PhiFeatures.toPair Features.Person.first ∧ Features.PhiFeatures.toPair Features.Number.dualF = Features.PhiFeatures.toPair Features.Person.second ∧ Features.PhiFeatures.toPair Features.Number.pluralF = Features.PhiFeatures.toPair Features.Person.third

Person and number share the same PrivativePair skeleton.

This is @cite{harbour-2016}'s "phi kernel" (Ch 9): the structural parallel between person (1st/2nd/3rd) and number (singular/dual/plural) is not accidental — both are instances of the same 2-feature containment geometry.

• Person maximal = 1st person = [+participant, +author]
• Number maximal = singular = [+minimal, +atomic]
• Both map to PrivativePair.maximal = ⟨true, true⟩

And so on for intermediate (2nd/dual) and minimal (3rd/plural).

theorem Harbour2016.person_number_via_cells : Features.PhiFeatures.toPair Features.Person.first = Features.PrivativePair.maximal ∧ Features.PhiFeatures.toPair Features.Person.second = Features.PrivativePair.intermediate ∧ Features.PhiFeatures.toPair Features.Person.third = Features.PrivativePair.minimal ∧ Features.PhiFeatures.toPair Features.Number.singularF = Features.PrivativePair.maximal ∧ Features.PhiFeatures.toPair Features.Number.dualF = Features.PrivativePair.intermediate ∧ Features.PhiFeatures.toPair Features.Number.pluralF = Features.PrivativePair.minimal

The isomorphism factors through PrivativePair's canonical cells.

def Harbour2016.clusivityFromGroup (g : DiscourseGroup) : Option Clusivity

Clusivity is derived, not stipulated.

A non-atomic [+author] group (= first person non-singular) is:

• inclusive iff it also contains the addressee
• exclusive iff it does not

No [±inclusive] feature is needed — clusivity falls out of the interaction between person features and group composition (Ch 5).

Equations

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

theorem Harbour2016.inclusive_iff_addressee (g : DiscourseGroup) (hna : g.isAtomic = false) (hspk : g.hasSpeaker = true) : clusivityFromGroup g = some Clusivity.inclusive ↔ g.hasAddressee = true

Inclusive groups are exactly those with both speaker and addressee.

theorem Harbour2016.clusivity_matches_category : clusivityFromGroup { hasSpeaker := true, hasAddressee := true, hasOther := false, isAtomic := false, nonempty := ⋯, atomic_exclusive := ⋯, nonatomic_multiple := ⋯ } = some Clusivity.inclusive ∧ clusivityFromGroup { hasSpeaker := true, hasAddressee := true, hasOther := true, isAtomic := false, nonempty := ⋯, atomic_exclusive := ⋯, nonatomic_multiple := ⋯ } = some Clusivity.inclusive ∧ clusivityFromGroup { hasSpeaker := true, hasAddressee := false, hasOther := true, isAtomic := false, nonempty := ⋯, atomic_exclusive := ⋯, nonatomic_multiple := ⋯ } = some Clusivity.exclusive

Clusivity agrees with Category.isInclusive: categories that Cysouw marks as inclusive (minIncl, augIncl) are exactly the non-atomic [+author] groups that contain the addressee.

theorem Harbour2016.no_four_singular_persons (a b c d : Features.Person.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. (Immediate from Features.Person.no_fourth_person.)

Since singular categories are atomic discourse groups, and person features on atomic groups reduce to individual-level features, the 3-cell PrivativePair limit applies directly (Ch 4).

theorem Harbour2016.no_exclusive_without_inclusive : (∃ (g : DiscourseGroup), clusivityFromGroup g = some Clusivity.exclusive) → ∃ (g : DiscourseGroup), clusivityFromGroup g = some Clusivity.inclusive

No exclusive without inclusive (system-level).

@cite{harbour-2016} Ch 5, §5.3: if a person system has the exclusive category (non-atomic [+author] groups without the addressee), then inclusive groups are also constructible from the same feature inventory. Both configurations use [+author] on a non-atomic group; they differ only in whether the addressee is present in the group.

The feature system [±participant, ±author] operating over non-atomic groups necessarily generates both inclusive and exclusive configurations. Any feature inventory supporting exclusive automatically supports inclusive — this is an inherent consequence of the feature system, not an independent parameter.

theorem Harbour2016.person_hierarchy_is_spec_ordering : Features.PhiFeatures.specLevel Features.Person.first > Features.PhiFeatures.specLevel Features.Person.second ∧ Features.PhiFeatures.specLevel Features.Person.second > Features.PhiFeatures.specLevel Features.Person.third

The person hierarchy 1 > 2 > 3 is the specification ordering of PrivativePair: maximal > intermediate > minimal. This connects @cite{harbour-2016}'s lattice approach to the person hierarchy used in @cite{bejar-rezac-2009}'s Cyclic Agree and @cite{preminger-2014}'s relativized probing.

theorem Harbour2016.number_hierarchy_is_spec_ordering : Features.PhiFeatures.specLevel Features.Number.singularF > Features.PhiFeatures.specLevel Features.Number.dualF ∧ Features.PhiFeatures.specLevel Features.Number.dualF > Features.PhiFeatures.specLevel Features.Number.pluralF

The number hierarchy sg > du > pl is the same specification ordering.

theorem Harbour2016.specLevel_agrees_with_segments (p : Features.Prominence.PersonLevel) : Features.PhiFeatures.specLevel p.toFeatures + 1 = (Minimalist.CyclicAgree.personSpec Minimalist.CyclicAgree.Geometry.standard p).length

The person hierarchy from PrivativePair.specLevel agrees with the segment count hierarchy from @cite{bejar-rezac-2009}'s Cyclic Agree.

In the standard geometry, specLevel + 1 = segment count:

• 1st: specLevel 2, segments [π, participant, speaker] (length 3)
• 2nd: specLevel 1, segments [π, participant] (length 2)
• 3rd: specLevel 0, segments [π] (length 1)

This is the formal bridge between @cite{harbour-2016}'s algebraic person hierarchy (PrivativePair specification level) and @cite{bejar-rezac-2009}'s syntactic one (articulated segment count). The person hierarchy is one hierarchy realized in two independent formalizations: featural (spec level) and configurational (probe depth).

Every attested number system from @cite{corbett-2000} can be generated by some well-formed @cite{harbour-2016} configuration. This bridges the typological inventory (observed systems) with the feature geometry (generative mechanism).

The bridge is a SUBSET relation: a language may not lexicalize all
categories its feature geometry makes available (syncretism, facultative
marking). What matters is that every attested category IS generated. 

theorem Harbour2016.attested_number_systems_derivable : (Corbett2000.pirahaNS.values.all fun (x : Corbett2000.NumberValue) => { hasAtomic := false, hasMinimal := false, hasAdditive := false, recurseOnPlural := false, recurseOnAdditive := false }.categories.contains x) = true ∧ (Corbett2000.englishNS.values.all fun (x : Corbett2000.NumberValue) => { hasAtomic := true, hasMinimal := false, hasAdditive := false, recurseOnPlural := false, recurseOnAdditive := false }.categories.contains x) = true ∧ (Corbett2000.russianNS.values.all fun (x : Corbett2000.NumberValue) => { hasAtomic := true, hasMinimal := false, hasAdditive := false, recurseOnPlural := false, recurseOnAdditive := false }.categories.contains x) = true ∧ (Corbett2000.upperSorbianNS.values.all fun (x : Corbett2000.NumberValue) => { hasAtomic := true, hasMinimal := true, hasAdditive := false, recurseOnPlural := false, recurseOnAdditive := false }.categories.contains x) = true ∧ (Corbett2000.baysoNS.values.all fun (x : Corbett2000.NumberValue) => { hasAtomic := true, hasMinimal := false, hasAdditive := true, recurseOnPlural := false, recurseOnAdditive := false }.categories.contains x) = true ∧ (Corbett2000.sloveneNS.values.all fun (x : Corbett2000.NumberValue) => { hasAtomic := true, hasMinimal := true, hasAdditive := false, recurseOnPlural := false, recurseOnAdditive := false }.categories.contains x) = true ∧ (Corbett2000.larikeNS.values.all fun (x : Corbett2000.NumberValue) => { hasAtomic := true, hasMinimal := true, hasAdditive := false, recurseOnPlural := true, recurseOnAdditive := false }.categories.contains x) = true ∧ (Corbett2000.lihirNS.values.all fun (x : Corbett2000.NumberValue) => { hasAtomic := true, hasMinimal := true, hasAdditive := true, recurseOnPlural := true, recurseOnAdditive := false }.categories.contains x) = true ∧ (Corbett2000.japaneseNS.values.all fun (x : Corbett2000.NumberValue) => { hasAtomic := true, hasMinimal := false, hasAdditive := false, recurseOnPlural := false, recurseOnAdditive := false }.categories.contains x) = true

Every attested number system's values are a subset of what some well-formed Harbour configuration generates.

• Pirahã: no features → no categories
• English/Russian/Japanese: [±atomic] only → {sg, pl}
• Upper Sorbian/Slovene: [±atomic, ±minimal] → {sg, du, pl}
• Bayso: [±atomic, ±additive] → {sg, pl, pauc}
• Larike: [±atomic, ±minimal] + [±minimal] recursion → {sg, du, pl, trial, grpl}
• Lihir: [±atomic, ±minimal, ±additive] + [±minimal] recursion → {sg, du, pl, trial, grpl, pauc}

theorem Harbour2016.minAug_systems_derivable : (Corbett2000.winnebagoNS.values.all fun (x : Corbett2000.NumberValue) => { hasAtomic := false, hasMinimal := true, hasAdditive := false, recurseOnPlural := false, recurseOnAdditive := false }.categories.contains x) = true ∧ (Corbett2000.rembarrnganS.values.all fun (x : Corbett2000.NumberValue) => { hasAtomic := false, hasMinimal := true, hasAdditive := false, recurseOnPlural := true, recurseOnAdditive := false }.categories.contains x) = true ∧ (Corbett2000.mebengokreNS.values.all fun (x : Corbett2000.NumberValue) => { hasAtomic := false, hasMinimal := true, hasAdditive := true, recurseOnPlural := false, recurseOnAdditive := false }.categories.contains x) = true

MIN/AUG systems from @cite{harbour-2014} Table 3, now expressible with the expanded Category type.

theorem Harbour2016.bridge_configs_wellFormed : { hasAtomic := false, hasMinimal := false, hasAdditive := false, recurseOnPlural := false, recurseOnAdditive := false }.wellFormed = true ∧ { hasAtomic := true, hasMinimal := false, hasAdditive := false, recurseOnPlural := false, recurseOnAdditive := false }.wellFormed = true ∧ { hasAtomic := true, hasMinimal := true, hasAdditive := false, recurseOnPlural := false, recurseOnAdditive := false }.wellFormed = true ∧ { hasAtomic := true, hasMinimal := false, hasAdditive := true, recurseOnPlural := false, recurseOnAdditive := false }.wellFormed = true ∧ { hasAtomic := true, hasMinimal := true, hasAdditive := false, recurseOnPlural := true, recurseOnAdditive := false }.wellFormed = true ∧ { hasAtomic := true, hasMinimal := true, hasAdditive := true, recurseOnPlural := true, recurseOnAdditive := false }.wellFormed = true ∧ { hasAtomic := false, hasMinimal := true, hasAdditive := false, recurseOnPlural := false, recurseOnAdditive := false }.wellFormed = true ∧ { hasAtomic := false, hasMinimal := true, hasAdditive := false, recurseOnPlural := true, recurseOnAdditive := false }.wellFormed = true ∧ { hasAtomic := false, hasMinimal := true, hasAdditive := true, recurseOnPlural := false, recurseOnAdditive := false }.wellFormed = true

The Harbour configurations used in the bridge are all well-formed.