K'iche' Voice System

The five transitive voice alternations of K'iche' (K'ichean Mayan), following [Mon17] Lessons 15–22, 26–30: active, simple passive, absolutive antipassive, agent-focus antipassive, and completed passive. Agent-Focus Antipassive is the voice used for subject extraction, which is why an extracted agent triggers AF morphology rather than the fronting particle wi.

Main declarations

• Kiche.KicheVoice, Kiche.allVoices: the five transitive voices.
• Kiche.dtvVoiceMarker, Kiche.rtvVoiceMarker: voice-marker exponents for derived vs radical transitive verbs.
• Kiche.ActiveVerbForm, Kiche.PassiveVerbForm, Kiche.AntipassiveVerbForm: morphological templates per voice.
• Kiche.KicheVoice.RealizesAgent, .RealizesPatient, .ConjugatesIntransitively: argument-realization predicates per voice.
• Kiche.subjectExtractionVoice: Agent Focus as the subject-extraction voice.
• Kiche.Negation, Kiche.negNonverbal, Kiche.negVerbal: the na...taj/ta circumfixal negation.

Implementation notes

Verb classes split derived transitives (DTVs: polysyllabic vowel-final roots, e.g. kuna 'to cure') from radical transitives (RTVs: monosyllabic consonant-final roots, e.g. b'an 'to do'), which take different voice-marker allomorphs. Aspect is incomplete k- (ka- before clusters) or completed x-. The passive demotes the agent to an oblique introduced by rumaal/kumaal 'by'. An instrumental voice exists but is not covered here. Agent-Focus Antipassive is the strategy for subject extraction ([Mon17] Lesson 22; [MR21] §2), so subjectExtraction.wiLicensed = false in Extraction.lean — the extracted agent takes AF morphology, not wi. The word-order profile lives in WordOrder.lean; the transitive/intransitive/passive conjugation contrast [Mon17] draws (Lesson 9) is paper-specific apparatus that nothing here consumes.

Verb classes

inductive Kiche.TransVerbClass : Type

K'iche' transitive verb classes ([Mon17] Lesson 15).

• derived : TransVerbClass

  Derived: polysyllabic roots ending in vowels.

• radical : TransVerbClass

  Radical: monosyllabic roots ending in consonants.

@[implicit_reducible]

instance Kiche.instDecidableEqTransVerbClass : DecidableEq TransVerbClass

Equations

• Kiche.instDecidableEqTransVerbClass x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Kiche.instReprTransVerbClass : Repr TransVerbClass

Equations

• Kiche.instReprTransVerbClass = { reprPrec := Kiche.instReprTransVerbClass.repr }

def Kiche.instReprTransVerbClass.repr : TransVerbClass → ℕ → Std.Format

Equations

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

Voice alternations

inductive Kiche.KicheVoice : Type

The five transitive voices of K'iche' ([Mon17] Lessons 15–22, 26–30).

• active : KicheVoice

  Active Voice: A and P both expressed.

• simplePassive : KicheVoice

  Simple Passive: P promoted to subject, A demoted to oblique.

• absolutiveAntipassive : KicheVoice

  Absolutive Antipassive: A is subject, P suppressed.

• agentFocus : KicheVoice

  Agent-Focus Antipassive: A is focused/extracted.

• completedPassive : KicheVoice

  Completed Passive (distinct morphology from Simple Passive in completed aspect).

@[implicit_reducible]

instance Kiche.instDecidableEqKicheVoice : DecidableEq KicheVoice

Equations

• Kiche.instDecidableEqKicheVoice x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Kiche.instReprKicheVoice : Repr KicheVoice

Equations

• Kiche.instReprKicheVoice = { reprPrec := Kiche.instReprKicheVoice.repr }

def Kiche.instReprKicheVoice.repr : KicheVoice → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Kiche.instReprKicheVoice.repr Kiche.KicheVoice.active prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Kiche.KicheVoice.active")).group prec✝
• Kiche.instReprKicheVoice.repr Kiche.KicheVoice.agentFocus prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Kiche.KicheVoice.agentFocus")).group prec✝

def Kiche.allVoices : List KicheVoice

All five voices.

Equations

• Kiche.allVoices = [Kiche.KicheVoice.active, Kiche.KicheVoice.simplePassive, Kiche.KicheVoice.absolutiveAntipassive, Kiche.KicheVoice.agentFocus, Kiche.KicheVoice.completedPassive]

Voice markers

def Kiche.dtvVoiceMarker : KicheVoice → String

Voice-marker suffix for derived transitive verbs (DTVs), per [Mon17]: active -j (Lesson 15), simple passive -x (Lesson 19), antipassive -n (Lesson 21), Agent Focus -n (Lesson 22), completed passive -taaj (Lesson 20).

Equations

• Kiche.dtvVoiceMarker Kiche.KicheVoice.active = "-j"
• Kiche.dtvVoiceMarker Kiche.KicheVoice.simplePassive = "-x"
• Kiche.dtvVoiceMarker Kiche.KicheVoice.absolutiveAntipassive = "-n"
• Kiche.dtvVoiceMarker Kiche.KicheVoice.agentFocus = "-n"
• Kiche.dtvVoiceMarker Kiche.KicheVoice.completedPassive = "-taaj"

def Kiche.rtvVoiceMarker : KicheVoice → String

Voice-marker suffix for radical transitive verbs (RTVs), per [Mon17]: active Ø (Lesson 26), simple passive -Vtaj (Lesson 28, V copying the root vowel), Agent Focus -Vk (Lesson 30).

Equations

• Kiche.rtvVoiceMarker Kiche.KicheVoice.active = "Ø"
• Kiche.rtvVoiceMarker Kiche.KicheVoice.simplePassive = "-Vtaj"
• Kiche.rtvVoiceMarker Kiche.KicheVoice.absolutiveAntipassive = "-n"
• Kiche.rtvVoiceMarker Kiche.KicheVoice.agentFocus = "-Vk"
• Kiche.rtvVoiceMarker Kiche.KicheVoice.completedPassive = "-Vtaj"

Aspect markers

inductive Kiche.Aspect : Type

K'iche' aspect markers ([Mon17] Lesson 9).

• incomplete : Aspect
• completed : Aspect

@[implicit_reducible]

instance Kiche.instDecidableEqAspect : DecidableEq Aspect

Equations

• Kiche.instDecidableEqAspect x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Kiche.instReprAspect.repr : Aspect → ℕ → Std.Format

Equations

• Kiche.instReprAspect.repr Kiche.Aspect.incomplete prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Kiche.Aspect.incomplete")).group prec✝
• Kiche.instReprAspect.repr Kiche.Aspect.completed prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Kiche.Aspect.completed")).group prec✝

@[implicit_reducible]

instance Kiche.instReprAspect : Repr Aspect

Equations

• Kiche.instReprAspect = { reprPrec := Kiche.instReprAspect.repr }

def Kiche.aspectMarker : Aspect → String

The morphological form of the aspect marker ([Mon17] Lesson 9): k- (ka-) for incomplete, x- for completed.

Equations

• Kiche.aspectMarker Kiche.Aspect.incomplete = "k-"
• Kiche.aspectMarker Kiche.Aspect.completed = "x-"

Morphological templates

structure Kiche.ActiveVerbForm : Type

Transitive active voice template: aspect + P(Set B) + A(Set A) + root + voice marker ([Mon17] Lesson 15).

• aspect : Aspect
• object : PhiFeatures
• subject : PhiFeatures
• root : String
• verbClass : TransVerbClass

def Kiche.instReprActiveVerbForm.repr : ActiveVerbForm → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Kiche.instReprActiveVerbForm : Repr ActiveVerbForm

Equations

• Kiche.instReprActiveVerbForm = { reprPrec := Kiche.instReprActiveVerbForm.repr }

structure Kiche.PassiveVerbForm : Type

Passive voice template: aspect + S(Set B) + root + passive marker, with the agent as an oblique (rumaal/kumaal) ([Mon17] Lesson 19).

• aspect : Aspect
• subject : PhiFeatures
• root : String
• verbClass : TransVerbClass

@[implicit_reducible]

instance Kiche.instReprPassiveVerbForm : Repr PassiveVerbForm

Equations

• Kiche.instReprPassiveVerbForm = { reprPrec := Kiche.instReprPassiveVerbForm.repr }

def Kiche.instReprPassiveVerbForm.repr : PassiveVerbForm → ℕ → Std.Format

Equations

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

structure Kiche.AntipassiveVerbForm : Type

Antipassive voice template: aspect + S(Set B) + root + antipassive marker; P is suppressed and the verb conjugates like an intransitive ([Mon17] Lesson 21).

• aspect : Aspect
• subject : PhiFeatures
• root : String
• verbClass : TransVerbClass

@[implicit_reducible]

instance Kiche.instReprAntipassiveVerbForm : Repr AntipassiveVerbForm

Equations

• Kiche.instReprAntipassiveVerbForm = { reprPrec := Kiche.instReprAntipassiveVerbForm.repr }

def Kiche.instReprAntipassiveVerbForm.repr : AntipassiveVerbForm → ℕ → Std.Format

Equations

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

Argument realization per voice

def Kiche.KicheVoice.RealizesAgent : KicheVoice → Prop

Does this voice realize A (the transitive agent) as a full agreement-bearing argument? In Active and Agent Focus, yes. In passives and Absolutive Antipassive, A is either demoted (oblique) or absent.

Equations

• Kiche.KicheVoice.active.RealizesAgent = True
• Kiche.KicheVoice.agentFocus.RealizesAgent = True
• x✝.RealizesAgent = False

@[implicit_reducible]

instance Kiche.instDecidablePredKicheVoiceRealizesAgent : DecidablePred KicheVoice.RealizesAgent

Equations

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

def Kiche.KicheVoice.RealizesPatient : KicheVoice → Prop

Does this voice realize P (the transitive patient) as a full agreement-bearing argument? In Active and passives, yes. In antipassives, P is suppressed or demoted.

Equations

• Kiche.KicheVoice.active.RealizesPatient = True
• Kiche.KicheVoice.simplePassive.RealizesPatient = True
• Kiche.KicheVoice.completedPassive.RealizesPatient = True
• x✝.RealizesPatient = False

@[implicit_reducible]

instance Kiche.instDecidablePredKicheVoiceRealizesPatient : DecidablePred KicheVoice.RealizesPatient

Equations

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

def Kiche.KicheVoice.ConjugatesIntransitively : KicheVoice → Prop

Is the verb in this voice conjugated like an intransitive (only Set B agreement, no Set A)? Passives and antipassives both conjugate intransitively. [Mon17] Lesson 19 (passive = "like intransitive"), Lesson 21 (antipassive = "exactly as Simple Intransitive Verbs").

Equations

• Kiche.KicheVoice.active.ConjugatesIntransitively = False
• Kiche.KicheVoice.agentFocus.ConjugatesIntransitively = False
• x✝.ConjugatesIntransitively = True

@[implicit_reducible]

instance Kiche.instDecidablePredKicheVoiceConjugatesIntransitively : DecidablePred KicheVoice.ConjugatesIntransitively

Equations

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

Agent Focus and subject extraction

def Kiche.subjectExtractionVoice : KicheVoice

Agent Focus is the voice used for subject extraction in K'iche': 'who' questions targeting the agent take AF, not Active, which is why wi is not licensed for subject extraction ([Mon17] Lesson 22; [MR21] §2).

Equations

• Kiche.subjectExtractionVoice = Kiche.KicheVoice.agentFocus

theorem Kiche.af_marker_eq_antip_marker : dtvVoiceMarker KicheVoice.agentFocus = dtvVoiceMarker KicheVoice.absolutiveAntipassive

Agent Focus and Absolutive Antipassive share the DTV marker -n but differ in function — [Mon17] Lesson 22: "In spite of the confusingly similar structure between the two voices, their meanings are quite different."

theorem Kiche.rtv_af_marker_neq_antip : rtvVoiceMarker KicheVoice.agentFocus ≠ rtvVoiceMarker KicheVoice.absolutiveAntipassive

For RTVs, Agent Focus and Absolutive Antipassive have DIFFERENT markers: -Vk vs -n.

Voice system profile

def Kiche.VoiceSystem.voices : List Voice.VoiceEntry

The five voices of K'iche'.

Equations

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

def Kiche.VoiceSystem.symmetry : Voice.VoiceSystemSymmetry

K'iche' is asymmetrical — Active is the basic voice.

Equations

• Kiche.VoiceSystem.symmetry = Voice.VoiceSystemSymmetry.asymmetrical

Voice system theorems

theorem Kiche.kiche_voice_count : Voice.voiceCount VoiceSystem.voices = 5

K'iche' has 5 voices.

theorem Kiche.kiche_asymmetrical : VoiceSystem.symmetry = Voice.VoiceSystemSymmetry.asymmetrical

K'iche' voice system is asymmetrical (Active is basic).

theorem Kiche.kiche_not_simple_active_passive : ¬Voice.isActivePassive VoiceSystem.voices

K'iche' is NOT a simple active/passive system (it has 5 voices, not 2).

DTV voice-marker verification

theorem Kiche.dtv_active_marker : dtvVoiceMarker KicheVoice.active = "-j"

theorem Kiche.dtv_passive_marker : dtvVoiceMarker KicheVoice.simplePassive = "-x"

theorem Kiche.dtv_antip_marker : dtvVoiceMarker KicheVoice.absolutiveAntipassive = "-n"

theorem Kiche.dtv_af_marker : dtvVoiceMarker KicheVoice.agentFocus = "-n"

theorem Kiche.dtv_comppass_marker : dtvVoiceMarker KicheVoice.completedPassive = "-taaj"

Negation template

structure Kiche.Negation : Type

K'iche' circumfixal negation na...taj/ta: na precedes the negated constituent, taj (or ta before verbs) follows it ([Mon17] Lesson 13).

• proclitic : String
• enclitic : String

@[implicit_reducible]

instance Kiche.instDecidableEqNegation : DecidableEq Negation

Equations

• Kiche.instDecidableEqNegation = Kiche.instDecidableEqNegation.decEq

def Kiche.instDecidableEqNegation.decEq (x✝ x✝¹ : Negation) : Decidable (x✝ = x✝¹)

Equations

• Kiche.instDecidableEqNegation.decEq { proclitic := a, enclitic := a_1 } { proclitic := b, enclitic := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

@[implicit_reducible]

instance Kiche.instReprNegation : Repr Negation

Equations

• Kiche.instReprNegation = { reprPrec := Kiche.instReprNegation.repr }

def Kiche.instReprNegation.repr : Negation → ℕ → Std.Format

Equations

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

def Kiche.negNonverbal : Negation

Negation of nonverbal predicates (pronouns, nouns, adjectives, adverbs, prepositions): na...taj.

Equations

• Kiche.negNonverbal = { enclitic := "taj" }

def Kiche.negVerbal : Negation

Negation of verbal predicates: na...ta.

Equations

• Kiche.negVerbal = { enclitic := "ta" }

theorem Kiche.neg_same_proclitic : negNonverbal.proclitic = negVerbal.proclitic

Both negation forms share the proclitic na.