Documentation

Linglib.Phenomena.FillerGap.Studies.ElkinsTorrenceBrown2026

Oblique Extraction in Mayan #

@cite{elkins-torrence-brown-2026} @cite{mendes-ranero-2021} @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 #

Parametric Differences #

PropertyMam =(y)a'K'ichean wi
LocusOn probe (Voice⁰)At extraction site
MechanismAgree reflexCopy spellout
Reason obliques ('why')=(y)a' ✓wi ✗
FPG (matrix wi ↔ embedded comp)Does not holdHolds
Conditioned by clause sizeYes (Voice project.)No
Multiple spellout in LDYes (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).
source
theorem Phenomena.FillerGap.Studies.ElkinsTorrenceBrown2026.both_mark_oblique :
Fragments.Mayan.Mam.mamExtractionProfile.strategy = Interfaces.ExtractionMarkingStrategy.dedicatedMorpheme ∧ Fragments.Mayan.Kiche.kicheanExtractionProfile.strategy = Interfaces.ExtractionMarkingStrategy.dedicatedMorpheme

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

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

Both exempt temporal obliques from extraction marking.

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

Neither marks subject extraction (Agent Focus instead).

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

Neither marks object extraction.

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

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

source
theorem Phenomena.FillerGap.Studies.ElkinsTorrenceBrown2026.clause_size_sensitivity :
Fragments.Mayan.Mam.MamClauseType.fullCP.projectsVoice = true ∧ Fragments.Mayan.Mam.MamClauseType.aspectless.projectsVoice = true ∧ Fragments.Mayan.Mam.MamClauseType.infinitival.projectsVoice = false

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

source
theorem Phenomena.FillerGap.Studies.ElkinsTorrenceBrown2026.kichean_fpg_holds :
(Fragments.Mayan.Kiche.ldData.all fun (d : Fragments.Mayan.Kiche.KicheLongDistanceDatum) => d.embeddedType.hasComp == d.wiOnMatrix) = true

The FPG holds for K'ichean: matrix wi tracks overt complementizer.

source
inductive Phenomena.FillerGap.Studies.ElkinsTorrenceBrown2026.ExtractionMorphologyMechanism :
Type

Genuinely different mechanisms producing superficially similar patterns.

Instances For
    source
    instance Phenomena.FillerGap.Studies.ElkinsTorrenceBrown2026.instDecidableEqExtractionMorphologyMechanism :
    DecidableEq ExtractionMorphologyMechanism
    Equations
    source
    def Phenomena.FillerGap.Studies.ElkinsTorrenceBrown2026.instBEqExtractionMorphologyMechanism.beq :
    ExtractionMorphologyMechanism → ExtractionMorphologyMechanism → Bool
    Equations
    Instances For
      source
      instance Phenomena.FillerGap.Studies.ElkinsTorrenceBrown2026.instBEqExtractionMorphologyMechanism :
      BEq ExtractionMorphologyMechanism
      Equations
      source
      def Phenomena.FillerGap.Studies.ElkinsTorrenceBrown2026.instReprExtractionMorphologyMechanism.repr :
      ExtractionMorphologyMechanism → ℕ → Std.Format
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        instance Phenomena.FillerGap.Studies.ElkinsTorrenceBrown2026.instReprExtractionMorphologyMechanism :
        Repr ExtractionMorphologyMechanism
        Equations
        • One or more equations did not get rendered due to their size.
        source
        def Phenomena.FillerGap.Studies.ElkinsTorrenceBrown2026.mamMechanism :
        ExtractionMorphologyMechanism
        Equations
        Instances For
          source
          def Phenomena.FillerGap.Studies.ElkinsTorrenceBrown2026.kicheanMechanism :
          ExtractionMorphologyMechanism
          Equations
          Instances For
            source
            theorem Phenomena.FillerGap.Studies.ElkinsTorrenceBrown2026.different_mechanisms :
            mamMechanism ≠ kicheanMechanism
            source
            theorem Phenomena.FillerGap.Studies.ElkinsTorrenceBrown2026.spellout_oblique_voice :
            Minimalism.spellout Fragments.Mayan.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'.

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

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

            source
            theorem Phenomena.FillerGap.Studies.ElkinsTorrenceBrown2026.spellout_oblique_wrong_context :
            Minimalism.spellout Fragments.Mayan.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).

            source
            def Phenomena.FillerGap.Studies.ElkinsTorrenceBrown2026.predictEqYa (spine : Minimalism.ClauseSpine) (obliqueExtracted : Bool) (isTemporal : Bool := false) :
            Fragments.Mayan.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.
            Instances For
              source
              theorem Phenomena.FillerGap.Studies.ElkinsTorrenceBrown2026.bridge_trans_obl :
              Fragments.Mayan.Mam.mamTransitiveSpine.projects Minimalism.Cat.Voice = true ∧ predictEqYa Fragments.Mayan.Mam.mamTransitiveSpine true = Fragments.Mayan.Mam.MamExtractionJudgment.licensed ∧ Fragments.Mayan.Mam.transOblExtraction.judgment = Fragments.Mayan.Mam.MamExtractionJudgment.licensed

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

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

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

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

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

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

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

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

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

              source
              def Phenomena.FillerGap.Studies.ElkinsTorrenceBrown2026.spineOf :
              Fragments.Mayan.Mam.MamClauseType → Minimalism.ClauseSpine

              Map MamClauseType to the corresponding ClauseSpine.

              Equations
              Instances For
                source
                theorem Phenomena.FillerGap.Studies.ElkinsTorrenceBrown2026.bridge_ld_fullCP :
                (spineOf Fragments.Mayan.Mam.ldFullCP.embeddedClauseType).projects Minimalism.Cat.Voice = true ∧ Fragments.Mayan.Mam.ldFullCP.matrixJudgment = Fragments.Mayan.Mam.MamExtractionJudgment.licensed ∧ Fragments.Mayan.Mam.ldFullCP.embeddedJudgment = Fragments.Mayan.Mam.MamExtractionJudgment.licensed

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

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

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

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

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

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

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

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

                All monoclausal predictions match.

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

                All LD embedded predictions match.

                source
                theorem Phenomena.FillerGap.Studies.ElkinsTorrenceBrown2026.eqya_not_resumptive :
                Fragments.Mayan.Mam.eqyaIslandSensitive = true

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

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

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

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

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

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

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

                source
                theorem Phenomena.FillerGap.Studies.ElkinsTorrenceBrown2026.dir_probe_matches_voice :
                Fragments.Mayan.Mam.dirCis.features = Fragments.Mayan.Mam.mamVoice.features

                Dir⁰ also carries [uOblique].

                source
                theorem Phenomena.FillerGap.Studies.ElkinsTorrenceBrown2026.dir_spellout_eqya :
                Minimalism.spellout Fragments.Mayan.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'.

                source
                theorem Phenomena.FillerGap.Studies.ElkinsTorrenceBrown2026.derivation_tree_size :
                Phenomena.FillerGap.Studies.ElkinsTorrenceBrown2026.cp✝.nodeCount = 6
                source
                theorem Phenomena.FillerGap.Studies.ElkinsTorrenceBrown2026.voice_has_uOblique :
                Minimalism.hasUnvaluedFeature Fragments.Mayan.Mam.mamVoice.features (Minimalism.FeatureVal.oblique false) = true
                source
                theorem Phenomena.FillerGap.Studies.ElkinsTorrenceBrown2026.voice_agree_values_oblique :
                Minimalism.applyAgree Fragments.Mayan.Mam.mamVoice.features Phenomena.FillerGap.Studies.ElkinsTorrenceBrown2026.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].

                source
                theorem Phenomena.FillerGap.Studies.ElkinsTorrenceBrown2026.voice_spellout_eqya :
                Minimalism.spellout Fragments.Mayan.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'".

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

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