Toosarvandani (2023): The Interpretation and Grammatical Representation of Animacy #
@cite{toosarvandani-2023} @cite{harbour-2016} @cite{kratzer-2009} @cite{foley-toosarvandani-2022}
Language 99(4): 760–808.
Formalizes the core empirical and theoretical contributions of Toosarvandani's analysis of Santiago Laxopa Zapotec (and other Southeastern Sierra Zapotec varieties), in which third-person plural pronouns encode a four-way animacy distinction (elder humans, nonelder humans, animals, inanimates) that exhibits ASSOCIATIVITY — the cluster of interpretive properties otherwise associated with first- and second-person plural pronouns.
Key formal apparatus (paper §3–§4) #
- Lattice-denoting features. SPEAKER, PARTICIPANT, π are person features denoting predicates over a lattice of singular and plural individuals (48). ELDER, HUMAN, ANIMATE are animacy features with parallel structure (58).
- ⊕ operator (50): pointwise lattice join of two feature denotations, generalising Kratzer's (2009) sum operator. Generates plural individuals (and thus heterogeneity) when applied to lattice-denoting features.
- Lexical Complementarity (LC) (52): for ⟦F⟧ ⊂ ⟦G⟧, use of G is restricted to ⟦G⟧ \ ⟦F⟧. Derives marked reference patterns.
- SINGULAR/PLURAL (56): intersection-composing number features.
- Composition order (57, 63): person/animacy features compose via ⊕ first, then number composes via ∩. The reverse order is non-functional — ⊕ would re-introduce pluralities that ∩ SINGULAR removed.
- Person Case Constraint (86): a functional head F Agrees with two pronouns A and B (A higher than B) iff A has all of the features of B.
File structure #
- §1 Operators (oplus, lexComp, singularFilter, pluralFilter, npow encoding)
- §2 PhiDomain and the Zapotec instantiation
- §3 Feature denotations
- §4 Pronoun composition (Zapotec 4-way animacy + LC)
- §5 PCC via feature containment (data from (77)–(82))
- §6 Structural properties of the PCC condition
- §7 Denotation ↔ PCC correspondence
- §8 Heterogeneity and SINGULAR/PLURAL composition order
- §9 Bridges to
Features.PersonandFeatures.Prominence
Note on absolute vs relative PCC #
(86) is the formal Agree condition. It predicts same-rank pairings (e.g. 1>1, 2>2) are licit because A trivially has all of A's features. The paper acknowledges (footnote 22, p. 798) that the empirical person-based PCC in many languages is ABSOLUTE — any local-person object is illicit, even with a local-person subject. The animacy-based PCC in Zapotec is RELATIVE and is what (86) directly derives. Cross-linguistic variation between absolute and relative PCC is attributed to the probe's featural relativization (§4.3, not formalized here).
Nonempty powerset: all nonempty subsets of atoms. Lean-side encoding
of the lattice of plural individuals — every nonempty sum of atoms
satisfying a feature predicate. The paper works in a Linkian/Krifkan
lattice (47); we represent that lattice as the powerset of an atomic
domain.
Equations
- Toosarvandani2023.npow atoms = atoms.powerset.erase ∅
Instances For
⊕ (oplus): pointwise lattice join of two feature denotations (50):
[⊕ G F] = λx . ∃y∃z[x = y ⊔ z, y ∈ ⟦F⟧, z ∈ ⟦G⟧].
Following @cite{harbour-2016}, generalising @cite{kratzer-2009}'s sum
operator. Generates heterogeneous pluralities: oplus SPEAKER ANIMATE
includes {speaker, animal}.
Defined directly via Finset.image (rather than the equivalent
Finset.image₂ (· ∪ ·)) so that decide can unfold concrete instances
without an extra image₂ layer. The structural lemmas
(oplus_subset, oplus_assoc) inherit from mathlib via defeq.
Equations
- Toosarvandani2023.oplus F G = Finset.image (fun (yz : Finset α × Finset α) => yz.1 ∪ yz.2) (F ×ˢ G)
Instances For
oplus agrees with Finset.image₂ (· ∪ ·) definitionally. Used to
inherit mathlib's image₂_* lemmas.
Monotonicity of ⊕: pointwise on both arguments. Inherits from
Finset.image₂_subset.
Membership in oplus: z ∈ oplus F G ↔ ∃ x ∈ F, ∃ y ∈ G, x ∪ y = z.
Inherits from Finset.mem_image₂ via oplus_eq_image₂.
Constructor form of membership: x ∈ F → y ∈ G → x ∪ y ∈ oplus F G.
Lexical Complementarity (52): for feature denotations ⟦F⟧ ⊂ ⟦G⟧, use of G is restricted to ⟦G⟧ \ ⟦F⟧. Forestalls a pronoun from being used to refer to individuals picked out by a more featurally specified pronoun (Harbour 2016:80).
Equations
- Toosarvandani2023.lexComp G F = G \ F
Instances For
SINGULAR (56a): ⟦SINGULAR⟧ = λx . ∀y[y ≤ x → x = y]. Picks out the
atomic individuals. In the Finset encoding, atomic = singleton. Number
features compose with person/animacy features by ∩ (intersection),
not ⊕.
Equations
- Toosarvandani2023.singularFilter den = {s ∈ den | s.card = 1}
Instances For
PLURAL (56b): ⟦PLURAL⟧ = λx . ∃y[y ≤ x ∧ x ≠ y]. Picks out the
nonatomic individuals. In the Finset encoding, nonatomic = card > 1.
Equations
- Toosarvandani2023.pluralFilter den = {s ∈ den | s.card > 1}
Instances For
A φ-domain: a finite set of individuals with speaker/addressee roles and animacy predicates forming the entailment hierarchy ELDER ⊂ HUMAN ⊂ ANIMATE (58, p. 786). Speaker and addressee are required to be human (per the paper's footnote 15, p. 787).
- Ind : Type
The type of atomic individuals.
- instDE : DecidableEq self.Ind
- instFT : Fintype self.Ind
- speaker : self.Ind
The speaker.
- addressee : self.Ind
The addressee.
- isElder : self.Ind → Bool
Elder predicate (salient social role per (58a)).
- isHuman : self.Ind → Bool
Human predicate (58b).
- isAnimate : self.Ind → Bool
Animate predicate (58c).
Hierarchy: ELDER entails HUMAN (commentary after (58)).
Hierarchy: HUMAN entails ANIMATE.
Speaker is human (footnote 15).
Addressee is human (footnote 15).
Speaker and addressee are distinct.
Instances For
Santiago Laxopa Zapotec instance #
Six representative individuals spanning the four-way animacy scale. This is Toosarvandani's didactic minimum for the Zapotec lattice — not real lexical data.
Equations
- Toosarvandani2023.instDecidableEqZapInd x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- Toosarvandani2023.instReprZapInd = { reprPrec := Toosarvandani2023.instReprZapInd.repr }
Equations
- One or more equations did not get rendered due to their size.
The Zapotec PhiDomain with 4-way animacy.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Convenience abbreviation.
Instances For
⟦SPEAKER⟧ (48a): singleton sums containing the speaker.
Equations
Instances For
⟦PARTICIPANT⟧ (48b): nonempty subsets of {speaker, addressee}.
Equations
Instances For
⟦π⟧ (48c): all nonempty sums of individuals — the maximal feature denotation.
Equations
- Toosarvandani2023.piDen pd = Toosarvandani2023.npow Finset.univ
Instances For
⟦ELDER⟧ (58a): individuals holding a salient social role. With (58a)'s semantics, the denotation includes SAPs as well as nonconversational elders, since SAPs trivially satisfy any salient-role test (paper p. 787). The pronoun-level restriction to nonconversational elders arises only after lexical complementarity (62).
Equations
- Toosarvandani2023.elderDen pd = Toosarvandani2023.npow {a : pd.Ind | (pd.isElder a || a == pd.speaker || a == pd.addressee) = true}
Instances For
⟦HUMAN⟧ (58b). SAPs are included via speaker_human/addressee_human.
Equations
- Toosarvandani2023.humanDen pd = Toosarvandani2023.npow {a : pd.Ind | pd.isHuman a = true}
Instances For
⟦ANIMATE⟧ (58c).
Equations
- Toosarvandani2023.animateDen pd = Toosarvandani2023.npow {a : pd.Ind | pd.isAnimate a = true}
Instances For
The 3SG.EL feature stack from (61a): π ⊕ ANIMATE ⊕ HUMAN ⊕ ELDER.
We elide the SINGULAR component (which is intersected separately) and
return the elder-pronoun denotation prior to LC. The actual pronoun
denotation in (62a) is lexComp elderPron over the next-less-marked
pronoun — but for the elder pronoun itself, LC is trivial since it's
the most marked.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The 3SG.HU stack from (61b): π ⊕ ANIMATE ⊕ HUMAN.
Equations
Instances For
The 3SG.AN stack from (61c): π ⊕ ANIMATE.
Equations
Instances For
The 3SG.IN stack from (61d): π only.
Equations
Instances For
Remove sums containing the speaker or addressee — restricts a pronoun denotation to third-person reference.
Equations
- Toosarvandani2023.thirdOnly pd den = {s ∈ den | pd.speaker ∉ s ∧ pd.addressee ∉ s}
Instances For
Third-person elder, human, animal, inanimate denotations (post-thirdOnly).
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Elder pronoun after LC: most marked, no subtraction needed (62a).
Equations
Instances For
Human pronoun after LC (62b): human \ elder.
Equations
Instances For
Animal pronoun after LC (62c): animal \ human.
Equations
Instances For
Inanimate pronoun after LC: π \ animal.
Equations
Instances For
Concrete checks on the Zapotec instance, proved structurally via
explicit mem_oplus_of_mem witness construction rather than decide.
The kernel decide on Finset-of-Finset membership over a 6-atom
universe is too heavy (each side up to 63 elements); the structural
witnesses build up {x} = {x} ∪ {x} decompositions through the
nested oplus.
Elder + animal group {e, a} is in the elder pronoun denotation.
Witness construction: e = {e}, y = {e, a} = {e} ∪ {a} where {e} ∈
humanDen (e is human, being elder) and {a} ∈ animalPron (a is in
animateDen ∩ piDen).
Base-feature containment: each animacy denotation is contained in
the next less-marked one. These follow from npow_mono plus a small
decide on the underlying 6-atom filter.
Denotation containment chain. Each pronoun is oplus of progressively
less-marked feature denotations. The proof pattern: replace the
most-marked component (e.g. elder in elderPron) with the next
component (human) using oplus_subset + base-feature monotonicity,
then use oplus_assoc and oplus_npow_self_subset to absorb the
duplicated component.
SPEAKER ⊂ PARTICIPANT at the feature-denotation level.
⊕ is associative on any Zapotec denotations. Direct corollary of the
generic oplus_assoc; no decide needed.
The PCC (Person Case Constraint), here extended with animacy, derived from feature containment per (86):
> A functional head F Agrees with two pronouns A and B, where A is
> higher than B, iff A has all of the features of B.
Person and animacy features occupy the same structural position (D),
forming a SINGLE hierarchy. Feature containment — not numeric ranking —
determines licitness.
Equations
- Toosarvandani2023.instDecidableEqDFeature x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯
Equations
- Toosarvandani2023.instReprDFeature = { reprPrec := Toosarvandani2023.instReprDFeature.repr }
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Equations
- Toosarvandani2023.instDecidableEqPronType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯
Equations
- Toosarvandani2023.instReprPronType = { reprPrec := Toosarvandani2023.instReprPronType.repr }
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
All 6 pronoun types.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Feature specification per pronoun type. SAPs include all animacy features because speaker/addressee are at least elder-rank under (58a)'s "salient social role" predicate. The feature sets form a strict containment chain: 1P ⊃ 2P ⊃ 3.EL ⊃ 3.HU ⊃ 3.AN ⊃ 3.IN.
Equations
- One or more equations did not get rendered due to their size.
- Toosarvandani2023.PronType.thirdElder.features = {Toosarvandani2023.DFeature.elder, Toosarvandani2023.DFeature.human, Toosarvandani2023.DFeature.animate, Toosarvandani2023.DFeature.pi}
- Toosarvandani2023.PronType.thirdHuman.features = {Toosarvandani2023.DFeature.human, Toosarvandani2023.DFeature.animate, Toosarvandani2023.DFeature.pi}
- Toosarvandani2023.PronType.thirdAnimal.features = {Toosarvandani2023.DFeature.animate, Toosarvandani2023.DFeature.pi}
- Toosarvandani2023.PronType.thirdInanimate.features = {Toosarvandani2023.DFeature.pi}
Instances For
PCC licitness via feature containment (86): subject Agrees with object
iff subject has all of object's features. Implemented directly via
Finset.Subset decidability.
Equations
- Toosarvandani2023.pccLicit subj obj = decide (obj.features ⊆ subj.features)
Instances For
21 licit subj×obj pairings (15 strict + 6 same-rank). Drift sentry for the per-cell theorems above.
Reflexivity: A ⊆ A always, so pccLicit p p = true.
Totality: at least one direction is licit. Follows from the containment
chain via Finset.Subset.
Antisymmetry on PronType: mutual licitness implies same pronoun type. This requires Zapotec-specific injectivity of the feature mapping (the abstract claim is just feature-set equality).
Within third person, denotation nesting (semantic, from ⊕ composition) mirrors PCC licitness (syntactic, from feature containment). The two main contributions of the paper — compositional animacy semantics and derived PCC — are formally connected: more features → smaller denotation → higher on hierarchy → can be subject.
The three semantic-side facts are `elderPron_sub_humanPron`,
`humanPron_sub_animalPron`, `animalPron_sub_piDen` (§4c above). The
syntactic-side facts are `pcc_3el_3hu`, `pcc_3hu_3an`, `pcc_3an_3in`
(licit) and `pcc_3hu_3el`, `pcc_3an_3hu`, `pcc_3in_3an` (illicit), all
in §5. Earlier drafts bundled them into a 9-conjunct
`denotation_pcc_full_chain` aggregator; that was a
no-aggregate-count-style sentry and is omitted to keep `decide`
recursion within mathlib defaults.
Third-person restriction strictly shrinks the elder pronoun denotation:
{i} is a witness that lives in elderPron (via the all-singletons
decomposition {i} ∪ {i} ∪ {i} ∪ {i}) but is filtered out of
thirdElderPron because it contains the speaker. Structural rather
than card-based to avoid computing two ~63-element Finset
cardinalities in the kernel.
LC produces disjoint third-person pronoun denotations.
Person/animacy features compose via ⊕; number features compose via ∩. These two modes MUST apply in a specific order: ⊕ first, then ∩. If SINGULAR were interleaved within the ⊕ chain, ⊕ would re-introduce pluralities by joining the singletons SINGULAR preserved (paper §3.2, derivation (63)). This non-commutativity is why person and number occupy distinct functional heads.
Correct composition (57): ⊕ all person features, then ∩ SINGULAR. First-person singular = {speaker}.
⊕ and SINGULAR do not commute. Interleaving SINGULAR within the ⊕ chain gives different (wrong) results because ⊕ creates new pluralities from the singletons SINGULAR preserved. (63).
The wrong order produces plural sums: ⊕ SPEAKER applied AFTER SINGULAR creates {speaker, addressee} from singleton {addressee}, undoing SINGULAR's filtering.
Map PronType to the coarser 3-way person distinction in
Features.Prominence. All third-person animacy subtypes collapse.
Equations
Instances For
PCC respects person prominence: when subject is strictly more prominent in person (not just animacy), PCC is licit.
Map PronType to binary person features (±participant, ±author).
Equations
- Toosarvandani2023.PronType.first.toPersonFeatures = { hasParticipant := true, hasAuthor := true }
- Toosarvandani2023.PronType.second.toPersonFeatures = { hasParticipant := true, hasAuthor := false }
- x✝.toPersonFeatures = { hasParticipant := false, hasAuthor := false }
Instances For
The two independent decompositions of person agree: PronType → PersonFeatures and PronType → PersonLevel → Features.
Map third-person pronoun types to AnimacyLevel. Elder and human both
map to .human — elder is a human subtype. SAPs return none.
Equations
- Toosarvandani2023.PronType.thirdElder.toAnimacyLevel = some Features.Prominence.AnimacyLevel.human
- Toosarvandani2023.PronType.thirdHuman.toAnimacyLevel = some Features.Prominence.AnimacyLevel.human
- Toosarvandani2023.PronType.thirdAnimal.toAnimacyLevel = some Features.Prominence.AnimacyLevel.animate
- Toosarvandani2023.PronType.thirdInanimate.toAnimacyLevel = some Features.Prominence.AnimacyLevel.inanimate
- x✝.toAnimacyLevel = none
Instances For
The 4-way Zapotec animacy system REFINES the 3-way typological scale. Elder and human collapse at AnimacyLevel.human, but PCC distinguishes them. Toosarvandani's central empirical contribution.
All PronType person features are well-formed (no [−participant, +author]).