K'iche' Voice System Fragment [Mon17]

The five transitive voice alternations of K'iche', following [Mon17] 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 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.

@[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.

inductive 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).

@[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]

def 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

• 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

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

• 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"

inductive Kiche.Aspect : Type

K'iche' aspect markers., 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. , Lesson 9: k- (ka-) for incomplete, x- for completed.

Equations

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

structure 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

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

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 Kiche.instReprPassiveVerbForm.repr : PassiveVerbForm → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Kiche.instReprPassiveVerbForm : Repr PassiveVerbForm

Equations

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

structure 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

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

Equations

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

@[implicit_reducible]

instance Kiche.instReprAntipassiveVerbForm : Repr AntipassiveVerbForm

Equations

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

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.

def 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; [MR21], §2.

Equations

• Kiche.subjectExtractionVoice = Kiche.KicheVoice.agentFocus

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

K'iche' voice system profile

Five voices, asymmetrical (Active is the basic form): 5 voices (+ instrumental, not covered); Active is basic ([Mon17]); Agent Focus used for subject extraction.

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

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).

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"

structure 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

@[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 ⋯

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

Equations

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

@[implicit_reducible]

instance Kiche.instReprNegation : Repr Negation

Equations

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

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.