K'iche' Extraction Morphology Fragment

@cite{mendes-ranero-2021} @cite{elkins-torrence-brown-2026} @cite{mondloch-2017}

Theory-neutral data on the extraction particle wi (the "fronting particle") in K'iche' and Kaqchikel (K'ichean Mayan).

The Phenomenon

When a low adjunct (locative, instrumental, comitative, indirect object) undergoes Ā-extraction in K'ichean languages, the particle wi appears as a verbal enclitic. M&R analyze wi as the result of Chain Reduction via Substitution: the lower copy of the moved adjunct (bearing [APPL]) is substituted by wi rather than being deleted.

Key Properties

1. Trigger: Low adjuncts only — those introduced in Spec,ApplP (instrumentals, locatives, comitatives, indirect objects). Temporal and reason adjuncts do NOT trigger wi.
2. Obligatoriness: Obligatory in K'iche', optional in Patzún Kaqchikel, absent in some Kaqchikel dialects (e.g. Tecpán).
3. Fronting Particle Generalization (definition 5 of M&R, first observed by Can Pixabaj 2015): In long-distance extraction from a single embedded clause, the presence of wi in the matrix clause is contingent on the presence of an overt complementizer in the embedded clause. Embedded CPs yield wi on both predicates; embedded AspPs yield wi only on the embedded predicate.
4. Not a pronoun, applicative head, movement trigger, or AF morpheme (M&R §4 rejects all four alternative analyses).

inductive Fragments.Mayan.Kiche.ExtractedArgType : Type

Types of extracted arguments relevant for wi distribution.

• obliqueSpatial : ExtractedArgType
• obliqueTemporal : ExtractedArgType
• obliqueReason : ExtractedArgType
• obliqueInstrumental : ExtractedArgType
• subject : ExtractedArgType
• object : ExtractedArgType

instance Fragments.Mayan.Kiche.instDecidableEqExtractedArgType : DecidableEq ExtractedArgType

Equations

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

instance Fragments.Mayan.Kiche.instBEqExtractedArgType : BEq ExtractedArgType

Equations

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

def Fragments.Mayan.Kiche.instBEqExtractedArgType.beq : ExtractedArgType → ExtractedArgType → Bool

Equations

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

instance Fragments.Mayan.Kiche.instReprExtractedArgType : Repr ExtractedArgType

Equations

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

def Fragments.Mayan.Kiche.instReprExtractedArgType.repr : ExtractedArgType → Nat → Std.Format

Equations

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

def Fragments.Mayan.Kiche.ExtractedArgType.isOblique : ExtractedArgType → Bool

Is this argument type an oblique?

Equations

• Fragments.Mayan.Kiche.ExtractedArgType.obliqueSpatial.isOblique = true
• Fragments.Mayan.Kiche.ExtractedArgType.obliqueTemporal.isOblique = true
• Fragments.Mayan.Kiche.ExtractedArgType.obliqueReason.isOblique = true
• Fragments.Mayan.Kiche.ExtractedArgType.obliqueInstrumental.isOblique = true
• Fragments.Mayan.Kiche.ExtractedArgType.subject.isOblique = false
• Fragments.Mayan.Kiche.ExtractedArgType.object.isOblique = false

structure Fragments.Mayan.Kiche.KicheExtractionDatum : Type

A K'iche' extraction data point: what is extracted and whether wi appears after the verb.

• label : String
• reference : String
• extractedType : ExtractedArgType
• wiLicensed : Bool

instance Fragments.Mayan.Kiche.instReprKicheExtractionDatum : Repr KicheExtractionDatum

Equations

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

def Fragments.Mayan.Kiche.instReprKicheExtractionDatum.repr : KicheExtractionDatum → Nat → Std.Format

Equations

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

def Fragments.Mayan.Kiche.spatialOblExtraction : KicheExtractionDatum

Spatial oblique extraction: wi licensed. "Where did you go yesterday?" — wi appears at extraction site. @cite{mondloch-2017} Lesson 14; @cite{mendes-ranero-2021} §2, ex. (9a).

Equations

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

def Fragments.Mayan.Kiche.instrumentalOblExtraction : KicheExtractionDatum

Instrumental oblique extraction: wi licensed. "With what did they eat their food?" — wi at extraction site. @cite{mendes-ranero-2021} §2, ex. (9b).

Equations

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

def Fragments.Mayan.Kiche.temporalOblExtraction : KicheExtractionDatum

Temporal oblique extraction: wi NOT licensed. "When did you eat beans?" — no wi. Parallel to Mam: temporal obliques are exempt in both language groups. @cite{mendes-ranero-2021} §2, ex. (12c).

Equations

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

def Fragments.Mayan.Kiche.reasonOblExtraction : KicheExtractionDatum

Reason oblique extraction: wi NOT licensed. "Why did Juan work?" — no wi. KEY CONTRAST with Mam: SJO =(y)a' IS licensed with reason extraction. @cite{mendes-ranero-2021} §2 (adapted from Elkins et al. Table 3).

Equations

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

def Fragments.Mayan.Kiche.subjectExtraction : KicheExtractionDatum

Subject extraction: wi NOT licensed (Agent Focus instead). "Who bought it?" — AF morphology -Vk instead of wi. @cite{mendes-ranero-2021} §2, item (6c).

Equations

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

def Fragments.Mayan.Kiche.objectExtraction : KicheExtractionDatum

Object extraction: wi NOT licensed. "What did you buy?" — no wi. @cite{elkins-torrence-brown-2026}.

Equations

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

def Fragments.Mayan.Kiche.allData : List KicheExtractionDatum

All K'iche' extraction data points.

Equations

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

theorem Fragments.Mayan.Kiche.wi_subset_of_obliques : (allData.all fun (d : KicheExtractionDatum) => d.wiLicensed == (d.extractedType == ExtractedArgType.obliqueSpatial || d.extractedType == ExtractedArgType.obliqueInstrumental)) = true

Among the formalized data points, wi is licensed exactly for spatial and instrumental obliques. The full set of wi-triggering obliques includes comitatives and indirect objects as well (@cite{mendes-ranero-2021} §2; @cite{elkins-torrence-brown-2026} Table 3), but those are not yet formalized here.

theorem Fragments.Mayan.Kiche.wi_not_core_args : subjectExtraction.wiLicensed = false ∧ objectExtraction.wiLicensed = false

wi does not appear with subject or object extraction.

theorem Fragments.Mayan.Kiche.temporal_exempt : temporalOblExtraction.wiLicensed = false

Temporal exemption is shared across Mayan: neither wi (K'ichean) nor =(y)a' (Mam) appears with temporal oblique extraction.

inductive Fragments.Mayan.Kiche.KicheEmbeddedClauseType : Type

Embedded clause types relevant for long-distance wi distribution. The crucial distinction is whether the embedded clause has an overt complementizer (= CP) or not (= AspP, a structurally reduced clause). @cite{mendes-ranero-2021} §2, exx. (17)–(20), (34)–(37).

• cp : KicheEmbeddedClauseType

  Full CP with overt complementizer chi.

• aspP : KicheEmbeddedClauseType

  Reduced AspP without complementizer.

instance Fragments.Mayan.Kiche.instDecidableEqKicheEmbeddedClauseType : DecidableEq KicheEmbeddedClauseType

Equations

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

def Fragments.Mayan.Kiche.instBEqKicheEmbeddedClauseType.beq : KicheEmbeddedClauseType → KicheEmbeddedClauseType → Bool

Equations

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

instance Fragments.Mayan.Kiche.instBEqKicheEmbeddedClauseType : BEq KicheEmbeddedClauseType

Equations

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

def Fragments.Mayan.Kiche.instReprKicheEmbeddedClauseType.repr : KicheEmbeddedClauseType → Nat → Std.Format

Equations

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

instance Fragments.Mayan.Kiche.instReprKicheEmbeddedClauseType : Repr KicheEmbeddedClauseType

Equations

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

def Fragments.Mayan.Kiche.KicheEmbeddedClauseType.hasComp : KicheEmbeddedClauseType → Bool

Does this clause type have an overt complementizer?

Equations

• Fragments.Mayan.Kiche.KicheEmbeddedClauseType.cp.hasComp = true
• Fragments.Mayan.Kiche.KicheEmbeddedClauseType.aspP.hasComp = false

structure Fragments.Mayan.Kiche.KicheLongDistanceDatum : Type

Long-distance extraction datum for K'ichean wi.

• label : String
• reference : String
• embeddedType : KicheEmbeddedClauseType
• wiOnMatrix : Bool

  Does wi appear on the matrix predicate?

• wiOnEmbedded : Bool

  Does wi appear on the embedded predicate?

instance Fragments.Mayan.Kiche.instReprKicheLongDistanceDatum : Repr KicheLongDistanceDatum

Equations

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

def Fragments.Mayan.Kiche.instReprKicheLongDistanceDatum.repr : KicheLongDistanceDatum → Nat → Std.Format

Equations

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

def Fragments.Mayan.Kiche.ldFromCP : KicheLongDistanceDatum

LD from embedded CP: wi on BOTH matrix and embedded predicates. @cite{mendes-ranero-2021} §3, ex. (34); adapted from Can Pixabaj 2015: 166–167.

Equations

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

def Fragments.Mayan.Kiche.ldFromAspP : KicheLongDistanceDatum

LD from embedded AspP: wi only on embedded predicate, NOT matrix. @cite{mendes-ranero-2021} §3, ex. (35); adapted from Can Pixabaj 2015: 163.

Equations

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

def Fragments.Mayan.Kiche.ldData : List KicheLongDistanceDatum

Equations

• Fragments.Mayan.Kiche.ldData = [Fragments.Mayan.Kiche.ldFromCP, Fragments.Mayan.Kiche.ldFromAspP]

theorem Fragments.Mayan.Kiche.fronting_particle_generalization : (ldData.all fun (d : KicheLongDistanceDatum) => d.embeddedType.hasComp == d.wiOnMatrix) = true

The Fronting Particle Generalization (@cite{mendes-ranero-2021}, definition (5); first discussed by Can Pixabaj 2015):

In long-distance A'-extraction of low adjuncts from a single embedded clause, the presence of wi in the matrix clause is contingent on the presence of an overt complementizer in the embedded clause.

Structural explanation (M&R §3): C⁰ is a phase head, so when the embedded clause is a CP, the extracted adjunct must stop over in the embedded Spec,CP. Chain Reduction via Substitution applies to this intermediate copy, yielding wi on the matrix predicate. When the embedded clause is an AspP (no C⁰, no phase boundary), the adjunct moves directly to the matrix Spec,CP — no intermediate copy, no matrix wi.

def Fragments.Mayan.Kiche.kicheanExtractionProfile : Interfaces.ExtractionProfile

K'ichean extraction profile: wi marks oblique extraction via copy spellout at the foot of the Ā-chain.

Equations

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

theorem Fragments.Mayan.Kiche.kichean_marks_oblique : kicheanExtractionProfile.marks Interfaces.ExtractionTarget.oblique = true