Harbour (2016): Impossible Persons

Harbour derives the person categories as the cells of a partition of the lattice of referents, induced by two features, [±author] and [±participant], whose values act on lattices rather than test membership. The plus value of a feature adds its lattice pairwise (17), the minus value subtracts the lattice's maximum (19), Lexical Complementarity confines a cell that properly contains a sibling to the difference (31), and the host head discards the empty set. Over the ontology of speaker, hearer and one other, composing [±author] outermost yields the quadripartition and composing [±participant] outermost the tripartition. Harbour's signs for Cysouw's categories keep the exclusive apart from the inclusive, and his number chapter is the calculus of his 2014 paper, which generates the number systems Corbett attests. The same partitions organize the deixis of objects and spaces, English this and that realizing the author bipartition. Against the three-feature theories he rejects (§8.2), the systems their features generate are exactly the partitions on which resolution is defined, seven of the fifteen, and the geometry that would select his five is one he considers and sets aside.

Main results

• Examples.quad_cells_eq_participantSets: each quadripartition cell holds the referents whose participants the corresponding person value covers.
• Examples.quad_covers, Examples.quad_disjoint: the four cells partition the lattice.
• Examples.tri_card, Examples.tri_ne_quad: composition order matters, the tripartition having three cells.
• Examples.five_partitions: the five parameter settings of Table 4.1 give five partitions.
• Examples.inclusive_has_no_singleton: the singular has only three persons.
• exists_generated, card_image_graph: the systems the three features [±participant], [±author] and [±hearer] generate are exactly the congruences for union, seven in all.
• card_image_graph_admissible, graph_not_admissible: the bivalent geometry (9) generates the five, excluding the hearer bipartition and Zwicky's tripartition.
• exclusive_sign_filtered, tamil_clusivity_distinguished: the exclusive is the [+author, −participant] sign a containment filter rejects, and Tamil naam and naan-ŋgæ realize the two signs.
• attested_number_systems_derivable: every attested number system is generated by a parameter setting of Harbour's 2014 calculus.
• english_demonstratives_author_bipartition, preimage_participants_this: English this and that realize the author bipartition, and this is anchored by the first person's referents.

Implementation notes

One other suffices for the person partition, whose four cells are fixed by the presence of the speaker and the hearer, so the ontology is Fin 3 and the third-person group is not modeled; every result is checked on this finite model. Lexical Complementarity applies once, after both features, not cyclically (appendix B.1.2.3). Pairwise addition is mathlib's ⊻; ominus and act come from Semantics/Plurality/FeatureAction.lean.

References

• [Har16a]
• [Har14a]
• [Cor00]
• [Cys03]

The partition construction (over Plurality.FeatureAction's operators)

def Harbour2016.refine {Ω : Type u_1} [DecidableEq Ω] (siblings : List (Finset (Finset Ω))) (c : Finset (Finset Ω)) : Finset (Finset Ω)

Refining a cell c against its siblings removes every sibling cell properly contained in it, Lexical Complementarity (31), and then discards the empty set, which no person denotes (§4.4).

Equations

• Harbour2016.refine siblings c = (List.foldl (fun (acc d : Finset (Finset Ω)) => if d ⊂ c then acc \ d else acc) c siblings).erase ∅

def Harbour2016.cellsOf {Ω : Type u_1} [DecidableEq Ω] (raws : List (Finset (Finset Ω))) : Finset (Finset (Finset Ω))

The cells of a partition are the raw denotations of its sign assignments, each refined against the whole family.

Equations

• Harbour2016.cellsOf raws = (List.map (Harbour2016.refine raws) raws).toFinset

The three-element ontology {i, u, o} and the derived results

Harbour's abbreviation i_o/iu_o/u_o/o_o collapses the π-lattice into four shape-classes; the minimal ontology realizing all four is {i, u, o}, taken here as Fin 3 with i = 0, u = 1, o = 2. A single o suffices for the person partition (the four cells are fixed by has i?/has u?, not the others' count); the 3rd-person group {o, o'} is not modelled, and no result below depends on it. All theorems are kernel-checked by decide on this finite model.

@[reducible, inline]

abbrev Harbour2016.Examples.Ω : Type

Equations

• Harbour2016.Examples.Ω = Fin 3

def Harbour2016.Examples.ℒau : Finset (Finset Ω)

The author lattice ℒau has the single group {i}.

Equations

• Harbour2016.Examples.ℒau = {{0}}

def Harbour2016.Examples.ℒpt : Finset (Finset Ω)

The participant lattice ℒpt has the groups {i}, {u} and {i, u}.

Equations

• Harbour2016.Examples.ℒpt = {{0}, {1}, {0, 1}}

def Harbour2016.Examples.ℒπ : Finset (Finset Ω)

The π lattice has every nonempty set of referents as a group.

Equations

• Harbour2016.Examples.ℒπ = Finset.Ioc ∅ Finset.univ

theorem Harbour2016.Examples.lattice_chain : ℒau ⊆ ℒpt ∧ ℒpt ⊆ ℒπ

The lattices are egocentrically nested, ℒau ⊆ ℒpt ⊆ ℒπ (p. 74).

Quadripartition — author composes outermost ([Har16a] §4.3.5)

def Harbour2016.Examples.quadRaw (sa sp : Bool) : Finset (Finset Ω)

The raw quadripartition cell for the author sign sa and the participant sign sp applies the participant value first and the author value outermost.

Equations

• Harbour2016.Examples.quadRaw sa sp = Plurality.FeatureAction.act sa Harbour2016.Examples.ℒau (Plurality.FeatureAction.act sp Harbour2016.Examples.ℒpt Harbour2016.Examples.ℒπ)

def Harbour2016.Examples.quadRaws : List (Finset (Finset Ω))

The raw quadripartition cells are those of the four sign assignments.

Equations

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

def Harbour2016.Examples.quadCell (sa sp : Bool) : Finset (Finset Ω)

A quadripartition cell is a raw cell refined against the others.

Equations

• Harbour2016.Examples.quadCell sa sp = Harbour2016.refine Harbour2016.Examples.quadRaws (Harbour2016.Examples.quadRaw sa sp)

def Harbour2016.Examples.inclusive : Finset (Finset Ω)

The first person inclusive is the +author +participant cell.

Equations

• Harbour2016.Examples.inclusive = Harbour2016.Examples.quadCell true true

def Harbour2016.Examples.exclusive : Finset (Finset Ω)

The first person exclusive is the +author −participant cell.

Equations

• Harbour2016.Examples.exclusive = Harbour2016.Examples.quadCell true false

def Harbour2016.Examples.secondP : Finset (Finset Ω)

The second person is the −author +participant cell.

Equations

• Harbour2016.Examples.secondP = Harbour2016.Examples.quadCell false true

def Harbour2016.Examples.thirdP : Finset (Finset Ω)

The third person is the −author −participant cell.

Equations

• Harbour2016.Examples.thirdP = Harbour2016.Examples.quadCell false false

The inclusive and the exclusive come out as distinct, disjoint cells by construction.

theorem Harbour2016.Examples.exclusive_excludes_addressee (s : Finset Ω) : s ∈ exclusive → 1 ∉ s

The exclusive never contains the addressee u, so it is −participant in Harbour's sense, the case a membership decomposition collapses.

theorem Harbour2016.Examples.exclusive_includes_speaker (s : Finset Ω) : s ∈ exclusive → 0 ∈ s

The exclusive always contains the speaker i.

theorem Harbour2016.Examples.inclusive_has_both (s : Finset Ω) : s ∈ inclusive → 0 ∈ s ∧ 1 ∈ s

The inclusive always contains both the speaker and the addressee.

theorem Harbour2016.Examples.inclusive_ne_exclusive : inclusive ≠ exclusive

The inclusive and the exclusive are distinct cells.

theorem Harbour2016.Examples.quad_covers : inclusive ∪ exclusive ∪ secondP ∪ thirdP = ℒπ

The four quadripartition cells cover the π-lattice.

theorem Harbour2016.Examples.quad_disjoint : Disjoint inclusive exclusive ∧ Disjoint inclusive secondP ∧ Disjoint inclusive thirdP ∧ Disjoint exclusive secondP ∧ Disjoint exclusive thirdP ∧ Disjoint secondP thirdP

The four quadripartition cells are pairwise disjoint.

theorem Harbour2016.Examples.quad_card : (cellsOf quadRaws).card = 4

The quadripartition has four cells.

def Harbour2016.Examples.participants (s : Finset Ω) : Finset Discourse.Role

The participants of a referent are the speaker if it contains 0 and the addressee if it contains 1.

Equations

• Harbour2016.Examples.participants s = {r : Discourse.Role | (match r with | Discourse.Role.speaker => 0 | Discourse.Role.addressee => 1) ∈ s}

theorem Harbour2016.Examples.quad_cells_eq_participantSets (s : Finset Ω) : s ∈ ℒπ → (s ∈ inclusive ↔ participants s ∈ Person.firstInclusive.participantSets) ∧ (s ∈ exclusive ↔ participants s ∈ Person.firstExclusive.participantSets) ∧ (s ∈ secondP ↔ participants s ∈ Person.second.participantSets) ∧ (s ∈ thirdP ↔ participants s ∈ Person.third.participantSets)

The calculus generates the library's quadripartition, each of the four cells holding exactly the referents whose participants the corresponding person value covers.

Standard tripartition — participant composes outermost ([Har16a] §4.3.4)

def Harbour2016.Examples.triRaw (sp sa : Bool) : Finset (Finset Ω)

The raw tripartition cell for the participant sign sp and the author sign sa applies the author value first and the participant value outermost.

Equations

• Harbour2016.Examples.triRaw sp sa = Plurality.FeatureAction.act sp Harbour2016.Examples.ℒpt (Plurality.FeatureAction.act sa Harbour2016.Examples.ℒau Harbour2016.Examples.ℒπ)

def Harbour2016.Examples.triRaws : List (Finset (Finset Ω))

The raw tripartition cells are those of the four sign assignments.

Equations

• Harbour2016.Examples.triRaws = [Harbour2016.Examples.triRaw true true, Harbour2016.Examples.triRaw true false, Harbour2016.Examples.triRaw false true, Harbour2016.Examples.triRaw false false]

theorem Harbour2016.Examples.tri_card : (cellsOf triRaws).card = 3

With participant outermost the two −participant specifications coincide, so the tripartition has three cells where the quadripartition has four, the noncommutativity of feature composition (§4.2.3).

theorem Harbour2016.Examples.tri_ne_quad : cellsOf triRaws ≠ cellsOf quadRaws

The five partitions ([Har16a] Table 4.1)

def Harbour2016.Examples.monoP : Finset (Finset (Finset Ω))

The monopartition has no feature active.

Equations

• Harbour2016.Examples.monoP = Harbour2016.cellsOf [Harbour2016.Examples.ℒπ]

def Harbour2016.Examples.authorBi : Finset (Finset (Finset Ω))

The author bipartition activates ±author alone.

Equations

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

def Harbour2016.Examples.participantBi : Finset (Finset (Finset Ω))

The participant bipartition activates ±participant alone.

Equations

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

def Harbour2016.Examples.triP : Finset (Finset (Finset Ω))

The tripartition is the set of its cells.

Equations

• Harbour2016.Examples.triP = Harbour2016.cellsOf Harbour2016.Examples.triRaws

def Harbour2016.Examples.quadP : Finset (Finset (Finset Ω))

The quadripartition is the set of its cells.

Equations

• Harbour2016.Examples.quadP = Harbour2016.cellsOf Harbour2016.Examples.quadRaws

theorem Harbour2016.Examples.five_partitions : [monoP, authorBi, participantBi, triP, quadP].Nodup

The five parameter settings of Table 4.1, no feature, ±author, ±participant, and the two composition orders of both, yield five distinct partitions.

No four-way singular person ([Har16a] Ch. 4)

def Harbour2016.Examples.singletons : Finset (Finset Ω)

The singleton referents are {i}, {u} and {o}.

Equations

• Harbour2016.Examples.singletons = {{0}, {1}, {2}}

theorem Harbour2016.Examples.inclusive_has_no_singleton : inclusive ∩ singletons = ∅

The inclusive, the only cell distinguishing the quadripartition from the tripartition, contains no singleton referent, so the singular realizes only three persons.

theorem Harbour2016.Examples.inclusive_card_ge_two (s : Finset Ω) : s ∈ inclusive → 2 ≤ s.card

Every inclusive referent has at least two members, the speaker and the addressee.

Three-feature theories (§8.2)

Theories with [±participant], [±author] and [±hearer] let a language activate any subset of the three, and the active features identify the participant sets that agree on them. A set bears [+participant] when it includes a participant, [+author] when it includes the speaker, and [+hearer] when it includes the addressee (p. 10). Each feature is preserved by union, so each system they generate is a congruence for union; conversely, the participant sets lacking a feature are those below a single set, and every partition on which resolution is defined is generated by the features it respects (exists_generated). The systems number seven: the five of Table 4.1 and the two Harbour names as these theories' overgeneration, the hearer bipartition and the tripartition Zwicky problematized, which groups inclusive with second person (p. 190). The bivalent geometry (9), which bars [±hearer] without [±author], generates exactly the five (p. 193); Harbour rejects it as one of sixteen geometries with nothing to select it (p. 194).

inductive Harbour2016.ThreeFeature : Type

A feature of the three-feature theories.

• participant : ThreeFeature
• author : ThreeFeature
• hearer : ThreeFeature

@[instance_reducible]

instance Harbour2016.instDecidableEqThreeFeature : DecidableEq ThreeFeature

Equations

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

@[instance_reducible]

instance Harbour2016.instFintypeThreeFeature : Fintype ThreeFeature

Equations

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

def Harbour2016.ThreeFeature.Holds : ThreeFeature → Finset Discourse.Role → Prop

A participant set bears [+participant] when it includes a participant, [+author] when it includes the speaker, and [+hearer] when it includes the addressee.

Equations

• Harbour2016.ThreeFeature.participant.Holds x✝ = x✝.Nonempty
• Harbour2016.ThreeFeature.author.Holds x✝ = (Discourse.Role.speaker ∈ x✝)
• Harbour2016.ThreeFeature.hearer.Holds x✝ = (Discourse.Role.addressee ∈ x✝)

@[instance_reducible]

instance Harbour2016.instDecidablePredFinsetRoleHolds (f : ThreeFeature) : DecidablePred f.Holds

Equations

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

def Harbour2016.bundle (F : Finset ThreeFeature) : SupHom (Finset Discourse.Role) (Finset ThreeFeature)

The features of F a participant set bears; union of participant sets is union of bundles.

Equations

• Harbour2016.bundle F = { toFun := fun (s : Finset Discourse.Role) => {x ∈ F | x.Holds s}, map_sup' := ⋯ }

def Harbour2016.generated (F : Finset ThreeFeature) : SupCon (Finset Discourse.Role)

The system a set of active features generates.

Equations

• Harbour2016.generated F = SupCon.ker (Harbour2016.bundle F)

theorem Harbour2016.generated_r_iff {F : Finset ThreeFeature} {s t : Finset Discourse.Role} : (generated F).toSetoid s t ↔ ∀ f ∈ F, f.Holds s ↔ f.Holds t

theorem Harbour2016.exists_generated (c : SupCon (Finset Discourse.Role)) : ∃ (F : Finset ThreeFeature), c.toSetoid = (generated F).toSetoid

Every congruence for union is generated by the features it respects.

theorem Harbour2016.generated_participant_author : (generated {ThreeFeature.participant, ThreeFeature.author}).toSetoid = Person.tripartition.toSetoid

[±participant] and [±author] generate the tripartition.

theorem Harbour2016.generated_hearer {s t : Finset Discourse.Role} : (generated {ThreeFeature.hearer}).toSetoid s t ↔ (Discourse.Role.addressee ∈ s ↔ Discourse.Role.addressee ∈ t)

[±hearer] alone generates the hearer bipartition, inclusive and second person against exclusive and third.

theorem Harbour2016.generated_hearer_participant {s t : Finset Discourse.Role} : (generated {ThreeFeature.hearer, ThreeFeature.participant}).toSetoid s t ↔ (s.Nonempty ↔ t.Nonempty) ∧ (Discourse.Role.addressee ∈ s ↔ Discourse.Role.addressee ∈ t)

[±hearer] and [±participant] generate Zwicky's tripartition, inclusive grouped with second person.

def Harbour2016.graph (F : Finset ThreeFeature) : Finset (Finset Discourse.Role × Finset Discourse.Role)

The graph of the system F generates, as a finset of pairs of participant sets.

Equations

• Harbour2016.graph F = {p : Finset Discourse.Role × Finset Discourse.Role | (Harbour2016.bundle F) p.1 = (Harbour2016.bundle F) p.2}

theorem Harbour2016.card_image_graph : (Finset.image graph Finset.univ).card = 7

The eight sets of active features generate seven systems.

def Harbour2016.Admissible (F : Finset ThreeFeature) : Prop

Geometry (9) admits [±hearer] only with [±author].

Equations

• Harbour2016.Admissible F = (Harbour2016.ThreeFeature.hearer ∈ F → Harbour2016.ThreeFeature.author ∈ F)

@[instance_reducible]

instance Harbour2016.instDecidablePredFinsetThreeFeatureAdmissible : DecidablePred Admissible

Equations

• Harbour2016.instDecidablePredFinsetThreeFeatureAdmissible x✝ = id inferInstance

theorem Harbour2016.card_image_graph_admissible : (Finset.image graph (Finset.filter Admissible Finset.univ)).card = 5

The admissible feature sets generate five systems.

theorem Harbour2016.graph_not_admissible (F : Finset ThreeFeature) : ¬Admissible F → graph F = graph {ThreeFeature.hearer} ∨ graph F = graph {ThreeFeature.hearer, ThreeFeature.participant}

The two systems only the inadmissible feature sets generate are the hearer bipartition and Zwicky's tripartition.

Number (chapter 6): the attested systems of [Cor00] are generated

def Harbour2016.winnebago : Number.System

Winnebago has minimal and augmented, from ±minimal alone ([Har14a] Table 3).

Equations

• Harbour2016.winnebago = { values := {Number.minimal, Number.augmented} }

def Harbour2016.mebengokre : Number.System

Mebengokre has minimal, paucal and plural, from ±additive and ±minimal ([Har14a] Table 3).

Equations

• Harbour2016.mebengokre = { values := {Number.minimal, Number.paucal, Number.plural} }

def Harbour2016.Generates (σ : Harbour2014.Setting) (c : Harbour2014.Convention) (values : Finset Number) : Prop

A setting generates a set of number values when every value is among its system's; a language need not lexicalize every number its features afford.

Equations

• Harbour2016.Generates σ c values = ∀ v ∈ values, v ∈ σ.values c 0

@[instance_reducible]

instance Harbour2016.instDecidableGenerates (σ : Harbour2014.Setting) (c : Harbour2014.Convention) (values : Finset Number) : Decidable (Generates σ c values)

Equations

• Harbour2016.instDecidableGenerates σ c values = { decide := decide (∀ a ∈ Finset.univ, (fun (v : Number) => v ∈ values → v ∈ σ.values c 0) a), reflects_decide := ⋯ }

theorem Harbour2016.attested_number_systems_derivable (p : Harbour2014.Setting × Harbour2014.Convention × Finset Number) : p ∈ [({ atomic := Harbour2014.Activation.inactive, minimal := Harbour2014.Activation.inactive, additive := Harbour2014.Activation.inactive }, Harbour2014.Convention.none, Corbett2000.piraha.values), ({ atomic := Harbour2014.Activation.active, minimal := Harbour2014.Activation.inactive, additive := Harbour2014.Activation.inactive }, Harbour2014.Convention.none, Corbett2000.english.toSystem.values), ({ atomic := Harbour2014.Activation.active, minimal := Harbour2014.Activation.inactive, additive := Harbour2014.Activation.inactive }, Harbour2014.Convention.none, Corbett2000.russian.toSystem.values), ({ atomic := Harbour2014.Activation.active, minimal := Harbour2014.Activation.inactive, additive := Harbour2014.Activation.inactive }, Harbour2014.Convention.none, Corbett2000.japanese.toSystem.values), ({ atomic := Harbour2014.Activation.active, minimal := Harbour2014.Activation.active, additive := Harbour2014.Activation.inactive }, Harbour2014.Convention.none, Corbett2000.upperSorbian.toSystem.values), ({ atomic := Harbour2014.Activation.active, minimal := Harbour2014.Activation.active, additive := Harbour2014.Activation.inactive }, Harbour2014.Convention.none, Corbett2000.slovene.toSystem.values), ({ atomic := Harbour2014.Activation.active, minimal := Harbour2014.Activation.inactive, additive := Harbour2014.Activation.active }, Harbour2014.Convention.one Harbour2014.Height.low, Corbett2000.bayso.toSystem.values), ({ atomic := Harbour2014.Activation.active, minimal := Harbour2014.Activation.recursive, additive := Harbour2014.Activation.inactive }, Harbour2014.Convention.none, Corbett2000.larike.toSystem.values), ({ atomic := Harbour2014.Activation.active, minimal := Harbour2014.Activation.recursive, additive := Harbour2014.Activation.active }, Harbour2014.Convention.one Harbour2014.Height.low, Corbett2000.lihir.toSystem.values), ({ atomic := Harbour2014.Activation.inactive, minimal := Harbour2014.Activation.active, additive := Harbour2014.Activation.inactive }, Harbour2014.Convention.none, winnebago.values), ({ atomic := Harbour2014.Activation.inactive, minimal := Harbour2014.Activation.recursive, additive := Harbour2014.Activation.inactive }, Harbour2014.Convention.none, Corbett2000.rembarrnga.values), ({ atomic := Harbour2014.Activation.inactive, minimal := Harbour2014.Activation.active, additive := Harbour2014.Activation.active }, Harbour2014.Convention.one Harbour2014.Height.low, mebengokre.values)] → p.2.1.Fits p.1.additive ∧ Generates p.1 p.2.1 p.2.2

Every attested number system of [Cor00] is generated by a setting, with no feature for Pirahã, {±atomic} for English, Russian, and Japanese, {±atomic, ±minimal} for Upper Sorbian and Slovene, {±atomic, ±additive} for Bayso, {±atomic, ±minimal*} for Larike and {±atomic, ±minimal*, ±additive} for Lihir; and the minimal–augmented systems of [Har14a] Table 3 by {±minimal} alone for Winnebago, with recursion for Rembarrnga and with {±additive} for Mebengokre.

Spatial deixis (chapter 7)

Object, space and path deixis attest the same five partitions as person (§7.2.1), so the person features generate them. English this and these denote things in the speaker's vicinity and that and those things beyond, the author bipartition (p. 171). The spatial head χ carries a person specification to the vicinity of the referents it denotes ((16), p. 180), so this denotes the vicinity of the first person's referents.

theorem Harbour2016.english_demonstratives_author_bipartition : English.Determiners.that.deixis = English.Determiners.this.deixisᶜ ∧ ∀ (s t : Finset Discourse.Role), (generated {ThreeFeature.author}).toSetoid s t ↔ (s ∈ English.Determiners.this.deixis ↔ t ∈ English.Determiners.this.deixis)

English this and that realize the author bipartition (p. 171). That covers the participant sets this does not, and two sets fall under the same demonstrative iff [±author] does not tell them apart.

theorem Harbour2016.preimage_participants_this {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} [PartialOrder E] (c : Reference.Context W E P T) : c.participants ⁻¹' ↑English.Determiners.this.deixis = Person.dom c (some Person.first)

The referents whose vicinity this picks out are the first person's referents ((16), p. 180), so the author feature that defines I and we defines the speaker's space.

A finite model of (16): the referents are the sets of two individuals under part-of, the speaker is {0} and the addressee {1}, and every referent is in every vicinity.

def Harbour2016.SpatialModel.ctx : Reference.Context Unit (Finset (Fin 2)) Unit Unit

The context of utterance has speaker {0} and addressee {1}.

Equations

• Harbour2016.SpatialModel.ctx = { agent := {0}, addressee := {1}, world := (), time := (), position := () }

def Harbour2016.SpatialModel.near : SetRel (Finset (Fin 2)) (Finset (Fin 2))

Every referent is in every vicinity.

Equations

• Harbour2016.SpatialModel.near = Set.univ

def Harbour2016.SpatialModel.g₀ : Assignment (Finset (Fin 2))

The assignment sends every index to the empty referent.

Equations

• Harbour2016.SpatialModel.g₀ x✝ = ∅

Harbour's signs for the Cysouw categories (Table 4.3)

The membership bundles Person.Category.toFeatures give the three groups including the speaker one bundle, {participant, author}. Harbour's signs distinguish them, a commitment of this theory derived from the partition above. A sign is a bivalent valuation Person.Feature → Bool rather than a membership bundle Person.Features: the exclusive's +author −participant is the combination the containment filter rejects, and the filter, which holds of membership, does not hold of operations (chapter 9).

def Harbour2016.signOf : Person.Category → Person.Feature → Bool

Harbour's sign for a Cysouw category (Table 4.3). The exclusive, and with it the singular speaker, which the quadripartition places in the exclusive cell (p. 96), is +author −participant, so it does not collapse with the inclusive +author +participant as under Category.toFeatures.

Equations

• Harbour2016.signOf Person.Category.speakerAddressee x✝ = true
• Harbour2016.signOf Person.Category.speakerAddresseeOthers x✝ = true
• Harbour2016.signOf Person.Category.speaker x✝ = (x✝ == Person.Feature.author)
• Harbour2016.signOf Person.Category.speakerOthers x✝ = (x✝ == Person.Feature.author)
• Harbour2016.signOf Person.Category.addressee x✝ = (x✝ == Person.Feature.participant)
• Harbour2016.signOf Person.Category.addresseeOthers x✝ = (x✝ == Person.Feature.participant)
• Harbour2016.signOf Person.Category.other x✝ = false
• Harbour2016.signOf Person.Category.others x✝ = false

theorem Harbour2016.signOf_speakerOthers_ne_speakerAddressee : signOf Person.Category.speakerOthers ≠ signOf Person.Category.speakerAddressee

Harbour's signs distinguish exclusive from inclusive, where the neutral membership decomposition (Category.toFeatures) collapses them (cf. Examples.inclusive_ne_exclusive).

The Tamil clusivity contrast

A pronoun entry reaches Harbour's signs through the categories its person, number and clusivity realize (Pronoun.categories). Tamil's first person plural forms naam (inclusive) and naan-ŋgæ (exclusive) realize distinct signs, where the membership bundles give both categories {participant, author}.

def Harbour2016.harbourSign (p : Pronoun) : Finset (Person.Feature → Bool)

The signs a pronoun realizes are those of its categories, several where its φ-features underdetermine the category.

Equations

• Harbour2016.harbourSign p = Finset.image Harbour2016.signOf p.categories

theorem Harbour2016.naam_sign : harbourSign Tamil.Pronouns.naam.toPronoun = {fun (x : Person.Feature) => true}

naam (1pl inclusive) realizes the inclusive sign +author +participant.

theorem Harbour2016.naanŋgæ_sign : harbourSign Tamil.Pronouns.naanŋgæ.toPronoun = {fun (x : Person.Feature) => x == Person.Feature.author}

naan-ŋgæ (1pl exclusive) realizes the exclusive sign +author −participant.

theorem Harbour2016.tamil_clusivity_distinguished : harbourSign Tamil.Pronouns.naam.toPronoun ≠ harbourSign Tamil.Pronouns.naanŋgæ.toPronoun

Harbour's signs distinguish naam from naan-ŋgæ through the Pronoun API.

theorem Harbour2016.tamil_clusivity_collapsed_by_toFeatures : Finset.image Person.Category.toFeatures Tamil.Pronouns.naam.categories = Finset.image Person.Category.toFeatures Tamil.Pronouns.naanŋgæ.categories

The membership decomposition collapses naam and naan-ŋgæ, mapping both first person plural categories to the same Category.toFeatures.

theorem Harbour2016.exclusive_sign_filtered : ¬IsLowerSet ↑{x : Person.Feature | signOf Person.Category.speakerOthers x = true}

The exclusive's sign is the [+author, −participant] combination the containment filter on membership bundles rejects (Person.wellFormed_iff_isIntent), the author as a non-participant, which the free combinatorics of chapter 9 generate and the calculus fills (Examples.exclusive_includes_speaker).