Case Discrimination in Agreement @cite{preminger-2014}

@cite{bobaljik-2008} @cite{scott-2023}

@cite{preminger-2014} formalizes the Moravcsik hierarchy: agreement is case-discriminating — probes are sensitive to the case of their potential targets.

The Moravcsik Hierarchy

Case accessibility for agreement is ordered:

unmarked > dependent > lexical/oblique

Where:

• Unmarked: NOM (in nom-acc systems) or ABS (in erg-abs systems)
• Dependent: ACC (in nom-acc) or ERG (in erg-abs)
• Lexical: DAT, GEN, PP-governed, etc.

Agreement targets DPs at or above a threshold in this hierarchy. The threshold is a contiguous prefix: {unmarked}, {unmarked, dependent}, or {all}. Crucially, a probe CANNOT target dependent-case DPs without also targeting unmarked-case DPs.

The Typological Gap

The hierarchy predicts an asymmetry:

• NOM-ACC case + NOM-ACC agreement: ✓ (English, French)
• ERG-ABS case + ERG-ABS agreement: ✓ (Basque, Georgian)
• ERG-ABS case + NOM-ACC agreement: ✓ (Hindi split-ERG)
• NOM-ACC case + ERG-ABS agreement: ✗ (UNATTESTED)

The gap follows from contiguity: in a NOM-ACC system, A and S both receive NOM (unmarked). Any probe that sees P (ACC = dependent) also sees A (NOM = unmarked ≥ dependent). So you cannot target S and P (= ABS-like) without also targeting A — ruling out ERG-ABS agreement.

Dative Intervention as Failed Agreement (§8.4)

When a dative DP intervenes between a probe and its intended target:

1. The probe encounters the dative's phi-features (minimality)
2. But the dative bears lexical case (below the threshold)
3. The probe cannot successfully Agree with the dative
4. The probe also cannot "look past" the dative (locality)
5. Result: the probe FAILS → default agreement surfaces

This unifies dative intervention with Kichean AF: both are instances of obligatory agreement failing without crashing (Ch. 5).

inductive Minimalism.CaseAccessibility : Type

Case accessibility for agreement.

The hierarchy determines which DPs are visible to agreement probes. Higher accessibility = more likely to be targeted by a probe.

• unmarked : CaseAccessibility

  Unmarked case: NOM (nom-acc) or ABS (erg-abs). Highest.

• dependent : CaseAccessibility

  Dependent case: ACC (nom-acc) or ERG (erg-abs). Middle.

• lexical : CaseAccessibility

  Lexical/oblique case: DAT, GEN, PP, etc. Lowest.

instance Minimalism.instDecidableEqCaseAccessibility : DecidableEq CaseAccessibility

Equations

• Minimalism.instDecidableEqCaseAccessibility x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Minimalism.instBEqCaseAccessibility.beq : CaseAccessibility → CaseAccessibility → Bool

Equations

• Minimalism.instBEqCaseAccessibility.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Minimalism.instBEqCaseAccessibility : BEq CaseAccessibility

Equations

• Minimalism.instBEqCaseAccessibility = { beq := Minimalism.instBEqCaseAccessibility.beq }

def Minimalism.instReprCaseAccessibility.repr : CaseAccessibility → Nat → Std.Format

Equations

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

instance Minimalism.instReprCaseAccessibility : Repr CaseAccessibility

Equations

• Minimalism.instReprCaseAccessibility = { reprPrec := Minimalism.instReprCaseAccessibility.repr }

def Minimalism.CaseAccessibility.rank : CaseAccessibility → Nat

Numeric rank for ordering. Higher = more accessible.

Equations

• Minimalism.CaseAccessibility.unmarked.rank = 2
• Minimalism.CaseAccessibility.dependent.rank = 1
• Minimalism.CaseAccessibility.lexical.rank = 0

def Minimalism.caseAccessible (dpLevel threshold : CaseAccessibility) : Bool

Is a DP with this case level accessible to a probe with the given threshold? Contiguity: a DP is accessible iff its level is at or above the threshold.

Equations

• Minimalism.caseAccessible dpLevel threshold = decide (dpLevel.rank ≥ threshold.rank)

structure Minimalism.CaseAlignment : Type

A case alignment maps argument positions (S, A, P) to case accessibility levels.

• S: intransitive subject (sole argument)
• A: transitive agent (external argument)
• P: transitive patient (internal argument)

• sLevel : CaseAccessibility

  Case accessibility of the intransitive subject.

• aLevel : CaseAccessibility

  Case accessibility of the transitive agent.

• pLevel : CaseAccessibility

  Case accessibility of the transitive patient.

def Minimalism.instReprCaseAlignment.repr : CaseAlignment → Nat → Std.Format

Equations

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

instance Minimalism.instReprCaseAlignment : Repr CaseAlignment

Equations

• Minimalism.instReprCaseAlignment = { reprPrec := Minimalism.instReprCaseAlignment.repr }

def Minimalism.nomAcc : CaseAlignment

Nominative-accusative alignment: S and A both get unmarked (NOM), P gets dependent (ACC).

Equations

• Minimalism.nomAcc = { sLevel := Minimalism.CaseAccessibility.unmarked, aLevel := Minimalism.CaseAccessibility.unmarked, pLevel := Minimalism.CaseAccessibility.dependent }

def Minimalism.ergAbs : CaseAlignment

Ergative-absolutive alignment: S and P both get unmarked (ABS), A gets dependent (ERG).

Equations

• Minimalism.ergAbs = { sLevel := Minimalism.CaseAccessibility.unmarked, aLevel := Minimalism.CaseAccessibility.dependent, pLevel := Minimalism.CaseAccessibility.unmarked }

def Minimalism.tripartite : CaseAlignment

Tripartite alignment: S gets unmarked (ABS), A gets dependent (ERG), P gets dependent (ACC). Mam.

Equations

• Minimalism.tripartite = { sLevel := Minimalism.CaseAccessibility.unmarked, aLevel := Minimalism.CaseAccessibility.dependent, pLevel := Minimalism.CaseAccessibility.dependent }

structure Minimalism.AgreementPattern : Type

Agreement pattern: which argument positions trigger agreement.

• sAgrees : Bool
• aAgrees : Bool
• pAgrees : Bool

instance Minimalism.instDecidableEqAgreementPattern : DecidableEq AgreementPattern

Equations

• Minimalism.instDecidableEqAgreementPattern = Minimalism.instDecidableEqAgreementPattern.decEq

def Minimalism.instDecidableEqAgreementPattern.decEq (x✝ x✝¹ : AgreementPattern) : Decidable (x✝ = x✝¹)

Equations

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

def Minimalism.instBEqAgreementPattern.beq : AgreementPattern → AgreementPattern → Bool

Equations

• Minimalism.instBEqAgreementPattern.beq { sAgrees := a, aAgrees := a_1, pAgrees := a_2 } { sAgrees := b, aAgrees := b_1, pAgrees := b_2 } = (a == b && (a_1 == b_1 && a_2 == b_2))
• Minimalism.instBEqAgreementPattern.beq x✝¹ x✝ = false

instance Minimalism.instBEqAgreementPattern : BEq AgreementPattern

Equations

• Minimalism.instBEqAgreementPattern = { beq := Minimalism.instBEqAgreementPattern.beq }

def Minimalism.instReprAgreementPattern.repr : AgreementPattern → Nat → Std.Format

Equations

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

instance Minimalism.instReprAgreementPattern : Repr AgreementPattern

Equations

• Minimalism.instReprAgreementPattern = { reprPrec := Minimalism.instReprAgreementPattern.repr }

def Minimalism.agreementFromThreshold (ca : CaseAlignment) (threshold : CaseAccessibility) : AgreementPattern

Given a case alignment and an accessibility threshold, compute which argument positions are visible to the probe.

Equations

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

def Minimalism.AgreementPattern.isErgAbs (ap : AgreementPattern) : Bool

Is this agreement pattern ergative-absolutive? S and P agree, A does not (S=P≠A).

Equations

• ap.isErgAbs = (ap.sAgrees && ap.pAgrees && !ap.aAgrees)

def Minimalism.AgreementPattern.isNomAcc (ap : AgreementPattern) : Bool

Is this agreement pattern nominative-accusative? S and A agree, P does not (S=A≠P).

Equations

• ap.isNomAcc = (ap.sAgrees && ap.aAgrees && !ap.pAgrees)

def Minimalism.thresholds : List CaseAccessibility

The three possible thresholds.

Equations

• Minimalism.thresholds = [Minimalism.CaseAccessibility.unmarked, Minimalism.CaseAccessibility.dependent, Minimalism.CaseAccessibility.lexical]

theorem Minimalism.nomAcc_a_equals_s (threshold : CaseAccessibility) : (agreementFromThreshold nomAcc threshold).aAgrees = (agreementFromThreshold nomAcc threshold).sAgrees

With NOM-ACC case, A always agrees whenever S agrees (both have unmarked = NOM). Therefore, the pattern S=P≠A (ergative-absolutive agreement) is impossible: you cannot target S without also targeting A.

This is @cite{bobaljik-2008}'s typological gap: NOM-ACC case + ERG-ABS agreement is unattested.

theorem Minimalism.nomAcc_no_ergAbs_agreement (threshold : CaseAccessibility) : (agreementFromThreshold nomAcc threshold).isErgAbs = false

Corollary: ERG-ABS agreement is impossible with NOM-ACC case. No threshold produces S=P≠A under NOM-ACC alignment.

theorem Minimalism.ergAbs_unmarked_yields_abs_agreement : (agreementFromThreshold ergAbs CaseAccessibility.unmarked).isErgAbs = true

With ERG-ABS case, threshold = unmarked yields ABS agreement: S and P agree (both have ABS = unmarked), A does not (ERG = dependent, below threshold). This is ergative-absolutive agreement.

theorem Minimalism.ergAbs_dependent_yields_all : have ap := agreementFromThreshold ergAbs CaseAccessibility.dependent; ap.sAgrees = true ∧ ap.aAgrees = true ∧ ap.pAgrees = true

With ERG-ABS case, threshold = dependent yields agreement with ALL arguments (S, A, P all accessible).

theorem Minimalism.contiguity_unmarked_dependent (threshold : CaseAccessibility) : caseAccessible CaseAccessibility.dependent threshold = true → caseAccessible CaseAccessibility.unmarked threshold = true

Contiguity: if a DP with dependent case is accessible, then any DP with unmarked case is also accessible (unmarked > dependent).

theorem Minimalism.contiguity_lexical (threshold : CaseAccessibility) : caseAccessible CaseAccessibility.lexical threshold = true → caseAccessible CaseAccessibility.dependent threshold = true ∧ caseAccessible CaseAccessibility.unmarked threshold = true

Contiguity: if a DP with lexical case is accessible, then DPs with dependent and unmarked case are also accessible.

structure Minimalism.DativeInterventionContext : Type

Dative intervention: a dative DP blocks the probe's search.

Components:

• dativePresent: a dative DP intervenes between probe and goal
• threshold: the probe's case accessibility threshold
• targetLevel: the case level of the intended goal

• dativePresent : Bool

  A dative (lexical case) DP intervenes.

• threshold : CaseAccessibility

  The probe's case accessibility threshold.

• targetLevel : CaseAccessibility

  Case level of the intended agreement target.

def Minimalism.instReprDativeInterventionContext.repr : DativeInterventionContext → Nat → Std.Format

Equations

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

instance Minimalism.instReprDativeInterventionContext : Repr DativeInterventionContext

Equations

• Minimalism.instReprDativeInterventionContext = { reprPrec := Minimalism.instReprDativeInterventionContext.repr }

def Minimalism.dativeVisibleToProbe (threshold : CaseAccessibility) : Bool

Is the dative visible to the probe? Only if the threshold is low enough to include lexical case.

Equations

• Minimalism.dativeVisibleToProbe threshold = Minimalism.caseAccessible Minimalism.CaseAccessibility.lexical threshold

def Minimalism.dativeIntervenes (ctx : DativeInterventionContext) : Bool

Does dative intervention cause agreement failure?

The dative intervenes (blocks the probe by locality/minimality) if it has matching phi-features. But it cannot be a valid goal because its case (lexical) is below the threshold. The probe fails without crashing.

This is modeled as: if a dative is present AND the dative's case is below the threshold (so the probe can't Agree with it) AND the dative blocks access to the real target by minimality, then agreement fails.

Equations

• Minimalism.dativeIntervenes ctx = (ctx.dativePresent && !Minimalism.dativeVisibleToProbe ctx.threshold)

theorem Minimalism.dative_blocks_at_unmarked : dativeIntervenes { dativePresent := true, threshold := CaseAccessibility.unmarked, targetLevel := CaseAccessibility.unmarked } = true

With a standard threshold (unmarked or dependent), a dative DP causes intervention: it blocks the probe but cannot be agreed with.

theorem Minimalism.dative_blocks_at_dependent : dativeIntervenes { dativePresent := true, threshold := CaseAccessibility.dependent, targetLevel := CaseAccessibility.unmarked } = true

theorem Minimalism.dative_no_intervention_at_lexical : dativeIntervenes { dativePresent := true, threshold := CaseAccessibility.lexical, targetLevel := CaseAccessibility.unmarked } = false

If the threshold includes lexical case, the dative does NOT intervene — it becomes a valid agreement target.

def Minimalism.kaqCaseAlignment : CaseAlignment

Kaqchikel has ergative-absolutive alignment: S and P get ABS (unmarked), A gets ERG (dependent).

Equations

• Minimalism.kaqCaseAlignment = Minimalism.ergAbs

theorem Minimalism.kaq_abs_agreement : (agreementFromThreshold kaqCaseAlignment CaseAccessibility.unmarked).sAgrees = true ∧ (agreementFromThreshold kaqCaseAlignment CaseAccessibility.unmarked).pAgrees = true ∧ (agreementFromThreshold kaqCaseAlignment CaseAccessibility.unmarked).aAgrees = false

Under Kaqchikel's alignment with threshold = unmarked, agreement targets S and P (Set B / absolutive agreement) but not A. This is consistent with the Set B (ABS) paradigm.

theorem Minimalism.kaq_erg_agreement_threshold : (agreementFromThreshold kaqCaseAlignment CaseAccessibility.dependent).aAgrees = true

Kaqchikel Set A agreement targets A (ERG): this requires a separate probe (Voice/v) with threshold = dependent, which sees both unmarked and dependent case DPs.