K'iche' Voice System Fragment @cite{mondloch-2017}

The five transitive voice alternations of K'iche', following @cite{mondloch-2017} Lessons 15–22, 26–30.

Voice Inventory

K'iche' has five voices for transitive verbs (plus an instrumental voice not covered in the grammar):

1. Active Voice (Lessons 15–18, 26–27): Subject (A), verb, and object (P) are all expressed. Voice marker: -j for derived transitive verbs (DTVs), -Ø for radical transitive verbs (RTVs). Template: aspect + P(SetB) + A(SetA) + root + voice.

2. Simple Passive (Lessons 19–20, 28–29): P is promoted to subject (triggers Set B); A is demoted to an oblique (introduced by rumaal/kumaal 'by'). Voice marker: -x (DTVs), -Vtaj (RTVs). Template: aspect + S(SetB) + root + passive.

3. Absolutive Antipassive (Lesson 21): A is kept as subject (triggers Set B as if intransitive); P is suppressed entirely. Voice marker: -n (DTVs). Verb conjugates like an intransitive. Template: aspect + S(SetB) + root + antipass.

4. Agent-Focus Antipassive (Lessons 22, 30): The subject (A) is focused/emphasized. P triggers Set B, A appears as a separated pronoun before the verb. Voice marker: -n (DTVs), -Vk (RTVs). This is the voice used for subject extraction (wh-questions about the agent), which is why subject extraction triggers Agent Focus morphology rather than wi.

5. Completed Passive (Lessons 20, 29): Like Simple Passive but with completed aspect. Voice marker: -taaj (DTVs for completed aspect only).

Verb Classes

• Derived Transitive Verbs (DTVs): Polysyllabic roots ending in vowels (e.g., kuna 'to cure', tzuku 'to look for').
• Radical Transitive Verbs (RTVs): Monosyllabic roots ending in consonants (e.g., b'an 'to do', ch'ay 'to hit').

Aspect Markers

• Incomplete: k- (ka- before consonant clusters)
• Completed: x-

Connection to Extraction Morphology

Agent Focus Antipassive (voice 4) is the morphological strategy used for subject extraction in K'iche'. When the agent is extracted via Ā-movement (e.g., 'Who bought it?'), the verb appears in Agent Focus voice with the -n or -Vk marker, not with the fronting particle wi. This is why subjectExtraction.wiLicensed = false in ExtractionMorphology.lean — subject extraction uses Agent Focus, not wi.

inductive Fragments.Mayan.Kiche.TransVerbClass : Type

K'iche' transitive verb classes., Lesson 15.

• derived : TransVerbClass

  Derived: polysyllabic roots ending in vowels.

• radical : TransVerbClass

  Radical: monosyllabic roots ending in consonants.

instance Fragments.Mayan.Kiche.instDecidableEqTransVerbClass : DecidableEq TransVerbClass

Equations

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

instance Fragments.Mayan.Kiche.instBEqTransVerbClass : BEq TransVerbClass

Equations

• Fragments.Mayan.Kiche.instBEqTransVerbClass = { beq := Fragments.Mayan.Kiche.instBEqTransVerbClass.beq }

def Fragments.Mayan.Kiche.instBEqTransVerbClass.beq : TransVerbClass → TransVerbClass → Bool

Equations

• Fragments.Mayan.Kiche.instBEqTransVerbClass.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Fragments.Mayan.Kiche.instReprTransVerbClass : Repr TransVerbClass

Equations

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

def Fragments.Mayan.Kiche.instReprTransVerbClass.repr : TransVerbClass → Nat → Std.Format

Equations

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

inductive Fragments.Mayan.Kiche.KicheVoice : Type

The five transitive voices of K'iche'., 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).

instance Fragments.Mayan.Kiche.instDecidableEqKicheVoice : DecidableEq KicheVoice

Equations

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

instance Fragments.Mayan.Kiche.instBEqKicheVoice : BEq KicheVoice

Equations

• Fragments.Mayan.Kiche.instBEqKicheVoice = { beq := Fragments.Mayan.Kiche.instBEqKicheVoice.beq }

def Fragments.Mayan.Kiche.instBEqKicheVoice.beq : KicheVoice → KicheVoice → Bool

Equations

• Fragments.Mayan.Kiche.instBEqKicheVoice.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Fragments.Mayan.Kiche.instReprKicheVoice : Repr KicheVoice

Equations

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

def Fragments.Mayan.Kiche.instReprKicheVoice.repr : KicheVoice → Nat → Std.Format

Equations

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

def Fragments.Mayan.Kiche.allVoices : List KicheVoice

All five voices.

Equations

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

def Fragments.Mayan.Kiche.dtvVoiceMarker : KicheVoice → String

The voice marker suffix for derived transitive verbs (DTVs). : Active = -j (Lesson 15), Simple Passive = -x (Lesson 19), Antipassive = -n (Lesson 21), Agent Focus = -n (Lesson 22), Completed Passive = -taaj (Lesson 20).

Equations

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

def Fragments.Mayan.Kiche.rtvVoiceMarker : KicheVoice → String

The voice marker suffix for radical transitive verbs (RTVs). : Active = Ø (Lesson 26), Simple Passive = -Vtaj (Lesson 28, where V is a copy of the root vowel), Agent Focus = -Vk (Lesson 30).

Equations

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

inductive Fragments.Mayan.Kiche.Aspect : Type

K'iche' aspect markers., Lesson 9.

• incomplete : Aspect
• completed : Aspect

instance Fragments.Mayan.Kiche.instDecidableEqAspect : DecidableEq Aspect

Equations

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

instance Fragments.Mayan.Kiche.instBEqAspect : BEq Aspect

Equations

• Fragments.Mayan.Kiche.instBEqAspect = { beq := Fragments.Mayan.Kiche.instBEqAspect.beq }

def Fragments.Mayan.Kiche.instBEqAspect.beq : Aspect → Aspect → Bool

Equations

• Fragments.Mayan.Kiche.instBEqAspect.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Fragments.Mayan.Kiche.instReprAspect.repr : Aspect → Nat → Std.Format

Equations

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

instance Fragments.Mayan.Kiche.instReprAspect : Repr Aspect

Equations

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

def Fragments.Mayan.Kiche.aspectMarker : Aspect → String

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

Equations

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

structure Fragments.Mayan.Kiche.ActiveVerbForm : Type

The transitive active voice template: aspect + P(Set B) + A(Set A) + root + voice marker. , Lesson 15.

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

instance Fragments.Mayan.Kiche.instReprActiveVerbForm : Repr ActiveVerbForm

Equations

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

def Fragments.Mayan.Kiche.instReprActiveVerbForm.repr : ActiveVerbForm → Nat → Std.Format

Equations

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

structure Fragments.Mayan.Kiche.PassiveVerbForm : Type

The passive voice template: aspect + S(Set B) + root + passive marker. The agent appears as an oblique (rumaal/kumaal). , Lesson 19.

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

def Fragments.Mayan.Kiche.instReprPassiveVerbForm.repr : PassiveVerbForm → Nat → Std.Format

Equations

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

instance Fragments.Mayan.Kiche.instReprPassiveVerbForm : Repr PassiveVerbForm

Equations

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

structure Fragments.Mayan.Kiche.AntipassiveVerbForm : Type

The antipassive voice template: aspect + S(Set B) + root + antipassive marker. P is suppressed. Verb conjugates like an intransitive. , Lesson 21.

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

instance Fragments.Mayan.Kiche.instReprAntipassiveVerbForm : Repr AntipassiveVerbForm

Equations

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

def Fragments.Mayan.Kiche.instReprAntipassiveVerbForm.repr : AntipassiveVerbForm → Nat → Std.Format

Equations

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

def Fragments.Mayan.Kiche.KicheVoice.realizesAgent : KicheVoice → Bool

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

• Fragments.Mayan.Kiche.KicheVoice.active.realizesAgent = true
• Fragments.Mayan.Kiche.KicheVoice.agentFocus.realizesAgent = true
• x✝.realizesAgent = false

def Fragments.Mayan.Kiche.KicheVoice.realizesPatient : KicheVoice → Bool

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

• Fragments.Mayan.Kiche.KicheVoice.active.realizesPatient = true
• Fragments.Mayan.Kiche.KicheVoice.simplePassive.realizesPatient = true
• Fragments.Mayan.Kiche.KicheVoice.completedPassive.realizesPatient = true
• x✝.realizesPatient = false

def Fragments.Mayan.Kiche.KicheVoice.conjugatesIntransitively : KicheVoice → Bool

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

Equations

• Fragments.Mayan.Kiche.KicheVoice.active.conjugatesIntransitively = false
• Fragments.Mayan.Kiche.KicheVoice.agentFocus.conjugatesIntransitively = false
• x✝.conjugatesIntransitively = true

def Fragments.Mayan.Kiche.subjectExtractionVoice : KicheVoice

Agent Focus is the voice used for subject extraction in K'iche'. When 'who' questions target the agent, the verb appears in Agent Focus, not Active Voice. This is why wi is not licensed for subject extraction — Agent Focus morphology is used instead. , Lesson 22; @cite{mendes-ranero-2021}, §2.

Equations

• Fragments.Mayan.Kiche.subjectExtractionVoice = Fragments.Mayan.Kiche.KicheVoice.agentFocus

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

Agent Focus Antipassive shares the same marker as Absolutive Antipassive for DTVs (-n), but their functions are distinct. , Lesson 22 notes: "In spite of the confusingly similar structure between the two voices, their meanings are quite different."

theorem Fragments.Mayan.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.

def Fragments.Mayan.Kiche.kicheVoiceSystem : Interfaces.VoiceSystemProfile

K'iche' voice system profile. Five voices, asymmetrical (Active is the basic form).

Equations

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

theorem Fragments.Mayan.Kiche.kiche_voice_count : kicheVoiceSystem.voiceCount = 5

K'iche' has 5 voices.

theorem Fragments.Mayan.Kiche.kiche_asymmetrical : kicheVoiceSystem.symmetry = Interfaces.VoiceSystemSymmetry.asymmetrical

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

theorem Fragments.Mayan.Kiche.kiche_not_simple_active_passive : kicheVoiceSystem.isActivePassive = false

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

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

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

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

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

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

structure Fragments.Mayan.Kiche.Negation : Type

K'iche' negation uses a circumfixal pattern: na...taj/ta. The first element na precedes the negated constituent; the second element taj (or ta before verbs) follows it. , Lesson 13.

• proclitic : String
• enclitic : String

instance Fragments.Mayan.Kiche.instDecidableEqNegation : DecidableEq Negation

Equations

• Fragments.Mayan.Kiche.instDecidableEqNegation = Fragments.Mayan.Kiche.instDecidableEqNegation.decEq

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

Equations

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

def Fragments.Mayan.Kiche.instBEqNegation.beq : Negation → Negation → Bool

Equations

• Fragments.Mayan.Kiche.instBEqNegation.beq { proclitic := a, enclitic := a_1 } { proclitic := b, enclitic := b_1 } = (a == b && a_1 == b_1)
• Fragments.Mayan.Kiche.instBEqNegation.beq x✝¹ x✝ = false

instance Fragments.Mayan.Kiche.instBEqNegation : BEq Negation

Equations

• Fragments.Mayan.Kiche.instBEqNegation = { beq := Fragments.Mayan.Kiche.instBEqNegation.beq }

def Fragments.Mayan.Kiche.instReprNegation.repr : Negation → Nat → Std.Format

Equations

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

instance Fragments.Mayan.Kiche.instReprNegation : Repr Negation

Equations

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

def Fragments.Mayan.Kiche.negNonverbal : Negation

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

Equations

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

def Fragments.Mayan.Kiche.negVerbal : Negation

Negation of verbal predicates: na...ta.

Equations

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

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

Both negation forms share the proclitic na.

inductive Fragments.Mayan.Kiche.BasicWordOrder : Type

K'iche' basic word order for intransitive clauses with noun subjects is Verb-Subject (VS). , Lesson 9: "the preferred word order appears to be: verb-subject."

• VS : BasicWordOrder
• VOS : BasicWordOrder
• VS_passive : BasicWordOrder

instance Fragments.Mayan.Kiche.instDecidableEqBasicWordOrder : DecidableEq BasicWordOrder

Equations

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

def Fragments.Mayan.Kiche.instBEqBasicWordOrder.beq : BasicWordOrder → BasicWordOrder → Bool

Equations

• Fragments.Mayan.Kiche.instBEqBasicWordOrder.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Fragments.Mayan.Kiche.instBEqBasicWordOrder : BEq BasicWordOrder

Equations

• Fragments.Mayan.Kiche.instBEqBasicWordOrder = { beq := Fragments.Mayan.Kiche.instBEqBasicWordOrder.beq }

def Fragments.Mayan.Kiche.instReprBasicWordOrder.repr : BasicWordOrder → Nat → Std.Format

Equations

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

instance Fragments.Mayan.Kiche.instReprBasicWordOrder : Repr BasicWordOrder

Equations

• Fragments.Mayan.Kiche.instReprBasicWordOrder = { reprPrec := Fragments.Mayan.Kiche.instReprBasicWordOrder.repr }

def Fragments.Mayan.Kiche.intransitiveOrder : BasicWordOrder

Intransitive basic word order is verb-initial.

Equations

• Fragments.Mayan.Kiche.intransitiveOrder = Fragments.Mayan.Kiche.BasicWordOrder.VS

def Fragments.Mayan.Kiche.transitiveOrder : BasicWordOrder

Transitive active basic word order is VOS. The object appears between the verb and the subject.

Equations

• Fragments.Mayan.Kiche.transitiveOrder = Fragments.Mayan.Kiche.BasicWordOrder.VOS