Coon, Mateo Pedro & Preminger (2014) @cite{coon-mateo-pedro-preminger-2014}

The role of Case in A-bar extraction asymmetries: Evidence from Mayan. Linguistic Variation 14(2), 179–242.

Core Claim

Syntactic ergativity — the ban on A-bar extracting transitive subjects in languages like Q'anjob'al — is not about properties of the ergative NP. It is a locality problem in case assignment to the absolutive object.

In HIGH-ABS languages (ABS=NOM), Infl⁰ assigns absolutive case. The transitive object must raise out of vP to receive this case, passing through the single escape hatch at the vP phase edge — trapping the subject. In LOW-ABS languages (ABS=DEF), v⁰ assigns absolutive locally within vP. The escape hatch is free and the subject extracts without issue.

The Agent Focus Construction

Q'anjob'al's AF morpheme -on is analyzed as a marked variant of Voice⁰ that assigns structural case to the internal argument (the transitive object). When Voice⁰_AF assigns case, Infl⁰ is freed to assign case to the subject. With the escape hatch unoccupied, the subject can extract. The intransitive status suffix -i surfaces because AF Voice is non-phasal (intransitive v⁰).

The Crazy Antipassive

The same -on morpheme appears in Q'anjob'al non-finite embedded transitives — environments where Infl⁰ is absent and thus cannot assign case to objects. The -on provides the needed case source, further supporting its role as a case-assigner.

Three Factors for Syntactic Ergativity in Q'anjob'al

1. Transitive vP is phasal (constitutes a locality domain)
2. The transitive subject is generated below vP (in Spec,VoiceP)
3. There is only a single specifier available for extraction out of vP

inductive CoonMateoPedroPreminger2014.AbstractCase : Type

Abstract case features assigned by functional heads. Following @cite{legate-2008}, "absolutive" is not an abstract case but a descriptive cover term for the morphological form shared by transitive objects and intransitive subjects. The actual abstract cases are:

• NOM: assigned by Infl⁰ (to intransitive subjects universally, and to transitive objects in ABS=NOM languages)
• ACC: assigned by v⁰ (to transitive objects in ABS=DEF languages)
• ERG: assigned by v⁰ (to transitive subjects universally)

• nom : AbstractCase
• acc : AbstractCase
• erg : AbstractCase

@[implicit_reducible]

instance CoonMateoPedroPreminger2014.instDecidableEqAbstractCase : DecidableEq AbstractCase

Equations

• CoonMateoPedroPreminger2014.instDecidableEqAbstractCase x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def CoonMateoPedroPreminger2014.instReprAbstractCase.repr : AbstractCase → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance CoonMateoPedroPreminger2014.instReprAbstractCase : Repr AbstractCase

Equations

• CoonMateoPedroPreminger2014.instReprAbstractCase = { reprPrec := CoonMateoPedroPreminger2014.instReprAbstractCase.repr }

inductive CoonMateoPedroPreminger2014.FunctionalHead : Type

Which functional head assigns each abstract case.

• infl : FunctionalHead
• v : FunctionalHead

@[implicit_reducible]

instance CoonMateoPedroPreminger2014.instDecidableEqFunctionalHead : DecidableEq FunctionalHead

Equations

• CoonMateoPedroPreminger2014.instDecidableEqFunctionalHead x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance CoonMateoPedroPreminger2014.instReprFunctionalHead : Repr FunctionalHead

Equations

• CoonMateoPedroPreminger2014.instReprFunctionalHead = { reprPrec := CoonMateoPedroPreminger2014.instReprFunctionalHead.repr }

def CoonMateoPedroPreminger2014.instReprFunctionalHead.repr : FunctionalHead → ℕ → Std.Format

Equations

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

def CoonMateoPedroPreminger2014.AbstractCase.assigner : AbstractCase → FunctionalHead

Equations

• CoonMateoPedroPreminger2014.AbstractCase.nom.assigner = CoonMateoPedroPreminger2014.FunctionalHead.infl
• CoonMateoPedroPreminger2014.AbstractCase.acc.assigner = CoonMateoPedroPreminger2014.FunctionalHead.v
• CoonMateoPedroPreminger2014.AbstractCase.erg.assigner = CoonMateoPedroPreminger2014.FunctionalHead.v

theorem CoonMateoPedroPreminger2014.erg_from_v : AbstractCase.erg.assigner = FunctionalHead.v

ERG is always from v⁰, NOM is always from Infl⁰.

theorem CoonMateoPedroPreminger2014.nom_from_infl : AbstractCase.nom.assigner = FunctionalHead.infl

def CoonMateoPedroPreminger2014.objectAbstractCase : Fragments.Mayan.CaseLocus → AbstractCase

The abstract case assigned to the transitive object depends on the case locus parameter.

Equations

• CoonMateoPedroPreminger2014.objectAbstractCase Fragments.Mayan.CaseLocus.absNom = CoonMateoPedroPreminger2014.AbstractCase.nom
• CoonMateoPedroPreminger2014.objectAbstractCase Fragments.Mayan.CaseLocus.absDef = CoonMateoPedroPreminger2014.AbstractCase.acc

def CoonMateoPedroPreminger2014.subjectAbstractCase (_locus : Fragments.Mayan.CaseLocus) : AbstractCase

Transitive subjects always receive ERG from v⁰, regardless of case locus. This uniformity is the paper's key insight: the variation is in how objects are licensed, not subjects.

Equations

• CoonMateoPedroPreminger2014.subjectAbstractCase _locus = CoonMateoPedroPreminger2014.AbstractCase.erg

theorem CoonMateoPedroPreminger2014.subject_case_uniform (l1 l2 : Fragments.Mayan.CaseLocus) : subjectAbstractCase l1 = subjectAbstractCase l2

def CoonMateoPedroPreminger2014.objectMustExitVP (locus : Fragments.Mayan.CaseLocus) : Bool

Does the object need to move out of vP for case? The object must escape the vP phase domain to reach Infl⁰ iff case is assigned by Infl⁰.

Equations

• CoonMateoPedroPreminger2014.objectMustExitVP Fragments.Mayan.CaseLocus.absNom = true
• CoonMateoPedroPreminger2014.objectMustExitVP Fragments.Mayan.CaseLocus.absDef = false

def CoonMateoPedroPreminger2014.objectCaseIsExternal (locus : Fragments.Mayan.CaseLocus) : Bool

The object case assigner determines whether the object is licensed inside or outside vP.

Equations

• CoonMateoPedroPreminger2014.objectCaseIsExternal locus = ((CoonMateoPedroPreminger2014.objectAbstractCase locus).assigner == CoonMateoPedroPreminger2014.FunctionalHead.infl)

def CoonMateoPedroPreminger2014.subjectTrapped (locus : Fragments.Mayan.CaseLocus) (transitive : Bool) : Bool

When the transitive object exits vP through the phase edge (Spec,vP), it occupies the single escape hatch. The subject, base-generated in Spec,VoiceP (below the vP phase boundary), cannot exit the phase domain because the escape hatch is occupied.

This is the paper's core contribution: the ban on extracting transitive subjects follows from a locality problem in how case is assigned to objects, not from any property of the ergative subject itself.

Equations

• CoonMateoPedroPreminger2014.subjectTrapped locus transitive = (transitive && CoonMateoPedroPreminger2014.objectMustExitVP locus)

def CoonMateoPedroPreminger2014.hasSyntacticErgativity (locus : Fragments.Mayan.CaseLocus) : Bool

Syntactic ergativity: the ban on A-bar extraction of transitive subjects. Predicted to occur iff the language is ABS=NOM (HIGH-ABS).

Equations

• CoonMateoPedroPreminger2014.hasSyntacticErgativity locus = CoonMateoPedroPreminger2014.subjectTrapped locus true

theorem CoonMateoPedroPreminger2014.absNom_has_syntactic_ergativity : hasSyntacticErgativity Fragments.Mayan.CaseLocus.absNom = true

theorem CoonMateoPedroPreminger2014.absDef_no_syntactic_ergativity : hasSyntacticErgativity Fragments.Mayan.CaseLocus.absDef = false

theorem CoonMateoPedroPreminger2014.intransitive_subject_never_trapped (locus : Fragments.Mayan.CaseLocus) : subjectTrapped locus false = false

Intransitive subjects are NEVER trapped, regardless of case locus: there is no transitive object to occupy the escape hatch. This correctly predicts that intransitive subjects extract freely in both HIGH-ABS and LOW-ABS languages.

def CoonMateoPedroPreminger2014.voiceAF : Minimalist.VoiceHead

Agent Focus Voice: a marked variant of Voice⁰ that assigns structural case to the internal argument (the transitive object).

Following @cite{ordonez-1995} on Popti', -on assigns case to the object. Unlike regular transitive Voice, AF Voice is NOT a phase head: its v⁰ is the intransitive variety (non-phasal), explaining why the intransitive status suffix -i surfaces rather than transitive -V'.

AF is a "last-resort" strategy, akin to English of-insertion: the marked variant of Voice⁰ is merged only when the normal derivation (with regular transitive Voice) would crash — i.e., when the subject must be A-bar extracted.

Equations

• CoonMateoPedroPreminger2014.voiceAF = { flavor := Minimalist.VoiceFlavor.agentive, hasD := true, phaseOverride := some false, checksCase := true }

theorem CoonMateoPedroPreminger2014.af_assigns_case : voiceAF.ChecksCase

AF Voice assigns case to the object.

theorem CoonMateoPedroPreminger2014.af_not_phase : ¬voiceAF.IsPhasal

AF Voice is NOT a phase head (intransitive v⁰).

theorem CoonMateoPedroPreminger2014.af_introduces_agent : voiceAF.AssignsTheta

AF Voice still introduces an external argument (the agent).

def CoonMateoPedroPreminger2014.AfCircumventsTrapping : Prop

AF Voice circumvents the trapping mechanism because it assigns case to the object (so the object need not move to Spec,vP) AND because AF's v⁰ is non-phasal (so vP is not a locality domain). Either property alone would free the subject, but both hold simultaneously for AF Voice.

Equations

• CoonMateoPedroPreminger2014.AfCircumventsTrapping = (CoonMateoPedroPreminger2014.voiceAF.ChecksCase ∧ ¬CoonMateoPedroPreminger2014.voiceAF.IsPhasal)

@[implicit_reducible]

instance CoonMateoPedroPreminger2014.instDecidableAfCircumventsTrapping : Decidable AfCircumventsTrapping

Equations

• CoonMateoPedroPreminger2014.instDecidableAfCircumventsTrapping = id inferInstance

theorem CoonMateoPedroPreminger2014.af_frees_subject : AfCircumventsTrapping

def CoonMateoPedroPreminger2014.CaseAloneFreesExtraction (v : Minimalist.VoiceHead) : Prop

The case-assignment property alone is what frees extraction: when Voice checks case, the object receives case inside vP and need not move to the escape hatch. This is the paper's primary explanation for why AF circumvents the extraction ban.

Equations

• CoonMateoPedroPreminger2014.CaseAloneFreesExtraction v = v.ChecksCase

@[implicit_reducible]

instance CoonMateoPedroPreminger2014.instDecidableCaseAloneFreesExtraction (v : Minimalist.VoiceHead) : Decidable (CaseAloneFreesExtraction v)

Equations

• CoonMateoPedroPreminger2014.instDecidableCaseAloneFreesExtraction v = id inferInstance

theorem CoonMateoPedroPreminger2014.af_case_frees : CaseAloneFreesExtraction voiceAF

theorem CoonMateoPedroPreminger2014.af_morphology_from_phase : ¬voiceAF.IsPhasal

The non-phasal status explains AF's morphology (intransitive status suffix -i) rather than the extraction facts. Since AF's v⁰ is intransitive, no ergative case is assigned to the subject.

theorem CoonMateoPedroPreminger2014.regular_voice_traps : Minimalist.voiceAgent.IsPhasal ∧ ¬Minimalist.voiceAgent.ChecksCase

Contrast with regular transitive Voice: phasal, does NOT check case.

def CoonMateoPedroPreminger2014.objectLicensedInNonFinite (locus : Fragments.Mayan.CaseLocus) : Bool

In non-finite embedded clauses, Infl⁰ is absent (no aspect marking). This makes predictions depending on the case locus:

• ABS=NOM: transitive objects cannot be licensed (Infl⁰ absent). They require -on ("Crazy Antipassive") or detransitivization.
• ABS=DEF: transitive objects are licensed by v⁰ (present even without Infl⁰). They are fine in non-finite clauses.

Intransitive subjects lose absolutive case in BOTH types (Infl⁰ assigns NOM to intransitive subjects universally in Mayan).

Equations

• CoonMateoPedroPreminger2014.objectLicensedInNonFinite Fragments.Mayan.CaseLocus.absNom = false
• CoonMateoPedroPreminger2014.objectLicensedInNonFinite Fragments.Mayan.CaseLocus.absDef = true

theorem CoonMateoPedroPreminger2014.absNom_objects_unlicensed_nonfinite : objectLicensedInNonFinite Fragments.Mayan.CaseLocus.absNom = false

theorem CoonMateoPedroPreminger2014.absDef_objects_licensed_nonfinite : objectLicensedInNonFinite Fragments.Mayan.CaseLocus.absDef = true

def CoonMateoPedroPreminger2014.intranSLicensedInNonFinite (_locus : Fragments.Mayan.CaseLocus) : Bool

Intransitive subjects are unlicensed in non-finite clauses regardless of case locus, because Infl⁰ (the universal NOM assigner for intransitive S) is absent.

Equations

• CoonMateoPedroPreminger2014.intranSLicensedInNonFinite _locus = false

theorem CoonMateoPedroPreminger2014.intranS_unlicensed_nonfinite (locus : Fragments.Mayan.CaseLocus) : intranSLicensedInNonFinite locus = false

inductive CoonMateoPedroPreminger2014.ObjectType : Type

Some objects do not require structural case: reflexive objects, extended reflexive objects, and bare (determinerless) NPs. These are licensed by pseudo-incorporation into the verb stem (§5.2).

Extended reflexives (possessor bound by subject, e.g., s-na? '3ERG-house') are formally identical to reflexives — the possessed nominal has lost its independent referential meaning.

Prediction: AF is impossible with caseless objects. Since AF exists precisely to assign case to the object, it is vacuous (and thus blocked as last-resort) when the object needs no case.

• fullDP : ObjectType
• reflexive : ObjectType
• extendedReflexive : ObjectType
• bareNP : ObjectType

@[implicit_reducible]

instance CoonMateoPedroPreminger2014.instDecidableEqObjectType : DecidableEq ObjectType

Equations

• CoonMateoPedroPreminger2014.instDecidableEqObjectType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance CoonMateoPedroPreminger2014.instReprObjectType : Repr ObjectType

Equations

• CoonMateoPedroPreminger2014.instReprObjectType = { reprPrec := CoonMateoPedroPreminger2014.instReprObjectType.repr }

def CoonMateoPedroPreminger2014.instReprObjectType.repr : ObjectType → ℕ → Std.Format

Equations

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

def CoonMateoPedroPreminger2014.ObjectType.needsCase : ObjectType → Bool

Equations

• CoonMateoPedroPreminger2014.ObjectType.fullDP.needsCase = true
• CoonMateoPedroPreminger2014.ObjectType.reflexive.needsCase = false
• CoonMateoPedroPreminger2014.ObjectType.extendedReflexive.needsCase = false
• CoonMateoPedroPreminger2014.ObjectType.bareNP.needsCase = false

def CoonMateoPedroPreminger2014.afAvailable (obj : ObjectType) : Bool

AF is available iff the object needs case.

Equations

• CoonMateoPedroPreminger2014.afAvailable obj = obj.needsCase

theorem CoonMateoPedroPreminger2014.af_available_fullDP : afAvailable ObjectType.fullDP = true

theorem CoonMateoPedroPreminger2014.af_unavailable_reflexive : afAvailable ObjectType.reflexive = false

theorem CoonMateoPedroPreminger2014.af_unavailable_extReflexive : afAvailable ObjectType.extendedReflexive = false

theorem CoonMateoPedroPreminger2014.af_unavailable_bareNP : afAvailable ObjectType.bareNP = false

def CoonMateoPedroPreminger2014.caselessObjectFreesSubject (obj : ObjectType) : Bool

When the object is caseless, regular transitive Voice is used even for agent extraction: the object remains inside vP (no case-driven movement) and does not block the escape hatch. The subject is NOT trapped.

Equations

• CoonMateoPedroPreminger2014.caselessObjectFreesSubject obj = !obj.needsCase

theorem CoonMateoPedroPreminger2014.reflexive_frees_subject : caselessObjectFreesSubject ObjectType.reflexive = true

theorem CoonMateoPedroPreminger2014.qanjobal_has_syntactic_ergativity : hasSyntacticErgativity Fragments.Mayan.CaseLocus.absNom = true

Q'anjob'al is a HIGH-ABS language with syntactic ergativity.

theorem CoonMateoPedroPreminger2014.chol_no_syntactic_ergativity : hasSyntacticErgativity Fragments.Mayan.CaseLocus.absDef = false

Chol is a LOW-ABS language without syntactic ergativity.

theorem CoonMateoPedroPreminger2014.qanjobal_erg_alignment : Fragments.Mayan.Qanjobal.ArgPosition.case Features.Prominence.ArgumentRole.A = UD.Case.erg ∧ Fragments.Mayan.Qanjobal.ArgPosition.case Features.Prominence.ArgumentRole.P = UD.Case.abs

Q'anjob'al's ergative alignment matches the standard pattern: transitive agent = ERG, transitive object = ABS.

theorem CoonMateoPedroPreminger2014.chol_erg_alignment : Fragments.Mayan.Chol.ArgPosition.case Features.Prominence.ArgumentRole.A = UD.Case.erg ∧ Fragments.Mayan.Chol.ArgPosition.case Features.Prominence.ArgumentRole.P = UD.Case.abs

Chol's ergative alignment matches the same standard pattern.

theorem CoonMateoPedroPreminger2014.shared_morphology_different_syntax : Fragments.Mayan.Qanjobal.ArgPosition.case Features.Prominence.ArgumentRole.A = Fragments.Mayan.Chol.ArgPosition.case Features.Prominence.ArgumentRole.A ∧ hasSyntacticErgativity Fragments.Mayan.CaseLocus.absNom ≠ hasSyntacticErgativity Fragments.Mayan.CaseLocus.absDef

Despite sharing ergative morphology, Q'anjob'al and Chol differ in whether agent extraction is banned. The difference traces to their distinct case loci, not to properties of the ergative NP.

theorem CoonMateoPedroPreminger2014.qanjobal_high_abs : Fragments.Mayan.Qanjobal.absPosition = Fragments.Mayan.ABSPosition.high

Fragment-grounded ABSPosition: Q'anjob'al is HIGH-ABS.

theorem CoonMateoPedroPreminger2014.chol_low_abs : Fragments.Mayan.Chol.absPosition = Fragments.Mayan.ABSPosition.low

Fragment-grounded ABSPosition: Chol is LOW-ABS.

theorem CoonMateoPedroPreminger2014.fragments_ground_tada : hasSyntacticErgativity (Fragments.Mayan.toCaseLocus Fragments.Mayan.Qanjobal.absPosition) = true ∧ hasSyntacticErgativity (Fragments.Mayan.toCaseLocus Fragments.Mayan.Chol.absPosition) = false

The fragment ABSPosition values derive the correct syntactic ergativity predictions: Q'anjob'al has it, Chol does not. This grounds Tada's Generalization in fragment data rather than hard-coded table entries.

theorem CoonMateoPedroPreminger2014.mayan_tada (lang : Fragments.Mayan.MayanLang) : hasSyntacticErgativity (Fragments.Mayan.toCaseLocus (Phenomena.Ergativity.MayanAlignment.absPositionOf lang)) = true ↔ Phenomena.Ergativity.MayanAlignment.absPositionOf lang = Fragments.Mayan.ABSPosition.high

Tada's Generalization, parameterized form: a Mayan language exhibits syntactic ergativity (the analytical predicate from §4) iff it is HIGH-ABS. Quantified over Fragments.Mayan.MayanLang via the cross-Mayan absPositionOf dispatcher (Phenomena.Ergativity.MayanAlignment).

Replaces the per-language enumeration in fragments_ground_tada with a single quantified theorem that scales as the MayanLang registry grows.

theorem CoonMateoPedroPreminger2014.qanjobal_extraction_consistent : Fragments.Mayan.Qanjobal.extractionProfile.Marks Typology.ExtractionTarget.subject

Q'anjob'al's extraction data is consistent with the prediction: agent extraction is marked (requires AF morphology in regular transitives). The substantive claim lives at extractionProfile's markedPositions := [.subject] field.

theorem CoonMateoPedroPreminger2014.chol_extraction_consistent : Fragments.Mayan.Chol.extractionProfile.strategy = Typology.ExtractionMarkingStrategy.unmarked

Chol's extraction data is consistent: no Agent Focus morphology required (every argument extracts freely under the absent strategy).

theorem CoonMateoPedroPreminger2014.qanjobal_af_itv : Fragments.Mayan.Qanjobal.agentFocusForm.statusSuffix = Fragments.Mayan.Qanjobal.StatusSuffix.itv

Q'anjob'al's AF form carries the intransitive status suffix, matching the prediction that AF Voice is non-phasal (intransitive v⁰).

theorem CoonMateoPedroPreminger2014.crazy_ap_unified : Fragments.Mayan.Qanjobal.crazyAntipassiveForm = Fragments.Mayan.Qanjobal.agentFocusForm

The Crazy Antipassive form is identical to AF: same -on morpheme, same intransitive status suffix. Supports the unified analysis of -on as a case-assigner in environments where case is otherwise unavailable.

theorem CoonMateoPedroPreminger2014.chol_nonfinite_predictions : Fragments.Mayan.Chol.absObjectInNonFinite = true ∧ Fragments.Mayan.Chol.absIntranSInNonFinite = false

Non-finite absolutive asymmetry in Chol: objects are available (v⁰ assigns case) but intransitive subjects are not (Infl⁰ absent). Follows from LOW-ABS: v⁰ handles objects, Infl⁰ handles intransitives.

theorem CoonMateoPedroPreminger2014.tada_derived_high : hasSyntacticErgativity (Fragments.Mayan.toCaseLocus Fragments.Mayan.ABSPosition.high) = true

Tada's Generalization is now DERIVED from the case-assignment analysis rather than merely stated as a correlation. The observable parameter ABSPosition maps to CaseLocus, which determines whether syntactic ergativity arises.

theorem CoonMateoPedroPreminger2014.tada_derived_low : hasSyntacticErgativity (Fragments.Mayan.toCaseLocus Fragments.Mayan.ABSPosition.low) = false

theorem CoonMateoPedroPreminger2014.tada_from_case_theory (pos : Fragments.Mayan.ABSPosition) : hasSyntacticErgativity (Fragments.Mayan.toCaseLocus pos) = (pos == Fragments.Mayan.ABSPosition.high)

The morphological observation (ABSPosition) and the syntactic observation (extraction asymmetry) are connected through the case-assignment locus: for both values of the parameter, the predicted syntactic ergativity matches what Tada's table reports for the non-outlier languages.

structure CoonMateoPedroPreminger2014.SyntacticErgativityFactors : Type

The three factors that combine to produce the ban on extracting transitive subjects in Q'anjob'al. All three are necessary; removing any one would free the subject.

• vPIsPhasal : Bool

  I. Transitive vP is phasal (locality domain).

• subjectBelowVP : Bool

  II. The transitive subject is generated below vP.

• singleEscapeHatch : Bool

  III. Only a single specifier available for extraction out of vP.

@[implicit_reducible]

instance CoonMateoPedroPreminger2014.instDecidableEqSyntacticErgativityFactors : DecidableEq SyntacticErgativityFactors

Equations

• CoonMateoPedroPreminger2014.instDecidableEqSyntacticErgativityFactors = CoonMateoPedroPreminger2014.instDecidableEqSyntacticErgativityFactors.decEq

def CoonMateoPedroPreminger2014.instDecidableEqSyntacticErgativityFactors.decEq (x✝ x✝¹ : SyntacticErgativityFactors) : Decidable (x✝ = x✝¹)

Equations

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

def CoonMateoPedroPreminger2014.instReprSyntacticErgativityFactors.repr : SyntacticErgativityFactors → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance CoonMateoPedroPreminger2014.instReprSyntacticErgativityFactors : Repr SyntacticErgativityFactors

Equations

• CoonMateoPedroPreminger2014.instReprSyntacticErgativityFactors = { reprPrec := CoonMateoPedroPreminger2014.instReprSyntacticErgativityFactors.repr }

def CoonMateoPedroPreminger2014.SyntacticErgativityFactors.producesTrapping (f : SyntacticErgativityFactors) : Bool

Equations

• f.producesTrapping = (f.vPIsPhasal && f.subjectBelowVP && f.singleEscapeHatch)

def CoonMateoPedroPreminger2014.qanjobalFactors : SyntacticErgativityFactors

Q'anjob'al instantiates all three factors.

Equations

• CoonMateoPedroPreminger2014.qanjobalFactors = { vPIsPhasal := true, subjectBelowVP := true, singleEscapeHatch := true }

theorem CoonMateoPedroPreminger2014.qanjobal_all_three : qanjobalFactors.producesTrapping = true

theorem CoonMateoPedroPreminger2014.factor1_necessary : (have __src := qanjobalFactors; { vPIsPhasal := false, subjectBelowVP := __src.subjectBelowVP, singleEscapeHatch := __src.singleEscapeHatch }).producesTrapping = false

Removing any single factor would free the subject.

theorem CoonMateoPedroPreminger2014.factor2_necessary : (have __src := qanjobalFactors; { vPIsPhasal := __src.vPIsPhasal, subjectBelowVP := false, singleEscapeHatch := __src.singleEscapeHatch }).producesTrapping = false

theorem CoonMateoPedroPreminger2014.factor3_necessary : (have __src := qanjobalFactors; { vPIsPhasal := __src.vPIsPhasal, subjectBelowVP := __src.subjectBelowVP, singleEscapeHatch := false }).producesTrapping = false

theorem CoonMateoPedroPreminger2014.voice_phase_is_factor1 : Minimalist.voiceAgent.IsPhasal

Agentive Voice is a phase head — this is factor I.

theorem CoonMateoPedroPreminger2014.af_removes_factor1 : ¬voiceAF.IsPhasal

AF removes factor I: AF Voice is not phasal. With a non-phasal vP, there is no locality boundary trapping the subject.

structure CoonMateoPedroPreminger2014.ErgativityTypology : Type

The paper's table (10): morphological ergativity and syntactic ergativity are logically independent. Morphological ergativity is shared by all Mayan languages; syntactic ergativity (the extraction ban) arises only in ABS=NOM (HIGH-ABS) languages.

	+morph.erg	-morph.erg
+syntactic ergativity	Q'anjob'al	unattested
-syntactic ergativity	Chol	English

The [-morph,+syn] cell is predicted unattested: syntactic ergativity requires Infl⁰ to assign case to the object, which only arises in morphologically ergative systems.

• morphErg : Bool
• synErg : Bool

def CoonMateoPedroPreminger2014.instDecidableEqErgativityTypology.decEq (x✝ x✝¹ : ErgativityTypology) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance CoonMateoPedroPreminger2014.instDecidableEqErgativityTypology : DecidableEq ErgativityTypology

Equations

• CoonMateoPedroPreminger2014.instDecidableEqErgativityTypology = CoonMateoPedroPreminger2014.instDecidableEqErgativityTypology.decEq

def CoonMateoPedroPreminger2014.instReprErgativityTypology.repr : ErgativityTypology → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance CoonMateoPedroPreminger2014.instReprErgativityTypology : Repr ErgativityTypology

Equations

• CoonMateoPedroPreminger2014.instReprErgativityTypology = { reprPrec := CoonMateoPedroPreminger2014.instReprErgativityTypology.repr }

def CoonMateoPedroPreminger2014.qanjobalTypology : ErgativityTypology

Equations

• CoonMateoPedroPreminger2014.qanjobalTypology = { morphErg := true, synErg := true }

def CoonMateoPedroPreminger2014.cholTypology : ErgativityTypology

Equations

• CoonMateoPedroPreminger2014.cholTypology = { morphErg := true, synErg := false }

def CoonMateoPedroPreminger2014.englishTypology : ErgativityTypology

Equations

• CoonMateoPedroPreminger2014.englishTypology = { morphErg := false, synErg := false }

theorem CoonMateoPedroPreminger2014.morph_erg_necessary_not_sufficient : qanjobalTypology.morphErg = cholTypology.morphErg ∧ qanjobalTypology.synErg ≠ cholTypology.synErg

Morphological ergativity is necessary but not sufficient for syntactic ergativity. Q'anjob'al and Chol are both morphologically ergative but differ in syntactic ergativity.

def CoonMateoPedroPreminger2014.predictedUnattested (t : ErgativityTypology) : Bool

The [-morph.erg, +syn.erg] cell is predicted unattested: syntactic ergativity requires HIGH-ABS (Infl⁰ licensing objects), which entails morphological ergativity.

Equations

• CoonMateoPedroPreminger2014.predictedUnattested t = (!t.morphErg && t.synErg)

theorem CoonMateoPedroPreminger2014.unattested_cell : predictedUnattested { morphErg := false, synErg := true } = true

theorem CoonMateoPedroPreminger2014.attested_cells : predictedUnattested qanjobalTypology = false ∧ predictedUnattested cholTypology = false ∧ predictedUnattested englishTypology = false

theorem CoonMateoPedroPreminger2014.af_person_restriction : Fragments.Mayan.Qanjobal.PersonRestriction.third.requiresAF = true ∧ Fragments.Mayan.Qanjobal.PersonRestriction.first.requiresAF = false

AF is restricted to 3rd person agents in Q'anjob'al (§5.1, ex. 72). The fragment's PersonRestriction captures this. The theoretical explanation: 1st/2nd person pronouns may be base-generated in Spec,CP (following Baker 2008), so they never need to extract through the vP phase edge — the trapping problem does not arise for them.

The Crazy Antipassive, by contrast, is NOT person-restricted: it applies in ALL non-finite embedded transitives regardless of the person of the subject, because the trigger there is the absence of Infl⁰ (not extraction through a phase edge).

theorem CoonMateoPedroPreminger2014.crazy_ap_no_person_restriction : Fragments.Mayan.Qanjobal.PersonRestriction.first.requiresCrazyAP = true ∧ Fragments.Mayan.Qanjobal.PersonRestriction.third.requiresCrazyAP = true

inductive CoonMateoPedroPreminger2014.VPInternalElement : Type

The paper's §5.3 prediction: in HIGH-ABS languages, not only subjects but NOTHING generated inside a transitive vP (besides the object itself) should be able to escape. The object's movement to Spec,vP for case renders the single escape hatch occupied — trapping everything inside the phase domain.

This distinguishes the case-based account from ergative-property accounts: the latter predict only subjects are banned; the former predicts a general vP-internal extraction restriction.

• subject : VPInternalElement
• lowAdverb : VPInternalElement
• secondObject : VPInternalElement

@[implicit_reducible]

instance CoonMateoPedroPreminger2014.instDecidableEqVPInternalElement : DecidableEq VPInternalElement

Equations

• CoonMateoPedroPreminger2014.instDecidableEqVPInternalElement x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def CoonMateoPedroPreminger2014.instReprVPInternalElement.repr : VPInternalElement → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance CoonMateoPedroPreminger2014.instReprVPInternalElement : Repr VPInternalElement

Equations

• CoonMateoPedroPreminger2014.instReprVPInternalElement = { reprPrec := CoonMateoPedroPreminger2014.instReprVPInternalElement.repr }

def CoonMateoPedroPreminger2014.VPInternalElement.canEscapeHighABS : VPInternalElement → Bool

Can this vP-internal element escape a transitive vP in a HIGH-ABS language? None can — the escape hatch is occupied by the object.

Equations

• CoonMateoPedroPreminger2014.VPInternalElement.subject.canEscapeHighABS = false
• CoonMateoPedroPreminger2014.VPInternalElement.lowAdverb.canEscapeHighABS = false
• CoonMateoPedroPreminger2014.VPInternalElement.secondObject.canEscapeHighABS = false

def CoonMateoPedroPreminger2014.VPInternalElement.canEscapeLowABS : VPInternalElement → Bool

In a LOW-ABS language, the escape hatch is free.

Equations

• CoonMateoPedroPreminger2014.VPInternalElement.subject.canEscapeLowABS = true
• CoonMateoPedroPreminger2014.VPInternalElement.lowAdverb.canEscapeLowABS = true
• CoonMateoPedroPreminger2014.VPInternalElement.secondObject.canEscapeLowABS = true

theorem CoonMateoPedroPreminger2014.vp_internal_ban_high_abs : VPInternalElement.subject.canEscapeHighABS = false ∧ VPInternalElement.lowAdverb.canEscapeHighABS = false ∧ VPInternalElement.secondObject.canEscapeHighABS = false

theorem CoonMateoPedroPreminger2014.vp_internal_free_low_abs : VPInternalElement.subject.canEscapeLowABS = true ∧ VPInternalElement.lowAdverb.canEscapeLowABS = true ∧ VPInternalElement.secondObject.canEscapeLowABS = true

def CoonMateoPedroPreminger2014.hasDoubleObjectConstruction (locus : Fragments.Mayan.CaseLocus) : Bool

Double-object constructions are systematically absent in HIGH-ABS languages (Q'anjob'al, Kaqchikel) but present in LOW-ABS Chol (via applicative). This is consistent with the general vP-internal ban.

Equations

• CoonMateoPedroPreminger2014.hasDoubleObjectConstruction Fragments.Mayan.CaseLocus.absNom = false
• CoonMateoPedroPreminger2014.hasDoubleObjectConstruction Fragments.Mayan.CaseLocus.absDef = true

theorem CoonMateoPedroPreminger2014.doc_absent_high_abs : hasDoubleObjectConstruction Fragments.Mayan.CaseLocus.absNom = false

theorem CoonMateoPedroPreminger2014.doc_present_low_abs : hasDoubleObjectConstruction Fragments.Mayan.CaseLocus.absDef = true

theorem CoonMateoPedroPreminger2014.reflexive_end_to_end : ObjectType.reflexive.needsCase = false ∧ afAvailable ObjectType.reflexive = false ∧ caselessObjectFreesSubject ObjectType.reflexive = true

End-to-end argumentation chain for reflexive objects (§5.2):

1. Reflexive objects are caseless (pseudo-incorporated)
2. AF exists to assign case → AF is vacuous with caseless objects
3. With no case-driven movement, the object stays in situ
4. The escape hatch is unoccupied
5. The subject is free to extract using regular transitive Voice
6. Therefore: reflexive + agent extraction = regular transitive form

theorem CoonMateoPedroPreminger2014.extReflexive_end_to_end : ObjectType.extendedReflexive.needsCase = false ∧ afAvailable ObjectType.extendedReflexive = false ∧ caselessObjectFreesSubject ObjectType.extendedReflexive = true

Extended reflexives (possessor bound by subject) pattern with reflexives: caseless, AF impossible, subject extracts freely. Examples (75a)–(76a) of @cite{coon-mateo-pedro-preminger-2014}.

theorem CoonMateoPedroPreminger2014.fullDP_end_to_end : ObjectType.fullDP.needsCase = true ∧ afAvailable ObjectType.fullDP = true ∧ caselessObjectFreesSubject ObjectType.fullDP = false

Contrast: full DP object requires case → AF needed → AF available.

theorem CoonMateoPedroPreminger2014.voice_phase_bridge : Minimalist.voiceAgent.IsPhasal ∧ ¬voiceAF.IsPhasal ∧ ¬Minimalist.voicePassive.IsPhasal ∧ ¬Minimalist.voiceAnticausative.IsPhasal

The trapping mechanism is grounded in Phase theory: regular transitive Voice is a phase head (v*), so vP constitutes a locality domain under the PIC. AF Voice is NOT a phase head, so it does not create a phase boundary — the complement remains accessible.

This connects IsPhasal on VoiceHead to the Phase module's isPhaseHeadOf .C/isPhaseHeadOf .Voice selectors.

def CoonMateoPedroPreminger2014.VoiceTrapsSubject (v : Minimalist.VoiceHead) (locus : Fragments.Mayan.CaseLocus) : Prop

Phase headedness partitions Voice into {trapping, non-trapping}: a Voice head traps the subject iff it is a phase head AND does not itself check case (freeing Infl⁰ to do so).

Equations

• CoonMateoPedroPreminger2014.VoiceTrapsSubject v locus = (v.IsPhasal ∧ ¬v.ChecksCase ∧ CoonMateoPedroPreminger2014.objectMustExitVP locus = true)

@[implicit_reducible]

instance CoonMateoPedroPreminger2014.instDecidableVoiceTrapsSubject (v : Minimalist.VoiceHead) (locus : Fragments.Mayan.CaseLocus) : Decidable (VoiceTrapsSubject v locus)

Equations

• CoonMateoPedroPreminger2014.instDecidableVoiceTrapsSubject v locus = id inferInstance

theorem CoonMateoPedroPreminger2014.agent_voice_traps_absNom : VoiceTrapsSubject Minimalist.voiceAgent Fragments.Mayan.CaseLocus.absNom

theorem CoonMateoPedroPreminger2014.agent_voice_free_absDef : ¬VoiceTrapsSubject Minimalist.voiceAgent Fragments.Mayan.CaseLocus.absDef

theorem CoonMateoPedroPreminger2014.af_voice_never_traps (locus : Fragments.Mayan.CaseLocus) : ¬VoiceTrapsSubject voiceAF locus

def CoonMateoPedroPreminger2014.AbstractCase.toCoreCase : AbstractCase → Core.Case

The paper's AbstractCase maps to the framework's Core.Case.

Equations

• CoonMateoPedroPreminger2014.AbstractCase.nom.toCoreCase = UD.Case.nom
• CoonMateoPedroPreminger2014.AbstractCase.acc.toCoreCase = UD.Case.acc
• CoonMateoPedroPreminger2014.AbstractCase.erg.toCoreCase = UD.Case.erg

theorem CoonMateoPedroPreminger2014.coreCase_bridge_object (locus : Fragments.Mayan.CaseLocus) : (objectAbstractCase locus).toCoreCase = match locus with | Fragments.Mayan.CaseLocus.absNom => UD.Case.nom | Fragments.Mayan.CaseLocus.absDef => UD.Case.acc

The mapping preserves the assigner structure: ERG comes from v⁰, NOM comes from Infl⁰, and the object case depends on the parameter.

theorem CoonMateoPedroPreminger2014.coreCase_bridge_subject (locus : Fragments.Mayan.CaseLocus) : (subjectAbstractCase locus).toCoreCase = UD.Case.erg

Theory-laden Voice/ClauseSpine apparatus for Kaqchikel, formerly in Fragments/Mayan/Kaqchikel/AgentFocus.lean. Lives here because this is the file that uses it (§18 cross-language bridge), and because Voice-flavor analysis is the @cite{coon-mateo-pedro-preminger-2014} side of the same author cluster's Mayan work (@cite{preminger-2014}'s Ch 4 covers the agreement side; CMP 2014 covers the case/Voice side). The fragment data (VerbForm.agentFocus.hasSetA, kaqAFType, etc.) stays typology-neutral.

def CoonMateoPedroPreminger2014.kaqClauseSpine : Minimalist.ClauseSpine

Both the transitive and AF derivations project the same clausal spine (CP > TP > vP > VP). The difference is in the v head: transitive v introduces the agent in Spec,vP; AF v does not.

Equations

• CoonMateoPedroPreminger2014.kaqClauseSpine = Minimalist.ClauseSpine.cP

def CoonMateoPedroPreminger2014.kaqVoice : Minimalist.VoiceHead

Kaqchikel agentive Voice/v head (parallel to Mam's Voice). Present in the transitive derivation; absent or altered in AF. Phasehood is the load-bearing property for §18's cross-language bridge: agentive Voice is a phase head (flavor default), creating the locality boundary that traps the subject in HIGH-ABS Mayan languages (CMP 2014 §4–§5).

Equations

• CoonMateoPedroPreminger2014.kaqVoice = { flavor := Minimalist.VoiceFlavor.agentive, hasD := true }

theorem CoonMateoPedroPreminger2014.kaq_has_voice : kaqClauseSpine.projects Minimalist.Cat.Voice = true

Kaqchikel clause projects Voice.

theorem CoonMateoPedroPreminger2014.kaq_voice_is_agentive : kaqVoice.flavor = Minimalist.VoiceFlavor.agentive

Kaqchikel Voice is agentive.

Different Mayan languages circumvent syntactic ergativity through different mechanisms (@cite{coon-mateo-pedro-preminger-2014} §4.2, §5). Q'anjob'al uses case assignment: Voice_AF assigns case to the object, freeing the escape hatch. Kaqchikel uses an anti-locality repair: AF structure avoids the too-local Spec,TP → Spec,CP movement step (SSAL), at the cost of losing Set A agreement (@cite{erlewine-2016}).

theorem CoonMateoPedroPreminger2014.af_mechanism_contrast : voiceAF.checksCase = true ∧ kaqVoice.checksCase = false

Q'anjob'al AF Voice checks case; Kaqchikel's regular Voice does NOT. This is the core parametric difference: Q'anjob'al's AF is a case-assigning repair, while Kaqchikel's AF is a locality repair.

theorem CoonMateoPedroPreminger2014.shared_phase_problem : Minimalist.voiceAgent.IsPhasal ∧ kaqVoice.IsPhasal

Both languages share the underlying problem: agentive Voice is a phase head, creating a locality boundary that traps the subject.

theorem CoonMateoPedroPreminger2014.both_have_extraction_asymmetries : Fragments.Mayan.Qanjobal.absPosition = Fragments.Mayan.ABSPosition.high ∧ Fragments.Mayan.Qanjobal.extractionProfile.Marks Typology.ExtractionTarget.subject ∧ Fragments.Mayan.Kaqchikel.kaqAFType = Fragments.Mayan.Kaqchikel.MayanAFType.afLanguage

Both Q'anjob'al and Kaqchikel are HIGH-ABS languages with extraction asymmetries: agent extraction is blocked without AF in both.

theorem CoonMateoPedroPreminger2014.both_af_lose_setA : Fragments.Mayan.Qanjobal.agentFocusForm.hasSetA = false ∧ Fragments.Mayan.Kaqchikel.VerbForm.agentFocus.hasSetA = false

Kaqchikel AF loses Set A agreement (the agent never enters Spec,TP). Q'anjob'al AF also loses Set A agreement. Same surface morphological effect, different underlying mechanism.