Oblique Extraction in Mayan

[ETB26] [MR21] [Ima20]

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 ✗
FPG (matrix wi ↔ embedded comp)	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 ElkinsTorrenceBrown2026.both_mark_oblique : Mam.mamExtractionStrategy = Extraction.ExtractionMarkingStrategy.dedicatedMorpheme ∧ Kiche.kicheanExtractionStrategy = Extraction.ExtractionMarkingStrategy.dedicatedMorpheme

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

theorem ElkinsTorrenceBrown2026.both_exempt_temporal : (Mam.temporalOblExtraction.isTemporal = true ∧ Mam.temporalOblExtraction.judgment = Mam.MamExtractionJudgment.blocked) ∧ Kiche.temporalOblExtraction.wiLicensed = false

Both exempt temporal obliques from extraction marking.

theorem ElkinsTorrenceBrown2026.neither_marks_subject : Mam.transSubjExtraction.judgment = Mam.MamExtractionJudgment.blocked ∧ Kiche.subjectExtraction.wiLicensed = false

Neither marks subject extraction (Agent Focus instead).

theorem ElkinsTorrenceBrown2026.neither_marks_object : Mam.transObjExtraction.judgment = Mam.MamExtractionJudgment.blocked ∧ Kiche.objectExtraction.wiLicensed = false

Neither marks object extraction.

theorem ElkinsTorrenceBrown2026.reason_oblique_contrast : Mam.transOblExtraction.judgment = Mam.MamExtractionJudgment.licensed ∧ Kiche.reasonOblExtraction.wiLicensed = false

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

theorem ElkinsTorrenceBrown2026.clause_size_sensitivity : Mam.MamClauseType.fullCP.projectsVoice = true ∧ Mam.MamClauseType.aspectless.projectsVoice = true ∧ 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).

theorem ElkinsTorrenceBrown2026.kichean_fpg_holds : (Kiche.ldData.all fun (d : Kiche.KicheLongDistanceDatum) => d.embeddedType.hasComp == d.wiOnMatrix) = true

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

inductive ElkinsTorrenceBrown2026.ExtractionMorphologyMechanism : Type

Genuinely different mechanisms producing superficially similar patterns.

• agreeReflex : ExtractionMorphologyMechanism
• copySpellout : ExtractionMorphologyMechanism

@[implicit_reducible]

instance ElkinsTorrenceBrown2026.instDecidableEqExtractionMorphologyMechanism : DecidableEq ExtractionMorphologyMechanism

Equations

• ElkinsTorrenceBrown2026.instDecidableEqExtractionMorphologyMechanism x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance ElkinsTorrenceBrown2026.instReprExtractionMorphologyMechanism : Repr ExtractionMorphologyMechanism

Equations

• ElkinsTorrenceBrown2026.instReprExtractionMorphologyMechanism = { reprPrec := ElkinsTorrenceBrown2026.instReprExtractionMorphologyMechanism.repr }

def ElkinsTorrenceBrown2026.instReprExtractionMorphologyMechanism.repr : ExtractionMorphologyMechanism → ℕ → Std.Format

Equations

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

def ElkinsTorrenceBrown2026.mamMechanism : ExtractionMorphologyMechanism

Equations

• ElkinsTorrenceBrown2026.mamMechanism = ElkinsTorrenceBrown2026.ExtractionMorphologyMechanism.agreeReflex

def ElkinsTorrenceBrown2026.kicheanMechanism : ExtractionMorphologyMechanism

Equations

• ElkinsTorrenceBrown2026.kicheanMechanism = ElkinsTorrenceBrown2026.ExtractionMorphologyMechanism.copySpellout

theorem ElkinsTorrenceBrown2026.different_mechanisms : mamMechanism ≠ kicheanMechanism

Mam Voice substrate (Minimalist)

This subsection houses the Minimalist VoiceHead, ClauseSpine, and MamDirHead definitions for Mam, formerly in Linglib/Fragments/Mayan/Mam/VoiceSystem.lean. Per CLAUDE.md "Per-language paper-specific apparatus lives in Studies, not Fragments," these belong with the paper that anchors them ([ETB26] for the =(y)a' analysis; [Sco23] for the antipassive). The Fragment file retains only the per-language Mam.VoiceSystem.voices/symmetry defs.

Studies/Scott2023.lean consumes mamVoice and eqYaVocab from this file via cross-Studies import.

def ElkinsTorrenceBrown2026.mamVoice : Minimalist.VoiceHead

Mam agentive Voice head with [uOblique] probe.

In Mam, Voice⁰ probes for an oblique feature on a passing Ā-moved constituent. When an oblique DP moves through Spec,VoiceP, Agree values [uOblique] as [+oblique], which is then spelled out as =(y)a' at PF.

Equations

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

def ElkinsTorrenceBrown2026.mamTransitiveSpine : Minimalist.ClauseSpine

Mam transitive clause spine: full CP with Voice.

Equations

• ElkinsTorrenceBrown2026.mamTransitiveSpine = Minimalist.ClauseSpine.cP

def ElkinsTorrenceBrown2026.mamAspectlessSpine : Minimalist.ClauseSpine

Mam aspectless complement spine: VoiceP-sized. Still has Voice → =(y)a' possible.

Equations

• ElkinsTorrenceBrown2026.mamAspectlessSpine = Minimalist.ClauseSpine.voiceP

def ElkinsTorrenceBrown2026.mamInfinitivalSpine : Minimalist.ClauseSpine

Mam infinitival complement spine: VP-sized. No Voice → =(y)a' impossible.

Equations

• ElkinsTorrenceBrown2026.mamInfinitivalSpine = Minimalist.ClauseSpine.bareVP

structure ElkinsTorrenceBrown2026.MamDirHead : Type

Mam directional auxiliary head (Dir⁰).

Dir is NOT a universal category — it is specific to Mayan languages. Modeled as a language-specific type rather than added to Cat. In Elkins et al.'s analysis, Dir⁰ occupies V1 position in the verbal template (Voice > V1(Dir) > Appl > V2(root)). Like Voice⁰, Dir⁰ bears [uOblique] and can host =(y)a'.

• cislocative : Bool

  Cislocative (toward speaker) vs translocative (away).

• hasUOblique : Bool

  Whether this Dir head carries [uOblique].

def ElkinsTorrenceBrown2026.instDecidableEqMamDirHead.decEq (x✝ x✝¹ : MamDirHead) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance ElkinsTorrenceBrown2026.instDecidableEqMamDirHead : DecidableEq MamDirHead

Equations

• ElkinsTorrenceBrown2026.instDecidableEqMamDirHead = ElkinsTorrenceBrown2026.instDecidableEqMamDirHead.decEq

def ElkinsTorrenceBrown2026.instReprMamDirHead.repr : MamDirHead → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance ElkinsTorrenceBrown2026.instReprMamDirHead : Repr MamDirHead

Equations

• ElkinsTorrenceBrown2026.instReprMamDirHead = { reprPrec := ElkinsTorrenceBrown2026.instReprMamDirHead.repr }

def ElkinsTorrenceBrown2026.MamDirHead.features (d : MamDirHead) : Minimalist.FeatureBundle

Dir⁰'s probe features when it carries [uOblique].

Equations

• d.features = if d.hasUOblique = true then Minimalist.FeatureBundle.ofGramFeatures [Minimalist.GramFeature.unvalued (Minimalist.FeatureVal.oblique false)] else ⊥

def ElkinsTorrenceBrown2026.dirCis : MamDirHead

Cislocative directional with [uOblique].

Equations

• ElkinsTorrenceBrown2026.dirCis = { cislocative := true, hasUOblique := true }

def ElkinsTorrenceBrown2026.dirTrans : MamDirHead

Translocative directional with [uOblique].

Equations

• ElkinsTorrenceBrown2026.dirTrans = { cislocative := false, hasUOblique := true }

def ElkinsTorrenceBrown2026.eqYaVocab : Minimalist.VocabEntry

Vocabulary entry for =(y)a': maps [+oblique] on Voice⁰ to "=(y)a'".

Equations

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

def ElkinsTorrenceBrown2026.mamVoiceVocab : Minimalist.Vocabulary

The Mam Voice vocabulary: just the =(y)a' entry.

Equations

• ElkinsTorrenceBrown2026.mamVoiceVocab = [ElkinsTorrenceBrown2026.eqYaVocab]

def ElkinsTorrenceBrown2026.mamPassiveVoice : Minimalist.VoiceHead

Mam passive Voice head: carries [uOblique] just like agentive Voice. [ETB26] §7.2: =(y)a' co-occurs with passive -njtz.

Equations

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

def ElkinsTorrenceBrown2026.mamAntipassiveVoice : Minimalist.VoiceHead

Mam antipassive Voice head ([Sco23] §2.5.4.1). Subject gets ABS not ERG; not a phase head.

Equations

• ElkinsTorrenceBrown2026.mamAntipassiveVoice = { flavor := Minimalist.VoiceFlavor.antipassive, hasD := true }

theorem ElkinsTorrenceBrown2026.mamVoice_has_uOblique : Minimalist.hasUnvaluedFeature mamVoice.features (Minimalist.FeatureVal.oblique false) = true

Mam Voice head carries [uOblique].

theorem ElkinsTorrenceBrown2026.mamVoice_is_phase : mamVoice.IsPhasal

Mam Voice is a phase head.

theorem ElkinsTorrenceBrown2026.mamVoice_assigns_theta : mamVoice.AssignsTheta

Mam Voice assigns a θ-role (agentive).

theorem ElkinsTorrenceBrown2026.mamTransitive_has_voice : mamTransitiveSpine.projects Minimalist.Cat.Voice = true

Mam transitive spine projects Voice.

theorem ElkinsTorrenceBrown2026.mamAspectless_has_voice : mamAspectlessSpine.projects Minimalist.Cat.Voice = true

Mam aspectless spine projects Voice.

theorem ElkinsTorrenceBrown2026.mamInfinitival_lacks_voice : mamInfinitivalSpine.projects Minimalist.Cat.Voice = false

Mam infinitival spine does NOT project Voice.

theorem ElkinsTorrenceBrown2026.dirCis_has_uOblique : dirCis.hasUOblique = true

Cislocative Dir carries [uOblique].

theorem ElkinsTorrenceBrown2026.dirTrans_has_uOblique : dirTrans.hasUOblique = true

Translocative Dir carries [uOblique].

theorem ElkinsTorrenceBrown2026.dir_features_match_voice : dirCis.features = mamVoice.features

Dir's probe features match Voice's.

theorem ElkinsTorrenceBrown2026.passive_voice_same_features : mamPassiveVoice.features = mamVoice.features ∧ mamPassiveVoice.flavor ≠ mamVoice.flavor

Passive and agentive Voice differ in flavor but share the same oblique probe features.

theorem ElkinsTorrenceBrown2026.mamAntipassive_assigns_theta : mamAntipassiveVoice.AssignsTheta

Antipassive Voice assigns a θ-role (the agent is present).

theorem ElkinsTorrenceBrown2026.mamAntipassive_not_phase : ¬mamAntipassiveVoice.IsPhasal

Antipassive Voice is NOT a phase head.

theorem ElkinsTorrenceBrown2026.antipassive_vs_agentive : (mamAntipassiveVoice.AssignsTheta ↔ mamVoice.AssignsTheta) ∧ (mamAntipassiveVoice.IsPhasal ↔ ¬mamVoice.IsPhasal)

Antipassive and agentive Voice differ in phase-head status but both assign θ-roles.

theorem ElkinsTorrenceBrown2026.spellout_oblique_voice : Minimalist.spellout mamVoiceVocab (Minimalist.FeatureBundle.ofGramFeatures [Minimalist.GramFeature.valued (Minimalist.FeatureVal.oblique true)]) (some Minimalist.Cat.Voice) = some "=(y)a'"

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

theorem ElkinsTorrenceBrown2026.spellout_no_oblique : Minimalist.spellout mamVoiceVocab (Minimalist.FeatureBundle.ofGramFeatures [Minimalist.GramFeature.valued (Minimalist.FeatureVal.oblique false)]) (some Minimalist.Cat.Voice) = none

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

theorem ElkinsTorrenceBrown2026.spellout_oblique_wrong_context : Minimalist.spellout mamVoiceVocab (Minimalist.FeatureBundle.ofGramFeatures [Minimalist.GramFeature.valued (Minimalist.FeatureVal.oblique true)]) (some Minimalist.Cat.T) = none

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

def ElkinsTorrenceBrown2026.predictEqYa (spine : Minimalist.ClauseSpine) (obliqueExtracted : Bool) (isTemporal : Bool := false) : 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 ElkinsTorrenceBrown2026.bridge_trans_obl : mamTransitiveSpine.projects Minimalist.Cat.Voice = true ∧ predictEqYa mamTransitiveSpine true = Mam.MamExtractionJudgment.licensed ∧ Mam.transOblExtraction.judgment = Mam.MamExtractionJudgment.licensed

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

theorem ElkinsTorrenceBrown2026.bridge_trans_subj : predictEqYa mamTransitiveSpine false = Mam.MamExtractionJudgment.blocked ∧ Mam.transSubjExtraction.judgment = Mam.MamExtractionJudgment.blocked

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

theorem ElkinsTorrenceBrown2026.bridge_trans_obj : predictEqYa mamTransitiveSpine false = Mam.MamExtractionJudgment.blocked ∧ Mam.transObjExtraction.judgment = Mam.MamExtractionJudgment.blocked

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

theorem ElkinsTorrenceBrown2026.bridge_passive_obl : mamTransitiveSpine.projects Minimalist.Cat.Voice = true ∧ predictEqYa mamTransitiveSpine true = Mam.MamExtractionJudgment.licensed ∧ Mam.passiveOblExtraction.judgment = Mam.MamExtractionJudgment.licensed

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

theorem ElkinsTorrenceBrown2026.bridge_temporal_obl : predictEqYa mamTransitiveSpine true true = Mam.MamExtractionJudgment.blocked ∧ Mam.temporalOblExtraction.judgment = Mam.MamExtractionJudgment.blocked

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

def ElkinsTorrenceBrown2026.spineOf : Mam.MamClauseType → Minimalist.ClauseSpine

Map MamClauseType to the corresponding ClauseSpine.

Equations

• ElkinsTorrenceBrown2026.spineOf Mam.MamClauseType.fullCP = ElkinsTorrenceBrown2026.mamTransitiveSpine
• ElkinsTorrenceBrown2026.spineOf Mam.MamClauseType.aspectless = ElkinsTorrenceBrown2026.mamAspectlessSpine
• ElkinsTorrenceBrown2026.spineOf Mam.MamClauseType.infinitival = ElkinsTorrenceBrown2026.mamInfinitivalSpine

theorem ElkinsTorrenceBrown2026.bridge_ld_fullCP : (spineOf Mam.ldFullCP.embeddedClauseType).projects Minimalist.Cat.Voice = true ∧ Mam.ldFullCP.matrixJudgment = Mam.MamExtractionJudgment.licensed ∧ Mam.ldFullCP.embeddedJudgment = Mam.MamExtractionJudgment.licensed

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

theorem ElkinsTorrenceBrown2026.bridge_ld_aspectless : (spineOf Mam.ldAspectless.embeddedClauseType).projects Minimalist.Cat.Voice = true ∧ Mam.ldAspectless.matrixJudgment = Mam.MamExtractionJudgment.licensed ∧ Mam.ldAspectless.embeddedJudgment = Mam.MamExtractionJudgment.licensed

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

theorem ElkinsTorrenceBrown2026.bridge_ld_infinitival : (spineOf Mam.ldInfinitival.embeddedClauseType).projects Minimalist.Cat.Voice = false ∧ Mam.ldInfinitival.matrixJudgment = Mam.MamExtractionJudgment.licensed ∧ Mam.ldInfinitival.embeddedJudgment = Mam.MamExtractionJudgment.blocked

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

theorem ElkinsTorrenceBrown2026.bridge_ld_eq : Mam.ldEmbeddedQuestion.matrixJudgment = Mam.MamExtractionJudgment.blocked ∧ Mam.ldEmbeddedQuestion.embeddedJudgment = Mam.MamExtractionJudgment.licensed

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

theorem ElkinsTorrenceBrown2026.all_mono_predictions_match : (Mam.monoData.all fun (d : Mam.MamExtractionDatum) => predictEqYa (spineOf d.clauseType) d.obliqueExtracted d.isTemporal == d.judgment) = true

All monoclausal predictions match.

theorem ElkinsTorrenceBrown2026.all_ld_embedded_predictions_match : (Mam.ldData.all fun (d : Mam.MamLongDistanceDatum) => d.embeddedClauseType.projectsVoice == (d.embeddedJudgment == Mam.MamExtractionJudgment.licensed)) = true

All LD embedded predictions match.

theorem ElkinsTorrenceBrown2026.eqya_not_resumptive : Mam.eqyaIslandSensitive = true

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

theorem ElkinsTorrenceBrown2026.eqya_not_agent_focus : mamPassiveVoice.features = mamVoice.features ∧ mamPassiveVoice.flavor ≠ mamVoice.flavor ∧ Mam.passiveOblExtraction.judgment = Mam.MamExtractionJudgment.licensed ∧ Mam.transSubjExtraction.judgment = Mam.MamExtractionJudgment.blocked ∧ Mam.transOblExtraction.judgment = Mam.MamExtractionJudgment.licensed

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

theorem ElkinsTorrenceBrown2026.eqya_not_copy_spellout : (spineOf Mam.MamClauseType.aspectless).projects Minimalist.Cat.Voice = true ∧ (spineOf Mam.MamClauseType.infinitival).projects Minimalist.Cat.Voice = false ∧ Mam.ldAspectless.embeddedJudgment = Mam.MamExtractionJudgment.licensed ∧ Mam.ldInfinitival.embeddedJudgment = Mam.MamExtractionJudgment.blocked

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

theorem ElkinsTorrenceBrown2026.clauseSpine_finer_than_complementSize : mamAspectlessSpine.projects Minimalist.Cat.Voice = true ∧ mamInfinitivalSpine.projects Minimalist.Cat.Voice = false

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

theorem ElkinsTorrenceBrown2026.dir_probe_matches_voice : dirCis.features = mamVoice.features

Dir⁰ also carries [uOblique].

theorem ElkinsTorrenceBrown2026.dir_spellout_eqya : Minimalist.spellout mamVoiceVocab (Minimalist.FeatureBundle.ofGramFeatures [Minimalist.GramFeature.valued (Minimalist.FeatureVal.oblique true)]) (some Minimalist.Cat.Voice) = some "=(y)a'"

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

theorem ElkinsTorrenceBrown2026.derivation_tree_size : ElkinsTorrenceBrown2026.cp✝.nodeCount = 6

theorem ElkinsTorrenceBrown2026.voice_has_uOblique : Minimalist.hasUnvaluedFeature mamVoice.features (Minimalist.FeatureVal.oblique false) = true

theorem ElkinsTorrenceBrown2026.voice_agree_values_oblique : Minimalist.applyAgree mamVoice.features ElkinsTorrenceBrown2026.oblique_goal_features✝ (Minimalist.FeatureVal.oblique false) = some (Minimalist.FeatureBundle.ofGramFeatures [Minimalist.GramFeature.valued (Minimalist.FeatureVal.oblique true)])

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

theorem ElkinsTorrenceBrown2026.voice_spellout_eqya : Minimalist.spellout mamVoiceVocab (Minimalist.FeatureBundle.ofGramFeatures [Minimalist.GramFeature.valued (Minimalist.FeatureVal.oblique true)]) (some Minimalist.Cat.Voice) = some "=(y)a'"

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

theorem ElkinsTorrenceBrown2026.full_derivation_pipeline : ((Minimalist.applyAgree mamVoice.features ElkinsTorrenceBrown2026.oblique_goal_features✝ (Minimalist.FeatureVal.oblique false)).bind fun (fb : Minimalist.FeatureBundle) => Minimalist.spellout mamVoiceVocab fb (some Minimalist.Cat.Voice)) = some "=(y)a'"

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

Voice⁰ in Mam carries two independent probes:

1. φ-probe [uPerson, uNumber] (analyzed by [Sco23]): Agrees with agent in Spec,VoiceP, yielding Set A morphology.
2. Oblique probe [uOblique] (analyzed by [ETB26], this file): Agrees with a passing Ā-moved oblique, yielding =(y)a' on Voice⁰.

Both are instances of the same abstract Agree operation: probe searches c-command domain, finds closest matching goal, copies features, and the valued features are spelled out by Vocabulary Insertion. They differ only in which features they probe for and what vocabulary entries match.

theorem ElkinsTorrenceBrown2026.both_probes_unvalued : Scott2023.voiceProbe.toGramFeatures.all Minimalist.GramFeature.isUnvalued = true ∧ ElkinsTorrenceBrown2026.voiceOblProbe✝.toGramFeatures.all Minimalist.GramFeature.isUnvalued = true

Both Voice probes are unvalued features.

theorem ElkinsTorrenceBrown2026.phi_and_oblique_agree_parallel : ((Minimalist.applyAgree Scott2023.voiceProbe Scott2023.dp3sg (Minimalist.FeatureVal.phi (Minimalist.PhiFeature.person Person.third))).bind fun (fb : Minimalist.FeatureBundle) => Minimalist.applyAgree fb Scott2023.dp3sg (Minimalist.FeatureVal.phi (Minimalist.PhiFeature.number Number.singular))) = some Scott2023.voiceFullyAgreed ∧ Minimalist.spellout Scott2023.setAVocab Scott2023.voiceFullyAgreed (some Minimalist.Cat.v) = some "t-" ∧ Minimalist.applyAgree ElkinsTorrenceBrown2026.voiceOblProbe✝ (Minimalist.FeatureBundle.ofGramFeatures [Minimalist.GramFeature.valued (Minimalist.FeatureVal.oblique true)]) (Minimalist.FeatureVal.oblique false) = some (Minimalist.FeatureBundle.ofGramFeatures [Minimalist.GramFeature.valued (Minimalist.FeatureVal.oblique true)]) ∧ Minimalist.spellout [eqYaVocab] (Minimalist.FeatureBundle.ofGramFeatures [Minimalist.GramFeature.valued (Minimalist.FeatureVal.oblique true)]) (some Minimalist.Cat.Voice) = some "=(y)a'"

φ-Agree (Scott 2023) and oblique-Agree (this paper) are parallel instances of the same operation, differing only in which features are probed and which vocabulary entries match.