Newman (2024) — When Arguments Merge @cite{newman-2024}

Elise Newman (2024). When Arguments Merge. MIT Press (Linguistic Inquiry Monographs 88). ISBN 9780262379960.

Overview

The Categorial Merge Hypothesis (CMH) proposes that all elements of category V share the same Merge features, with only three argument-introducing features: [·D·] (DP-specific), [·X·] (category-unspecified), and [·V·] (VP-merge, v only). Combined with Feature Maximality, Weak Economy, and Generalized Tucking In (@cite{paille-2020}), the CMH derives:

1. Non-DP First: XPs merge before DPs when V bears both features
2. VP-as-specifier: When v bears [·X·], VP is forced to be a specifier of v (not complement)
3. Symmetric passives: In "high IO" ditransitives, neither internal argument c-commands the other, so either can passivize
4. DOMA: Weak Economy forces IO to be passive subject when IO is a wh-phrase (checks more features)
5. No IO passives with inherent case: KPs can't check [·D·], so they can't A-move to subject (Greek, Tamil, German, Turkish, Spanish)
6. Agent Focus in Mayan: Anti-redundancy deletes lower agreement copies when both probes target the same extracted argument

Formalized Predictions

This file formalizes the verb type space, structural predictions about VP-specifierhood and its consequences, the KP/DP distinction for passive accessibility, and anti-redundancy for agreement.

CMH Apparatus (relocated from Minimalism/CMH.lean)

The Categorial Merge Hypothesis primitives below are paper-specific to @cite{newman-2024} (with @cite{paille-2020} for Generalized Tucking In) and not consumed elsewhere in the library, so they live here under namespace Minimalist.CMH for symmetry with other Minimalist apparatus and to support qualified lookup if a future paper picks them up.

inductive Minimalist.CMH.MergeFeature : Type

The three argument-introducing Merge features for verbal heads.

These are the only features that determine how V and v combine with their arguments. All other selectional requirements (c-selection for CPs, PPs, etc.) reduce to [·X·] — category-unspecified Merge.

• D: Merges with DPs only (subjects, objects)
• X: Merges with any non-DP phrase (PPs, CPs, APs, etc.)
• V: Merges with VP (only on v; v selects V)

• D : MergeFeature
• X : MergeFeature
• V : MergeFeature

@[implicit_reducible]

instance Minimalist.CMH.instDecidableEqMergeFeature : DecidableEq MergeFeature

Equations

• Minimalist.CMH.instDecidableEqMergeFeature x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Minimalist.CMH.instReprMergeFeature : Repr MergeFeature

Equations

• Minimalist.CMH.instReprMergeFeature = { reprPrec := Minimalist.CMH.instReprMergeFeature.repr }

def Minimalist.CMH.instReprMergeFeature.repr : MergeFeature → ℕ → Std.Format

Equations

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

def Minimalist.CMH.instBEqMergeFeature.beq : MergeFeature → MergeFeature → Bool

Equations

• Minimalist.CMH.instBEqMergeFeature.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

@[implicit_reducible]

instance Minimalist.CMH.instBEqMergeFeature : BEq MergeFeature

Equations

• Minimalist.CMH.instBEqMergeFeature = { beq := Minimalist.CMH.instBEqMergeFeature.beq }

structure Minimalist.CMH.MergeBundle : Type

A bundle of Merge features on a single head. Represented as counts (0 or 1) of each feature type, reflecting Feature Maximality (a head checks at most one instance of each Merge feature type).

• hasD : Bool
• hasX : Bool
• hasV : Bool

@[implicit_reducible]

instance Minimalist.CMH.instDecidableEqMergeBundle : DecidableEq MergeBundle

Equations

• Minimalist.CMH.instDecidableEqMergeBundle = Minimalist.CMH.instDecidableEqMergeBundle.decEq

def Minimalist.CMH.instDecidableEqMergeBundle.decEq (x✝ x✝¹ : MergeBundle) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance Minimalist.CMH.instReprMergeBundle : Repr MergeBundle

Equations

• Minimalist.CMH.instReprMergeBundle = { reprPrec := Minimalist.CMH.instReprMergeBundle.repr }

def Minimalist.CMH.instReprMergeBundle.repr : MergeBundle → ℕ → Std.Format

Equations

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

def Minimalist.CMH.instBEqMergeBundle.beq : MergeBundle → MergeBundle → Bool

Equations

• Minimalist.CMH.instBEqMergeBundle.beq { hasD := a, hasX := a_1, hasV := a_2 } { hasD := b, hasX := b_1, hasV := b_2 } = (a == b && (a_1 == b_1 && a_2 == b_2))
• Minimalist.CMH.instBEqMergeBundle.beq x✝¹ x✝ = false

@[implicit_reducible]

instance Minimalist.CMH.instBEqMergeBundle : BEq MergeBundle

Equations

• Minimalist.CMH.instBEqMergeBundle = { beq := Minimalist.CMH.instBEqMergeBundle.beq }

def Minimalist.CMH.MergeBundle.featureCount (b : MergeBundle) : ℕ

Number of Merge features in a bundle.

Equations

• b.featureCount = ((if b.hasD = true then 1 else 0) + if b.hasX = true then 1 else 0) + if b.hasV = true then 1 else 0

def Minimalist.CMH.MergeBundle.toList (b : MergeBundle) : List MergeFeature

Convert a bundle to a list of features.

Equations

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

def Minimalist.CMH.isVerbalHead : Cat → Prop

Whether a category is a verbal head in the CMH sense.

Equations

• Minimalist.CMH.isVerbalHead Minimalist.Cat.V = True
• Minimalist.CMH.isVerbalHead Minimalist.Cat.v = True
• Minimalist.CMH.isVerbalHead x✝ = False

@[implicit_reducible]

instance Minimalist.CMH.instDecidablePredCatIsVerbalHead : DecidablePred isVerbalHead

Equations

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

structure Minimalist.CMH.CMHHead : Type

A CMH-compliant verbal head: a V or v with a Merge feature bundle.

Constraint: [·V·] may only appear on v (not V), because V does not select VP — v does.

• cat : Cat

  The category (V or v)

• features : MergeBundle

  The Merge feature bundle

• v_constraint : self.cat = Cat.V → self.features.hasV = false

  V heads may not bear [·V·]

def Minimalist.CMH.instReprCMHHead.repr : CMHHead → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Minimalist.CMH.instReprCMHHead : Repr CMHHead

Equations

• Minimalist.CMH.instReprCMHHead = { reprPrec := Minimalist.CMH.instReprCMHHead.repr }

def Minimalist.CMH.mkVHead (hasD hasX : Bool) : CMHHead

A V head: introduces internal arguments (complements and specifiers).

Equations

• Minimalist.CMH.mkVHead hasD hasX = { cat := Minimalist.Cat.V, features := { hasD := hasD, hasX := hasX, hasV := false }, v_constraint := ⋯ }

def Minimalist.CMH.mkVLittleHead (hasD hasX : Bool) : CMHHead

A v head: introduces external arguments and selects VP.

Equations

• Minimalist.CMH.mkVLittleHead hasD hasX = { cat := Minimalist.Cat.v, features := { hasD := hasD, hasX := hasX, hasV := true }, v_constraint := ⋯ }

structure Minimalist.CMH.VPProfile : Type

Profile of a verb phrase: how many DP and XP arguments V and v collectively introduce. This determines the verb type.

The 4×4 matrix (V's args × v's args) produces all attested verb types, from weather verbs (0+0) to betting verbs (2DP + 2XP).

• vDPArgs : ℕ

  DPs from V (0, 1, or 2)

• vXPArgs : ℕ

  XPs from V (0 or 1)

• littleVDPArgs : ℕ

  DPs from v (0 or 1)

• littleVXPArgs : ℕ

  XPs from v (0 or 1)

def Minimalist.CMH.instDecidableEqVPProfile.decEq (x✝ x✝¹ : VPProfile) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance Minimalist.CMH.instDecidableEqVPProfile : DecidableEq VPProfile

Equations

• Minimalist.CMH.instDecidableEqVPProfile = Minimalist.CMH.instDecidableEqVPProfile.decEq

@[implicit_reducible]

instance Minimalist.CMH.instReprVPProfile : Repr VPProfile

Equations

• Minimalist.CMH.instReprVPProfile = { reprPrec := Minimalist.CMH.instReprVPProfile.repr }

def Minimalist.CMH.instReprVPProfile.repr : VPProfile → ℕ → Std.Format

Equations

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

def Minimalist.CMH.VPProfile.totalDP (p : VPProfile) : ℕ

Total number of DP arguments.

Equations

• p.totalDP = p.vDPArgs + p.littleVDPArgs

def Minimalist.CMH.VPProfile.totalXP (p : VPProfile) : ℕ

Total number of XP arguments.

Equations

• p.totalXP = p.vXPArgs + p.littleVXPArgs

def Minimalist.CMH.VPProfile.totalArgs (p : VPProfile) : ℕ

Total argument count.

Equations

• p.totalArgs = p.totalDP + p.totalXP

def Minimalist.CMH.vpProfile (vHead littleV : CMHHead) : VPProfile

Construct a VPProfile from a V head and v head.

Equations

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

def Minimalist.CMH.weatherVerb : VPProfile

Weather verbs: no arguments (V: ∅, v: [·V·])

Equations

• Minimalist.CMH.weatherVerb = Minimalist.CMH.vpProfile (Minimalist.CMH.mkVHead false false) (Minimalist.CMH.mkVLittleHead false false)

def Minimalist.CMH.unergative : VPProfile

Unergative: one DP subject (V: ∅, v: [·D·][·V·])

Equations

• Minimalist.CMH.unergative = Minimalist.CMH.vpProfile (Minimalist.CMH.mkVHead false false) (Minimalist.CMH.mkVLittleHead true false)

def Minimalist.CMH.unaccusative : VPProfile

Unaccusative: one DP object (V: [·D·], v: [·V·])

Equations

• Minimalist.CMH.unaccusative = Minimalist.CMH.vpProfile (Minimalist.CMH.mkVHead true false) (Minimalist.CMH.mkVLittleHead false false)

def Minimalist.CMH.transitive : VPProfile

Transitive: subject + object (V: [·D·], v: [·D·][·V·])

Equations

• Minimalist.CMH.transitive = Minimalist.CMH.vpProfile (Minimalist.CMH.mkVHead true false) (Minimalist.CMH.mkVLittleHead true false)

def Minimalist.CMH.ditransitiveXP : VPProfile

Ditransitive with XP: e.g. "put the book on the table" (V: [·D·][·X·], v: [·D·][·V·])

Equations

• Minimalist.CMH.ditransitiveXP = Minimalist.CMH.vpProfile (Minimalist.CMH.mkVHead true true) (Minimalist.CMH.mkVLittleHead true false)

def Minimalist.CMH.ditransitiveDOC : VPProfile

Ditransitive DOC: double object (V: [·D·], v: [·D·][·X·][·V·]) where the indirect object is a non-DP introduced by v

Equations

• Minimalist.CMH.ditransitiveDOC = Minimalist.CMH.vpProfile (Minimalist.CMH.mkVHead true false) (Minimalist.CMH.mkVLittleHead true true)

def Minimalist.CMH.raising : VPProfile

Raising: V selects non-DP complement only (e.g., "seem [to VP]") (V: [·X·], v: [·V·])

Equations

• Minimalist.CMH.raising = Minimalist.CMH.vpProfile (Minimalist.CMH.mkVHead false true) (Minimalist.CMH.mkVLittleHead false false)

def Minimalist.CMH.maximalVerb : VPProfile

Maximal verb: both V and v bear both [·D·] and [·X·] (V: [·D·][·X·], v: [·D·][·X·][·V·]) — e.g., "bet"

Equations

• Minimalist.CMH.maximalVerb = Minimalist.CMH.vpProfile (Minimalist.CMH.mkVHead true true) (Minimalist.CMH.mkVLittleHead true true)

inductive Minimalist.CMH.MergeOrder : Type

When V bears both [·D·] and [·X·], the XP merges first (as complement) and the DP second (as specifier).

This follows from Feature Maximality: V can check at most one Merge feature per step. If V first merges with an XP (checking [·X·]), the resulting V' can then merge with a DP (checking [·D·]). The reverse order is blocked because a DP cannot check [·X·].

Represented as an ordering constraint on the features.

• complement : MergeOrder
• specifier : MergeOrder

@[implicit_reducible]

instance Minimalist.CMH.instDecidableEqMergeOrder : DecidableEq MergeOrder

Equations

• Minimalist.CMH.instDecidableEqMergeOrder x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Minimalist.CMH.instReprMergeOrder : Repr MergeOrder

Equations

• Minimalist.CMH.instReprMergeOrder = { reprPrec := Minimalist.CMH.instReprMergeOrder.repr }

def Minimalist.CMH.instReprMergeOrder.repr : MergeOrder → ℕ → Std.Format

Equations

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

def Minimalist.CMH.nonDPFirst (_vHead : CMHHead) (_hD : _vHead.features.hasD = true) (_hX : _vHead.features.hasX = true) : MergeOrder × MergeOrder

For a V head with both [·D·] and [·X·], the XP is the complement and the DP is the specifier.

Equations

• Minimalist.CMH.nonDPFirst _vHead _hD _hX = (Minimalist.CMH.MergeOrder.complement, Minimalist.CMH.MergeOrder.specifier)

def Minimalist.CMH.vpIsSpecifier (littleV : CMHHead) : Bool

When v introduces an XP (v bears [·X·]), VP is forced to become a specifier of v rather than its complement.

This is because v's [·X·] must be checked before [·V·]: the XP merges as v's complement, and then VP merges as v's specifier.

Equations

• Minimalist.CMH.vpIsSpecifier littleV = littleV.features.hasX

def Minimalist.CMH.vAndVFormComplex (littleV : CMHHead) : Bool

When VP is a specifier of v, V and v do not form a complex head (they are not in a head-complement relation). This has consequences for verb movement and ellipsis.

Equations

• Minimalist.CMH.vAndVFormComplex littleV = !Minimalist.CMH.vpIsSpecifier littleV

structure Minimalist.CMH.PendingOp : Type

A pending operation: a possible Merge at a given derivational step. Tracks which features would be checked and whether the operation bleeds any other pending operation.

• featuresChecked : ℕ

  How many features this operation checks

• bleeds : List ℕ

  Which other operations this one would bleed (make impossible)

@[implicit_reducible]

instance Minimalist.CMH.instReprPendingOp : Repr PendingOp

Equations

• Minimalist.CMH.instReprPendingOp = { reprPrec := Minimalist.CMH.instReprPendingOp.repr }

def Minimalist.CMH.instReprPendingOp.repr : PendingOp → ℕ → Std.Format

Equations

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

def Minimalist.CMH.weakEconomyValid (ops : List PendingOp) (chosenIdx : ℕ) : Bool

Equations

• Minimalist.CMH.weakEconomyValid ops chosenIdx = match ops[chosenIdx]? with | none => false | some chosen => Minimalist.CMH.weakEconomyValidAux✝ chosen chosenIdx ops 0

def Minimalist.CMH.mutuallyBleeding (op1 op2 : PendingOp) (i j : ℕ) : Bool

When two operations stand in a bleeding relation (one bleeds the other), Weak Economy does not enforce a preference — either may apply. This captures the optionality in cases like Greek clitic doubling.

Equations

• Minimalist.CMH.mutuallyBleeding op1 op2 i j = (op1.bleeds.contains j || op2.bleeds.contains i)

inductive Minimalist.CMH.SpecPosition : Type

Specifier position in a tree with multiple specifiers. Under Generalized Tucking In, new specifiers merge below existing ones — as close to the head as possible.

• innermost : SpecPosition
• outer (n : ℕ) : SpecPosition

@[implicit_reducible]

instance Minimalist.CMH.instDecidableEqSpecPosition : DecidableEq SpecPosition

Equations

• Minimalist.CMH.instDecidableEqSpecPosition = Minimalist.CMH.instDecidableEqSpecPosition.decEq

def Minimalist.CMH.instDecidableEqSpecPosition.decEq (x✝ x✝¹ : SpecPosition) : Decidable (x✝ = x✝¹)

Equations

• Minimalist.CMH.instDecidableEqSpecPosition.decEq Minimalist.CMH.SpecPosition.innermost Minimalist.CMH.SpecPosition.innermost = isTrue ⋯
• Minimalist.CMH.instDecidableEqSpecPosition.decEq Minimalist.CMH.SpecPosition.innermost (Minimalist.CMH.SpecPosition.outer n) = isFalse ⋯
• Minimalist.CMH.instDecidableEqSpecPosition.decEq (Minimalist.CMH.SpecPosition.outer n) Minimalist.CMH.SpecPosition.innermost = isFalse ⋯
• Minimalist.CMH.instDecidableEqSpecPosition.decEq (Minimalist.CMH.SpecPosition.outer a) (Minimalist.CMH.SpecPosition.outer b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

def Minimalist.CMH.instReprSpecPosition.repr : SpecPosition → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Minimalist.CMH.instReprSpecPosition : Repr SpecPosition

Equations

• Minimalist.CMH.instReprSpecPosition = { reprPrec := Minimalist.CMH.instReprSpecPosition.repr }

def Minimalist.CMH.tuckIn (_existingSpecs : ℕ) : SpecPosition

Tucking in: a new specifier merges below all existing specifiers. Given n existing specifiers, the new one gets position innermost and all existing specifiers shift outward by one.

Equations

• Minimalist.CMH.tuckIn _existingSpecs = Minimalist.CMH.SpecPosition.innermost

inductive Minimalist.CMH.NominalType : Type

Types of nominals, ordered by feature-checking capacity. The CMH establishes an entailment hierarchy among nominal types: wh-DP ⊇ DP ⊇ non-DP in which Merge features each can check.

This hierarchy drives multiple predictions:

• KPs (inherent case → non-DP) cannot A-move (no [·D·] checking)
• wh-DPs check more features than plain DPs (DOMA)
• DPs can satisfy both [·D·] and [·X·] probes

• whDP : NominalType
• dp : NominalType
• nonDP : NominalType

@[implicit_reducible]

instance Minimalist.CMH.instDecidableEqNominalType : DecidableEq NominalType

Equations

• Minimalist.CMH.instDecidableEqNominalType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Minimalist.CMH.instReprNominalType.repr : NominalType → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Minimalist.CMH.instReprNominalType : Repr NominalType

Equations

• Minimalist.CMH.instReprNominalType = { reprPrec := Minimalist.CMH.instReprNominalType.repr }

def Minimalist.CMH.instBEqNominalType.beq : NominalType → NominalType → Bool

Equations

• Minimalist.CMH.instBEqNominalType.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

@[implicit_reducible]

instance Minimalist.CMH.instBEqNominalType : BEq NominalType

Equations

• Minimalist.CMH.instBEqNominalType = { beq := Minimalist.CMH.instBEqNominalType.beq }

def Minimalist.CMH.NominalType.checksMerge : NominalType → MergeFeature → Bool

Which Merge features a nominal type can check.

• wh-DP: checks [·D·] and [·X·]
• DP: checks [·D·] and [·X·]
• non-DP: checks [·X·] only No nominal checks [·V·] (only VP can).

Equations

• Minimalist.CMH.NominalType.whDP.checksMerge Minimalist.CMH.MergeFeature.D = true
• Minimalist.CMH.NominalType.whDP.checksMerge Minimalist.CMH.MergeFeature.X = true
• Minimalist.CMH.NominalType.dp.checksMerge Minimalist.CMH.MergeFeature.D = true
• Minimalist.CMH.NominalType.dp.checksMerge Minimalist.CMH.MergeFeature.X = true
• Minimalist.CMH.NominalType.nonDP.checksMerge Minimalist.CMH.MergeFeature.X = true
• x✝¹.checksMerge x✝ = false

def Minimalist.CMH.NominalType.checksWh : NominalType → Bool

wh-DPs can additionally check [·wh·] on C. This is NOT a Merge feature on V/v but appears on functional heads (C). It is what makes wh-DPs strictly more powerful than plain DPs in the feature-checking hierarchy.

Equations

• Minimalist.CMH.NominalType.whDP.checksWh = true
• x✝.checksWh = false

def Minimalist.CMH.NominalType.aMovementFeatures : NominalType → ℕ

Feature-checking capacity for A-movement (to Spec,TP via [·D·]) plus Ā-features ([·wh·]). This count drives Weak Economy comparisons in DOMA configurations.

Equations

• Minimalist.CMH.NominalType.whDP.aMovementFeatures = 2
• Minimalist.CMH.NominalType.dp.aMovementFeatures = 1
• Minimalist.CMH.NominalType.nonDP.aMovementFeatures = 0

def Minimalist.CMH.NominalType.subsumes : NominalType → NominalType → Bool

The entailment hierarchy: wh-DP ⊇ DP ⊇ non-DP. Each type can check a superset of the features checkable by the types below it.

Equations

• Minimalist.CMH.NominalType.whDP.subsumes x✝ = true
• Minimalist.CMH.NominalType.dp.subsumes Minimalist.CMH.NominalType.dp = true
• Minimalist.CMH.NominalType.dp.subsumes Minimalist.CMH.NominalType.nonDP = true
• Minimalist.CMH.NominalType.nonDP.subsumes Minimalist.CMH.NominalType.nonDP = true
• x✝¹.subsumes x✝ = false

def Minimalist.CMH.NominalType.canAMove (n : NominalType) : Bool

Can this nominal type undergo A-movement? Requires checking [·D·] on T.

Equations

• n.canAMove = n.checksMerge Minimalist.CMH.MergeFeature.D

structure Minimalist.CMH.AgreeCopy : Type

When two adjacent φ-probes copy features of the same goal, the lower copy is deleted at PF. This is the anti-redundancy principle that derives Agent Focus morphology in Mayan languages.

Adjacency is required: only probes with no intervening probe between them trigger deletion of the lower copy.

• probePosition : ℕ
• goalId : ℕ

@[implicit_reducible]

instance Minimalist.CMH.instDecidableEqAgreeCopy : DecidableEq AgreeCopy

Equations

• Minimalist.CMH.instDecidableEqAgreeCopy = Minimalist.CMH.instDecidableEqAgreeCopy.decEq

def Minimalist.CMH.instDecidableEqAgreeCopy.decEq (x✝ x✝¹ : AgreeCopy) : Decidable (x✝ = x✝¹)

Equations

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

def Minimalist.CMH.instReprAgreeCopy.repr : AgreeCopy → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Minimalist.CMH.instReprAgreeCopy : Repr AgreeCopy

Equations

• Minimalist.CMH.instReprAgreeCopy = { reprPrec := Minimalist.CMH.instReprAgreeCopy.repr }

def Minimalist.CMH.probesAdjacent (copies : List AgreeCopy) (c1 c2 : AgreeCopy) : Bool

Two probes are adjacent if no other probe in the configuration has a position strictly between them.

Equations

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

def Minimalist.CMH.redundantCopies (copies : List AgreeCopy) : List AgreeCopy

Identify redundant copies: lower copies where an adjacent higher probe targets the same goal.

Equations

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

def Minimalist.CMH.applyAntiRedundancy (copies : List AgreeCopy) : List AgreeCopy

Delete redundant copies. Returns surviving copies after PF deletion of redundant agreement.

Equations

• Minimalist.CMH.applyAntiRedundancy copies = List.filter (fun (c : Minimalist.CMH.AgreeCopy) => !(Minimalist.CMH.redundantCopies copies).contains c) copies

theorem Newman2024.weather_zero_args : Minimalist.CMH.weatherVerb.totalArgs = 0

Weather verbs have zero arguments.

theorem Newman2024.unergative_one_arg : Minimalist.CMH.unergative.totalArgs = 1

Unergatives have exactly one argument (the subject from v).

theorem Newman2024.unergative_subject_only : Minimalist.CMH.unergative.totalDP = 1 ∧ Minimalist.CMH.unergative.totalXP = 0

theorem Newman2024.unaccusative_one_arg : Minimalist.CMH.unaccusative.totalArgs = 1

Unaccusatives have exactly one argument (the object from V).

theorem Newman2024.unaccusative_object_only : Minimalist.CMH.unaccusative.totalDP = 1 ∧ Minimalist.CMH.unaccusative.totalXP = 0

theorem Newman2024.transitive_two_args : Minimalist.CMH.transitive.totalArgs = 2

Transitives have exactly two DP arguments.

theorem Newman2024.transitive_two_dps : Minimalist.CMH.transitive.totalDP = 2 ∧ Minimalist.CMH.transitive.totalXP = 0

theorem Newman2024.ditrans_xp_three_args : Minimalist.CMH.ditransitiveXP.totalArgs = 3

Ditransitives with an XP argument have three arguments.

theorem Newman2024.ditrans_doc_three_args : Minimalist.CMH.ditransitiveDOC.totalArgs = 3

DOC ditransitives also have three arguments.

theorem Newman2024.raising_one_arg : Minimalist.CMH.raising.totalArgs = 1

Raising verbs have exactly one argument (the XP complement).

theorem Newman2024.maximal_four_args : Minimalist.CMH.maximalVerb.totalArgs = 4

Maximal verbs ("bet") have four arguments.

theorem Newman2024.low_xp_vp_is_complement : Minimalist.CMH.vpIsSpecifier (Minimalist.CMH.mkVLittleHead true false) = false

In a low-XP ditransitive (V: [·D·][·X·], v: [·D·][·V·]), VP is NOT a specifier of v because v lacks [·X·].

theorem Newman2024.high_xp_vp_is_specifier : Minimalist.CMH.vpIsSpecifier (Minimalist.CMH.mkVLittleHead true true) = true

In a high-XP / DOC ditransitive (v: [·D·][·X·][·V·]), VP IS a specifier of v because v bears [·X·].

theorem Newman2024.doc_no_complex_head : Minimalist.CMH.vAndVFormComplex (Minimalist.CMH.mkVLittleHead true true) = false

When VP is a specifier, V and v do NOT form a complex head. This predicts VP-ellipsis mismatches: Voice mismatches are tolerated in simple transitives (V-v complex) but not in DOC ditransitives (VP as specifier).

theorem Newman2024.transitive_forms_complex : Minimalist.CMH.vAndVFormComplex (Minimalist.CMH.mkVLittleHead true false) = true

theorem Newman2024.nonDP_cannot_check_D : Minimalist.CMH.NominalType.nonDP.checksMerge Minimalist.CMH.MergeFeature.D = false

non-DPs (KPs) cannot check [·D·].

theorem Newman2024.nonDP_can_check_X : Minimalist.CMH.NominalType.nonDP.checksMerge Minimalist.CMH.MergeFeature.X = true

theorem Newman2024.dp_checks_D : Minimalist.CMH.NominalType.dp.checksMerge Minimalist.CMH.MergeFeature.D = true

DPs can check both [·D·] and [·X·].

theorem Newman2024.dp_checks_X : Minimalist.CMH.NominalType.dp.checksMerge Minimalist.CMH.MergeFeature.X = true

theorem Newman2024.whDP_checks_wh : Minimalist.CMH.NominalType.whDP.checksWh = true

wh-DPs additionally check [·wh·] on C.

theorem Newman2024.dp_no_wh : Minimalist.CMH.NominalType.dp.checksWh = false

theorem Newman2024.whDP_subsumes_dp : Minimalist.CMH.NominalType.whDP.subsumes Minimalist.CMH.NominalType.dp = true

The entailment hierarchy is a total preorder.

theorem Newman2024.dp_subsumes_nonDP : Minimalist.CMH.NominalType.dp.subsumes Minimalist.CMH.NominalType.nonDP = true

theorem Newman2024.nonDP_not_subsumes_dp : Minimalist.CMH.NominalType.nonDP.subsumes Minimalist.CMH.NominalType.dp = false

theorem Newman2024.nonDP_cannot_amove : Minimalist.CMH.NominalType.nonDP.canAMove = false

A-movement accessibility: DPs and wh-DPs can A-move; non-DPs cannot. This is the core of the no-IO-passive explanation for languages with inherent case on indirect objects.

theorem Newman2024.dp_can_amove : Minimalist.CMH.NominalType.dp.canAMove = true

theorem Newman2024.whDP_can_amove : Minimalist.CMH.NominalType.whDP.canAMove = true

theorem Newman2024.high_io_has_vp_spec : Minimalist.CMH.vpIsSpecifier (Minimalist.CMH.mkVLittleHead true true) = true

The high-IO structure has VP as specifier.

def Newman2024.ioToSubjectWh : Minimalist.CMH.PendingOp

IO-to-subject in wh-passive: IO is a wh-DP. Feature count derived from NominalType.aMovementFeatures .whDP. Unlike Greek CD (§7), DOMA operations are pure alternatives at the same derivational step — not in a bleeding relation.

Equations

• Newman2024.ioToSubjectWh = { featuresChecked := Minimalist.CMH.NominalType.whDP.aMovementFeatures, bleeds := [] }

def Newman2024.doToSubjectWh : Minimalist.CMH.PendingOp

DO-to-subject in wh-passive: DO is a plain DP. Feature count derived from NominalType.aMovementFeatures .dp.

Equations

• Newman2024.doToSubjectWh = { featuresChecked := Minimalist.CMH.NominalType.dp.aMovementFeatures, bleeds := [] }

theorem Newman2024.doma_prefers_io : Minimalist.CMH.weakEconomyValid [ioToSubjectWh, doToSubjectWh] 0 = true

Weak Economy prefers IO-to-subject (checks more features).

theorem Newman2024.doma_disprefers_do : Minimalist.CMH.weakEconomyValid [ioToSubjectWh, doToSubjectWh] 1 = false

Weak Economy disprefers DO-to-subject when IO checks more.

def Newman2024.mayanAFCopies : List Minimalist.CMH.AgreeCopy

Two probes (C at height 3, v at height 1) agree with the same agent (goal 0).

Equations

• Newman2024.mayanAFCopies = [{ probePosition := 3, goalId := 0 }, { probePosition := 1, goalId := 0 }]

theorem Newman2024.af_lower_is_redundant : (Minimalist.CMH.redundantCopies mayanAFCopies).length = 1

Anti-redundancy identifies the lower copy as redundant.

theorem Newman2024.af_surviving_copy : (Minimalist.CMH.applyAntiRedundancy mayanAFCopies).length = 1

After anti-redundancy, only the higher copy (C's agreement) survives.

theorem Newman2024.af_c_probe_survives : (Minimalist.CMH.applyAntiRedundancy mayanAFCopies).head? = some { probePosition := 3, goalId := 0 }

The surviving copy is the one on C (height 3).

def Newman2024.cliticDouble : Minimalist.CMH.PendingOp

In Greek active transitives, three operations compete after IO merges as XP:

1. Clitic double the IO (checks [·D_weak·] + [uφ] = 2 features)
2. Merge VP (checks [·V·] = 1 feature)
3. Merge transitive subject DP (checks [·D·] = 1 feature)

Weak Economy prefers (1) over (2) but NOT over (3): merging the subject checks [·D·] which also checks [·D_weak·], bleeding clitic doubling. Since (1) and (3) stand in a bleeding relation, Weak Economy allows either order — making clitic doubling optional.

Equations

• Newman2024.cliticDouble = { featuresChecked := 2, bleeds := [] }

def Newman2024.mergeVP : Minimalist.CMH.PendingOp

Equations

• Newman2024.mergeVP = { featuresChecked := 1, bleeds := [] }

def Newman2024.mergeSubject : Minimalist.CMH.PendingOp

Equations

• Newman2024.mergeSubject = { featuresChecked := 1, bleeds := [0] }

theorem Newman2024.greek_cd_valid : Minimalist.CMH.weakEconomyValid [cliticDouble, mergeVP, mergeSubject] 0 = true

Clitic doubling is valid under Weak Economy.

theorem Newman2024.greek_subject_valid : Minimalist.CMH.weakEconomyValid [cliticDouble, mergeVP, mergeSubject] 2 = true

Merging the subject is also valid (bleeding licenses either order).

theorem Newman2024.agentive_has_D : (Minimalist.CMH.mkVLittleHead true false).features.hasD = true

CMH v with [·D·] introduces an external argument (thematic).

def Newman2024.passiveV : Minimalist.CMH.CMHHead

CMH v without [·D·] does not introduce an external argument.

Equations

• Newman2024.passiveV = Minimalist.CMH.mkVLittleHead false false

theorem Newman2024.passive_lacks_D : passiveV.features.hasD = false

theorem Newman2024.voice_hasD_ne_assignsTheta : Minimalist.voiceAnticausative.HasD ∧ ¬Minimalist.voiceAnticausative.AssignsTheta ∧ Minimalist.voicePassive.HasD ∧ ¬Minimalist.voicePassive.AssignsTheta

Voice's hasD (PF subcategorization) and assignsTheta (θ-role assignment) do NOT always coincide — confirming that these are distinct features. The CMH's [·D·] corresponds to assignsTheta, not to hasD. Anticausative and passive Voice have hasD = true (anticausative for SE marking, passive for by-phrase licensing) but assignsTheta = false (no θ-role).

def Newman2024.cmhFeatureModel : Minimalist.AgreementModel

The CMH adopts the obligatory-no-crash model for Merge features. This is @cite{newman-2024}'s Assumption 19c: features can go unchecked without crashing.

Equations

• Newman2024.cmhFeatureModel = Minimalist.AgreementModel.obligatoryNocrash

theorem Newman2024.feature_failure_converges (outcome : Minimalist.ProbeOutcome) : Minimalist.derivationConverges cmhFeatureModel outcome = true

Under Feature Failure, unchecked Merge features do not crash.

theorem Newman2024.feature_failure_vs_crash : Minimalist.derivationConverges cmhFeatureModel Minimalist.ProbeOutcome.unvalued = true ∧ Minimalist.derivationConverges Minimalist.AgreementModel.crashOnFailure Minimalist.ProbeOutcome.unvalued = false

The crash model would reject derivations with unchecked features. Feature Failure is what separates the CMH from standard Minimalism on this point.

theorem Newman2024.weather_needs_feature_failure : Minimalist.CMH.weatherVerb.totalDP = 0 ∧ Minimalist.derivationConverges cmhFeatureModel Minimalist.ProbeOutcome.unvalued = true

Weather verbs introduce zero DP arguments. In pro-drop languages without expletives, T's [·D·] goes unchecked — Feature Failure prevents a crash. Under the crash model, an expletive would be required to check T's [·D·].

theorem Newman2024.impersonal_passive_converges : passiveV.features.hasD = false ∧ Minimalist.derivationConverges cmhFeatureModel Minimalist.ProbeOutcome.unvalued = true

Passive v lacks [·D·], so no external argument merges. If no internal argument is available for A-movement to Spec,TP (impersonal passives), T's [·D·] goes unchecked — tolerated by Feature Failure.

def Newman2024.lowXPTree : Minimalist.SyntacticObject

Equations

• Newman2024.lowXPTree = Newman2024.agent₁✝.node (Newman2024.v₁✝.node (Newman2024.DO₁✝.node (Newman2024.V₁✝.node Newman2024.XP₁✝)))

def Newman2024.docTree : Minimalist.SyntacticObject

Equations

• Newman2024.docTree = Newman2024.VP₂✝.node (Newman2024.agent₂✝.node (Newman2024.v₂✝.node Newman2024.IO₂✝))

theorem Newman2024.low_xp_DO_ccommands_XP : Minimalist.cCommandsIn lowXPTree Newman2024.DO₁✝ Newman2024.XP₁✝

Low-XP: DO asymmetrically c-commands XP — binding asymmetry. DO (specifier of V, by Non-DP First) c-commands into the complement position.

theorem Newman2024.low_xp_XP_not_ccommands_DO : ¬Minimalist.cCommandsIn lowXPTree Newman2024.XP₁✝ Newman2024.DO₁✝

theorem Newman2024.doc_DO_not_ccommands_IO : ¬Minimalist.cCommandsIn docTree Newman2024.DO₂✝ Newman2024.IO₂✝

DOC: neither internal argument c-commands the other — symmetric. DO is inside VP (outer specifier), IO is complement of v. They are in separate branches.

theorem Newman2024.doc_IO_not_ccommands_DO : ¬Minimalist.cCommandsIn docTree Newman2024.IO₂✝ Newman2024.DO₂✝

theorem Newman2024.binding_asymmetry_iff_vp_complement : (Minimalist.cCommandsIn lowXPTree Newman2024.DO₁✝ Newman2024.XP₁✝ ∧ ¬Minimalist.cCommandsIn lowXPTree Newman2024.XP₁✝ Newman2024.DO₁✝) ∧ ¬Minimalist.cCommandsIn docTree Newman2024.DO₂✝ Newman2024.IO₂✝ ∧ ¬Minimalist.cCommandsIn docTree Newman2024.IO₂✝ Newman2024.DO₂✝

The structural asymmetry derived from VP-as-specifier: VP-as-complement gives binding asymmetry between internal arguments; VP-as-specifier gives symmetric binding.

theorem Newman2024.low_xp_agent_ccommands_DO : Minimalist.cCommandsIn lowXPTree Newman2024.agent₁✝ Newman2024.DO₁✝

In the low-XP structure, the agent c-commands both internal arguments (VP is complement, fully inside agent's sister).

theorem Newman2024.low_xp_agent_ccommands_XP : Minimalist.cCommandsIn lowXPTree Newman2024.agent₁✝ Newman2024.XP₁✝

theorem Newman2024.doc_agent_ccommands_IO : Minimalist.cCommandsIn docTree Newman2024.agent₂✝ Newman2024.IO₂✝

In the DOC structure with Tucking In, the agent (inner specifier) c-commands IO (complement of v) but NOT DO (inside VP, the outer specifier). The agent and VP are in separate branches — a direct consequence of VP being a specifier rather than a complement.

theorem Newman2024.doc_agent_not_ccommands_DO : ¬Minimalist.cCommandsIn docTree Newman2024.agent₂✝ Newman2024.DO₂✝