Oblique Extraction in Mayan

@cite{elkins-imanishi-coon-2026} @cite{henderson-2008} @cite{imanishi-2020}

Part I: Cross-Linguistic Comparison

Cross-linguistic comparison of extraction morphology in two Mayan language groups: SJO Mam (=(y)a') and K'ichean (wi). Both mark oblique extraction with a dedicated morpheme, but the underlying mechanisms and distributional properties differ.

Shared Properties

• Both mark oblique extraction (spatial, instrumental)
• Both exempt temporal obliques ('when')
• Neither marks subject extraction (Agent Focus instead)
• Neither marks object extraction

Parametric Differences

Property	Mam =(y)a'	K'ichean wi
Locus	On probe (Voice⁰)	At extraction site
Mechanism	Agree reflex	Copy spellout
Reason obliques ('why')	=(y)a' ✓	wi ✗
Fronting Particle Generalization	Does not hold	Holds
Conditioned by clause size	Yes (Voice project.)	No
Multiple spellout in LD	Yes (per Voice/Dir)	Unclear

Part II: Minimalist Analysis

Connects three Minimalist abstractions — ClauseSpine, Agree/feature-valuation, and Spellout — to the empirical data on =(y)a' distribution in SJO Mam.

1. Voice⁰ (and Dir⁰) in Mam carry [uOblique] (an unvalued probe feature).
2. When an oblique DP undergoes successive-cyclic Ā-movement through Spec,VoiceP, Agree values [uOblique] as [+oblique] on Voice⁰.
3. At Spellout (PF), [+oblique] on Voice⁰ is realized as =(y)a'.
4. In infinitival complements, Voice is not projected (VP-sized), so there is no [uOblique] probe — =(y)a' cannot appear.
5. In long-distance extraction, each Voice⁰/Dir⁰ along the movement path independently Agrees, yielding multiple =(y)a' (one per Voice/Dir).

theorem Phenomena.FillerGap.Studies.ElkinsImanishiCoon2026.both_mark_oblique : Fragments.Mam.mamExtractionProfile.strategy = Interfaces.ExtractionMarkingStrategy.dedicatedMorpheme ∧ Fragments.Kiche.kicheanExtractionProfile.strategy = Interfaces.ExtractionMarkingStrategy.dedicatedMorpheme

Both Mam and K'ichean use dedicated morphemes for oblique extraction.

theorem Phenomena.FillerGap.Studies.ElkinsImanishiCoon2026.both_exempt_temporal : (Fragments.Mam.temporalOblExtraction.isTemporal = true ∧ Fragments.Mam.temporalOblExtraction.judgment = Fragments.Mam.MamExtractionJudgment.blocked) ∧ Fragments.Kiche.temporalOblExtraction.wiLicensed = false

Both exempt temporal obliques from extraction marking.

theorem Phenomena.FillerGap.Studies.ElkinsImanishiCoon2026.neither_marks_subject : Fragments.Mam.transSubjExtraction.judgment = Fragments.Mam.MamExtractionJudgment.blocked ∧ Fragments.Kiche.subjectExtraction.wiLicensed = false

Neither marks subject extraction (Agent Focus instead).

theorem Phenomena.FillerGap.Studies.ElkinsImanishiCoon2026.neither_marks_object : Fragments.Mam.transObjExtraction.judgment = Fragments.Mam.MamExtractionJudgment.blocked ∧ Fragments.Kiche.objectExtraction.wiLicensed = false

Neither marks object extraction.

theorem Phenomena.FillerGap.Studies.ElkinsImanishiCoon2026.reason_oblique_contrast : Fragments.Mam.transOblExtraction.judgment = Fragments.Mam.MamExtractionJudgment.licensed ∧ Fragments.Kiche.reasonOblExtraction.wiLicensed = false

KEY CONTRAST — Reason obliques ('why'): Mam =(y)a' IS licensed with reason extraction; K'ichean wi is NOT.

theorem Phenomena.FillerGap.Studies.ElkinsImanishiCoon2026.clause_size_sensitivity : Fragments.Mam.MamClauseType.fullCP.projectsVoice = true ∧ Fragments.Mam.MamClauseType.aspectless.projectsVoice = true ∧ Fragments.Mam.MamClauseType.infinitival.projectsVoice = false ∧ Fragments.Kiche.frontingParticleGeneralization = true

Mam =(y)a' is conditioned by clause size (Voice must project); K'ichean wi is not.

inductive Phenomena.FillerGap.Studies.ElkinsImanishiCoon2026.ExtractionMorphologyMechanism : Type

Genuinely different mechanisms producing superficially similar patterns.

• agreeReflex : ExtractionMorphologyMechanism
• copySpellout : ExtractionMorphologyMechanism

instance Phenomena.FillerGap.Studies.ElkinsImanishiCoon2026.instDecidableEqExtractionMorphologyMechanism : DecidableEq ExtractionMorphologyMechanism

Equations

• Phenomena.FillerGap.Studies.ElkinsImanishiCoon2026.instDecidableEqExtractionMorphologyMechanism x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Phenomena.FillerGap.Studies.ElkinsImanishiCoon2026.instBEqExtractionMorphologyMechanism : BEq ExtractionMorphologyMechanism

Equations

• Phenomena.FillerGap.Studies.ElkinsImanishiCoon2026.instBEqExtractionMorphologyMechanism = { beq := Phenomena.FillerGap.Studies.ElkinsImanishiCoon2026.instBEqExtractionMorphologyMechanism.beq }

def Phenomena.FillerGap.Studies.ElkinsImanishiCoon2026.instBEqExtractionMorphologyMechanism.beq : ExtractionMorphologyMechanism → ExtractionMorphologyMechanism → Bool

Equations

• Phenomena.FillerGap.Studies.ElkinsImanishiCoon2026.instBEqExtractionMorphologyMechanism.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.FillerGap.Studies.ElkinsImanishiCoon2026.instReprExtractionMorphologyMechanism : Repr ExtractionMorphologyMechanism

Equations

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

def Phenomena.FillerGap.Studies.ElkinsImanishiCoon2026.instReprExtractionMorphologyMechanism.repr : ExtractionMorphologyMechanism → ℕ → Std.Format

Equations

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

def Phenomena.FillerGap.Studies.ElkinsImanishiCoon2026.mamMechanism : ExtractionMorphologyMechanism

Equations

• Phenomena.FillerGap.Studies.ElkinsImanishiCoon2026.mamMechanism = Phenomena.FillerGap.Studies.ElkinsImanishiCoon2026.ExtractionMorphologyMechanism.agreeReflex

def Phenomena.FillerGap.Studies.ElkinsImanishiCoon2026.kicheanMechanism : ExtractionMorphologyMechanism

Equations

• Phenomena.FillerGap.Studies.ElkinsImanishiCoon2026.kicheanMechanism = Phenomena.FillerGap.Studies.ElkinsImanishiCoon2026.ExtractionMorphologyMechanism.copySpellout

theorem Phenomena.FillerGap.Studies.ElkinsImanishiCoon2026.different_mechanisms : mamMechanism ≠ kicheanMechanism

theorem Phenomena.FillerGap.Studies.ElkinsImanishiCoon2026.spellout_oblique_voice : Minimalism.spellout Fragments.Mam.mamVoiceVocab [Minimalism.GramFeature.valued (Minimalism.FeatureVal.oblique true)] (some Minimalism.Cat.Voice) = some "=(y)a'"

Valued [+oblique] on Voice spells out as =(y)a'.

theorem Phenomena.FillerGap.Studies.ElkinsImanishiCoon2026.spellout_no_oblique : Minimalism.spellout Fragments.Mam.mamVoiceVocab [Minimalism.GramFeature.valued (Minimalism.FeatureVal.oblique false)] (some Minimalism.Cat.Voice) = none

Without [+oblique], Voice has no exponent from this vocabulary.

theorem Phenomena.FillerGap.Studies.ElkinsImanishiCoon2026.spellout_oblique_wrong_context : Minimalism.spellout Fragments.Mam.mamVoiceVocab [Minimalism.GramFeature.valued (Minimalism.FeatureVal.oblique true)] (some Minimalism.Cat.T) = none

[+oblique] on a non-Voice head does not yield =(y)a' (context restriction blocks insertion).

def Phenomena.FillerGap.Studies.ElkinsImanishiCoon2026.predictEqYa (spine : Minimalism.ClauseSpine) (obliqueExtracted : Bool) (isTemporal : Bool := false) : Fragments.Mam.MamExtractionJudgment

Predict whether =(y)a' is licensed from a clause spine and extraction type.

Equations

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

theorem Phenomena.FillerGap.Studies.ElkinsImanishiCoon2026.bridge_trans_obl : Fragments.Mam.mamTransitiveSpine.projects Minimalism.Cat.Voice = true ∧ predictEqYa Fragments.Mam.mamTransitiveSpine true = Fragments.Mam.MamExtractionJudgment.licensed ∧ Fragments.Mam.transOblExtraction.judgment = Fragments.Mam.MamExtractionJudgment.licensed

Transitive clause + oblique extraction → =(y)a' licensed.

theorem Phenomena.FillerGap.Studies.ElkinsImanishiCoon2026.bridge_trans_subj : predictEqYa Fragments.Mam.mamTransitiveSpine false = Fragments.Mam.MamExtractionJudgment.blocked ∧ Fragments.Mam.transSubjExtraction.judgment = Fragments.Mam.MamExtractionJudgment.blocked

Transitive + subject extraction → no =(y)a'.

theorem Phenomena.FillerGap.Studies.ElkinsImanishiCoon2026.bridge_trans_obj : predictEqYa Fragments.Mam.mamTransitiveSpine false = Fragments.Mam.MamExtractionJudgment.blocked ∧ Fragments.Mam.transObjExtraction.judgment = Fragments.Mam.MamExtractionJudgment.blocked

Transitive + object extraction → no =(y)a'.

theorem Phenomena.FillerGap.Studies.ElkinsImanishiCoon2026.bridge_passive_obl : Fragments.Mam.mamTransitiveSpine.projects Minimalism.Cat.Voice = true ∧ predictEqYa Fragments.Mam.mamTransitiveSpine true = Fragments.Mam.MamExtractionJudgment.licensed ∧ Fragments.Mam.passiveOblExtraction.judgment = Fragments.Mam.MamExtractionJudgment.licensed

Passive + oblique → =(y)a' licensed.

theorem Phenomena.FillerGap.Studies.ElkinsImanishiCoon2026.bridge_temporal_obl : predictEqYa Fragments.Mam.mamTransitiveSpine true true = Fragments.Mam.MamExtractionJudgment.blocked ∧ Fragments.Mam.temporalOblExtraction.judgment = Fragments.Mam.MamExtractionJudgment.blocked

Temporal oblique + full clause → =(y)a' BLOCKED.

def Phenomena.FillerGap.Studies.ElkinsImanishiCoon2026.spineOf : Fragments.Mam.MamClauseType → Minimalism.ClauseSpine

Map MamClauseType to the corresponding ClauseSpine.

Equations

• Phenomena.FillerGap.Studies.ElkinsImanishiCoon2026.spineOf Fragments.Mam.MamClauseType.fullCP = Fragments.Mam.mamTransitiveSpine
• Phenomena.FillerGap.Studies.ElkinsImanishiCoon2026.spineOf Fragments.Mam.MamClauseType.aspectless = Fragments.Mam.mamAspectlessSpine
• Phenomena.FillerGap.Studies.ElkinsImanishiCoon2026.spineOf Fragments.Mam.MamClauseType.infinitival = Fragments.Mam.mamInfinitivalSpine

theorem Phenomena.FillerGap.Studies.ElkinsImanishiCoon2026.bridge_ld_fullCP : (spineOf Fragments.Mam.ldFullCP.embeddedClauseType).projects Minimalism.Cat.Voice = true ∧ Fragments.Mam.ldFullCP.matrixJudgment = Fragments.Mam.MamExtractionJudgment.licensed ∧ Fragments.Mam.ldFullCP.embeddedJudgment = Fragments.Mam.MamExtractionJudgment.licensed

LD from full CP → =(y)a' licensed on both predicates.

theorem Phenomena.FillerGap.Studies.ElkinsImanishiCoon2026.bridge_ld_aspectless : (spineOf Fragments.Mam.ldAspectless.embeddedClauseType).projects Minimalism.Cat.Voice = true ∧ Fragments.Mam.ldAspectless.matrixJudgment = Fragments.Mam.MamExtractionJudgment.licensed ∧ Fragments.Mam.ldAspectless.embeddedJudgment = Fragments.Mam.MamExtractionJudgment.licensed

LD from aspectless → =(y)a' licensed on both.

theorem Phenomena.FillerGap.Studies.ElkinsImanishiCoon2026.bridge_ld_infinitival : (spineOf Fragments.Mam.ldInfinitival.embeddedClauseType).projects Minimalism.Cat.Voice = false ∧ Fragments.Mam.ldInfinitival.matrixJudgment = Fragments.Mam.MamExtractionJudgment.licensed ∧ Fragments.Mam.ldInfinitival.embeddedJudgment = Fragments.Mam.MamExtractionJudgment.blocked

LD from infinitival → =(y)a' on matrix only.

theorem Phenomena.FillerGap.Studies.ElkinsImanishiCoon2026.bridge_ld_eq : Fragments.Mam.ldEmbeddedQuestion.matrixJudgment = Fragments.Mam.MamExtractionJudgment.blocked ∧ Fragments.Mam.ldEmbeddedQuestion.embeddedJudgment = Fragments.Mam.MamExtractionJudgment.licensed

EQ → =(y)a' on embedded only.

theorem Phenomena.FillerGap.Studies.ElkinsImanishiCoon2026.all_mono_predictions_match : (Fragments.Mam.monoData.all fun (d : Fragments.Mam.MamExtractionDatum) => predictEqYa (spineOf d.clauseType) d.obliqueExtracted d.isTemporal == d.judgment) = true

All monoclausal predictions match.

theorem Phenomena.FillerGap.Studies.ElkinsImanishiCoon2026.all_ld_embedded_predictions_match : (Fragments.Mam.ldData.all fun (d : Fragments.Mam.MamLongDistanceDatum) => d.embeddedClauseType.projectsVoice == (d.embeddedJudgment == Fragments.Mam.MamExtractionJudgment.licensed)) = true

All LD embedded predictions match.

theorem Phenomena.FillerGap.Studies.ElkinsImanishiCoon2026.eqya_not_resumptive : Fragments.Mam.eqyaIslandSensitive = true

Against resumptive-pronoun analysis: =(y)a' is island-sensitive.

theorem Phenomena.FillerGap.Studies.ElkinsImanishiCoon2026.eqya_not_agent_focus : Fragments.Mam.mamPassiveVoice.features = Fragments.Mam.mamVoice.features ∧ Fragments.Mam.mamPassiveVoice.flavor ≠ Fragments.Mam.mamVoice.flavor ∧ Fragments.Mam.passiveOblExtraction.judgment = Fragments.Mam.MamExtractionJudgment.licensed ∧ Fragments.Mam.transSubjExtraction.judgment = Fragments.Mam.MamExtractionJudgment.blocked ∧ Fragments.Mam.transOblExtraction.judgment = Fragments.Mam.MamExtractionJudgment.licensed

Against Agent Focus analysis: =(y)a' co-occurs with passive voice.

theorem Phenomena.FillerGap.Studies.ElkinsImanishiCoon2026.eqya_not_copy_spellout : (spineOf Fragments.Mam.MamClauseType.aspectless).projects Minimalism.Cat.Voice = true ∧ (spineOf Fragments.Mam.MamClauseType.infinitival).projects Minimalism.Cat.Voice = false ∧ Fragments.Mam.ldAspectless.embeddedJudgment = Fragments.Mam.MamExtractionJudgment.licensed ∧ Fragments.Mam.ldInfinitival.embeddedJudgment = Fragments.Mam.MamExtractionJudgment.blocked

Against copy spellout: =(y)a' disappears when Voice is absent.

theorem Phenomena.FillerGap.Studies.ElkinsImanishiCoon2026.clauseSpine_finer_than_complementSize : Fragments.Mam.mamAspectlessSpine.projects Minimalism.Cat.Voice = true ∧ Fragments.Mam.mamInfinitivalSpine.projects Minimalism.Cat.Voice = false

ClauseSpine is finer than ComplementSize: it can distinguish infinitival (VP) from aspectless (VoiceP).

theorem Phenomena.FillerGap.Studies.ElkinsImanishiCoon2026.dir_probe_matches_voice : Fragments.Mam.dirCis.features = Fragments.Mam.mamVoice.features

Dir⁰ also carries [uOblique].

theorem Phenomena.FillerGap.Studies.ElkinsImanishiCoon2026.dir_spellout_eqya : Minimalism.spellout Fragments.Mam.mamVoiceVocab [Minimalism.GramFeature.valued (Minimalism.FeatureVal.oblique true)] (some Minimalism.Cat.Voice) = some "=(y)a'"

Dir⁰ with valued [+oblique] also spells out as =(y)a'.

theorem Phenomena.FillerGap.Studies.ElkinsImanishiCoon2026.derivation_tree_size : Phenomena.FillerGap.Studies.ElkinsImanishiCoon2026.cp✝.nodeCount = 6

theorem Phenomena.FillerGap.Studies.ElkinsImanishiCoon2026.voice_has_uOblique : Minimalism.hasUnvaluedFeature Fragments.Mam.mamVoice.features (Minimalism.FeatureVal.oblique false) = true

theorem Phenomena.FillerGap.Studies.ElkinsImanishiCoon2026.voice_agree_values_oblique : Minimalism.applyAgree Fragments.Mam.mamVoice.features Phenomena.FillerGap.Studies.ElkinsImanishiCoon2026.oblique_goal_features✝ (Minimalism.FeatureVal.oblique false) = some [Minimalism.GramFeature.valued (Minimalism.FeatureVal.oblique true)]

Agree at Voice: [uOblique] valued by oblique DP's [+oblique].

theorem Phenomena.FillerGap.Studies.ElkinsImanishiCoon2026.voice_spellout_eqya : Minimalism.spellout Fragments.Mam.mamVoiceVocab [Minimalism.GramFeature.valued (Minimalism.FeatureVal.oblique true)] (some Minimalism.Cat.Voice) = some "=(y)a'"

Spellout: valued [+oblique] on Voice maps to "=(y)a'".

theorem Phenomena.FillerGap.Studies.ElkinsImanishiCoon2026.full_derivation_pipeline : ((Minimalism.applyAgree Fragments.Mam.mamVoice.features Phenomena.FillerGap.Studies.ElkinsImanishiCoon2026.oblique_goal_features✝ (Minimalism.FeatureVal.oblique false)).bind fun (fb : Minimalism.FeatureBundle) => Minimalism.spellout Fragments.Mam.mamVoiceVocab fb (some Minimalism.Cat.Voice)) = some "=(y)a'"

Full derivation pipeline: Agree then Spellout → "=(y)a'".