Kaqchikel Agent Focus Fragment [Erl16]

Theory-neutral typological data for Agent Focus (AF) in Kaqchikel (K'ichean, Mayan): verb-form types, the empirical extraction profile, and the typological AF/extraction-gap classification.

The theory-laden apparatus that interprets this data lives in study files per the project Fragment-discipline rule (CLAUDE.md):

• OT competing-derivations + SSAL/XRef constraints + ranking → Studies/Erlewine2016.lean
• Minimalist Voice/ClauseSpine for Kaqchikel → Studies/CoonMateoPedroPreminger2014.lean

The Paradigm

Extracted arg	Verb form	Agreement
None (declarative)	Transitive	Set A + Set B
Patient/Abs	Transitive	Set A + Set B
Agent/Erg (local)	AF (-Vn)	Set B only
Agent/Erg (long)	Transitive	Set A + Set B

AF is obligatory for clause-local agent extraction and ungrammatical for patient extraction or long-distance agent extraction — it is not a free alternation but a locality-sensitive, structurally conditioned repair. The structural analysis (SSAL ≫ XRef OT competition) lives in the Erlewine2016 study file.

inductive Kaqchikel.VerbForm : Type

Verbal morphology in a Kaqchikel clause: either the normal transitive form (with Set A ergative agreement) or Agent Focus (with -Vn and no Set A).

• transitive : VerbForm

  Normal transitive: Set A (erg) + Set B (abs) agreement.

• agentFocus : VerbForm

  Agent Focus: suffix -Vn, Set B only, no Set A (erg).

@[implicit_reducible]

instance Kaqchikel.instDecidableEqVerbForm : DecidableEq VerbForm

Equations

• Kaqchikel.instDecidableEqVerbForm x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Kaqchikel.instReprVerbForm.repr : VerbForm → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Kaqchikel.instReprVerbForm : Repr VerbForm

Equations

• Kaqchikel.instReprVerbForm = { reprPrec := Kaqchikel.instReprVerbForm.repr }

def Kaqchikel.VerbForm.hasSetA : VerbForm → Bool

Does this verb form bear ergative (Set A) agreement?

Equations

• Kaqchikel.VerbForm.transitive.hasSetA = true
• Kaqchikel.VerbForm.agentFocus.hasSetA = false

def Kaqchikel.VerbForm.hasAFSuffix : VerbForm → Bool

Does this verb form bear the AF suffix -Vn?

Equations

• Kaqchikel.VerbForm.transitive.hasAFSuffix = false
• Kaqchikel.VerbForm.agentFocus.hasAFSuffix = true

structure Kaqchikel.ExtractionDatum : Type

An extraction datum: which argument is extracted and which verb form surfaces.

• extracted : Extraction.ArgumentRole
• verbForm : VerbForm
• judgment : Extraction.ExtractionMarkingStrategy

def Kaqchikel.instReprExtractionDatum.repr : ExtractionDatum → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Kaqchikel.instReprExtractionDatum : Repr ExtractionDatum

Equations

• Kaqchikel.instReprExtractionDatum = { reprPrec := Kaqchikel.instReprExtractionDatum.repr }

def Kaqchikel.agentExtractionAF : ExtractionDatum

Agent extraction (clause-local) requires AF.

Equations

• Kaqchikel.agentExtractionAF = { extracted := Extraction.ArgumentRole.agent, verbForm := Kaqchikel.VerbForm.agentFocus, judgment := Extraction.ExtractionMarkingStrategy.dedicatedMorpheme }

def Kaqchikel.agentExtractionTrans : ExtractionDatum

Agent extraction with normal transitive (clause-local) is ungrammatical.

Equations

• Kaqchikel.agentExtractionTrans = { extracted := Extraction.ArgumentRole.agent, verbForm := Kaqchikel.VerbForm.transitive, judgment := Extraction.ExtractionMarkingStrategy.dedicatedMorpheme }

def Kaqchikel.patientExtractionTrans : ExtractionDatum

Patient extraction uses normal transitive.

Equations

• Kaqchikel.patientExtractionTrans = { extracted := Extraction.ArgumentRole.patient, verbForm := Kaqchikel.VerbForm.transitive, judgment := Extraction.ExtractionMarkingStrategy.unmarked }

def Kaqchikel.longDistanceAgentExtraction : ExtractionDatum

Long-distance agent extraction uses normal transitive, NOT AF. When the agent extracts from an embedded clause, it passes through intermediate Spec,CP positions via successive-cyclic movement. Each step crosses enough structure to satisfy SSAL — the too-local Spec,TP → Spec,CP step within the embedded clause is avoided.

This is the key evidence that AF is triggered by locality of movement, not simply by agent extraction ([Erl16] §2.3, examples 21–22).

Equations

• Kaqchikel.longDistanceAgentExtraction = { extracted := Extraction.ArgumentRole.agent, verbForm := Kaqchikel.VerbForm.transitive, judgment := Extraction.ExtractionMarkingStrategy.unmarked }

def Kaqchikel.extractionStrategy : Extraction.ExtractionMarkingStrategy

Kaqchikel's extraction data: agent focus alternation (extractionStrategy = .dedicatedMorpheme, marking subject extraction). AF (-Vn) is obligatory for clause-local agent extraction ([Erl16]).

Equations

• Kaqchikel.extractionStrategy = Extraction.ExtractionMarkingStrategy.dedicatedMorpheme

def Kaqchikel.extractionMarkedPositions : List Extraction.ExtractionTarget

Equations

• Kaqchikel.extractionMarkedPositions = [Extraction.ExtractionTarget.subject]

def Kaqchikel.extractionDistinguishesPosition : Bool

Equations

• Kaqchikel.extractionDistinguishesPosition = true

inductive Kaqchikel.MayanAFType : Type

Mayan languages vary in whether AF is available, depending on the ranking of SSAL vs XRef. This produces a two-way typological split:

• AF languages: SSAL >> XRef. Anti-locality violation is repaired by switching to AF morphology. E.g., Kaqchikel, Q'anjob'al.
• Extraction-gap languages: XRef >> SSAL. No AF repair available; clause-local agent extraction is simply ungrammatical. E.g., Chol.

Both types share the same underlying problem (SSAL blocks clause-local agent extraction); they differ only in whether the grammar provides a repair strategy.

• afLanguage : MayanAFType

  SSAL >> XRef: AF available as repair for anti-locality.

• extractionGap : MayanAFType

  XRef >> SSAL: no repair; extraction gap.

@[implicit_reducible]

instance Kaqchikel.instDecidableEqMayanAFType : DecidableEq MayanAFType

Equations

• Kaqchikel.instDecidableEqMayanAFType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Kaqchikel.instReprMayanAFType.repr : MayanAFType → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Kaqchikel.instReprMayanAFType : Repr MayanAFType

Equations

• Kaqchikel.instReprMayanAFType = { reprPrec := Kaqchikel.instReprMayanAFType.repr }

def Kaqchikel.kaqAFType : MayanAFType

Kaqchikel is an AF language (SSAL >> XRef).

Equations

• Kaqchikel.kaqAFType = Kaqchikel.MayanAFType.afLanguage

theorem Kaqchikel.af_no_set_a : VerbForm.agentFocus.hasSetA = false

AF does not bear Set A (ergative) agreement.

theorem Kaqchikel.trans_has_set_a : VerbForm.transitive.hasSetA = true

Normal transitive does bear Set A agreement.

theorem Kaqchikel.af_has_suffix : VerbForm.agentFocus.hasAFSuffix = true

AF bears the -Vn suffix.

Kaqchikel voice system: two-way asymmetrical (transitive/AF).

Not a true pivot system — AF is a locality-sensitive repair for
clause-local agent extraction, not a symmetric voice alternation.
Transitive is the basic form; AF is derived (triggered by SSAL).

Language: "Kaqchikel".
Notes: AF is locality-sensitive repair, not symmetric pivot (Erlewine 2016). 

def Kaqchikel.VoiceSystem.voices : List Voice.VoiceEntry

The voices of the Kaqchikel system.

Equations

• Kaqchikel.VoiceSystem.voices = [{ name := "Transitive", promotes := Voice.PivotTarget.agent }, { name := "Agent Focus", promotes := Voice.PivotTarget.agent }]

def Kaqchikel.VoiceSystem.symmetry : Voice.VoiceSystemSymmetry

System symmetry: asymmetrical (transitive is the basic form).

Equations

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

theorem Kaqchikel.kaq_voice_system_asymmetrical : VoiceSystem.symmetry = Voice.VoiceSystemSymmetry.asymmetrical

theorem Kaqchikel.kaq_voice_count : Voice.voiceCount VoiceSystem.voices = 2

theorem Kaqchikel.kaq_both_promote_agent : (VoiceSystem.voices.all fun (x : Voice.VoiceEntry) => x.promotes == Voice.PivotTarget.agent) = true

Both Kaqchikel voices promote agent — AF is not a patient-promoting voice but an alternative agent-extracting structure.

theorem Kaqchikel.kaq_not_active_passive : ¬Voice.isActivePassive VoiceSystem.voices

Kaqchikel is NOT an active/passive system: it lacks a patient-promoting voice.