Mongolian Case System

@cite{gong-2022} @cite{baker-vinokurova-2010}

Mongolian (Khalkha/Chakhar) uses a hybrid case assignment system:

• Accusative: dependent case, assigned when two argumental NPs in the same phase compete and the higher NP c-commands the lower one (following @cite{baker-vinokurova-2010}'s analysis of Sakha)
• Nominative: assigned by finite T via Agree
• Dative: nonstructural (inherent) case

This hybrid system is the key to understanding Condition C reconstruction effects in Mongolian scrambling (@cite{gong-2022}): because ACC is a dependent case, it can be assigned at intermediate positions on a scrambling chain (wherever a case competitor exists), providing the case positions needed for Wholesale Late Merger.

Scrambling types

Mongolian has three clause-internal scrambling types (short, intermediate, long-distance) and two clause-external types (subject and object cross-clausal). All behave like A-movement in terms of anaphor binding and WCO amelioration, but differ in Condition C reconstruction — tracking case positions, not the A/A-bar distinction.

Case assignment rules

@cite{gong-2022} (26)/(84): a. If two distinct argumental NPs in the same phase are such that NP1 c-commands NP2, value NP2 as ACC, unless NP1 is already marked for case. b. NOM is assigned by finite T. c. DAT is a nonstructural case.

def Fragments.Mongolian.Case.mongolianCaseConfig : Syntax.Case.CaseSystemConfig

Mongolian case system: accusative alignment with Agree-based NOM and nonstructural DAT.

Equations

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

theorem Fragments.Mongolian.Case.mongolian_is_accusative : mongolianCaseConfig.langType = Syntax.Case.CaseLanguageType.accusative

theorem Fragments.Mongolian.Case.mongolian_nom_is_agree : mongolianCaseConfig.nomMode = Syntax.Case.NomAssignment.agreeT

theorem Fragments.Mongolian.Case.mongolian_dat_is_nonstructural : mongolianCaseConfig.datMode = Syntax.Case.DatAssignment.nonstructural

inductive Fragments.Mongolian.Case.ScrambleType : Type

Scrambling types in Mongolian, classified by distance and landing site. @cite{gong-2022} section 2.

• SS : ScrambleType

  Short scrambling: DO moves past IO within the clause.

• IS : ScrambleType

  Intermediate scrambling: DO moves past the subject to pre-subject position within the clause.

• LDS : ScrambleType

  Long-distance scrambling: an argument moves out of an embedded finite clause into the matrix clause.

@[implicit_reducible]

instance Fragments.Mongolian.Case.instDecidableEqScrambleType : DecidableEq ScrambleType

Equations

• Fragments.Mongolian.Case.instDecidableEqScrambleType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Fragments.Mongolian.Case.instReprScrambleType.repr : ScrambleType → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Fragments.Mongolian.Case.instReprScrambleType : Repr ScrambleType

Equations

• Fragments.Mongolian.Case.instReprScrambleType = { reprPrec := Fragments.Mongolian.Case.instReprScrambleType.repr }

inductive Fragments.Mongolian.Case.BinderRole : Type

The grammatical role of the pronoun binder in the base order. This determines which case the binder bears, which in turn determines the structural height of the binder and whether a dependent ACC position exists above it.

• io : BinderRole

  Indirect object binder (bears DAT, nonstructural).

• subject : BinderRole

  Subject binder (bears NOM, assigned by T).

@[implicit_reducible]

instance Fragments.Mongolian.Case.instDecidableEqBinderRole : DecidableEq BinderRole

Equations

• Fragments.Mongolian.Case.instDecidableEqBinderRole x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Fragments.Mongolian.Case.instReprBinderRole.repr : BinderRole → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Fragments.Mongolian.Case.instReprBinderRole : Repr BinderRole

Equations

• Fragments.Mongolian.Case.instReprBinderRole = { reprPrec := Fragments.Mongolian.Case.instReprBinderRole.repr }

def Fragments.Mongolian.Case.caseInventory : Finset Core.Case

Mongolian case inventory. NOM, ACC, GEN, DAT, ABL, INST, COM. @cite{gong-2022}: the cases relevant to scrambling and WLM are NOM (Agree-based), ACC (dependent), and DAT (nonstructural).

Note: Mongolian lacks a dedicated locative suffix (LOC is expressed via postpositions like deer 'on'), creating a Blake hierarchy gap at rank 3 between DAT (rank 4) and ABL/INST (rank 2). This is a known counterexample to strict hierarchy contiguity.

Equations

• Fragments.Mongolian.Case.caseInventory = {UD.Case.nom, UD.Case.acc, UD.Case.gen, UD.Case.dat, UD.Case.abl, UD.Case.inst, UD.Case.com}

def Fragments.Mongolian.Case.mongolianLangType : Syntax.Case.CaseLanguageType

Mongolian is an accusative language.

Equations

• Fragments.Mongolian.Case.mongolianLangType = Syntax.Case.CaseLanguageType.accusative

def Fragments.Mongolian.Case.ditransSubject : Syntax.Case.NPInDomain

A Mongolian ditransitive clause has three argumental NPs in the spell-out domain: Subject > DO > IO. The IO bears DAT (nonstructural, so lexically assigned). Subject and DO compete for dependent case.

Equations

• Fragments.Mongolian.Case.ditransSubject = { label := "subject", lexicalCase := none }

def Fragments.Mongolian.Case.ditransDO : Syntax.Case.NPInDomain

Equations

• Fragments.Mongolian.Case.ditransDO = { label := "DO", lexicalCase := none }

def Fragments.Mongolian.Case.ditransIO : Syntax.Case.NPInDomain

Equations

• Fragments.Mongolian.Case.ditransIO = { label := "IO", lexicalCase := some UD.Case.dat }

theorem Fragments.Mongolian.Case.do_gets_dependent_acc : Syntax.Case.dependentAccusative [ditransSubject] ditransDO = some UD.Case.acc

Dependent ACC is available for the DO: the subject is a caseless NP above it, so dependentAccusative succeeds. This is the key fact that enables WLM above the IO binder.

theorem Fragments.Mongolian.Case.subject_gets_unmarked : Syntax.Case.dependentAccusative [] ditransSubject = none

The subject gets NOM (unmarked in an accusative language with no higher competitor). There is no dependent case position above it.

theorem Fragments.Mongolian.Case.io_has_lexical_case : ditransIO.lexicalCase = some UD.Case.dat

IO bears DAT (lexical/nonstructural), so it does not compete for dependent case and does not create a case position.

def Fragments.Mongolian.Case.ioHeight : ℕ

Structural height encoding for Mongolian clause positions. Higher numbers = structurally higher positions.

Equations

• Fragments.Mongolian.Case.ioHeight = 1

def Fragments.Mongolian.Case.subjectHeight : ℕ

Equations

• Fragments.Mongolian.Case.subjectHeight = 2

def Fragments.Mongolian.Case.specVPHeight : ℕ

Equations

• Fragments.Mongolian.Case.specVPHeight = 3

def Fragments.Mongolian.Case.casePositionsAbove (role : BinderRole) : List Minimalist.ChainPosition

Case positions available on a scrambling chain in Mongolian.

These are derived from the dependent case algorithm, not stipulated:

• Above IO: dependentAccusative [subject] do = some .acc (theorem do_gets_dependent_acc), so Spec,VP is a case position
• Above Subject: dependentAccusative [] subject = none (theorem subject_gets_unmarked), so no case position exists

Equations

• Fragments.Mongolian.Case.casePositionsAbove Fragments.Mongolian.Case.BinderRole.io = [{ height := Fragments.Mongolian.Case.specVPHeight, caseAvailable := true }]
• Fragments.Mongolian.Case.casePositionsAbove Fragments.Mongolian.Case.BinderRole.subject = []

def Fragments.Mongolian.Case.binderHeight (role : BinderRole) : ℕ

Binder height from its grammatical role.

Equations

• Fragments.Mongolian.Case.binderHeight Fragments.Mongolian.Case.BinderRole.io = Fragments.Mongolian.Case.ioHeight
• Fragments.Mongolian.Case.binderHeight Fragments.Mongolian.Case.BinderRole.subject = Fragments.Mongolian.Case.subjectHeight

def Fragments.Mongolian.Case.predictsReconstruction (role : BinderRole) : Bool

Whether WLM predicts Condition C reconstruction in a given scenario. This is the central prediction of @cite{gong-2022}: reconstruction tracks case positions, not scrambling type or A/A-bar status.

Equations

• Fragments.Mongolian.Case.predictsReconstruction role = Minimalist.wlmForcesReconstruction (Fragments.Mongolian.Case.casePositionsAbove role) (Fragments.Mongolian.Case.binderHeight role)

theorem Fragments.Mongolian.Case.io_binder_no_reconstruction : predictsReconstruction BinderRole.io = false

Scrambling over IO: WLM bleeds Condition C. @cite{gong-2022} (4), (18b), (27): dependent ACC is available at Spec,VP (derived from do_gets_dependent_acc), so the NP restrictor can merge above the IO binder without violating Condition C.

theorem Fragments.Mongolian.Case.subject_binder_forces_reconstruction : predictsReconstruction BinderRole.subject = true

Scrambling over Subject: WLM forces Condition C reconstruction. @cite{gong-2022} (3), (20), (21), (29): no dependent case position exists above the subject (derived from subject_gets_unmarked), so the NP restrictor must merge below the subject binder.

def Fragments.Mongolian.Case.ppReconstructsOverIO : Bool

PP-scrambling always forces Condition C reconstruction. PPs lack the DP-internal structure (determiner + NP restrictor) required for WLM. @cite{gong-2022} (93)-(94): scrambling of PPs headed by esreg 'against' always shows obligatory reconstruction, regardless of whether the binder is an IO or Subject.

Equations

• Fragments.Mongolian.Case.ppReconstructsOverIO = Minimalist.ppAlwaysReconstructs

def Fragments.Mongolian.Case.ppReconstructsOverSubj : Bool

Equations

• Fragments.Mongolian.Case.ppReconstructsOverSubj = Minimalist.ppAlwaysReconstructs

theorem Fragments.Mongolian.Case.pp_always_reconstructs_io : ppReconstructsOverIO = true

theorem Fragments.Mongolian.Case.pp_always_reconstructs_subj : ppReconstructsOverSubj = true