Newman (2024): When Arguments Merge

This file formalizes Newman's theory of feature-driven Merge and its consequences for the verb phrase. A head bears Merge features, and an element merging with it checks every unchecked feature it can. Features may go unchecked, and they belong to categories rather than to lexical items: V bears [·D·], checked by a DP, and [·X·], checked by anything, and v in addition [·V·] and [·wh·]. Since a DP checks everything a non-DP checks and a wh-DP everything a DP checks, a phrase checking a subset of another's features must merge first. Among the operations possible at a step, Weak Economy prefers one checking more features unless one would bleed the other. Newman derives from this where arguments go in the verb phrase, the binding pattern of the dative alternation, agent focus in Mayan subject questions, and the subjects of passive ditransitives.

Main definitions

• Licensed: a sequence of merges with one head, each checking a feature still unchecked.
• Phrase.checks, bundleV, bundlev: the features a phrase checks and those V and v bear.
• configuration: the binding theory, m-command without reverse c-command.
• AgentFocus: Voice and T cross-reference one argument, so Voice is spelled out as agent focus.
• System.Derivation: a derivation at v in which every step respects Weak Economy.

Main results

• Licensed.not_sublist: an element checking only features another checks cannot follow it.
• nonDP_first, not_dp_after_dp: non-DP arguments are complements, one DP per head.
• wordOrder_binding: the direct object can bind the indirect object only when it precedes it.
• transitive_derivations, agentFocus_iff: agent focus arises exactly when the object checks [·D·] before the wh-subject merges.
• npObject_no_agentFocus, multipleFronting: the environments that obviate agent focus.
• doma, lowPassive_subject, om_iobj_subject: the subjects of passive ditransitives.
• greek_passive, greek_whPassive, greek_active: when Greek clitic doubling is obligatory.
• literal_greek_whPassive: Weak Economy read as worded makes clitic doubling obligatory in wh passives, against the data.
• System.exists_derivation: Weak Economy never blocks every operation.
• whSubject_complement, overlap_subjectQuestions, overlap_passives: Weak Economy makes a wh-subject v's complement unless operations checking a common feature are exempt.

Implementation notes

A phrase's checkable features are read off its category and the features it bears. The first specifier merged is outermost, by Paillé's generalization of Richards's tucking in; m-command is Barker and Pullum's command relation generated by the maximal projections, and case is Marantz's dependent case. An operation is possible when it checks a Merge feature of an accessible phrase, and a derivation ends only when nothing possible remains, as Preminger's obligatory operations require.

TODO

The person-hierarchy effects on agent focus and the weak-crossover account of anaphoric objects in chapter 3, and chapters 6 and 7, are not formalized.

References

• [New24]
• [Pre14]
• [Ric97]
• [Pai20]
• [Mar91]
• [BP90]

Feature-driven Merge

def Newman2024.Licensed {F : Type u_1} {α : Type u_2} [DecidableEq F] (κ : α → Finset F) (P : Finset F) : Finset F → List α → Prop

Licensed κ P s es holds when the elements es can merge in order with a head whose unchecked Merge features are s, where κ e is the set of features e can check and the features in P stay active once checked. Each element checks every unchecked feature it can, and at least one; features left over at the end are allowed.

Equations

• Newman2024.Licensed κ P x✝ [] = True
• Newman2024.Licensed κ P x✝ (e :: es) = ((x✝ ∩ κ e).Nonempty ∧ Newman2024.Licensed κ P (x✝ \ (κ e \ P)) es)

@[instance_reducible]

instance Newman2024.decLicensed {F : Type u_1} {α : Type u_2} [DecidableEq F] (κ : α → Finset F) (P s : Finset F) (es : List α) : Decidable (Licensed κ P s es)

Equations

• Newman2024.decLicensed κ P x✝ [] = isTrue trivial
• Newman2024.decLicensed κ P x✝ (e :: es) = { decide := decide (x✝ ∩ κ e).Nonempty && decide (Newman2024.Licensed κ P (x✝ \ (κ e \ P)) es), reflects_decide := ⋯ }

@[simp]

theorem Newman2024.licensed_nil {F : Type u_1} {α : Type u_2} [DecidableEq F] {κ : α → Finset F} {P s : Finset F} : Licensed κ P s []

@[simp]

theorem Newman2024.licensed_cons {F : Type u_1} {α : Type u_2} [DecidableEq F] {κ : α → Finset F} {P s : Finset F} {es : List α} {e : α} : Licensed κ P s (e :: es) ↔ (s ∩ κ e).Nonempty ∧ Licensed κ P (s \ (κ e \ P)) es

theorem Newman2024.Licensed.nonempty_of_mem {F : Type u_1} {α : Type u_2} [DecidableEq F] {κ : α → Finset F} {P s : Finset F} {es : List α} (h : Licensed κ P s es) {b : α} (hb : b ∈ es) : (s ∩ κ b).Nonempty

Every element of a licensed sequence can check one of the head's features.

theorem Newman2024.Licensed.not_sublist {F : Type u_1} {α : Type u_2} [DecidableEq F] {κ : α → Finset F} {P s : Finset F} {es : List α} (h : Licensed κ P s es) {a b : α} (hab : s ∩ κ b ⊆ κ a \ P) : ¬[a, b].Sublist es

If b can check only features of the head that a checks and uses up, b cannot merge after a.

theorem Newman2024.Licensed.head?_eq {F : Type u_1} {α : Type u_2} [DecidableEq F] {κ : α → Finset F} {P s : Finset F} {es : List α} (h : Licensed κ P s es) {b : α} (hb : b ∈ es) (hsub : ∀ a ∈ es, s ∩ κ b ⊆ κ a \ P) : es.head? = some b

If every element can check and use up whatever b can check among the head's features, b merges first.

theorem Newman2024.Licensed.nodup {F : Type u_1} {α : Type u_2} [DecidableEq F] {κ : α → Finset F} {s : Finset F} {es : List α} (h : Licensed κ ∅ s es) : es.Nodup

When no feature stays active, no element merges twice.

theorem Newman2024.Licensed.length_le {F : Type u_1} {α : Type u_2} [DecidableEq F] {κ : α → Finset F} {s : Finset F} {es : List α} (h : Licensed κ ∅ s es) : es.length ≤ s.card

When no feature stays active, a head licenses at most as many merges as it has features.

The Categorial Merge Hypothesis

inductive Newman2024.Feature : Type

The features that drive Merge and Agree at a head are [·D·], checked by a full DP, [·Dweak·], checked by anything bearing D including a clitic, the category-unspecified [·X·], checked by anything, [·V·], checked by a VP, [·wh·], checked by a wh-phrase, the object-marking feature, checked by a phrase with the discourse status object marking tracks, and the φ-probe [uφ], valued by Agree.

• D : Feature
• Dweak : Feature
• X : Feature
• V : Feature
• wh : Feature
• om : Feature
• phi : Feature

@[instance_reducible]

instance Newman2024.instDecidableEqFeature : DecidableEq Feature

Equations

• Newman2024.instDecidableEqFeature x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Newman2024.instReprFeature.repr : Feature → ℕ → Std.Format

Equations

• Newman2024.instReprFeature.repr Newman2024.Feature.D prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Newman2024.Feature.D")).group prec✝
• Newman2024.instReprFeature.repr Newman2024.Feature.Dweak prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Newman2024.Feature.Dweak")).group prec✝
• Newman2024.instReprFeature.repr Newman2024.Feature.X prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Newman2024.Feature.X")).group prec✝
• Newman2024.instReprFeature.repr Newman2024.Feature.V prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Newman2024.Feature.V")).group prec✝
• Newman2024.instReprFeature.repr Newman2024.Feature.wh prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Newman2024.Feature.wh")).group prec✝
• Newman2024.instReprFeature.repr Newman2024.Feature.om prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Newman2024.Feature.om")).group prec✝
• Newman2024.instReprFeature.repr Newman2024.Feature.phi prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Newman2024.Feature.phi")).group prec✝

@[instance_reducible]

instance Newman2024.instReprFeature : Repr Feature

Equations

• Newman2024.instReprFeature = { reprPrec := Newman2024.instReprFeature.repr }

def Newman2024.Feature.IsMerge (f : Feature) : Prop

Every feature but the φ-probe is a Merge feature.

Equations

• f.IsMerge = (f ≠ Newman2024.Feature.phi)

@[instance_reducible]

instance Newman2024.instDecidablePredFeatureIsMerge : DecidablePred Feature.IsMerge

Equations

• Newman2024.instDecidablePredFeatureIsMerge f = { decide := !decide (f = Newman2024.Feature.phi), reflects_decide := ⋯ }

structure Newman2024.Phrase : Type

A phrase, as Merge features see it, is its category and the further features it bears, such as [wh].

• cat : Minimalist.Cat
• bears : Finset Feature

@[instance_reducible]

instance Newman2024.instDecidableEqPhrase : DecidableEq Phrase

Equations

• Newman2024.instDecidableEqPhrase = Newman2024.instDecidableEqPhrase.decEq

def Newman2024.instDecidableEqPhrase.decEq (x✝ x✝¹ : Phrase) : Decidable (x✝ = x✝¹)

Equations

• Newman2024.instDecidableEqPhrase.decEq { cat := a, bears := a_1 } { cat := b, bears := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

def Newman2024.Phrase.checks (p : Phrase) : Finset Feature

A phrase checks [·X·], [·D·] and [·Dweak·] when it is a DP, [·V·] when it is a VP, and the features it bears.

Equations

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

@[simp]

theorem Newman2024.Phrase.mem_checks {p : Phrase} {f : Feature} : f ∈ p.checks ↔ f = Feature.X ∨ (f = Feature.D ∨ f = Feature.Dweak) ∧ p.cat = Minimalist.Cat.D ∨ f = Feature.V ∧ p.cat = Minimalist.Cat.V ∨ f ∈ p.bears

def Newman2024.Phrase.dp : Phrase

dp is a DP bearing nothing further.

Equations

• Newman2024.Phrase.dp = { cat := Minimalist.Cat.D }

def Newman2024.Phrase.whDP : Phrase

whDP is a wh-DP.

Equations

• Newman2024.Phrase.whDP = { cat := Minimalist.Cat.D, bears := {Newman2024.Feature.wh} }

def Newman2024.Phrase.vp : Phrase

vp is a VP.

Equations

• Newman2024.Phrase.vp = { cat := Minimalist.Cat.V }

theorem Newman2024.Phrase.checks_eq_X {p : Phrase} (hD : p.cat ≠ Minimalist.Cat.D) (hV : p.cat ≠ Minimalist.Cat.V) (hb : p.bears = ∅) : p.checks = {Feature.X}

A phrase that is neither a DP nor a VP and bears nothing checks only [·X·].

theorem Newman2024.Phrase.checks_dp_subset_whDP : dp.checks ⊆ whDP.checks

A wh-DP checks everything a DP checks.

theorem Newman2024.Phrase.checks_subset_dp {p : Phrase} (hV : p.cat ≠ Minimalist.Cat.V) (hb : p.bears = ∅) : p.checks ⊆ dp.checks

A DP checks everything a phrase that is not a VP and bears nothing checks.

def Newman2024.bundleV : Finset Feature

V bears [·D·] and [·X·], whatever the verb.

Equations

• Newman2024.bundleV = {Newman2024.Feature.D, Newman2024.Feature.X}

def Newman2024.bundlev : Finset Feature

v bears V's features, [·V·] for merging VP, and [·wh·] for successive-cyclic movement.

Equations

• Newman2024.bundlev = {Newman2024.Feature.D, Newman2024.Feature.X, Newman2024.Feature.V, Newman2024.Feature.wh}

The distribution of DPs and non-DPs

theorem Newman2024.nonDP_first {α : Type u_1} {f : α → Phrase} {s : Finset Feature} {es : List α} (h : Licensed (Phrase.checks ∘ f) ∅ s es) {b : α} (hb : b ∈ es) (hD : (f b).cat ≠ Minimalist.Cat.D) (hV : (f b).cat ≠ Minimalist.Cat.V) (hbears : (f b).bears = ∅) : es.head? = some b

The non-DP first theorem. A phrase that checks nothing but [·X·] merges first with any head it merges with, so it is that head's complement.

theorem Newman2024.vp_specifier {α : Type u_1} {f : α → Phrase} {es : List α} (h : Licensed (Phrase.checks ∘ f) ∅ bundlev es) {b vp : α} (hb : b ∈ es) (hD : (f b).cat ≠ Minimalist.Cat.D) (hV : (f b).cat ≠ Minimalist.Cat.V) (hbears : (f b).bears = ∅) (hne : vp ≠ b) : es.head? ≠ some vp

A non-DP argument of v makes VP a specifier rather than v's complement.

theorem Newman2024.not_dp_after_dp {α : Type u_1} {f : α → Phrase} {s : Finset Feature} {es : List α} (h : Licensed (Phrase.checks ∘ f) ∅ s es) {a b : α} (ha : (f a).cat = Minimalist.Cat.D) (hb : (f b).cat = Minimalist.Cat.D) (hbears : (f b).bears ⊆ (f a).bears) : ¬[a, b].Sublist es

One DP per head. A DP cannot merge after another DP bearing everything it bears.

theorem Newman2024.length_filter_dp_le_one {α : Type u_1} {f : α → Phrase} {s : Finset Feature} {es : List α} (h : Licensed (Phrase.checks ∘ f) ∅ s es) : (List.filter (fun (a : α) => decide ((f a).cat = Minimalist.Cat.D ∧ (f a).bears = ∅)) es).length ≤ 1

A head introduces at most one DP bearing nothing further.

theorem Newman2024.length_filter_nonDP_le_one {α : Type u_1} {f : α → Phrase} {s : Finset Feature} {es : List α} (h : Licensed (Phrase.checks ∘ f) ∅ s es) : (List.filter (fun (a : α) => decide ((f a).cat ≠ Minimalist.Cat.D ∧ (f a).cat ≠ Minimalist.Cat.V ∧ (f a).bears = ∅)) es).length ≤ 1

A head introduces at most one argument that is neither a DP nor a VP and bears nothing.

The dative alternation

inductive Newman2024.Leaf : Type

A leaf of a ditransitive vP is the external argument, v, V, the direct object, or the phrase containing the indirect object.

• subj : Leaf
• v : Leaf
• V : Leaf
• dobj : Leaf
• iobj : Leaf

@[instance_reducible]

instance Newman2024.instDecidableEqLeaf : DecidableEq Leaf

Equations

• Newman2024.instDecidableEqLeaf x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Newman2024.instReprLeaf.repr : Leaf → ℕ → Std.Format

Equations

• Newman2024.instReprLeaf.repr Newman2024.Leaf.subj prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Newman2024.Leaf.subj")).group prec✝
• Newman2024.instReprLeaf.repr Newman2024.Leaf.v prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Newman2024.Leaf.v")).group prec✝
• Newman2024.instReprLeaf.repr Newman2024.Leaf.V prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Newman2024.Leaf.V")).group prec✝
• Newman2024.instReprLeaf.repr Newman2024.Leaf.dobj prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Newman2024.Leaf.dobj")).group prec✝
• Newman2024.instReprLeaf.repr Newman2024.Leaf.iobj prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Newman2024.Leaf.iobj")).group prec✝

@[instance_reducible]

instance Newman2024.instReprLeaf : Repr Leaf

Equations

• Newman2024.instReprLeaf = { reprPrec := Newman2024.instReprLeaf.repr }

@[reducible, inline]

abbrev Newman2024.XTree : Type

An XTree is a tree whose nodes carry a category. Which nodes are heads, intermediate or maximal projections is read off the tree: a node's head daughter is its daughter of its category.

Equations

• Newman2024.XTree = PhraseStructure.Tree Minimalist.Cat Newman2024.Leaf

def Newman2024.XTree.checks (t : XTree) : Finset Feature

A tree counts for Merge features as a phrase of its root's category.

Equations

• t.checks = { cat := PhraseStructure.Tree.cat t }.checks

def Newman2024.bar (c : Minimalist.Cat) (h comp : XTree) : List XTree → XTree

bar c h comp specs is the stack of intermediate projections of the phrase headed by h, with complement comp and specifiers specs.

Equations

• Newman2024.bar c h comp [] = PhraseStructure.Tree.node c [h, comp]
• Newman2024.bar c h comp (s :: ss) = PhraseStructure.Tree.node c [s, Newman2024.bar c h comp ss]

def Newman2024.project (c : Minimalist.Cat) (h : XTree) : List XTree → XTree

project c h es is the phrase the head h of category c projects when es merge with it. The first is the complement, and each later one tucks in below the specifiers already merged, so the first specifier is outermost.

Equations

• Newman2024.project c h [] = PhraseStructure.Tree.node c [h]
• Newman2024.project c h [comp] = PhraseStructure.Tree.node c [h, comp]
• Newman2024.project c h (comp :: s :: ss) = PhraseStructure.Tree.node c [s, Newman2024.bar c h comp ss]

def Newman2024.subjP : XTree

subjP is the external argument, a DP.

Equations

• Newman2024.subjP = PhraseStructure.Tree.terminal Minimalist.Cat.D Newman2024.Leaf.subj

def Newman2024.dobjP : XTree

dobjP is the direct object, a DP.

Equations

• Newman2024.dobjP = PhraseStructure.Tree.terminal Minimalist.Cat.D Newman2024.Leaf.dobj

def Newman2024.iobjP : XTree

iobjP is the phrase containing the indirect object, a PP or an applicative phrase.

Equations

• Newman2024.iobjP = PhraseStructure.Tree.terminal Minimalist.Cat.P Newman2024.Leaf.iobj

def Newman2024.vHead : XTree

vHead is the head v.

Equations

• Newman2024.vHead = PhraseStructure.Tree.terminal Minimalist.Cat.v Newman2024.Leaf.v

def Newman2024.VHead : XTree

VHead is the head V.

Equations

• Newman2024.VHead = PhraseStructure.Tree.terminal Minimalist.Cat.V Newman2024.Leaf.V

def Newman2024.lowXP : XTree

lowXP is the ditransitive with the indirect object in V's complement.

Equations

• Newman2024.lowXP = Newman2024.project Minimalist.Cat.v Newman2024.vHead [Newman2024.project Minimalist.Cat.V Newman2024.VHead [Newman2024.iobjP, Newman2024.dobjP], Newman2024.subjP]

def Newman2024.highXP : XTree

highXP is the ditransitive with the indirect object in v's complement and VP a specifier linearized on the left.

Equations

• Newman2024.highXP = Newman2024.project Minimalist.Cat.v Newman2024.vHead [Newman2024.iobjP, Newman2024.subjP, Newman2024.project Minimalist.Cat.V Newman2024.VHead [Newman2024.dobjP]]

def Newman2024.highXPRight : XTree

highXPRight is highXP with the VP specifier linearized on the right.

Equations

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

def Newman2024.ditransitives : List XTree

ditransitives lists the three ditransitive vPs.

Equations

• Newman2024.ditransitives = [Newman2024.lowXP, Newman2024.highXP, Newman2024.highXPRight]

theorem Newman2024.ditransitives_licensed : Licensed XTree.checks ∅ bundleV [iobjP, dobjP] ∧ Licensed XTree.checks ∅ bundlev [project Minimalist.Cat.V VHead [iobjP, dobjP], subjP] ∧ Licensed XTree.checks ∅ bundleV [dobjP] ∧ Licensed XTree.checks ∅ bundlev [iobjP, subjP, project Minimalist.Cat.V VHead [dobjP]] ∧ ¬Licensed XTree.checks ∅ bundlev [project Minimalist.Cat.V VHead [dobjP], iobjP, subjP]

Both structures come from licensed derivations, and VP cannot be v's complement when the phrase containing the indirect object merges with v.

def Newman2024.configuration (t : XTree) : Binding.Configuration Core.Order.TreePath

In the binding configuration of a tree, a commands b when every maximal projection properly dominating a dominates b and b does not c-command a. Binding is not restricted to a domain.

Equations

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

@[instance_reducible]

instance Newman2024.instDecidableRelTreePathCommandsConfiguration (t : XTree) : DecidableRel (configuration t).commands

Equations

• Newman2024.instDecidableRelTreePathCommandsConfiguration t a b = { decide := decide ((a, b) ∈ PhraseStructure.Tree.maxCommand t) && decide ¬RoseTree.CCommands t b a, reflects_decide := ⋯ }

def Newman2024.leafPaths (t : XTree) : List (Leaf × Core.Order.TreePath)

leafPaths t pairs each leaf of t with its position.

Equations

• Newman2024.leafPaths t = List.map (fun (x : Core.Order.TreePath × Minimalist.Cat × Newman2024.Leaf) => (x.2.2, x.1)) (PhraseStructure.Tree.positionedTerminals t)

def Newman2024.CanBind (t : XTree) (x y : Leaf) : Prop

The leaf x can bind the leaf y in t.

Equations

• Newman2024.CanBind t x y = ∃ a ∈ List.lookup x (Newman2024.leafPaths t), ∃ b ∈ List.lookup y (Newman2024.leafPaths t), (Newman2024.configuration t).commands a b

@[instance_reducible]

instance Newman2024.instDecidableCanBind (t : XTree) (x y : Leaf) : Decidable (CanBind t x y)

Equations

• Newman2024.instDecidableCanBind t x y = Newman2024.instDecidableCanBind._aux_1 t x y

def Newman2024.Precedes (t : XTree) (x y : Leaf) : Prop

The leaf x precedes the leaf y in t when its position precedes y's.

Equations

• Newman2024.Precedes t x y = ∃ a ∈ List.lookup x (Newman2024.leafPaths t), ∃ b ∈ List.lookup y (Newman2024.leafPaths t), a.Precedes b

@[instance_reducible]

instance Newman2024.instDecidablePrecedes (t : XTree) (x y : Leaf) : Decidable (Precedes t x y)

Equations

• Newman2024.instDecidablePrecedes t x y = Newman2024.instDecidablePrecedes._aux_1 t x y

theorem Newman2024.canBind_dobj_iobj : CanBind lowXP Leaf.dobj Leaf.iobj ∧ ¬CanBind lowXP Leaf.iobj Leaf.dobj ∧ ∀ t ∈ [highXP, highXPRight], CanBind t Leaf.iobj Leaf.dobj ∧ ¬CanBind t Leaf.dobj Leaf.iobj

With the indirect object in V's complement, the direct object binds it and not conversely; with it in v's complement, the converse holds, however VP is linearized.

theorem Newman2024.highXP_not_cCommands : ∃ a ∈ List.lookup Leaf.dobj (leafPaths highXP), ∃ b ∈ List.lookup Leaf.iobj (leafPaths highXP), ¬RoseTree.CCommands highXP a b ∧ ¬RoseTree.CCommands highXP b a

With the indirect object in v's complement neither object c-commands the other.

theorem Newman2024.wordOrder_binding : (∀ t ∈ ditransitives, Precedes t Leaf.iobj Leaf.dobj → ¬CanBind t Leaf.dobj Leaf.iobj) ∧ (∃ t ∈ ditransitives, Precedes t Leaf.dobj Leaf.iobj ∧ CanBind t Leaf.dobj Leaf.iobj) ∧ ∃ t ∈ ditransitives, Precedes t Leaf.dobj Leaf.iobj ∧ CanBind t Leaf.iobj Leaf.dobj

Word order and binding. When the indirect object precedes the direct object, the direct object cannot bind it; when it follows, either can bind the other.

Subject questions and agent focus

inductive Newman2024.Transitive : Type

The phrases merging with v in a transitive clause are VP, the internal argument moving out of it, and the external argument.

• vp : Transitive
• obj : Transitive
• subj : Transitive

@[instance_reducible]

instance Newman2024.instDecidableEqTransitive : DecidableEq Transitive

Equations

• Newman2024.instDecidableEqTransitive x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Newman2024.instReprTransitive.repr : Transitive → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Newman2024.instReprTransitive.repr Newman2024.Transitive.vp prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Newman2024.Transitive.vp")).group prec✝
• Newman2024.instReprTransitive.repr Newman2024.Transitive.obj prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Newman2024.Transitive.obj")).group prec✝

@[instance_reducible]

instance Newman2024.instReprTransitive : Repr Transitive

Equations

• Newman2024.instReprTransitive = { reprPrec := Newman2024.instReprTransitive.repr }

def Newman2024.Transitive.phrase (obj : Minimalist.Cat) (whs : List Transitive) : Transitive → Phrase

Transitive.phrase obj whs a is the phrase a is, with an object of category obj and the phrases in whs bearing [wh].

Equations

• Newman2024.Transitive.phrase obj whs Newman2024.Transitive.vp = Newman2024.Phrase.vp
• Newman2024.Transitive.phrase obj whs Newman2024.Transitive.obj = { cat := obj, bears := if Newman2024.Transitive.obj ∈ whs then {Newman2024.Feature.wh} else ∅ }
• Newman2024.Transitive.phrase obj whs Newman2024.Transitive.subj = { cat := Minimalist.Cat.D, bears := if Newman2024.Transitive.subj ∈ whs then {Newman2024.Feature.wh} else ∅ }

@[reducible, inline]

abbrev Newman2024.TransitiveDerivation (P : Finset Feature) (obj : Minimalist.Cat) (whs es : List Transitive) : Prop

TransitiveDerivation P obj whs es says that VP merges with v as its complement and then the specifiers es merge, with the features in P staying active.

Equations

• Newman2024.TransitiveDerivation P obj whs es = Newman2024.Licensed (Newman2024.Phrase.checks ∘ Newman2024.Transitive.phrase obj whs) P Newman2024.bundlev (Newman2024.Transitive.vp :: es)

theorem Newman2024.transitive_derivations {es : List Transitive} : (TransitiveDerivation ∅ Minimalist.Cat.D [Transitive.subj] es ∧ Transitive.subj ∈ es ↔ es = [Transitive.subj] ∨ es = [Transitive.obj, Transitive.subj]) ∧ (TransitiveDerivation ∅ Minimalist.Cat.D [Transitive.obj] es ∧ Transitive.subj ∈ es ∧ Transitive.obj ∈ es ↔ es = [Transitive.subj, Transitive.obj])

Subject and object questions. With an external argument and the wh-phrase passing through the edge of vP, a subject question has two derivations, the subject checking [·D·] and [·wh·] at once or the object checking [·D·] first; an object question has one, the subject merging before the wh-object.

def Newman2024.heightOrder (es : List Transitive) : List Transitive

heightOrder es lists the arguments from the highest down once the specifiers es have merged, the specifiers first with the first merged outermost, then the object in situ unless it has moved.

Equations

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

def Newman2024.caseOf (es : List Transitive) (a : Transitive) : Option Case

When the first specifier merges, the dependent rules of an ergative grammar assign case to the arguments then in vP, highest first and without the moved object's lower copy. A specifier merged later is unmarked.

Equations

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

def Newman2024.setA (es : List Transitive) : Option Transitive

Voice's φ-probe, spelled out as Set A, agrees with the closest argument.

Equations

• Newman2024.setA es = (Newman2024.heightOrder es).head?

def Newman2024.setB (es : List Transitive) : Option Transitive

T's φ-probe, spelled out as Set B, agrees with the closest absolutive argument.

Equations

• Newman2024.setB es = List.find? (fun (a : Newman2024.Transitive) => decide (Newman2024.caseOf es a = some Case.abs)) (Newman2024.heightOrder es)

def Newman2024.AgentFocus (es : List Transitive) : Prop

When the adjacent probes on Voice and T cross-reference the same argument, anti-redundancy deletes Voice's copy, and Voice is spelled out as the agent-focus morpheme.

Equations

• Newman2024.AgentFocus es = (Newman2024.setA es = Newman2024.setB es)

@[instance_reducible]

instance Newman2024.instDecidableAgentFocus (es : List Transitive) : Decidable (AgentFocus es)

Equations

• Newman2024.instDecidableAgentFocus es = Newman2024.instDecidableAgentFocus._aux_1 es

theorem Newman2024.agentFocus_iff {whs : List Transitive} (hw : whs ∈ [[], [Transitive.subj], [Transitive.obj], [Transitive.subj, Transitive.obj]]) {es : List Transitive} (h : TransitiveDerivation ∅ Minimalist.Cat.D whs es) (hs : Transitive.subj ∈ es) : AgentFocus es ↔ es = [Transitive.obj, Transitive.subj]

Agent focus. Whichever phrases are wh-phrases, in a transitive derivation with an external argument Voice and T cross-reference the same argument exactly when the object checks [·D·] before the subject merges.

theorem Newman2024.npObject_no_agentFocus {es : List Transitive} (h : TransitiveDerivation ∅ Minimalist.Cat.N [Transitive.subj] es) (hs : Transitive.subj ∈ es) : es = [Transitive.subj] ∧ setA es = some Transitive.subj ∧ setB es = some Transitive.obj ∧ ¬AgentFocus es

NP objects obviate agent focus. An NP object cannot check [·D·], so a subject question has only the derivation in which the subject checks [·D·] and [·wh·] at once; Set A cross-references the subject and Set B the object, as in a transitive clause.

theorem Newman2024.multipleFronting_blocked {es : List Transitive} (h : TransitiveDerivation ∅ Minimalist.Cat.D [Transitive.subj, Transitive.obj] es) : ¬(Transitive.subj ∈ es ∧ Transitive.obj ∈ es)

When [·wh·] is checked once, a wh-subject and a wh-object cannot both become specifiers of v, whichever merges first.

theorem Newman2024.multipleFronting {es : List Transitive} (hnd : es.Nodup) (hs : Transitive.subj ∈ es) (ho : Transitive.obj ∈ es) : (TransitiveDerivation {Feature.wh} Minimalist.Cat.D [Transitive.subj] es ↔ es = [Transitive.obj, Transitive.subj]) ∧ (TransitiveDerivation {Feature.wh} Minimalist.Cat.D [Transitive.obj] es ↔ es = [Transitive.subj, Transitive.obj]) ∧ (TransitiveDerivation {Feature.wh} Minimalist.Cat.D [Transitive.subj, Transitive.obj] es ↔ es = [Transitive.subj, Transitive.obj] ∨ es = [Transitive.obj, Transitive.subj]) ∧ ∀ whs ∈ [[Transitive.subj], [Transitive.obj], [Transitive.subj, Transitive.obj]], TransitiveDerivation {Feature.wh} Minimalist.Cat.D whs es → (AgentFocus es ↔ es = [Transitive.obj, Transitive.subj])

Multiple fronting. When [·wh·] stays active, a wh-subject and a plain object merge object first, a wh-object and a plain subject subject first, and two wh-phrases in either order; agent focus arises exactly when the object is the outer specifier.

Weak Economy

structure Newman2024.System (ι : Type u_1) : Type u_1

A system of operations at v fixes the features each operation checks, the operations, and when an operation is available given the ones already applied.

• checks : ι → Finset Feature

  checks a is the set of features operation a checks.

• ops : List ι

  ops lists the operations.

• Available : List ι → ι → Prop

  Available done a holds when a is available after the operations done.

• decAvailable (done : List ι) (a : ι) : Decidable (self.Available done a)

  Availability is decidable.

def Newman2024.System.Possible {ι : Type u_1} (S : System ι) (s : Finset Feature) (done : List ι) (a : ι) : Prop

An operation is possible when it has not applied, is available, and would check an unchecked Merge feature.

Equations

• S.Possible s done a = (a ∉ done ∧ S.Available done a ∧ ∃ f ∈ s ∩ S.checks a, f.IsMerge)

@[instance_reducible]

instance Newman2024.System.instDecidablePossible {ι : Type u_1} [DecidableEq ι] (S : System ι) (s : Finset Feature) (done : List ι) (a : ι) : Decidable (S.Possible s done a)

Equations

• S.instDecidablePossible s done a = { decide := decide (a ∉ done) && decide (S.Available done a ∧ ∃ f ∈ s ∩ S.checks a, f.IsMerge), reflects_decide := ⋯ }

def Newman2024.System.Bleeds {ι : Type u_1} (S : System ι) (s : Finset Feature) (done : List ι) (a b : ι) : Prop

Doing a bleeds b when b is possible now but not once a has applied, Kiparsky's bleeding over the unchecked features and the operations done.

Equations

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

@[instance_reducible]

instance Newman2024.System.instDecidableBleeds {ι : Type u_1} [DecidableEq ι] (S : System ι) (s : Finset Feature) (done : List ι) (a b : ι) : Decidable (S.Bleeds s done a b)

Equations

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

def Newman2024.System.Exempt {ι : Type u_1} (S : System ι) (s : Finset Feature) (done : List ι) (a b : ι) : Prop

Weak Economy does not compare two operations when either would bleed the other.

Equations

• S.Exempt s done a b = (S.Bleeds s done a b ∨ S.Bleeds s done b a)

@[instance_reducible]

instance Newman2024.System.instDecidableExempt {ι : Type u_1} [DecidableEq ι] (S : System ι) (s : Finset Feature) (done : List ι) (a b : ι) : Decidable (S.Exempt s done a b)

Equations

• S.instDecidableExempt s done a b = { decide := decide (S.Bleeds s done a b) || decide (S.Bleeds s done b a), reflects_decide := ⋯ }

def Newman2024.System.ExemptLiteral {ι : Type u_1} (S : System ι) (s : Finset Feature) (done : List ι) (a b : ι) : Prop

Weak Economy as Newman words it exempts a from comparison with an operation b checking more features only when doing b would bleed a.

Equations

• S.ExemptLiteral s done a b = S.Bleeds s done b a

@[instance_reducible]

instance Newman2024.System.instDecidableExemptLiteral {ι : Type u_1} [DecidableEq ι] (S : System ι) (s : Finset Feature) (done : List ι) (a b : ι) : Decidable (S.ExemptLiteral s done a b)

Equations

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

def Newman2024.System.ExemptOverlap {ι : Type u_1} (S : System ι) (s : Finset Feature) (done : List ι) (a b : ι) : Prop

Newman's conjecture further exempts two operations that would check a common feature.

Equations

• S.ExemptOverlap s done a b = (S.Exempt s done a b ∨ (s ∩ S.checks a ∩ S.checks b).Nonempty)

@[instance_reducible]

instance Newman2024.System.instDecidableExemptOverlap {ι : Type u_1} [DecidableEq ι] (S : System ι) (s : Finset Feature) (done : List ι) (a b : ι) : Decidable (S.ExemptOverlap s done a b)

Equations

• S.instDecidableExemptOverlap s done a b = { decide := decide (S.Exempt s done a b) || decide (s ∩ S.checks a ∩ S.checks b).Nonempty, reflects_decide := ⋯ }

def Newman2024.System.WeakEconomy {ι : Type u_1} (S : System ι) (E : Finset Feature → List ι → ι → ι → Prop) (s : Finset Feature) (done : List ι) (a : ι) : Prop

Weak Economy permits a unless some possible operation would check more features and is not exempt from comparison with it under E.

Equations

• S.WeakEconomy E s done a = ∀ b ∈ S.ops, S.Possible s done b → (s ∩ S.checks a).card < (s ∩ S.checks b).card → E s done a b

@[instance_reducible]

instance Newman2024.System.instDecidableWeakEconomy {ι : Type u_1} [DecidableEq ι] (S : System ι) (E : Finset Feature → List ι → ι → ι → Prop) [(s : Finset Feature) → (d : List ι) → (a b : ι) → Decidable (E s d a b)] (s : Finset Feature) (done : List ι) (a : ι) : Decidable (S.WeakEconomy E s done a)

Equations

• S.instDecidableWeakEconomy E s done a = Newman2024.System.instDecidableWeakEconomy._aux_1 S E s done a

def Newman2024.System.Derivation {ι : Type u_1} (S : System ι) (E : Finset Feature → List ι → ι → ι → Prop) : Finset Feature → List ι → List ι → Prop

S.Derivation E s done es holds when, after the operations done and with s unchecked, the operations es apply in order, each possible and permitted by Weak Economy, until no operation is possible.

Equations

• S.Derivation E x✝¹ x✝ [] = ∀ b ∈ S.ops, ¬S.Possible x✝¹ x✝ b
• S.Derivation E x✝¹ x✝ (e :: es) = (e ∈ S.ops ∧ S.Possible x✝¹ x✝ e ∧ S.WeakEconomy E x✝¹ x✝ e ∧ S.Derivation E (x✝¹ \ S.checks e) (x✝ ++ [e]) es)

@[instance_reducible]

instance Newman2024.System.decDerivation {ι : Type u_1} [DecidableEq ι] (S : System ι) (E : Finset Feature → List ι → ι → ι → Prop) [(s : Finset Feature) → (d : List ι) → (a b : ι) → Decidable (E s d a b)] (s : Finset Feature) (done es : List ι) : Decidable (S.Derivation E s done es)

Equations

• One or more equations did not get rendered due to their size.
• S.decDerivation E x✝¹ x✝ [] = Newman2024.System.decDerivation._aux_1 S E x✝¹ x✝

@[reducible, inline]

abbrev Newman2024.System.Economical {ι : Type u_1} (S : System ι) (s : Finset Feature) (es : List ι) : Prop

An economical derivation is one under Weak Economy as Newman applies it, from scratch.

Equations

• S.Economical s es = S.Derivation S.Exempt s [] es

@[reducible, inline]

abbrev Newman2024.System.OverlapEconomical {ι : Type u_1} (S : System ι) (s : Finset Feature) (es : List ι) : Prop

An overlap-economical derivation is one under Newman's conjecture, from scratch.

Equations

• S.OverlapEconomical s es = S.Derivation S.ExemptOverlap s [] es

def Newman2024.System.subject {ι : Type u_1} (S : System ι) (es : List ι) : Option ι

The subject of a derivation is the first operation that can check v's [·D·].

Equations

• S.subject es = List.find? (fun (a : ι) => decide (Newman2024.Feature.D ∈ S.checks a)) es

theorem Newman2024.System.derivation_cons {ι : Type u_1} {S : System ι} {E : Finset Feature → List ι → ι → ι → Prop} {s : Finset Feature} {done es : List ι} {e : ι} : S.Derivation E s done (e :: es) ↔ e ∈ S.ops ∧ S.Possible s done e ∧ S.WeakEconomy E s done e ∧ S.Derivation E (s \ S.checks e) (done ++ [e]) es

theorem Newman2024.System.Derivation.nodup {ι : Type u_1} {S : System ι} {E : Finset Feature → List ι → ι → ι → Prop} {s : Finset Feature} {done es : List ι} (h : S.Derivation E s done es) : es.Nodup ∧ es ⊆ S.ops ∧ ∀ e ∈ es, e ∉ done

The operations of a derivation are distinct, drawn from the system, and new.

theorem Newman2024.System.exists_derivation {ι : Type u_1} [DecidableEq ι] {S : System ι} (E : Finset Feature → List ι → ι → ι → Prop) (s : Finset Feature) (done : List ι) : ∃ (es : List ι), S.Derivation E s done es

Weak Economy never blocks every operation. The possible operation checking the most features is always permitted, so from any state some derivation runs to completion, whatever the exemptions.

theorem Newman2024.System.Derivation.licensed {ι : Type u_1} {S : System ι} {E : Finset Feature → List ι → ι → ι → Prop} {s : Finset Feature} {done es : List ι} (h : S.Derivation E s done es) : Licensed S.checks ∅ s es

Every derivation is licensed, since Weak Economy only restricts the order of operations.

Passives of ditransitives

inductive Newman2024.Passive : Type

The operations at v in a passive ditransitive are raising the indirect object, merging VP, and raising the direct object.

• iobj : Passive
• vp : Passive
• dobj : Passive

@[instance_reducible]

instance Newman2024.instDecidableEqPassive : DecidableEq Passive

Equations

• Newman2024.instDecidableEqPassive x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Newman2024.instReprPassive.repr : Passive → ℕ → Std.Format

Equations

• Newman2024.instReprPassive.repr Newman2024.Passive.iobj prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Newman2024.Passive.iobj")).group prec✝
• Newman2024.instReprPassive.repr Newman2024.Passive.vp prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Newman2024.Passive.vp")).group prec✝
• Newman2024.instReprPassive.repr Newman2024.Passive.dobj prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Newman2024.Passive.dobj")).group prec✝

@[instance_reducible]

instance Newman2024.instReprPassive : Repr Passive

Equations

• Newman2024.instReprPassive = { reprPrec := Newman2024.instReprPassive.repr }

def Newman2024.Passive.phrase (io dobj : Phrase) : Passive → Phrase

Passive.phrase io dobj a is the phrase operation a merges, given the indirect object io and the direct object dobj.

Equations

• Newman2024.Passive.phrase io dobj Newman2024.Passive.iobj = io
• Newman2024.Passive.phrase io dobj Newman2024.Passive.vp = Newman2024.Phrase.vp
• Newman2024.Passive.phrase io dobj Newman2024.Passive.dobj = dobj

def Newman2024.highPassive (io dobj : Phrase) : System Passive

In a double object passive the indirect object sits in v's complement, accessible from the start, and the direct object is accessible once VP has merged.

Equations

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

def Newman2024.lowPassive (io dobj : Phrase) : System Passive

In a prepositional passive VP is v's complement and the direct object c-commands the indirect object, so the indirect object is accessible only once the direct object has moved.

Equations

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

def Newman2024.afterXP : Finset Feature

afterXP is the set of v's features left once the phrase containing the indirect object has checked [·X·].

Equations

• Newman2024.afterXP = Newman2024.bundlev \ { cat := Minimalist.Cat.P }.checks

theorem Newman2024.symmetric_passive : (∃ (es : List Passive), (highPassive Phrase.dp Phrase.dp).Economical afterXP es ∧ (highPassive Phrase.dp Phrase.dp).subject es = some Passive.iobj) ∧ ∃ (es : List Passive), (highPassive Phrase.dp Phrase.dp).Economical afterXP es ∧ (highPassive Phrase.dp Phrase.dp).subject es = some Passive.dobj

Symmetric passives. With plain objects either one can become the subject of a double object passive.

theorem Newman2024.doma {es : List Passive} (h : (highPassive Phrase.whDP Phrase.dp).Economical afterXP es) : (highPassive Phrase.whDP Phrase.dp).subject es = some Passive.iobj

The double object movement asymmetry. A wh indirect object checks [·D·] and [·wh·] at once, so Weak Economy raises it before VP merges, and it is the subject of every passive.

theorem Newman2024.whDobj_symmetric : (∃ (es : List Passive), (highPassive Phrase.dp Phrase.whDP).Economical afterXP es ∧ (highPassive Phrase.dp Phrase.whDP).subject es = some Passive.iobj) ∧ ∃ (es : List Passive), (highPassive Phrase.dp Phrase.whDP).Economical afterXP es ∧ (highPassive Phrase.dp Phrase.whDP).subject es = some Passive.dobj

A wh direct object becomes accessible only after VP merges, too late to force the order, so either object can still become the subject.

theorem Newman2024.lowPassive_subject {io : Phrase} (hio : io ∈ [Phrase.dp, Phrase.whDP]) {es : List Passive} (h : (lowPassive io Phrase.dp).Economical bundlev es) : (lowPassive io Phrase.dp).subject es = some Passive.dobj

In a prepositional passive only the direct object can become the subject, even when the indirect object is a wh-phrase.

theorem Newman2024.iobj_kp_not_subject {bears : Finset Feature} (hD : Feature.D ∉ bears) (dobj : Phrase) (es : List Passive) : (highPassive { cat := Minimalist.Cat.K, bears := bears } dobj).subject es ≠ some Passive.iobj

No indirect object passives with inherent case. An indirect object with an inherent-case shell cannot check [·D·], so it is never the passive subject.

Object marking

def Newman2024.bundlevOM : Finset Feature

v in a language with object marking also bears the object-marking feature.

Equations

• Newman2024.bundlevOM = insert Newman2024.Feature.om Newman2024.bundlev

def Newman2024.afterXPOM : Finset Feature

afterXPOM is the set of such a v's features left once the phrase containing the indirect object has checked [·X·].

Equations

• Newman2024.afterXPOM = Newman2024.bundlevOM \ { cat := Minimalist.Cat.P }.checks

def Newman2024.omDP : Phrase

omDP is a DP controlling object marking.

Equations

• Newman2024.omDP = { cat := Minimalist.Cat.D, bears := {Newman2024.Feature.om} }

theorem Newman2024.om_iobj_subject {es : List Passive} (h : (highPassive omDP Phrase.dp).Economical afterXPOM es) : (highPassive omDP Phrase.dp).subject es = some Passive.iobj

An indirect object controlling object marking checks [·D·] and the object-marking feature at once, so it is the subject of every passive.

theorem Newman2024.om_dobj_recipientPassive : ∃ (es : List Passive), (highPassive Phrase.dp omDP).Economical afterXPOM es ∧ (highPassive Phrase.dp omDP).subject es = some Passive.iobj ∧ Passive.dobj ∈ es

A direct object can control object marking in a passive whose subject is the indirect object.

Greek clitic doubling

inductive Newman2024.Greek : Type

The operations at Greek v after the phrase containing the indirect object has merged are clitic doubling the indirect object, wh-moving its KP, merging VP, raising the direct object, and merging the external argument.

• clitic : Greek
• kp : Greek
• vp : Greek
• dobj : Greek
• subj : Greek

@[instance_reducible]

instance Newman2024.instDecidableEqGreek : DecidableEq Greek

Equations

• Newman2024.instDecidableEqGreek x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Newman2024.instReprGreek : Repr Greek

Equations

• Newman2024.instReprGreek = { reprPrec := Newman2024.instReprGreek.repr }

def Newman2024.instReprGreek.repr : Greek → ℕ → Std.Format

Equations

• Newman2024.instReprGreek.repr Newman2024.Greek.clitic prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Newman2024.Greek.clitic")).group prec✝
• Newman2024.instReprGreek.repr Newman2024.Greek.kp prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Newman2024.Greek.kp")).group prec✝
• Newman2024.instReprGreek.repr Newman2024.Greek.vp prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Newman2024.Greek.vp")).group prec✝
• Newman2024.instReprGreek.repr Newman2024.Greek.dobj prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Newman2024.Greek.dobj")).group prec✝
• Newman2024.instReprGreek.repr Newman2024.Greek.subj prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Newman2024.Greek.subj")).group prec✝

def Newman2024.bundlevGreek : Finset Feature

Greek v bears [·Dweak·] and a φ-probe besides v's features.

Equations

• Newman2024.bundlevGreek = {Newman2024.Feature.D, Newman2024.Feature.Dweak, Newman2024.Feature.X, Newman2024.Feature.V, Newman2024.Feature.wh, Newman2024.Feature.phi}

def Newman2024.afterXPGreek : Finset Feature

afterXPGreek is the set of Greek v's features left once the phrase containing the indirect object has checked [·X·].

Equations

• Newman2024.afterXPGreek = Newman2024.bundlevGreek \ { cat := Minimalist.Cat.P }.checks

def Newman2024.Greek.checks (kp : Phrase) : Greek → Finset Feature

Clitic doubling Agrees with the DP inside the indirect object's KP and moves a clitic, a weak D-element, so it checks [uφ] and [·Dweak·]; the other operations check what their phrases check.

Equations

• Newman2024.Greek.checks kp Newman2024.Greek.clitic = {Newman2024.Feature.Dweak, Newman2024.Feature.phi}
• Newman2024.Greek.checks kp Newman2024.Greek.kp = kp.checks
• Newman2024.Greek.checks kp Newman2024.Greek.vp = Newman2024.Phrase.vp.checks
• Newman2024.Greek.checks kp Newman2024.Greek.dobj = Newman2024.Phrase.dp.checks
• Newman2024.Greek.checks kp Newman2024.Greek.subj = Newman2024.Phrase.dp.checks

def Newman2024.greek (kp : Phrase) (ops : List Greek) : System Greek

greek kp ops is Greek v with the indirect object's KP kp and the operations ops. The clitic is accessible while the KP is in v's complement, the direct object once VP has merged.

Equations

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

def Newman2024.greekPassive : List Greek

greekPassive lists the operations of a Greek passive.

Equations

• Newman2024.greekPassive = [Newman2024.Greek.clitic, Newman2024.Greek.kp, Newman2024.Greek.vp, Newman2024.Greek.dobj]

def Newman2024.greekActive : List Greek

greekActive lists the operations of a Greek active.

Equations

• Newman2024.greekActive = [Newman2024.Greek.clitic, Newman2024.Greek.kp, Newman2024.Greek.vp, Newman2024.Greek.dobj, Newman2024.Greek.subj]

theorem Newman2024.greek_passive {es : List Greek} (h : (greek { cat := Minimalist.Cat.K } greekPassive).Economical afterXPGreek es) : es.head? = some Greek.clitic ∧ (greek { cat := Minimalist.Cat.K } greekPassive).subject es = some Greek.dobj

Dative intervention. In a Greek passive, clitic doubling checks two features and merging VP one, so the indirect object is clitic doubled before the direct object can raise.

theorem Newman2024.greek_whPassive : (∀ (es : List Greek), (greek { cat := Minimalist.Cat.K, bears := {Feature.wh} } greekPassive).Economical afterXPGreek es → (greek { cat := Minimalist.Cat.K, bears := {Feature.wh} } greekPassive).subject es = some Greek.dobj) ∧ (∃ (es : List Greek), (greek { cat := Minimalist.Cat.K, bears := {Feature.wh} } greekPassive).Economical afterXPGreek es ∧ Greek.clitic ∉ es) ∧ ∃ (es : List Greek), (greek { cat := Minimalist.Cat.K, bears := {Feature.wh} } greekPassive).Economical afterXPGreek es ∧ Greek.clitic ∈ es

A wh indirect object makes clitic doubling optional. Wh-moving the KP out of v's complement bleeds clitic doubling, so Weak Economy does not compare the two, and the direct object is the subject either way.

theorem Newman2024.greek_active : (∃ (es : List Greek), (greek { cat := Minimalist.Cat.K } greekActive).Economical afterXPGreek es ∧ Greek.subj ∈ es ∧ Greek.clitic ∈ es) ∧ ∃ (es : List Greek), (greek { cat := Minimalist.Cat.K } greekActive).Economical afterXPGreek es ∧ Greek.subj ∈ es ∧ Greek.clitic ∉ es

In a Greek active clitic doubling is optional. The external argument checks [·D·] and [·Dweak·], as many features as clitic doubling, and bleeds it by checking [·Dweak·].

def Newman2024.greekFlat (kp : Phrase) (ops : List Greek) : System Greek

greekFlat kp ops is Greek v in a system where wh-movement of the KP would leave the clitic accessible.

Equations

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

theorem Newman2024.greekFlat_whPassive {es : List Greek} (h : (greekFlat { cat := Minimalist.Cat.K, bears := {Feature.wh} } greekPassive).Economical afterXPGreek es) : Greek.clitic ∈ es

Without the structural bleeding, Weak Economy would force clitic doubling in wh passives, so the optionality of Greek clitic doubling depends on wh-movement removing the KP from v's complement.

theorem Newman2024.literal_greek_whPassive {es : List Greek} (h : (greek { cat := Minimalist.Cat.K, bears := {Feature.wh} } greekPassive).Derivation (greek { cat := Minimalist.Cat.K, bears := {Feature.wh} } greekPassive).ExemptLiteral afterXPGreek [] es) : Greek.clitic ∈ es

The wording of Weak Economy. Read as worded, Weak Economy exempts an operation only when the operation checking more features would bleed it. Clitic doubling checks more features than wh-movement of the KP and does not bleed it, so under that reading clitic doubling would be obligatory in Greek wh passives, contrary to the passives without a clitic that Newman cites; her analysis needs the bleeding of either operation by the other to exempt them.

Weak Economy in subject questions

def Newman2024.transitiveSystem (whs : List Transitive) : System Transitive

transitiveSystem whs has the operations at v in a transitive clause with the phrases in whs bearing [wh], namely merging VP, moving the object once VP has merged, and merging the external argument.

Equations

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

theorem Newman2024.whSubject_complement {es : List Transitive} (h : (transitiveSystem [Transitive.subj]).Economical bundlev es) : es.head? = some Transitive.subj

Weak Economy makes a wh-subject v's complement. The wh-subject checks [·D·], [·X·] and [·wh·], VP only [·X·] and [·V·], and neither bleeds the other, so Weak Economy merges the subject first, ruling out both subject-question derivations with VP as v's complement.

theorem Newman2024.plainSubject_either : (∃ (es : List Transitive), (transitiveSystem []).Economical bundlev es ∧ es.head? = some Transitive.vp) ∧ ∃ (es : List Transitive), (transitiveSystem []).Economical bundlev es ∧ es.head? = some Transitive.subj

With a plain subject, VP and the subject check two features each, so either can be v's complement.

theorem Newman2024.overlap_subjectQuestions : (transitiveSystem [Transitive.subj]).OverlapEconomical bundlev [Transitive.vp, Transitive.subj] ∧ (transitiveSystem [Transitive.subj]).OverlapEconomical bundlev [Transitive.vp, Transitive.obj, Transitive.subj] ∧ (transitiveSystem [Transitive.obj]).OverlapEconomical bundlev [Transitive.vp, Transitive.subj, Transitive.obj]

Newman's conjecture restores the subject-question derivations. When operations checking a common feature are exempt, VP and a wh-subject, which share [·X·], are not compared, and both subject-question derivations and the object-question derivation are economical.

theorem Newman2024.overlap_passives : (∀ (es : List Passive), (highPassive Phrase.whDP Phrase.dp).OverlapEconomical afterXP es → (highPassive Phrase.whDP Phrase.dp).subject es = some Passive.iobj) ∧ (∀ (es : List Greek), (greek { cat := Minimalist.Cat.K } greekPassive).OverlapEconomical afterXPGreek es → es.head? = some Greek.clitic) ∧ (∃ (es : List Greek), (greek { cat := Minimalist.Cat.K, bears := {Feature.wh} } greekPassive).OverlapEconomical afterXPGreek es ∧ Greek.clitic ∉ es) ∧ ∃ (es : List Greek), (greek { cat := Minimalist.Cat.K } greekActive).OverlapEconomical afterXPGreek es ∧ Greek.subj ∈ es ∧ Greek.clitic ∉ es

The conjecture leaves the passive results intact. The wh indirect object is still the subject of every double object passive, and Greek clitic doubling is still obligatory in plain passives and optional in wh passives and actives.