Gong (2022): Case in Wholesale Late Merger: Evidence from Mongolian Scrambling

This file formalizes [Gon22]'s argument that Condition C reconstruction in Mongolian scrambling tracks case rather than the A/Ā distinction or the subject status of the binder. Under [TH09]'s wholesale late merger a determiner moves alone and its restrictor merges countercyclically at a chain position where the resulting DP receives case, so scrambling bleeds Condition C exactly when the chain has a case position above the pronoun binder, the paper's condition (2) (Bleeds). The hybrid case rules (26) make accusative a dependent case, valued on an NP that an unmarked argumental NP of the same domain c-commands, nominative the case finite T assigns, and dative nonstructural (Site.DependentAcc, Site.Nominative). Read off the derivations (27b), (28b), (29c), (55), and (57), the chain positions of short, intermediate, and long-distance scrambling predict every judgment of the pool (rows_reconstruction): a dative binder is bled and a subject binder is not, while the embedded-subject binder of (61) is bled because the matrix VP-adjoined position competes for case with the matrix subject, which refutes [FLR96]'s Subject Binding Generalization (sbg_fails) and is what an account by movement type cannot state (is_not_uniform). The same dependent-case rule licenses accusative on an embedded subject exactly when a nominative matrix competitor is present, section 5.1 (acc_subjects), and the Mongolian grammar differs from [BV10]'s Sakha only in having no dependent dative (mongolian_differs_from_sakha_in_dat_only).

Implementation notes

Heights order the positions of a clause and, for clause-external scrambling, the matrix clause above the embedded one. A site records the arguments of its spell-out domain with the case they bear when the mover lands, so the presubject position sees a subject already valued nominative, the paper's assumption that case is valued as soon as its conditions are met. A lexically cased DP is licensed in its base position and a PP has no restrictor to late-merge, so neither can be bled. The CP edge of an embedded clause is a step of successive-cyclic movement without a case competitor.

References

• [Gon22]
• [TH09]
• [BV10]
• [FLR96]
• [Leb88]

The hybrid case rules (26) at a landing site

structure Gong2022.Arg : Type

An argumental NP of a spell-out domain: its height and the case it bears, if any, when the mover lands.

• height : ℕ
• valued : Option Case

@[instance_reducible]

instance Gong2022.instDecidableEqArg : DecidableEq Arg

Equations

• Gong2022.instDecidableEqArg = Gong2022.instDecidableEqArg.decEq

def Gong2022.instDecidableEqArg.decEq (x✝ x✝¹ : Arg) : Decidable (x✝ = x✝¹)

Equations

• Gong2022.instDecidableEqArg.decEq { height := a, valued := a_1 } { height := b, valued := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

@[instance_reducible]

instance Gong2022.instReprArg : Repr Arg

Equations

• Gong2022.instReprArg = { reprPrec := Gong2022.instReprArg.repr }

def Gong2022.instReprArg.repr : Arg → ℕ → Std.Format

Equations

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

structure Gong2022.Site : Type

A landing site of a scrambling chain: its height, the arguments of its spell-out domain, and whether it is the specifier finite T agrees into.

• height : ℕ
• domain : List Arg
• specTP : Bool

def Gong2022.instDecidableEqSite.decEq (x✝ x✝¹ : Site) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Gong2022.instDecidableEqSite : DecidableEq Site

Equations

• Gong2022.instDecidableEqSite = Gong2022.instDecidableEqSite.decEq

@[instance_reducible]

instance Gong2022.instReprSite : Repr Site

Equations

• Gong2022.instReprSite = { reprPrec := Gong2022.instReprSite.repr }

def Gong2022.instReprSite.repr : Site → ℕ → Std.Format

Equations

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

def Gong2022.Site.DependentAcc (s : Site) : Prop

(26a): an unmarked argument of the domain c-commands the site, so a DP there is valued accusative as a dependent case.

Equations

• s.DependentAcc = ∃ a ∈ s.domain, s.height < a.height ∧ a.valued = none

def Gong2022.Site.Nominative (s : Site) : Prop

(26b): finite T values a DP at its specifier nominative when no unmarked argument is closer to T.

Equations

• s.Nominative = (s.specTP = true ∧ ∀ a ∈ s.domain, s.height < a.height → a.valued ≠ none)

def Gong2022.Site.HasCase (s : Site) : Prop

A position where the late-merged restrictor's DP receives structural case.

Equations

• s.HasCase = (s.DependentAcc ∨ s.Nominative)

@[instance_reducible]

instance Gong2022.instDecidableDependentAcc (s : Site) : Decidable s.DependentAcc

Equations

• Gong2022.instDecidableDependentAcc s = Gong2022.instDecidableDependentAcc._aux_1 s

@[instance_reducible]

instance Gong2022.instDecidableNominative (s : Site) : Decidable s.Nominative

Equations

• Gong2022.instDecidableNominative s = { decide := decide (s.specTP = true) && decide (∀ a ∈ s.domain, s.height < a.height → a.valued ≠ none), reflects_decide := ⋯ }

@[instance_reducible]

instance Gong2022.instDecidableHasCase (s : Site) : Decidable s.HasCase

Equations

• Gong2022.instDecidableHasCase s = { decide := decide s.DependentAcc || decide s.Nominative, reflects_decide := ⋯ }

inductive Gong2022.Mover : Type

What scrambles: a DP with structural case, a DP with lexical dative, or a PP.

• dp : Mover
• lexicalDP : Mover
• pp : Mover

@[instance_reducible]

instance Gong2022.instDecidableEqMover : DecidableEq Mover

Equations

• Gong2022.instDecidableEqMover x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Gong2022.instReprMover.repr : Mover → ℕ → Std.Format

Equations

• Gong2022.instReprMover.repr Gong2022.Mover.dp prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Gong2022.Mover.dp")).group prec✝
• Gong2022.instReprMover.repr Gong2022.Mover.lexicalDP prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Gong2022.Mover.lexicalDP")).group prec✝
• Gong2022.instReprMover.repr Gong2022.Mover.pp prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Gong2022.Mover.pp")).group prec✝

@[instance_reducible]

instance Gong2022.instReprMover : Repr Mover

Equations

• Gong2022.instReprMover = { reprPrec := Gong2022.instReprMover.repr }

def Gong2022.Bleeds (m : Mover) (chain : List Site) (binder : ℕ) : Prop

Condition (2): scrambling bleeds Condition C when the mover is a DP whose restrictor can receive structural case at a chain position above the binder.

Equations

• Gong2022.Bleeds m chain binder = (m = Gong2022.Mover.dp ∧ Minimalist.LateMergerBleeds Gong2022.Site.HasCase Gong2022.Site.height chain binder)

@[instance_reducible]

instance Gong2022.instDecidableBleeds (m : Mover) (chain : List Site) (binder : ℕ) : Decidable (Bleeds m chain binder)

Equations

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

The positions of the paper's derivations

def Gong2022.subjectUnmarked : Arg

The subject at the edge of the verb phrase, unmarked until T merges, above the dative indirect object.

Equations

• Gong2022.subjectUnmarked = { height := 3, valued := none }

def Gong2022.io : Arg

The dative indirect object.

Equations

• Gong2022.io = { height := 1, valued := some Case.dat }

def Gong2022.vpEdge : Site

The VP-edge position of (27b) and (28b): between the subject and the indirect object, valued accusative by competition with the subject.

Equations

• Gong2022.vpEdge = { height := 2, domain := [Gong2022.subjectUnmarked, Gong2022.io] }

def Gong2022.presubject : Site

The presubject position of (29c): the subject below it is already nominative, and nothing c-commands it.

Equations

• Gong2022.presubject = { height := 4, domain := [{ height := 3, valued := some Case.nom }, Gong2022.io] }

def Gong2022.cpEdge : Site

The edge of the embedded CP, a step of successive-cyclic movement, (55b).

Equations

• Gong2022.cpEdge = { height := 4, domain := [] }

def Gong2022.matrixVP : Site

The matrix VP-adjoined position of (55c): above the matrix dative argument, below the matrix subject, which has not yet been valued.

Equations

• Gong2022.matrixVP = { height := 6, domain := [{ height := 7, valued := none }, { height := 5, valued := some Case.dat }] }

def Gong2022.matrixPresubject : Site

The matrix presubject position of (57): the matrix subject is nominative by then.

Equations

• Gong2022.matrixPresubject = { height := 8, domain := [{ height := 7, valued := some Case.nom }, { height := 5, valued := some Case.dat }] }

def Gong2022.specTP : Site

The specifier of finite T in the passive (85b): the agent is instrumental, the goal dative, so T values the derived subject nominative.

Equations

• Gong2022.specTP = { height := 4, domain := [{ height := 2, valued := some Case.inst }, Gong2022.io], specTP := true }

The Mongolian grammar of structural case (26)

def Gong2022.grammar : Minimalist.CaseAssigners

The Mongolian grammar of structural case: accusative on the lower of two NPs in the clause, nominative from T and genitive from D under Agree, and no dependent dative.

Equations

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

inductive Gong2022.DitransitiveArg : Type

The arguments of a ditransitive.

• subject : DitransitiveArg
• directObject : DitransitiveArg
• indirectObject : DitransitiveArg

@[instance_reducible]

instance Gong2022.instDecidableEqDitransitiveArg : DecidableEq DitransitiveArg

Equations

• Gong2022.instDecidableEqDitransitiveArg x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Gong2022.instReprDitransitiveArg : Repr DitransitiveArg

Equations

• Gong2022.instReprDitransitiveArg = { reprPrec := Gong2022.instReprDitransitiveArg.repr }

def Gong2022.instReprDitransitiveArg.repr : DitransitiveArg → ℕ → Std.Format

Equations

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

def Gong2022.DitransitiveArg.position : DitransitiveArg → Minimalist.PhasedNP

Their positions in a Mongolian ditransitive: the subject above the direct object, shifted to the clause edge, above the dative indirect object.

Equations

• Gong2022.DitransitiveArg.subject.position = { }
• Gong2022.DitransitiveArg.directObject.position = { phase := Minimalist.Cat.v, shifted := true }
• Gong2022.DitransitiveArg.indirectObject.position = { lexicalCase := some Case.dat, phase := Minimalist.Cat.v }

def Gong2022.ditransitive : List DitransitiveArg

A ditransitive's arguments, highest first.

Equations

• Gong2022.ditransitive = [Gong2022.DitransitiveArg.subject, Gong2022.DitransitiveArg.directObject, Gong2022.DitransitiveArg.indirectObject]

def Gong2022.ditransitiveCases : Case.Valuation DitransitiveArg (Case × Case.Mechanism)

Its cases, with finite T probing the clause.

Equations

• Gong2022.ditransitiveCases = Gong2022.grammar.assign Gong2022.DitransitiveArg.position [(Minimalist.Cat.T, Minimalist.Cat.C)] Gong2022.ditransitive

theorem Gong2022.do_gets_dependent_acc : Case.Valuation.valueOf DitransitiveArg.directObject ditransitiveCases = some (Case.acc, Case.Mechanism.dependent)

The direct object is valued accusative by the dependent rule, the subject being the caseless NP above it.

theorem Gong2022.subject_gets_nom_by_agree : Case.Valuation.valueOf DitransitiveArg.subject ditransitiveCases = some (Case.nom, Case.Mechanism.agree)

The subject is valued nominative by T, not by a dependent rule.

theorem Gong2022.io_has_lexical_case : Case.Valuation.valueOf DitransitiveArg.indirectObject ditransitiveCases = some (Case.dat, Case.Mechanism.lexical)

The indirect object keeps its lexical dative and neither competes for dependent case nor creates a case position.

theorem Gong2022.vpEdge_dependentAcc : vpEdge.DependentAcc ∧ ¬presubject.HasCase ∧ Option.map (fun (x : Case × Case.Mechanism) => x.2) (Case.Valuation.valueOf DitransitiveArg.directObject ditransitiveCases) = some Case.Mechanism.dependent

The VP edge is a dependent-case position, as the grammar values the shifted direct object of a ditransitive, and the presubject position is none.

The scrambling constructions and their chains

inductive Gong2022.Construction : Type

The scrambling constructions of the pool.

• SS : Construction

  Short scrambling, the direct object over the indirect object.

• IS : Construction

  Intermediate scrambling, an object to the presubject position.

• LDS : Construction

  Clause-external scrambling of an accusative embedded subject or of an embedded object, to the matrix presubject position.

• intermediate : Construction

  Clause-external scrambling stopping at the matrix VP-adjoined position, (58).

• IO : Construction

  Scrambling of the dative indirect object over the subject, (79).

• passive : Construction

  Passivization, (85).

@[instance_reducible]

instance Gong2022.instDecidableEqConstruction : DecidableEq Construction

Equations

• Gong2022.instDecidableEqConstruction x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Gong2022.instReprConstruction : Repr Construction

Equations

• Gong2022.instReprConstruction = { reprPrec := Gong2022.instReprConstruction.repr }

def Gong2022.instReprConstruction.repr : Construction → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Gong2022.instReprConstruction.repr Gong2022.Construction.SS prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Gong2022.Construction.SS")).group prec✝
• Gong2022.instReprConstruction.repr Gong2022.Construction.IS prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Gong2022.Construction.IS")).group prec✝
• Gong2022.instReprConstruction.repr Gong2022.Construction.LDS prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Gong2022.Construction.LDS")).group prec✝
• Gong2022.instReprConstruction.repr Gong2022.Construction.IO prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Gong2022.Construction.IO")).group prec✝

def Gong2022.Construction.chain : Construction → List Site

The chain positions each construction makes available, in the paper's derivations.

Equations

• Gong2022.Construction.SS.chain = [Gong2022.vpEdge]
• Gong2022.Construction.IS.chain = [Gong2022.vpEdge, Gong2022.presubject]
• Gong2022.Construction.IO.chain = [Gong2022.vpEdge, Gong2022.presubject]
• Gong2022.Construction.LDS.chain = [Gong2022.cpEdge, Gong2022.matrixVP, Gong2022.matrixPresubject]
• Gong2022.Construction.intermediate.chain = [Gong2022.cpEdge, Gong2022.matrixVP]
• Gong2022.Construction.passive.chain = [Gong2022.specTP]

inductive Gong2022.Binder : Type

The pronoun that binds the R-expression in the base order.

• io : Binder
• subject : Binder
• matrixDat : Binder
• matrixSubject : Binder
• embeddedSubject : Binder

@[instance_reducible]

instance Gong2022.instDecidableEqBinder : DecidableEq Binder

Equations

• Gong2022.instDecidableEqBinder x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Gong2022.instReprBinder.repr : Binder → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Gong2022.instReprBinder.repr Gong2022.Binder.io prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Gong2022.Binder.io")).group prec✝
• Gong2022.instReprBinder.repr Gong2022.Binder.subject prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Gong2022.Binder.subject")).group prec✝
• Gong2022.instReprBinder.repr Gong2022.Binder.matrixDat prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Gong2022.Binder.matrixDat")).group prec✝

@[instance_reducible]

instance Gong2022.instReprBinder : Repr Binder

Equations

• Gong2022.instReprBinder = { reprPrec := Gong2022.instReprBinder.repr }

def Gong2022.Binder.height : Binder → ℕ

The binder's height.

Equations

• Gong2022.Binder.io.height = 1
• Gong2022.Binder.subject.height = 3
• Gong2022.Binder.embeddedSubject.height = 3
• Gong2022.Binder.matrixDat.height = 5
• Gong2022.Binder.matrixSubject.height = 7

def Gong2022.Binder.IsSubject : Binder → Prop

Whether the binder is a subject, the Subject Binding Generalization's criterion.

Equations

• Gong2022.Binder.subject.IsSubject = True
• Gong2022.Binder.matrixSubject.IsSubject = True
• Gong2022.Binder.embeddedSubject.IsSubject = True
• Gong2022.Binder.io.IsSubject = False
• Gong2022.Binder.matrixDat.IsSubject = False

@[instance_reducible]

instance Gong2022.instDecidableIsSubject (b : Binder) : Decidable b.IsSubject

Equations

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

The pool

structure Gong2022.Row : Type

A scrambled order: its construction, the base-order binder, the mover, and the worst mark the paper prints on it (??/* counts as *).

• construction : Construction
• binder : Binder
• mover : Mover
• judgment : Judgment

@[instance_reducible]

instance Gong2022.instDecidableEqRow : DecidableEq Row

Equations

• Gong2022.instDecidableEqRow = Gong2022.instDecidableEqRow.decEq

def Gong2022.instDecidableEqRow.decEq (x✝ x✝¹ : Row) : Decidable (x✝ = x✝¹)

Equations

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

def Gong2022.instReprRow.repr : Row → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Gong2022.instReprRow : Repr Row

Equations

• Gong2022.instReprRow = { reprPrec := Gong2022.instReprRow.repr }

def Gong2022.Row.Reconstructs (r : Row) : Prop

The paper's obligatory reconstruction: the coindexed reading is rejected.

Equations

• r.Reconstructs = (r.judgment = Judgment.ungrammatical ∨ r.judgment = Judgment.unacceptable)

@[instance_reducible]

instance Gong2022.instDecidableReconstructs (r : Row) : Decidable r.Reconstructs

Equations

• Gong2022.instDecidableReconstructs r = { decide := decide (r.judgment = Judgment.ungrammatical) || decide (r.judgment = Judgment.unacceptable), reflects_decide := ⋯ }

def Gong2022.Row.ofDatum (ex : Datum) : Option Row

Equations

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

def Gong2022.rows : List Row

The scrambled orders (18b) to (21b), (32b), (33), (40), (41), (58), (61), (79), (85b), (86), (93b), and (94b).

Equations

• Gong2022.rows = List.filterMap Gong2022.Row.ofDatum Gong2022.Examples.all

theorem Gong2022.rows_reconstruction (r : Row) : r ∈ rows → (r.Reconstructs ↔ ¬Bleeds r.mover r.construction.chain r.binder.height)

Condition (2) with the hybrid case rules predicts every judgment: reconstruction is obligatory exactly when no chain position above the binder receives case.

theorem Gong2022.is_not_uniform : ∃ r₁ ∈ rows, ∃ r₂ ∈ rows, r₁.construction = Construction.IS ∧ r₂.construction = Construction.IS ∧ r₁.mover = Mover.dp ∧ r₂.mover = Mover.dp ∧ ¬r₁.Reconstructs ∧ r₂.Reconstructs

Section 2.3: intermediate scrambling of a DP to one landing site reconstructs in (20b) but not in (19b), so no classification of the movement as A or Ā decides reconstruction.

theorem Gong2022.sbg_fails : (∀ r ∈ rows, r.construction = Construction.SS ∨ r.construction = Construction.IS → (r.Reconstructs ↔ r.binder.IsSubject)) ∧ (∃ r ∈ rows, r.binder = Binder.embeddedSubject ∧ r.mover = Mover.dp ∧ ¬r.Reconstructs) ∧ ∃ r ∈ rows, ¬r.binder.IsSubject ∧ r.Reconstructs

Section 4.2: the Subject Binding Generalization (24) fits the clause-internal data, but (61), where the embedded subject binds, is bled because the matrix VP-adjoined position competes for case with the matrix subject; and the PP of (94b) reconstructs under a dative binder.

Section 5.1: accusative on embedded subjects

inductive Gong2022.Competitor : Type

The matrix argument that could compete with the embedded subject for case.

• nom : Competitor
• dat : Competitor
• absent : Competitor

@[instance_reducible]

instance Gong2022.instDecidableEqCompetitor : DecidableEq Competitor

Equations

• Gong2022.instDecidableEqCompetitor x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Gong2022.instReprCompetitor.repr : Competitor → ℕ → Std.Format

Equations

• Gong2022.instReprCompetitor.repr Gong2022.Competitor.nom prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Gong2022.Competitor.nom")).group prec✝
• Gong2022.instReprCompetitor.repr Gong2022.Competitor.dat prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Gong2022.Competitor.dat")).group prec✝
• Gong2022.instReprCompetitor.repr Gong2022.Competitor.absent prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Gong2022.Competitor.absent")).group prec✝

@[instance_reducible]

instance Gong2022.instReprCompetitor : Repr Competitor

Equations

• Gong2022.instReprCompetitor = { reprPrec := Gong2022.instReprCompetitor.repr }

def Gong2022.Competitor.site : Competitor → Site

The embedded subject at the edge of its clause, in the matrix domain: the site (26a) evaluates.

Equations

• Gong2022.Competitor.nom.site = { height := 4, domain := [{ height := 7, valued := none }] }
• Gong2022.Competitor.dat.site = { height := 4, domain := [{ height := 7, valued := some Case.dat }] }
• Gong2022.Competitor.absent.site = { height := 4, domain := [] }

structure Gong2022.AccRow : Type

An accusative-marked embedded subject with its matrix competitor and judgment.

• competitor : Competitor
• judgment : Judgment

def Gong2022.instDecidableEqAccRow.decEq (x✝ x✝¹ : AccRow) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Gong2022.instDecidableEqAccRow : DecidableEq AccRow

Equations

• Gong2022.instDecidableEqAccRow = Gong2022.instDecidableEqAccRow.decEq

def Gong2022.instReprAccRow.repr : AccRow → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Gong2022.instReprAccRow : Repr AccRow

Equations

• Gong2022.instReprAccRow = { reprPrec := Gong2022.instReprAccRow.repr }

def Gong2022.AccRow.ofDatum (ex : Datum) : Option AccRow

Equations

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

def Gong2022.accRows : List AccRow

(47), (48), (63), (64), and (65).

Equations

• Gong2022.accRows = List.filterMap Gong2022.AccRow.ofDatum Gong2022.Examples.all

theorem Gong2022.acc_subjects (r : AccRow) : r ∈ accRows → (r.judgment = Judgment.acceptable ↔ r.competitor.site.DependentAcc)

Accusative on the embedded subject is licensed exactly when an unmarked matrix argument c-commands it: a nominative subject competes, a dative or impersonal predicate's argument does not.

Section 5.3: dative is not a dependent case

theorem Gong2022.mongolian_differs_from_sakha_in_dat_only : (grammar.rules Minimalist.Cat.v = have __src := BakerVinokurova2010.grammar.rules Minimalist.Cat.v; { low := __src.low, unmarked := __src.unmarked }) ∧ grammar.rules Minimalist.Cat.C = BakerVinokurova2010.grammar.rules Minimalist.Cat.C ∧ grammar.agree = BakerVinokurova2010.grammar.agree

Mongolian differs from Sakha in the verb phrase's high case alone: no dependent dative.

inductive Gong2022.SakhaArg : Type

The arguments of a Sakha ditransitive.

• subject : SakhaArg
• goal : SakhaArg
• theme : SakhaArg

@[instance_reducible]

instance Gong2022.instDecidableEqSakhaArg : DecidableEq SakhaArg

Equations

• Gong2022.instDecidableEqSakhaArg x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Gong2022.instReprSakhaArg : Repr SakhaArg

Equations

• Gong2022.instReprSakhaArg = { reprPrec := Gong2022.instReprSakhaArg.repr }

def Gong2022.instReprSakhaArg.repr : SakhaArg → ℕ → Std.Format

Equations

• Gong2022.instReprSakhaArg.repr Gong2022.SakhaArg.subject prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Gong2022.SakhaArg.subject")).group prec✝
• Gong2022.instReprSakhaArg.repr Gong2022.SakhaArg.goal prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Gong2022.SakhaArg.goal")).group prec✝
• Gong2022.instReprSakhaArg.repr Gong2022.SakhaArg.theme prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Gong2022.SakhaArg.theme")).group prec✝

def Gong2022.SakhaArg.position : SakhaArg → Minimalist.PhasedNP

Their positions: a subject, a VP-internal goal, and a theme shifted to the phase edge.

Equations

• Gong2022.SakhaArg.subject.position = { }
• Gong2022.SakhaArg.goal.position = { phase := Minimalist.Cat.v }
• Gong2022.SakhaArg.theme.position = { phase := Minimalist.Cat.v, shifted := true }

def Gong2022.sakhaDitransitive : List SakhaArg

The Sakha ditransitive, highest first.

Equations

• Gong2022.sakhaDitransitive = [Gong2022.SakhaArg.subject, Gong2022.SakhaArg.goal, Gong2022.SakhaArg.theme]

theorem Gong2022.mongolian_derives_no_dative : (∀ s ∈ grammar.assign SakhaArg.position [(Minimalist.Cat.T, Minimalist.Cat.C)] sakhaDitransitive, Option.map (fun (x : Case × Case.Mechanism) => x.1) s.2 ≠ some Case.dat) ∧ Option.map (fun (x : Case × Case.Mechanism) => x.1) (Case.Valuation.valueOf SakhaArg.goal (grammar.assign SakhaArg.position [(Minimalist.Cat.T, Minimalist.Cat.C)] sakhaDitransitive)) ≠ Option.map (fun (x : Case × Case.Mechanism) => x.1) (Case.Valuation.valueOf SakhaArg.goal (BakerVinokurova2010.grammar.assign SakhaArg.position [(Minimalist.Cat.T, Minimalist.Cat.C)] sakhaDitransitive))

The Mongolian grammar values no NP of the Sakha ditransitive dative, so the goal Sakha values dative comes out otherwise: the dative of a Mongolian goal is nonstructural.