San Juan Atitán Mam Pronouns

Pronoun lexicon for San Juan Atitán Mam (SJA Mam, Mayan), from [Sco23] ch. 4. Scott's central claim is that the reduced subject/possessor forms are true pronouns in argument position — not agreement markers (contra her own Scott 2020 analysis) and not a special clitic series (she explicitly prefers an impoverishment derivation over "positing a unique series of 'clitic' pronouns", p. 162, citing the Agree-affects-pronouns family: Cardinaletti & Starke, Nevins, Kramer, Stegovec, Yuan). The entries therefore live here as PersonalPronoun values flowing through the shared Pronoun API.

Two series (her Table 4.1 / 4.9, p. 160 / 185):

• Independent ("most morphosyntactically rich", her fn. 2 — the 2SG "independent" form is the enclitic =i itself): qini (= qin+=i), qoy (= qo'+=y), qo, =i, qi (= q+=i), 3SG ∅, qa.
• Subject/possessor (reduced): first-person cells lose their base morphemes (qin [+author,+sg], qo [+author,−sg], Table 4.10) via an impoverishment rule conditioned on agreement (§4.4); 2nd/3rd cells are identical to the independent series.

The disagreement enclitic =i (gloss DISAGR; [Noy92], [Har16a]; her §4.3.3) realizes disagreeing values of [±author]/[±participant] — enclitic_iff_disagrees verifies the XOR distribution across the paradigm. reduction_iff_author verifies that the two series differ exactly at [+author] cells.

Feature values follow her Table 4.4 (p. 183). NB the convention: Harbour's [±participant] "functions more like a [+/−hearer] or [+/−addressee] feature" (p. 182), so 1EXCL is [−participant] — this deliberately diverges from Person.Features, whose wellFormed invariant (author → participant) encodes the speech-act-participant convention; hence the fragment-local ScottFeatures.

Wordhood: =i is a morphological enclitic with promiscuous attachment (nouns, verbs, pronouns, other clitics; allomorphs <i>/<y>, =ni after [m]); whether qi/qa are words or enclitics is left open by Scott (p. 163, her p. 39) — none of this is a Cardinaletti–Starke deficiency classification, so strength is left unset throughout.

Lexical entries

def Mam.iDisagr : PersonalPronoun

=i — the disagreement enclitic pronoun (DISAGR): realizes disagreeing [±author]/[±participant] values, hence φ-underspecified (it serves 1SG, 1PL.EXCL, 2SG, and — with the plural piece q — 2PL; Table 4.11). Doubles as the 2SG "independent" form (her fn. 2).

Equations

• Mam.iDisagr = { form := "=i" }

def Mam.qini : PersonalPronoun

qini — 1SG independent pronoun; bimorphemic qin+=i (base qin [+author,+sg] + disagreement enclitic, Table 4.9).

Equations

• Mam.qini = { form := "qini", person := some Person.first, number := some Number.singular }

def Mam.qoy : PersonalPronoun

qoy — 1PL exclusive independent pronoun; bimorphemic qo'+=y (base qo [+author,−sg] + enclitic; glottalization from the enclitic, her fn. 7).

Equations

• Mam.qoy = { form := "qoy", person := some Person.firstExclusive, number := some Number.plural }

def Mam.qo : PersonalPronoun

qo — 1PL inclusive independent pronoun; monomorphemic (1INCL's [+author,+participant] values agree, so no enclitic).

Equations

• Mam.qo = { form := "qo", person := some Person.firstInclusive, number := some Number.plural }

def Mam.qi : PersonalPronoun

qi — 2PL pronoun, both series; bimorphemic q+=i (§4.3.3.2). Word-vs-enclitic status left open by Scott (p. 163).

Equations

• Mam.qi = { form := "qi", person := some Person.second, number := some Number.plural }

def Mam.qa : PersonalPronoun

qa — 3PL pronoun, both series; also the generic plural marker of the language (her (42)–(44)). Word-vs-enclitic status left open.

Equations

• Mam.qa = { form := "qa", person := some Person.third, number := some Number.plural }

theorem Mam.clusive_entries_wellFormed : qoy.WellFormed ∧ qo.WellFormed

The clusivity-marked entries satisfy the API's well-formedness invariant (clusivity only on 1st-person non-singular).

The paradigm

inductive Mam.PronCell : Type

A cell of the SJA Mam pronominal paradigm: the quadripartition (1EXCL/1INCL/2/3, Table 4.3) crossed with number, minus the principled gap *1SG-inclusive (Table 4.4).

• firstSg : PronCell
• firstPlExcl : PronCell
• firstPlIncl : PronCell
• secondSg : PronCell
• secondPl : PronCell
• thirdSg : PronCell
• thirdPl : PronCell

@[implicit_reducible]

instance Mam.instDecidableEqPronCell : DecidableEq PronCell

Equations

• Mam.instDecidableEqPronCell x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Mam.instReprPronCell.repr : PronCell → ℕ → Std.Format

Equations

• Mam.instReprPronCell.repr Mam.PronCell.firstSg prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Mam.PronCell.firstSg")).group prec✝
• Mam.instReprPronCell.repr Mam.PronCell.firstPlExcl prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Mam.PronCell.firstPlExcl")).group prec✝
• Mam.instReprPronCell.repr Mam.PronCell.firstPlIncl prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Mam.PronCell.firstPlIncl")).group prec✝
• Mam.instReprPronCell.repr Mam.PronCell.secondSg prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Mam.PronCell.secondSg")).group prec✝
• Mam.instReprPronCell.repr Mam.PronCell.secondPl prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Mam.PronCell.secondPl")).group prec✝
• Mam.instReprPronCell.repr Mam.PronCell.thirdSg prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Mam.PronCell.thirdSg")).group prec✝
• Mam.instReprPronCell.repr Mam.PronCell.thirdPl prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Mam.PronCell.thirdPl")).group prec✝

@[implicit_reducible]

instance Mam.instReprPronCell : Repr PronCell

Equations

• Mam.instReprPronCell = { reprPrec := Mam.instReprPronCell.repr }

def Mam.PronCell.person : PronCell → UD.Person

PronCell person, in the API's vocabulary.

Equations

• Mam.PronCell.firstSg.person = UD.Person.first
• Mam.PronCell.firstPlExcl.person = UD.Person.first
• Mam.PronCell.firstPlIncl.person = UD.Person.first
• Mam.PronCell.secondSg.person = UD.Person.second
• Mam.PronCell.secondPl.person = UD.Person.second
• Mam.PronCell.thirdSg.person = UD.Person.third
• Mam.PronCell.thirdPl.person = UD.Person.third

def Mam.PronCell.number : PronCell → UD.Number

PronCell number, in the API's vocabulary.

Equations

• Mam.PronCell.firstSg.number = UD.Number.Sing
• Mam.PronCell.secondSg.number = UD.Number.Sing
• Mam.PronCell.thirdSg.number = UD.Number.Sing
• x✝.number = UD.Number.Plur

def Mam.PronCell.toPerson : PronCell → Person

PronCell person in the canonical inventory: clusivity rides on the person value.

Equations

• Mam.PronCell.firstSg.toPerson = Person.first
• Mam.PronCell.firstPlExcl.toPerson = Person.firstExclusive
• Mam.PronCell.firstPlIncl.toPerson = Person.firstInclusive
• Mam.PronCell.secondSg.toPerson = Person.second
• Mam.PronCell.secondPl.toPerson = Person.second
• Mam.PronCell.thirdSg.toPerson = Person.third
• Mam.PronCell.thirdPl.toPerson = Person.third

structure Mam.ScottFeatures : Type

[Sco23]'s bivalent φ-features (Table 4.4, after [Har16a]): [±author], [±participant], [±singular]. Fragment-local because the participant convention (≈ [±hearer]: 1EXCL is [−participant]) is incompatible with Person.Features' author → participant invariant.

• author : Bool
• participant : Bool
• singular : Bool

def Mam.instDecidableEqScottFeatures.decEq (x✝ x✝¹ : ScottFeatures) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance Mam.instDecidableEqScottFeatures : DecidableEq ScottFeatures

Equations

• Mam.instDecidableEqScottFeatures = Mam.instDecidableEqScottFeatures.decEq

@[implicit_reducible]

instance Mam.instReprScottFeatures : Repr ScottFeatures

Equations

• Mam.instReprScottFeatures = { reprPrec := Mam.instReprScottFeatures.repr }

def Mam.instReprScottFeatures.repr : ScottFeatures → ℕ → Std.Format

Equations

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

def Mam.PronCell.features : PronCell → ScottFeatures

Feature values per cell — a transcription of Table 4.4.

Equations

• Mam.PronCell.firstSg.features = { author := true, participant := false, singular := true }
• Mam.PronCell.firstPlExcl.features = { author := true, participant := false, singular := false }
• Mam.PronCell.firstPlIncl.features = { author := true, participant := true, singular := false }
• Mam.PronCell.secondSg.features = { author := false, participant := true, singular := true }
• Mam.PronCell.secondPl.features = { author := false, participant := true, singular := false }
• Mam.PronCell.thirdSg.features = { author := false, participant := false, singular := true }
• Mam.PronCell.thirdPl.features = { author := false, participant := false, singular := false }

def Mam.PronCell.Disagrees (c : PronCell) : Prop

[±author]/[±participant] values disagree — the condition under which the enclitic =i is inserted ([Noy92]; [Sco23] §4.3.3).

Equations

• c.Disagrees = (c.features.author ≠ c.features.participant)

@[implicit_reducible]

instance Mam.instDecidablePredPronCellDisagrees : DecidablePred PronCell.Disagrees

Equations

• Mam.instDecidablePredPronCellDisagrees c = id inferInstance

theorem Mam.author_iff_first (c : PronCell) : c.features.author = true ↔ c.person = UD.Person.first

The feature table is faithful to the API-side person values: [+author] exactly at first person.

theorem Mam.singular_iff_sing (c : PronCell) : c.features.singular = true ↔ c.number = UD.Number.Sing

The feature table is faithful to the API-side number values: [+singular] exactly at singular cells.

def Mam.independent : PronCell → Option PersonalPronoun

Independent pronoun by cell (Table 4.1 right column; 3SG has no overt pronoun).

Equations

• Mam.independent Mam.PronCell.firstSg = some Mam.qini
• Mam.independent Mam.PronCell.firstPlExcl = some Mam.qoy
• Mam.independent Mam.PronCell.firstPlIncl = some Mam.qo
• Mam.independent Mam.PronCell.secondSg = some Mam.iDisagr
• Mam.independent Mam.PronCell.secondPl = some Mam.qi
• Mam.independent Mam.PronCell.thirdSg = none
• Mam.independent Mam.PronCell.thirdPl = some Mam.qa

def Mam.subjPoss : PronCell → Option PersonalPronoun

Subject/possessor (reduced) pronoun by cell (Table 4.1 left column): first-person bases are bled by impoverishment (§4.4), so 1SG/1PL.EXCL surface as bare =i and 1PL.INCL as ∅; 2nd/3rd are identical to the independent series.

Equations

• Mam.subjPoss Mam.PronCell.firstSg = some Mam.iDisagr
• Mam.subjPoss Mam.PronCell.firstPlExcl = some Mam.iDisagr
• Mam.subjPoss Mam.PronCell.firstPlIncl = none
• Mam.subjPoss Mam.PronCell.secondSg = some Mam.iDisagr
• Mam.subjPoss Mam.PronCell.secondPl = some Mam.qi
• Mam.subjPoss Mam.PronCell.thirdSg = none
• Mam.subjPoss Mam.PronCell.thirdPl = some Mam.qa

def Mam.bearsEnclitic (p : PersonalPronoun) : Bool

Morphological-parse data (Table 4.9): the form contains the disagreement enclitic. qini = qin+=i, qoy = qo'+=y, qi = q+=i, and =i itself; qo and qa contain no enclitic.

Equations

• Mam.bearsEnclitic p = (p == Mam.iDisagr || p == Mam.qini || p == Mam.qoy || p == Mam.qi)

Verification theorems

theorem Mam.enclitic_iff_disagrees (c : PronCell) : Option.any bearsEnclitic (independent c) = true ↔ c.Disagrees

Noyer/Scott's disagreement generalization, verified across the whole paradigm: a cell's independent form contains =i iff its [±author]/[±participant] values disagree (Table 4.4 × Table 4.9/4.11).

theorem Mam.reduction_iff_author (c : PronCell) : subjPoss c ≠ independent c ↔ c.features.author = true

Reduction is exactly first-personhood: the subject/possessor form differs from the independent form precisely at [+author] cells (Table 4.1; the impoverishment rule targets [+author] under agreement, §4.4).

theorem Mam.reduced_residue (c : PronCell) (h : subjPoss c ≠ independent c) : subjPoss c = some iDisagr ∨ subjPoss c = none

What reduction leaves behind is never a base: every reduced (≠ independent) cell surfaces as bare =i or as ∅ — the enclitic is all that survives impoverishment.