Nested Agree and apparent minimality violations: [Ama25]

[Ama25] derives apparent minimality violations from Nested Agree (Definition (1)): the probes on a head are extrinsically ordered, and a later probe must exploit the dependency an earlier one established, so its search starts from the earlier probe's goal — everything the head c-commands above that goal lies outside its domain, and a structurally closer matching goal is skipped with minimality respected at every step. run is that engine on the substrate's FeatureBundle slots and Probe.search: a probe's domain is the c-command-ordered list of accessible heads (the paper's own notation in (6), (8), (32), (34)), read off a projection spine by domain, which stops at a phase head's complement (PIC); a valued probe (a case assigner, [∗Infl:perf∗]) matches only an unvalued slot and values its goal, an unvalued probe matches any specified slot and is valued by an active goal (fn. 23, defective intervention).

The paper's derivations then run as stated: Standard Italian auxiliary selection ((9)–(20), over the substrate's TransitivityClass and impersonal/passive Voice.Flavor) under the Vocabulary Items (14), the Ariellese and Tufillese orderings and entries (22)–(24), the ditransitive case/agreement alignments (25)–(28) with [Bar24]'s typological gap, Icelandic DAT-NOM (29a/b), Lak perfective agreement (32), Spanish VOS (34), Bulgarian multiple wh-fronting (36), and Hindi-Urdu (38)–(40). Out of scope: Merge and binding inside v's cycle (the SCC ordering of (16)–(17) enters as v's input), participle agreement (§4.3.2), and the Appendix's comparison with MME, Multitasking and ECoMPS.

The engine

@[reducible, inline]

abbrev Amato2025.State (H : Type u_2) : Type u_2

The feature state of a derivation assigns every head its bundle.

Equations

• Amato2025.State H = (H → Minimalist.FeatureBundle)

structure Amato2025.Layer (H : Type u_2) : Type u_2

A projection has its specifiers, highest first, over its head.

• specs : List H
• head : H

def Amato2025.domain {H : Type u_1} (phase : H → Bool) : List (Layer H) → List H

The heads a probe above these projections can reach, in c-command order — each projection's specifiers then its head, down to and including the first phase head, whose complement the PIC freezes.

Equations

• Amato2025.domain phase [] = []
• Amato2025.domain phase (l :: ls) = l.specs ++ l.head :: if phase l.head = true then [] else Amato2025.domain phase ls

def Amato2025.goalMatches {H : Type u_1} (s : State H) (α : H) (t : Minimalist.FeatureType) (g : H) : Bool

Goal g matches the probe at dimension t on α (fn. 23): an unvalued probe matches any specified slot — an unvalued one too, defective intervention — while a valued probe (a case assigner, [∗Infl:perf∗]) matches only an unvalued slot, so a DP whose case is already valued is invisible to case assignment.

Equations

• Amato2025.goalMatches s α t g = match s α t with | some none => (s g t).isSpecified | some (some val) => (s g t).isUnvalued | none => false

def Amato2025.agree {H : Type u_1} [DecidableEq H] (act : H → Minimalist.FeatureType → Bool) (s : State H) (α : H) (t : Minimalist.FeatureType) (g : H) : State H

In Agree between α and its goal g at t, an unvalued probe copies the goal's value when the goal has one and is active for t (an inactive goal is matched but values nothing), and a valued probe values the goal.

Equations

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

def Amato2025.run {H : Type u_1} [DecidableEq H] (act : H → Minimalist.FeatureType → Bool) (α : H) (dom : List H) (ts : List Minimalist.FeatureType) (s : State H) : List (Option H) × State H

Discharge the probes on α in their extrinsic order over dom (Definition (1)): each probe searches for its closest matching goal from the previous probe's goal on — reusing that "Agree-channel", so what α c-commands above it is outside the search — and from the top of dom when the previous probe found no goal (§4.1.2). Returns each probe's goal and the resulting state.

Equations

• Amato2025.run act α dom ts s = Amato2025.run.go act α dom none ts s

def Amato2025.run.go {H : Type u_1} [DecidableEq H] (act : H → Minimalist.FeatureType → Bool) (α : H) (dom : List H) : Option H → List Minimalist.FeatureType → State H → List (Option H) × State H

Equations

• One or more equations did not get rendered due to their size.
• Amato2025.run.go act α dom a✝¹ [] a✝ = ([], a✝)

theorem Amato2025.nestedDomain {H : Type u_1} [DecidableEq H] {pre post : List H} {β : H} (hβ : β ∉ pre) : List.dropWhile (fun (x : H) => decide (x ≠ β)) (pre ++ β :: post) = β :: post

The domain of a probe nested under the goal β is the suffix of the c-command order from β.

theorem Amato2025.notMem_nestedDomain {H : Type u_1} [DecidableEq H] {pre post : List H} {β δ : H} (hnd : (pre ++ β :: post).Nodup) (hδ : δ ∈ pre) : δ ∉ List.dropWhile (fun (x : H) => decide (x ≠ β)) (pre ++ β :: post)

In trees (2)–(3), the alleged intervener δ, c-commanded above the goal β of the first probe, lies outside the domain of every probe nested under β.

def Amato2025.multipleAgree {H : Type u_1} (s : State H) (α : H) (t : Minimalist.FeatureType) (dom : List H) : List H

Under Multiple Agree [∗wh∗] reaches every matching goal in c-command order (§4.2.3).

Equations

• Amato2025.multipleAgree s α t dom = List.filter (Amato2025.goalMatches s α t) dom

def Amato2025.whFronting {H : Type u_1} [DecidableEq H] (s : State H) (α : H) (dom : List H) : List H

In (36) the Merge feature [·wh·], nested under the last goal of [∗wh∗], raises it first, and each later application, its landing site being above the probe, searches the remaining domain afresh. The result lists the movers in order of movement.

Equations

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

def Amato2025.whFronting.rest {H : Type u_1} [DecidableEq H] (p : Minimalist.Probe H) : ℕ → List H → List H

Equations

• Amato2025.whFronting.rest p 0 a✝ = []
• Amato2025.whFronting.rest p n.succ a✝ = match p.search a✝ with | none => [] | some g => g :: Amato2025.whFronting.rest p n (a✝.erase g)

The paper's heads

inductive Amato2025.Head : Type

The heads of the paper's trees.

• t : Head
• perf : Head
• asp : Head
• c : Head
• v : Head
• voice : Head
• appl : Head
• verb : Head
• dpSbj : Head
• dpObj : Head
• dpR : Head
• dpT : Head
• dpDat : Head
• dpNom : Head
• si : Head
• whSbj : Head
• whObj : Head

@[instance_reducible]

instance Amato2025.instDecidableEqHead : DecidableEq Head

Equations

• Amato2025.instDecidableEqHead x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Amato2025.instReprHead : Repr Head

Equations

• Amato2025.instReprHead = { reprPrec := Amato2025.instReprHead.repr }

def Amato2025.instReprHead.repr : Head → ℕ → Std.Format

Equations

• Amato2025.instReprHead.repr Amato2025.Head.t prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Amato2025.Head.t")).group prec✝
• Amato2025.instReprHead.repr Amato2025.Head.perf prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Amato2025.Head.perf")).group prec✝
• Amato2025.instReprHead.repr Amato2025.Head.asp prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Amato2025.Head.asp")).group prec✝
• Amato2025.instReprHead.repr Amato2025.Head.c prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Amato2025.Head.c")).group prec✝
• Amato2025.instReprHead.repr Amato2025.Head.v prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Amato2025.Head.v")).group prec✝
• Amato2025.instReprHead.repr Amato2025.Head.voice prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Amato2025.Head.voice")).group prec✝
• Amato2025.instReprHead.repr Amato2025.Head.appl prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Amato2025.Head.appl")).group prec✝
• Amato2025.instReprHead.repr Amato2025.Head.verb prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Amato2025.Head.verb")).group prec✝
• Amato2025.instReprHead.repr Amato2025.Head.dpSbj prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Amato2025.Head.dpSbj")).group prec✝
• Amato2025.instReprHead.repr Amato2025.Head.dpObj prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Amato2025.Head.dpObj")).group prec✝
• Amato2025.instReprHead.repr Amato2025.Head.dpR prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Amato2025.Head.dpR")).group prec✝
• Amato2025.instReprHead.repr Amato2025.Head.dpT prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Amato2025.Head.dpT")).group prec✝
• Amato2025.instReprHead.repr Amato2025.Head.dpDat prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Amato2025.Head.dpDat")).group prec✝
• Amato2025.instReprHead.repr Amato2025.Head.dpNom prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Amato2025.Head.dpNom")).group prec✝
• Amato2025.instReprHead.repr Amato2025.Head.si prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Amato2025.Head.si")).group prec✝
• Amato2025.instReprHead.repr Amato2025.Head.whSbj prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Amato2025.Head.whSbj")).group prec✝
• Amato2025.instReprHead.repr Amato2025.Head.whObj prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Amato2025.Head.whObj")).group prec✝

@[instance_reducible]

instance Amato2025.instFintypeHead : Fintype Head

Equations

• Amato2025.instFintypeHead = { elems := { val := ↑Amato2025.Head.enumList, nodup := Amato2025.Head.enumList_nodup }, complete := Amato2025.instFintypeHead._proof_1 }

def Amato2025.isPhase : Head → Bool

v and Voice are phase heads (§3.4.2, fn. 18).

Equations

• Amato2025.isPhase Amato2025.Head.v = true
• Amato2025.isPhase Amato2025.Head.voice = true
• Amato2025.isPhase x✝ = false

def Amato2025.allActive : Head → Minimalist.FeatureType → Bool

Every goal values its probe.

Equations

• Amato2025.allActive x✝¹ x✝ = true

def Amato2025.person (p : Person) : (t : Minimalist.FeatureType) × Minimalist.FeatureSlot t.ValueOf

[ϕ:p].

Equations

• Amato2025.person p = ⟨Minimalist.FeatureType.person, Minimalist.FeatureSlot.valued p⟩

Standard Italian auxiliary selection (§3)

Perf bears [∗Infl:perf∗] and [∗π:_∗], ordered as in (7) or (22). v first runs its own cycle over the object ((9), (16)); Perf then probes the vP, T the PerfP (11).

inductive Amato2025.VoiceHead : Type

The paper has two Voice heads, Voice_imp of the impersonal si (§3.4.4) and Voice_pass (fn. 18), both Minimalist.Voice.passive's cell, an implicit external argument.

• impersonal : VoiceHead
• passive : VoiceHead

@[instance_reducible]

instance Amato2025.instDecidableEqVoiceHead : DecidableEq VoiceHead

Equations

• Amato2025.instDecidableEqVoiceHead x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Amato2025.instReprVoiceHead : Repr VoiceHead

Equations

• Amato2025.instReprVoiceHead = { reprPrec := Amato2025.instReprVoiceHead.repr }

def Amato2025.instReprVoiceHead.repr : VoiceHead → ℕ → Std.Format

Equations

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

structure Amato2025.Clause : Type

A clause of §3.4 has v's class (TransitivityClass; an unergative verb is transitive with a covert cognate object bearing default features, fn. 10) under no Voice head, or under Voice_imp (§3.4.4) or Voice_pass (fn. 18).

• verb : ArgumentStructure.TransitivityClass
• voice : Option VoiceHead

@[instance_reducible]

instance Amato2025.instDecidableEqClause : DecidableEq Clause

Equations

• Amato2025.instDecidableEqClause = Amato2025.instDecidableEqClause.decEq

def Amato2025.instDecidableEqClause.decEq (x✝ x✝¹ : Clause) : Decidable (x✝ = x✝¹)

Equations

• Amato2025.instDecidableEqClause.decEq { verb := a, voice := a_1 } { verb := b, voice := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

def Amato2025.instReprClause.repr : Clause → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Amato2025.instReprClause : Repr Clause

Equations

• Amato2025.instReprClause = { reprPrec := Amato2025.instReprClause.repr }

def Amato2025.initial (cl : Clause) (p : Person) : Head → Minimalist.FeatureBundle

Before Agree, with subject person p, Perf bears [∗Infl:perf∗], [∗π:_∗]; T [∗case:nom∗], [∗ϕ:_∗]; a transitive v [Infl:_], [∗case:acc∗], [∗π:_∗] or, in (15), a defective v [Infl:_]; Voice_imp [Infl:_], [π:_] (20), Voice_pass [Infl:_]; the subject [ϕ:p], [case:_]; a full object [ϕ:3], [case:_] (the unaccusative theme, [ϕ:p]), a reflexive object [ϕ:_], [case:_] (16); and si [π:_], [case:_].

Equations

• One or more equations did not get rendered due to their size.
• Amato2025.initial cl p Amato2025.Head.dpSbj = Minimalist.FeatureBundle.ofList [Amato2025.person p, ⟨Minimalist.FeatureType.case, Minimalist.FeatureSlot.unvalued⟩]
• Amato2025.initial cl p x✝ = ⊥

def Amato2025.perfSpine (cl : Clause) : List (Layer Head)

The projections below Perf are (10)/(18) for a transitive v and (15) for a defective one, under the Voice layer of (20) when there is one.

Equations

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

def Amato2025.afterV (cl : Clause) (p : Person) : State Head

In v's cycle ((9), (16)) v assigns accusative and then π-agrees with the object; a defective v does neither.

Equations

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

def Amato2025.perfCycle (ord : List Minimalist.FeatureType) (cl : Clause) (p : Person) : List (Option Head) × State Head

Perf's cycle under the feature ordering ord.

Equations

• Amato2025.perfCycle ord cl p = Amato2025.run Amato2025.allActive Amato2025.Head.perf (Amato2025.domain Amato2025.isPhase (Amato2025.perfSpine cl)) ord (Amato2025.afterV cl p)

def Amato2025.tCycle (ord : List Minimalist.FeatureType) (cl : Clause) (p : Person) : List (Option Head) × State Head

In T's cycle (11) T assigns nominative and then ϕ-agrees.

Equations

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

def Amato2025.derive (ord : List Minimalist.FeatureType) (cl : Clause) (p : Person) : State Head

The state after v, Perf and T have probed.

Equations

• Amato2025.derive ord cl p = (Amato2025.tCycle ord cl p).2

def Amato2025.standardItalian : List Minimalist.FeatureType

Standard Italian orders its probes by argument structure, Infl before person (7).

Equations

• Amato2025.standardItalian = [Minimalist.FeatureType.infl, Minimalist.FeatureType.person]

def Amato2025.ariellese : List Minimalist.FeatureType

Ariellese orders its probes by the subject, person before Infl (22).

Equations

• Amato2025.ariellese = [Minimalist.FeatureType.person, Minimalist.FeatureType.infl]

theorem Amato2025.perf_targets_v (c : ArgumentStructure.TransitivityClass) (hc : c ≠ ArgumentStructure.TransitivityClass.unaccusative) (p : Person) : (perfCycle standardItalian { verb := c } p).1 = [some Head.v, some Head.v]

In (10) and (18), [∗Infl:perf∗] finds v, and [∗π:_∗], nested under it, agrees with v across the subject, for transitive, unergative and reflexive v alike.

theorem Amato2025.perf_unaccusative (p : Person) : (perfCycle standardItalian { verb := ArgumentStructure.TransitivityClass.unaccusative } p).1 = [some Head.v, none]

In (15) π-Agree on Perf fails, since the defective v bears no person feature and the raised theme in Spec,v is above the Nested-Agree goal.

theorem Amato2025.perf_impersonal (c : ArgumentStructure.TransitivityClass) (p : Person) : (perfCycle standardItalian { verb := c, voice := some VoiceHead.impersonal } p).1 = [some Head.voice, some Head.voice]

In (20) both probes on Perf target Voice_imp, whose person feature is unvalued.

theorem Amato2025.t_targets_subject (p : Person) : (tCycle standardItalian { verb := ArgumentStructure.TransitivityClass.transitive } p).1 = [some Head.dpSbj, some Head.dpSbj]

In (11) T assigns nominative to the subject and, nested under that dependency, ϕ-agrees with it rather than with the higher Perf.

def Amato2025.standardItalianAux (s : State Head) : Verb.PerfectAuxiliary

The Vocabulary Items (14) insert /AVERE/ ↔ Perf[π:α], and /ESSERE/ elsewhere.

Equations

• Amato2025.standardItalianAux s = if (s Amato2025.Head.perf Minimalist.FeatureType.person).isValued = true then Verb.PerfectAuxiliary.have else Verb.PerfectAuxiliary.be

theorem Amato2025.standardItalian_aux (c : ArgumentStructure.TransitivityClass) (p : Person) : standardItalianAux (derive standardItalian { verb := c } p) = c.canonicalSelection

As in (4)–(5), the derivation yields exactly the canonical Romance distribution, HAVE with transitive and unergative verbs and BE with unaccusative and reflexive ones, for every subject person.

theorem Amato2025.standardItalian_voice (c : ArgumentStructure.TransitivityClass) (f : VoiceHead) (hf : f = VoiceHead.impersonal ∨ f = VoiceHead.passive) (p : Person) : standardItalianAux (derive standardItalian { verb := c, voice := some f } p) = Verb.PerfectAuxiliary.be

Under Voice_imp or Voice_pass the auxiliary is BE whatever the verb ((5d), fn. 18), since Perf's π-probe, nested under Infl-Agree with Voice, meets an unvalued or absent person feature.

def Amato2025.arielleseAux (s : State Head) : Verb.PerfectAuxiliary

Ariellese (23) inserts /AVERE/ ↔ Perf[π:-participant].

Equations

• Amato2025.arielleseAux s = if s Amato2025.Head.perf Minimalist.FeatureType.person = Minimalist.FeatureSlot.valued Person.third then Verb.PerfectAuxiliary.have else Verb.PerfectAuxiliary.be

theorem Amato2025.ariellese_aux (c : ArgumentStructure.TransitivityClass) (p : Person) : arielleseAux (derive ariellese { verb := c } p) = if p = Person.third then Verb.PerfectAuxiliary.have else Verb.PerfectAuxiliary.be

Under the ordering (22) the auxiliary follows the subject's person alone (21), BBH whatever the argument structure (§3.5).

def Amato2025.tufilleseAux (s : State Head) : Verb.PerfectAuxiliary

Tufillese (24) inserts /AVERE/ ↔ Perf[π:α] / T[ϕ:3sg].

Equations

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

theorem Amato2025.tufillese_aux (c : ArgumentStructure.TransitivityClass) (p : Person) : tufilleseAux (derive standardItalian { verb := c } p) = if c.canonicalSelection = Verb.PerfectAuxiliary.have ∧ p = Person.third then Verb.PerfectAuxiliary.have else Verb.PerfectAuxiliary.be

The mixed system has BBH where Standard Italian has HAVE and BE where it has BE (§3.5).

Case and agreement in ditransitive clauses (§4.1.1)

inductive Amato2025.ProbeOrder : Type

The two orderings of [∗case∗] and [∗ϕ:_∗] on a head.

• caseFirst : ProbeOrder
• phiFirst : ProbeOrder

@[instance_reducible]

instance Amato2025.instDecidableEqProbeOrder : DecidableEq ProbeOrder

Equations

• Amato2025.instDecidableEqProbeOrder x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Amato2025.instReprProbeOrder.repr : ProbeOrder → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Amato2025.instReprProbeOrder : Repr ProbeOrder

Equations

• Amato2025.instReprProbeOrder = { reprPrec := Amato2025.instReprProbeOrder.repr }

@[instance_reducible]

instance Amato2025.instFintypeProbeOrder : Fintype ProbeOrder

Equations

• Amato2025.instFintypeProbeOrder = { elems := { val := ↑Amato2025.ProbeOrder.enumList, nodup := Amato2025.ProbeOrder.enumList_nodup }, complete := Amato2025.instFintypeProbeOrder._proof_1 }

def Amato2025.ProbeOrder.probes : ProbeOrder → List Minimalist.FeatureType

The probes on v, in order.

Equations

• Amato2025.ProbeOrder.caseFirst.probes = [Minimalist.FeatureType.case, Minimalist.FeatureType.person]
• Amato2025.ProbeOrder.phiFirst.probes = [Minimalist.FeatureType.person, Minimalist.FeatureType.case]

def Amato2025.ditransitiveInitial (applDat : Bool) : Head → Minimalist.FeatureBundle

In (25)–(28) v bears [∗case:acc∗], [∗ϕ:_∗] over DP_R … Appl … V … DP_T, the recipient already dative from Appl or not.

Equations

• One or more equations did not get rendered due to their size.
• Amato2025.ditransitiveInitial applDat Amato2025.Head.dpT = Minimalist.FeatureBundle.ofList [Amato2025.person Person.third, ⟨Minimalist.FeatureType.case, Minimalist.FeatureSlot.unvalued⟩]
• Amato2025.ditransitiveInitial applDat x✝ = ⊥

structure Amato2025.Alignment : Type

Which argument v assigns accusative to and which it ϕ-agrees with.

• caseTarget : Option Head
• agrTarget : Option Head

def Amato2025.instDecidableEqAlignment.decEq (x✝ x✝¹ : Alignment) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Amato2025.instDecidableEqAlignment : DecidableEq Alignment

Equations

• Amato2025.instDecidableEqAlignment = Amato2025.instDecidableEqAlignment.decEq

def Amato2025.instReprAlignment.repr : Alignment → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Amato2025.instReprAlignment : Repr Alignment

Equations

• Amato2025.instReprAlignment = { reprPrec := Amato2025.instReprAlignment.repr }

def Amato2025.ditransitive (o : ProbeOrder) (applDat : Bool) : Alignment

The alignment v derives under ordering o with or without dative from Appl.

Equations

• Amato2025.ditransitive Amato2025.ProbeOrder.caseFirst applDat = { caseTarget := c, agrTarget := a }
• Amato2025.ditransitive Amato2025.ProbeOrder.phiFirst applDat = { caseTarget := c, agrTarget := a }
• Amato2025.ditransitive o✝ applDat = { caseTarget := none, agrTarget := none }

theorem Amato2025.ditransitive_caseFirst_dat : ditransitive ProbeOrder.caseFirst true = { caseTarget := some Head.dpT, agrTarget := some Head.dpT }

Example (25) has indirective case and agreement, ϕ-Agree with the theme across the recipient.

theorem Amato2025.ditransitive_caseFirst_noDat : ditransitive ProbeOrder.caseFirst false = { caseTarget := some Head.dpR, agrTarget := some Head.dpR }

Example (26) has secundative case and agreement.

theorem Amato2025.ditransitive_phiFirst_dat : ditransitive ProbeOrder.phiFirst true = { caseTarget := some Head.dpT, agrTarget := some Head.dpR }

Example (27) has indirective case and secundative agreement.

theorem Amato2025.ditransitive_phiFirst_noDat : ditransitive ProbeOrder.phiFirst false = { caseTarget := some Head.dpR, agrTarget := some Head.dpR }

Example (28) has secundative case and agreement again.

theorem Amato2025.no_secundativeCase_indirectiveAgreement (o : ProbeOrder) (d : Bool) : ditransitive o d ≠ { caseTarget := some Head.dpR, agrTarget := some Head.dpT }

Table 1's gap ([Bar24]): no ordering and no Appl setting gives accusative on the recipient with agreement on the theme.

Icelandic DAT-NOM constructions (§4.1.2)

inductive Amato2025.Clausal : Type

(29a) versus (29b).

• monoclausal : Clausal
• biclausal : Clausal

@[instance_reducible]

instance Amato2025.instDecidableEqClausal : DecidableEq Clausal

Equations

• Amato2025.instDecidableEqClausal x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Amato2025.instReprClausal.repr : Clausal → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Amato2025.instReprClausal.repr Amato2025.Clausal.biclausal prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Amato2025.Clausal.biclausal")).group prec✝

@[instance_reducible]

instance Amato2025.instReprClausal : Repr Clausal

Equations

• Amato2025.instReprClausal = { reprPrec := Amato2025.instReprClausal.repr }

@[instance_reducible]

instance Amato2025.instFintypeClausal : Fintype Clausal

Equations

• Amato2025.instFintypeClausal = { elems := { val := ↑Amato2025.Clausal.enumList, nodup := Amato2025.Clausal.enumList_nodup }, complete := Amato2025.instFintypeClausal._proof_1 }

def Amato2025.icelandicInitial : Clausal → Head → Minimalist.FeatureBundle

T [∗case:nom∗], [∗ϕ:_∗] over DP_dat … DP_nom; in (29b) the lower T has already assigned nominative.

Equations

• One or more equations did not get rendered due to their size.
• Amato2025.icelandicInitial x✝¹ x✝ = ⊥

def Amato2025.icelandicActive : Head → Minimalist.FeatureType → Bool

Datives are defective goals for ϕ-Agree: matched, never valuing.

Equations

• Amato2025.icelandicActive Amato2025.Head.dpDat (Minimalist.FeatureType.agr Agreement.Dimension.number) = false
• Amato2025.icelandicActive x✝¹ x✝ = true

def Amato2025.icelandicOrder : ProbeOrder → List Minimalist.FeatureType

The two orderings that coexist on Icelandic T.

Equations

• Amato2025.icelandicOrder Amato2025.ProbeOrder.caseFirst = [Minimalist.FeatureType.case, Minimalist.FeatureType.number]
• Amato2025.icelandicOrder Amato2025.ProbeOrder.phiFirst = [Minimalist.FeatureType.number, Minimalist.FeatureType.case]

def Amato2025.icelandic (k : Clausal) (o : ProbeOrder) : Minimalist.FeatureSlot Minimalist.FeatureType.number.ValueOf

T's number slot after probing.

Equations

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

theorem Amato2025.icelandic_monoclausal_caseFirst : icelandic Clausal.monoclausal ProbeOrder.caseFirst = Minimalist.FeatureSlot.valued Number.plural

In (29a) with case first, T assigns nominative to the object and then ϕ-agrees with it across the dative (líka).

theorem Amato2025.icelandic_monoclausal_phiFirst : icelandic Clausal.monoclausal ProbeOrder.phiFirst = Minimalist.FeatureSlot.unvalued

In (29a) with ϕ first, the dative intervenes defectively, giving default agreement (líkar).

theorem Amato2025.icelandic_biclausal (o : ProbeOrder) : icelandic Clausal.biclausal o = Minimalist.FeatureSlot.unvalued

In (29b), with nominative assigned below, matrix T's case probe finds no goal, so ϕ is unrestricted and meets the dative under either ordering, giving default agreement only.

Person agreement in the Lak perfective (§4.2.1)

def Amato2025.lakInitial (ps po : Person) : Head → Minimalist.FeatureBundle

In (32) Asp bears [∗Infl:perf∗], [∗π:_∗] and v [Infl:_], [∗π:_∗], with subject person ps and object person po.

Equations

• One or more equations did not get rendered due to their size.
• Amato2025.lakInitial ps po Amato2025.Head.dpSbj = Minimalist.FeatureBundle.ofList [Amato2025.person ps]
• Amato2025.lakInitial ps po Amato2025.Head.dpObj = Minimalist.FeatureBundle.ofList [Amato2025.person po]
• Amato2025.lakInitial ps po x✝ = ⊥

def Amato2025.lak (ps po : Person) : Minimalist.FeatureSlot Minimalist.FeatureType.person.ValueOf

Asp's person slot after v has agreed with the object and Asp with v.

Equations

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

theorem Amato2025.lak_agrees_with_object (ps po : Person) : lak ps po = Minimalist.FeatureSlot.valued po

In (31c)–(31d) the perfective auxiliary carries the internal argument's person, whatever the external argument's.

Subject agreement in Spanish VOS (§4.2.2)

def Amato2025.vosInitial : Head → Minimalist.FeatureBundle

In (34) T bears [∗case:nom∗], [∗ϕ:_∗] over the shifted object [case:acc], [ϕ:α] and the subject [case:_], [ϕ:β].

Equations

• One or more equations did not get rendered due to their size.
• Amato2025.vosInitial Amato2025.Head.dpObj = Minimalist.FeatureBundle.ofList [⟨Minimalist.FeatureType.case, Minimalist.FeatureSlot.valued Case.acc⟩, Amato2025.person Person.third]
• Amato2025.vosInitial Amato2025.Head.dpSbj = Minimalist.FeatureBundle.ofList [⟨Minimalist.FeatureType.case, Minimalist.FeatureSlot.unvalued⟩, Amato2025.person Person.third]
• Amato2025.vosInitial x✝ = ⊥

theorem Amato2025.vos_subject_agreement : (run allActive Head.t [Head.dpObj, Head.dpSbj] [Minimalist.FeatureType.case, Minimalist.FeatureType.person] vosInitial).1 = [some Head.dpSbj, some Head.dpSbj]

In (33) the case-marked object is no goal for nominative, and ϕ-Agree, nested under case assignment, targets the subject.

Bulgarian multiple wh-fronting (§4.2.3)

def Amato2025.bulgarianInitial : Head → Minimalist.FeatureBundle

In (36) C bears [∗wh∗] ≻ [·wh·] over wh-sbj in Spec,T, T, and wh-obj at the edge of vP.

Equations

• Amato2025.bulgarianInitial Amato2025.Head.c = Minimalist.FeatureBundle.ofList [⟨Minimalist.FeatureType.wh, Minimalist.FeatureSlot.unvalued⟩]
• Amato2025.bulgarianInitial Amato2025.Head.whSbj = Minimalist.FeatureBundle.ofList [⟨Minimalist.FeatureType.wh, Minimalist.FeatureSlot.valued true⟩]
• Amato2025.bulgarianInitial Amato2025.Head.whObj = Minimalist.FeatureBundle.ofList [⟨Minimalist.FeatureType.wh, Minimalist.FeatureSlot.valued true⟩]
• Amato2025.bulgarianInitial x✝ = ⊥

def Amato2025.bulgarianDomain : List Head

C's domain in (36).

Equations

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

theorem Amato2025.bulgarian_order : whFronting bulgarianInitial Head.c bulgarianDomain = [Head.whObj, Head.whSbj]

In (35) the object fronts first, the subject lands in the outer specifier, and the base order is preserved.

Agreement with unmarked DPs in Hindi-Urdu (§4.3.1)

inductive Amato2025.HindiClause : Type

The ergative subject is in Spec,Asp in (37)/(39), both arguments are case-marked in Spec,Asp in (38a)/(40), and the unmarked subject is in Spec,v under imperfective Asp in (38b).

• ergSubject : HindiClause
• bothMarked : HindiClause
• unmarkedSubject : HindiClause

@[instance_reducible]

instance Amato2025.instDecidableEqHindiClause : DecidableEq HindiClause

Equations

• Amato2025.instDecidableEqHindiClause x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Amato2025.instReprHindiClause.repr : HindiClause → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Amato2025.instReprHindiClause : Repr HindiClause

Equations

• Amato2025.instReprHindiClause = { reprPrec := Amato2025.instReprHindiClause.repr }

@[instance_reducible]

instance Amato2025.instFintypeHindiClause : Fintype HindiClause

Equations

• Amato2025.instFintypeHindiClause = { elems := { val := ↑Amato2025.HindiClause.enumList, nodup := Amato2025.HindiClause.enumList_nodup }, complete := Amato2025.instFintypeHindiClause._proof_1 }

def Amato2025.hindiInitial (k : HindiClause) (ps po : Person) : Head → Minimalist.FeatureBundle

T [∗Infl:_∗], [∗ϕ:_∗]; Asp [Infl:perf] or [Infl:impf]; v [∗ϕ:_∗]; the DPs with the case Asp assigned them.

Equations

• One or more equations did not get rendered due to their size.
• Amato2025.hindiInitial k ps po Amato2025.Head.v = Minimalist.FeatureBundle.ofList [⟨Minimalist.FeatureType.person, Minimalist.FeatureSlot.unvalued⟩]
• Amato2025.hindiInitial k ps po x✝ = ⊥

def Amato2025.hindiSpine : HindiClause → List (Layer Head)

The projections below T in (39), (40) and (38b).

Equations

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

def Amato2025.hindi (k : HindiClause) (ps po : Person) : Minimalist.FeatureSlot Minimalist.FeatureType.person.ValueOf

T's person slot after v has probed its complement (empty in (40), the object having moved, fn. 33) and T has Infl-agreed with Asp and, nested under it, probed for ϕ.

Equations

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

theorem Amato2025.hindi_object_agreement (ps po : Person) : hindi HindiClause.ergSubject ps po = Minimalist.FeatureSlot.valued po

In (37), starting from Asp, ϕ-Agree skips the ergative subject and reaches v's copy of the object's features.

theorem Amato2025.hindi_default_agreement (ps po : Person) : hindi HindiClause.bothMarked ps po = Minimalist.FeatureSlot.unvalued

In (38a), with both DPs case-marked above Asp, only v's unvalued slot remains, giving default agreement.

theorem Amato2025.hindi_subject_agreement (ps po : Person) : hindi HindiClause.unmarkedSubject ps po = Minimalist.FeatureSlot.valued ps

In (38b) an unmarked subject in Spec,v is the first ϕ-goal below Asp.