Toosarvandani (2023): The Interpretation and Grammatical Representation of Animacy

The third person plural pronouns of Southeastern Sierra Zapotec distinguish elders, other humans, animals and inanimates, refer to heterogeneous groups, and give a mixed group the most marked pronoun (14). Toosarvandani composes animacy features as Harbour and Kratzer compose person features: a feature denotes the lattice of groups of its atoms (48), (58), features combine by the pairwise join ⊕ (50), mathlib's ⊻, and Lexical Complementarity (52) restricts a pronoun to what no more specified pronoun denotes. Because person and animacy features share one head, the condition on Agree behind the person-case constraint (86) compares them together.

Main results

• specification_eq_containing: along an entailment chain, a specification denotes the groups containing an atom of its most specific feature (53), (62).
• mixed_group_marked, mem_elder_lexComp_iff: a mixed group takes the most marked pronoun, and the local persons take the speaker and addressee away from the elder pronoun.
• singular_containing, exists_plural_sups_singular: number composes by intersection after person and animacy and cannot precede them (57), (63).
• gender_incomparable: disjoint feature denotations give pronouns neither of which is the more specified (71).
• Feature.le_iff_atoms_subset, Pronoun.le_iff_denotation_subset: the feature chain is semantic entailment and the hierarchy of pronouns is the inclusion of their denotations (58), (60)–(62).
• agrees_iff, yalalag_rows: Agree (86) fails exactly in the upstream scenarios, where the object outranks the subject, as the Yalálag examples (77)–(81) show.
• AgreesUnder.mono: a probe relativized to fewer animacy features, as in Laxopa and Zoogocho, collapses the distinctions it does not see.

Implementation notes

Individuals are a finite type and a group a nonempty finite set of atoms, the join being union, as in Semantics/Plurality/FeatureAction.lean, where the composition and complementarity lemmas live; a feature's atoms are a Finset, with the speaker and addressee among the elders, (58a). In section 4 a concrete model has one atom per class of the schematic extensions (59), so that the feature chain of (60) is entailment rather than stipulation, and a subject and an object pronoun form a scenario (Clause.Scenario) of the subject over the object. Context-dependence, (54), is not modelled: the associate relation is left to the context, so the English examples (16)–(18) are rows without a theorem. The person-based constraint is absolute in Zapotec while (86) derives a relative one, a difference the paper attributes to the probe's relativization (fn. 22), and the same-category pairings that (86) licenses are not in the data. The Agree-based theory generalizes Deal's, with the probe's features sequenced after Coon and Keine so that only the features of the highest head, person and animacy, enter the comparison.

References

• [Too23]
• [Har16a]
• [Kra09b]
• [Lin83]
• [Dea24]
• [CK21]

Features and their composition (section 3)

def Toosarvandani2023.piDen {Ind : Type u_1} [DecidableEq Ind] [Fintype Ind] : Finset (Finset Ind)

The denotation of π holds every singular or plural individual (48c).

Equations

• Toosarvandani2023.piDen = Finset.Ioc ∅ Finset.univ

def Toosarvandani2023.specification {Ind : Type u_1} [DecidableEq Ind] [Fintype Ind] (fs : List (Finset Ind)) : Finset (Finset Ind)

A feature specification adds the features' lattices by ⊻ over π, the last listed innermost (51), (61).

Equations

• Toosarvandani2023.specification fs = List.foldr (fun (X : Finset Ind) (acc : Finset (Finset Ind)) => Finset.Ioc ∅ X ⊻ acc) Toosarvandani2023.piDen fs

@[simp]

theorem Toosarvandani2023.specification_nil {Ind : Type u_1} [DecidableEq Ind] [Fintype Ind] : specification [] = piDen

@[simp]

theorem Toosarvandani2023.specification_cons {Ind : Type u_1} [DecidableEq Ind] [Fintype Ind] (X : Finset Ind) (fs : List (Finset Ind)) : specification (X :: fs) = Finset.Ioc ∅ X ⊻ specification fs

theorem Toosarvandani2023.specification_eq_containing {Ind : Type u_1} [DecidableEq Ind] [Fintype Ind] {fs : List (Finset Ind)} {X : Finset Ind} : List.Pairwise (fun (x1 x2 : Finset Ind) => x1 ⊆ x2) (X :: fs) → specification (X :: fs) = Plurality.FeatureAction.containing X Finset.univ

Along an entailment chain of features, a specification denotes the groups containing an atom of its most specific feature (53), (62).

theorem Toosarvandani2023.mixed_group_marked {Ind : Type u_1} [DecidableEq Ind] [Fintype Ind] {E H : Finset Ind} {e h : Ind} (he : e ∈ E) (hh : h ∈ H) : {e, h} ∈ Plurality.FeatureAction.containing E Finset.univ ∧ {e, h} ∈ Plurality.FeatureAction.containing H Finset.univ ∧ {e, h} ∉ Plurality.FeatureAction.containing H Finset.univ \ Plurality.FeatureAction.containing E Finset.univ

A group of an elder and a nonelder human lies in the elder and the human specifications, and lexical complementarity removes it from the human pronoun, marked reference (62).

theorem Toosarvandani2023.mem_elder_lexComp_iff {Ind : Type u_1} [DecidableEq Ind] [Fintype Ind] {E : Finset Ind} {i u : Ind} {s : Finset Ind} : s ∈ Plurality.FeatureAction.containing E Finset.univ \ Plurality.FeatureAction.containing {i, u} Finset.univ ↔ (s ∩ E).Nonempty ∧ i ∉ s ∧ u ∉ s

Against the local persons, whose most specific features have the speaker and the addressee as atoms, the elder pronoun refers to the groups with an elder and no conversational participant (62a).

Number (section 3.2)

def Toosarvandani2023.singular {Ind : Type u_1} (L : Finset (Finset Ind)) : Finset (Finset Ind)

Singular keeps the atomic individuals, composing by intersection (56a).

Equations

• Toosarvandani2023.singular L = {s ∈ L | s.card = 1}

theorem Toosarvandani2023.singular_containing {Ind : Type u_1} [DecidableEq Ind] [Fintype Ind] (X : Finset Ind) : singular (Plurality.FeatureAction.containing X Finset.univ) = Finset.image (fun (x : Ind) => {x}) X

Composed after person and animacy, singular leaves a specification's atoms (57).

theorem Toosarvandani2023.pair_mem_sups_singular {Ind : Type u_1} [DecidableEq Ind] [Fintype Ind] {X : Finset Ind} {x : Ind} (hx : x ∈ X) (y : Ind) : {x, y} ∈ Finset.Ioc ∅ X ⊻ singular piDen

A feature composed by ⊻ after singular restores pluralities (63).

theorem Toosarvandani2023.exists_plural_sups_singular {Ind : Type u_1} [DecidableEq Ind] [Fintype Ind] {X : Finset Ind} {x y : Ind} (hx : x ∈ X) (hxy : x ≠ y) : ∃ s ∈ Finset.Ioc ∅ X ⊻ singular piDen, s.card ≠ 1

So person and animacy must compose before number.

Social gender (section 3.5)

theorem Toosarvandani2023.gender_incomparable {Ind : Type u_1} [DecidableEq Ind] [Fintype Ind] {F M : Finset Ind} (hd : Disjoint F M) (hF : F.Nonempty) (hM : M.Nonempty) : ¬Plurality.FeatureAction.containing F Finset.univ ⊆ Plurality.FeatureAction.containing M Finset.univ ∧ ¬Plurality.FeatureAction.containing M Finset.univ ⊆ Plurality.FeatureAction.containing F Finset.univ

Feminine and masculine atoms are disjoint, so the pronouns their features would compose by ⊻ are incomparable and lexical complementarity cannot restrict either (71).

The person-case constraint (section 4)

inductive Toosarvandani2023.Atom : Type

The atoms of the schematic extensions (59) and (62) are the speaker i, the addressee u, an elder e, a nonelder human h, an animal a, and an inanimate o.

• i : Atom
• u : Atom
• e : Atom
• h : Atom
• a : Atom
• o : Atom

@[instance_reducible]

instance Toosarvandani2023.instDecidableEqAtom : DecidableEq Atom

Equations

• Toosarvandani2023.instDecidableEqAtom x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Toosarvandani2023.instFintypeAtom : Fintype Atom

Equations

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

inductive Toosarvandani2023.Feature : Type

The person and animacy features of the highest nominal head in Zapotec (60).

• speaker : Feature
• participant : Feature
• elder : Feature
• human : Feature
• animate : Feature
• pi : Feature

@[instance_reducible]

instance Toosarvandani2023.instDecidableEqFeature : DecidableEq Feature

Equations

• Toosarvandani2023.instDecidableEqFeature x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Toosarvandani2023.instFintypeFeature : Fintype Feature

Equations

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

@[instance_reducible]

instance Toosarvandani2023.instReprFeature : Repr Feature

Equations

• Toosarvandani2023.instReprFeature = { reprPrec := Toosarvandani2023.instReprFeature.repr }

def Toosarvandani2023.instReprFeature.repr : Feature → ℕ → Std.Format

Equations

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

def Toosarvandani2023.Feature.atoms : Feature → Finset Atom

The atoms a feature holds of (48), (58). The elder feature holds of the conversational participants as well, the human one of every human, and the animate one of every animate.

Equations

• Toosarvandani2023.Feature.speaker.atoms = {Toosarvandani2023.Atom.i}
• Toosarvandani2023.Feature.participant.atoms = {Toosarvandani2023.Atom.i, Toosarvandani2023.Atom.u}
• Toosarvandani2023.Feature.elder.atoms = {Toosarvandani2023.Atom.i, Toosarvandani2023.Atom.u, Toosarvandani2023.Atom.e}
• Toosarvandani2023.Feature.human.atoms = {Toosarvandani2023.Atom.i, Toosarvandani2023.Atom.u, Toosarvandani2023.Atom.e, Toosarvandani2023.Atom.h}
• Toosarvandani2023.Feature.animate.atoms = {Toosarvandani2023.Atom.i, Toosarvandani2023.Atom.u, Toosarvandani2023.Atom.e, Toosarvandani2023.Atom.h, Toosarvandani2023.Atom.a}
• Toosarvandani2023.Feature.pi.atoms = Finset.univ

@[instance_reducible]

instance Toosarvandani2023.instLinearOrderFeature : LinearOrder Feature

The features are a chain, from the most specific.

Equations

• Toosarvandani2023.instLinearOrderFeature = LinearOrder.lift' (fun (x : Toosarvandani2023.Feature) => x.ctorIdx) Toosarvandani2023.instLinearOrderFeature._proof_1

theorem Toosarvandani2023.Feature.le_iff_atoms_subset {f g : Feature} : f ≤ g ↔ f.atoms ⊆ g.atoms

The chain is entailment, one feature below another exactly when it holds of no atom the other does not (58).

inductive Toosarvandani2023.Pronoun : Type

The pronoun categories of Table 1, clusivity set aside.

• first : Pronoun
• second : Pronoun
• thirdElder : Pronoun
• thirdHuman : Pronoun
• thirdAnimal : Pronoun
• thirdInanimate : Pronoun

@[instance_reducible]

instance Toosarvandani2023.instDecidableEqPronoun : DecidableEq Pronoun

Equations

• Toosarvandani2023.instDecidableEqPronoun x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Toosarvandani2023.instFintypePronoun : Fintype Pronoun

Equations

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

@[instance_reducible]

instance Toosarvandani2023.instReprPronoun : Repr Pronoun

Equations

• Toosarvandani2023.instReprPronoun = { reprPrec := Toosarvandani2023.instReprPronoun.repr }

def Toosarvandani2023.instReprPronoun.repr : Pronoun → ℕ → Std.Format

Equations

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

def Toosarvandani2023.Pronoun.top : Pronoun → Feature

The most specific feature of a category's specification, (60)–(61).

Equations

• Toosarvandani2023.Pronoun.first.top = Toosarvandani2023.Feature.speaker
• Toosarvandani2023.Pronoun.second.top = Toosarvandani2023.Feature.participant
• Toosarvandani2023.Pronoun.thirdElder.top = Toosarvandani2023.Feature.elder
• Toosarvandani2023.Pronoun.thirdHuman.top = Toosarvandani2023.Feature.human
• Toosarvandani2023.Pronoun.thirdAnimal.top = Toosarvandani2023.Feature.animate
• Toosarvandani2023.Pronoun.thirdInanimate.top = Toosarvandani2023.Feature.pi

def Toosarvandani2023.Pronoun.features (p : Pronoun) : Finset Feature

A category's feature specification is its most specific feature and every feature it entails, closed under entailment as Béjar's mapping principle requires (60), (61).

Equations

• p.features = {f : Toosarvandani2023.Feature | p.top ≤ f}

@[instance_reducible]

instance Toosarvandani2023.instLinearOrderPronoun : LinearOrder Pronoun

Pronouns are ordered by specification, one at least as high as another when its most specific feature entails the other's.

Equations

• Toosarvandani2023.instLinearOrderPronoun = LinearOrder.lift' (fun (p : Toosarvandani2023.Pronoun) => OrderDual.toDual p.top) Toosarvandani2023.instLinearOrderPronoun._proof_1

theorem Toosarvandani2023.Pronoun.le_iff_top_le {p q : Pronoun} : p ≤ q ↔ q.top ≤ p.top

theorem Toosarvandani2023.Pronoun.le_iff_features_subset {p q : Pronoun} : p ≤ q ↔ p.features ⊆ q.features

A pronoun is at least as high as another exactly when it has all of the other's features.

def Toosarvandani2023.Pronoun.denotation (p : Pronoun) : Finset (Finset Atom)

A pronoun denotes, before lexical complementarity, the groups containing an atom of its most specific feature (62), its specification by specification_eq_containing.

Equations

• p.denotation = Plurality.FeatureAction.containing p.top.atoms Finset.univ

theorem Toosarvandani2023.Pronoun.le_iff_denotation_subset {p q : Pronoun} : p ≤ q ↔ q.denotation ⊆ p.denotation

A pronoun is at least as high as another exactly when its denotation lies inside the other's, so the hierarchy of featural specification is one of semantic specificity.

def Toosarvandani2023.Agrees (s : Clause.Scenario Pronoun) : Prop

A head Agrees with the subject and the object pronoun of a scenario, and both cliticize, iff the subject has all of the object's features (86).

Equations

• Toosarvandani2023.Agrees s = (s.low.features ⊆ s.high.features)

@[instance_reducible]

instance Toosarvandani2023.instDecidablePredScenarioPronounAgrees : DecidablePred Agrees

Equations

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

theorem Toosarvandani2023.agrees_iff {s : Clause.Scenario Pronoun} : Agrees s ↔ s.kind ≠ Clause.Scenario.Kind.upstream

Agree fails, and the object clitic is blocked, exactly in the upstream scenarios, where the object outranks the subject on the hierarchy (77)–(81).

def Toosarvandani2023.AgreesUnder (R : Finset Feature) (s : Clause.Scenario Pronoun) : Prop

A probe relativized to the features R compares only those.

Equations

• Toosarvandani2023.AgreesUnder R s = (s.low.features ∩ R ⊆ s.high.features ∩ R)

@[instance_reducible]

instance Toosarvandani2023.instDecidablePredScenarioPronounAgreesUnder (R : Finset Feature) : DecidablePred (AgreesUnder R)

Equations

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

theorem Toosarvandani2023.agreesUnder_univ {s : Clause.Scenario Pronoun} : AgreesUnder Finset.univ s ↔ Agrees s

theorem Toosarvandani2023.AgreesUnder.mono {R R' : Finset Feature} {s : Clause.Scenario Pronoun} (h : R ⊆ R') (ha : AgreesUnder R' s) : AgreesUnder R s

The fewer features a probe sees, the weaker the constraint.

theorem Toosarvandani2023.laxopa_human_elder : AgreesUnder {Feature.speaker, Feature.participant, Feature.human, Feature.animate, Feature.pi} { high := Pronoun.thirdHuman, low := Pronoun.thirdElder } ∧ ¬Agrees { high := Pronoun.thirdHuman, low := Pronoun.thirdElder }

The Laxopa probe does not see elder, so elder and nonelder human clitics combine freely, where Yalálag's full relativization blocks (79b).

theorem Toosarvandani2023.zoogocho_animal_elder : AgreesUnder {Feature.speaker, Feature.participant, Feature.animate, Feature.pi} { high := Pronoun.thirdAnimal, low := Pronoun.thirdElder }

The Zoogocho probe sees only animate among the animacy features, so any animate clitics combine.

The Yalálag examples (77)–(81)

def Toosarvandani2023.pronoun? (e : Datum) (key : String) : Option Pronoun

The pronoun category a row's tag names.

Equations

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

def Toosarvandani2023.scenario? (e : Datum) : Option (Clause.Scenario Pronoun)

The scenario of a row's subject over its object.

Equations

• Toosarvandani2023.scenario? e = do let __do_lift ← Toosarvandani2023.pronoun? e "subject" let __do_lift_1 ← Toosarvandani2023.pronoun? e "object" pure { high := __do_lift, low := __do_lift_1 }

def Toosarvandani2023.yalalag : List Datum

The Yalálag rows.

Equations

• Toosarvandani2023.yalalag = List.filter (fun (x : Datum) => decide (x.language = "yala1267")) Toosarvandani2023.Examples.all

theorem Toosarvandani2023.yalalag_rows : yalalag ≠ [] ∧ ∀ e ∈ yalalag, ∃ s ∈ scenario? e, e.judgment = Judgment.acceptable ↔ Agrees s

Every Yalálag example is grammatical exactly when its head Agrees with both pronouns, so the object clitic is blocked in the upstream scenarios and only there.