Documentation

Linglib.Theories.Syntax.Minimalism.Ellipsis.DeletionDomain

Ellipsis: [E] Features and Deletion Domains #

@cite{merchant-2001} @cite{merchant-2013} @cite{benz-salzmann-2025}

The [E] feature on a functional head triggers PF-deletion of the head's complement and presupposes e-GIVENness (@cite{merchant-2001}). Different ellipsis types correspond to different [E] positions in a functional spine.

Generic Framework (`DeletionSpine`) #

The deletion-domain mechanism is domain-general: the same theory governs clausal ellipsis (VP-ellipsis, sluicing) and nominal ellipsis (NP-ellipsis, N-stranding). The DeletionSpine class captures the shared structure:

A set of spine positions with a complement-of relation (isBelow)
[E] on position p → everything strictly below p is deleted
Monotonicity: lower [E] → smaller domain → more external positions
X-stranding (@cite{liptak-saab-2014}): head movement out of the deletion domain lets the moved head survive ellipsis

Two instances:

Clausal (SpinePos): V, VP_adj, v, Voice, T, C
Nominal (NomSpinePos): N, NP_adj, n, Num, D

Clausal Ellipsis (@cite{merchant-2013}) #

Voice mismatch tolerance tracks the height of ellipsis:

VPE ([E] on Voice): Voice is external → voice mismatch OK
Sluicing ([E] on C): Voice is internal → voice mismatch blocked
vVPE ([E] on v): both v and Voice are external → voice and transitivity mismatches OK (@cite{kalyakin-2026})

Nominal Ellipsis (@cite{benz-salzmann-2025}) #

Variable [E] placement in the nominal spine:

N-stranding NP-ellipsis ([E] on n): N survives via N-to-n movement; postnominal material (PPs, relatives) deleted; prenominal adjectives survive
nP-ellipsis ([E] on Num): N, n, and adjectives all deleted
NumP-ellipsis ([E] on D): everything below D deleted

Monotonicity (@cite{sailor-2014}'s Generalization) #

Lower [E] position → smaller deletion domain → more features external → more mismatches tolerated. This is a strict monotonicity proved generically for all DeletionSpine instances.

class Minimalism.Ellipsis.DeletionSpine (α : Type) :

A deletion spine: a finite set of positions in a functional spine equipped with a deletion-domain relation and structural ordering.

Both clausal spines (V, v, Voice, T, C) and nominal spines (N, n, Num, D) are instances. The class captures the domain-general logic of @cite{merchant-2001}'s [E]-feature theory:

[E] on head H → complement of H (everything isBelow H) is deleted
Monotonicity: lower [E] → smaller deletion domain
Irreflexivity: H itself is never in its own deletion domain

isBelow : α → α → Bool
isBelow p₁ p₂ = true iff p₁ is in the deletion domain when [E] is at p₂. Encodes the complement-of relation, NOT simple structural ordering — adjunction sites may be structurally between two heads without being in the lower head's complement.
isAtOrBelow : α → α → Bool
isAtOrBelow p₁ p₂ = true iff p₁ is structurally at or below p₂. A simple linear ordering used for monotonicity reasoning.
isBelow_irrefl (p : α) : isBelow p p = false
No position is in its own deletion domain.
isBelow_mono (d p₁ p₂ : α) : isBelow d p₁ = false → isAtOrBelow p₂ p₁ = true → isBelow d p₂ = false
If d is external (not below) at p₁, it is external at any lower p₂. This is @cite{sailor-2014}'s monotonicity generalization.

Instances

def Minimalism.Ellipsis.inDomain {α : Type} [DeletionSpine α] (c ePos : α) :

Generic: is position c in the deletion domain of [E] at ePos?

Equations

Minimalism.Ellipsis.inDomain c ePos = Minimalism.Ellipsis.DeletionSpine.isBelow c ePos

Instances For

def Minimalism.Ellipsis.toleratesMismatch {α : Type} [DeletionSpine α] (ePos dPos : α) :

Generic: a mismatch at head position dPos is tolerated under [E] at ePos iff dPos is external (not in the deletion domain).

Equations

Minimalism.Ellipsis.toleratesMismatch ePos dPos = !Minimalism.Ellipsis.inDomain dPos ePos

Instances For

theorem Minimalism.Ellipsis.eHead_external {α : Type} [DeletionSpine α] (ePos : α) :

inDomain ePos ePos = false

The [E]-bearing head is always external to its own deletion domain.

theorem Minimalism.Ellipsis.toleratesMismatch_mono {α : Type} [DeletionSpine α] (dPos ePos₁ ePos₂ : α) (h₁ : toleratesMismatch ePos₁ dPos = true) (h₂ : DeletionSpine.isAtOrBelow ePos₂ ePos₁ = true) :

toleratesMismatch ePos₂ dPos = true

Generic monotonicity: if a mismatch is tolerated at ePos₁, it is tolerated at any structurally lower ePos₂. @cite{sailor-2014}'s generalization, proved once for all spines.

theorem Minimalism.Ellipsis.xStranding {α : Type} [DeletionSpine α] (ePos base : α) (h_base_in_domain : DeletionSpine.isBelow base ePos = true) :

inDomain ePos ePos = false ∧ inDomain base ePos = true

X-stranding (@cite{liptak-saab-2014}): if X has moved from base to the [E]-bearing head at ePos, X is external (survives ellipsis) while its base position is deleted.

This is the abstract core of the X-stranding diagnostic for head movement: X-stranding XP-ellipsis exists in a language iff both X-movement and XP-ellipsis exist independently.

Instances:

V-stranding VPE: V moves to v, [E] on v → V survives, VP deleted
N-stranding NP-ellipsis: N moves to n, [E] on n → N survives, NP deleted

inductive Minimalism.Ellipsis.SpinePos :

Positions in the clausal spine, ordered from lowest to highest. This is a deliberately coarse-grained linear order sufficient for ellipsis domain computation. It does not replace Cat or ExtendedProjection; it captures the relative height relevant to Merchant's deletion-domain theory.

VP_adj encodes VP-adjunction — the attachment site of restitutive again and result-state modifiers. Structurally below v but NOT in v's complement: adjuncts to XP are part of the XP projection but not selected by the head that takes XP as complement. This matters for vVPE (@cite{kalyakin-2026}): VP-adjuncts survive when [E] is on v (complement of v = bare VP, excluding adjuncts) but are deleted when [E] is on Voice (complement of Voice = full vP, including VP-adjuncts).

V : SpinePos
VP_adj : SpinePos
v : SpinePos
Voice : SpinePos
T : SpinePos
C : SpinePos

Instances For

instance Minimalism.Ellipsis.instDecidableEqSpinePos :

DecidableEq SpinePos

Equations

Minimalism.Ellipsis.instDecidableEqSpinePos x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Minimalism.Ellipsis.instBEqSpinePos :

Equations

Minimalism.Ellipsis.instBEqSpinePos = { beq := Minimalism.Ellipsis.instBEqSpinePos.beq }

def Minimalism.Ellipsis.instBEqSpinePos.beq :

SpinePos → SpinePos → Bool

Equations

Minimalism.Ellipsis.instBEqSpinePos.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

def Minimalism.Ellipsis.instReprSpinePos.repr :

SpinePos → ℕ → Std.Format

Equations

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

Instances For

instance Minimalism.Ellipsis.instReprSpinePos :

Equations

Minimalism.Ellipsis.instReprSpinePos = { reprPrec := Minimalism.Ellipsis.instReprSpinePos.repr }

def Minimalism.Ellipsis.SpinePos.isBelow :

SpinePos → SpinePos → Bool

Strict "in deletion domain of" relation on spine positions.

isBelow p₁ p₂ means "p₁ is inside the deletion domain when [E] is at p₂." This is NOT a simple structural ordering — it encodes the complement-vs-adjunction distinction:

V.isBelow .v = true: V is in v's complement (VP)
VP_adj.isBelow .v = false: VP-adjuncts are NOT in v's complement
VP_adj.isBelow .Voice = true: VP-adjuncts ARE inside Voice's complement (vP contains the full VP projection including adjuncts)

This distinction is what makes vVPE (@cite{kalyakin-2026}) predict both again readings survive: restitutive again (VP-adjoined) is outside the complement of v but inside vP.

Equations

Instances For

def Minimalism.Ellipsis.SpinePos.isAtOrBelow :

SpinePos → SpinePos → Bool

Structural height comparison (non-strict). Used for monotonicity: p₁.isAtOrBelow p₂ means p₁ is structurally at or below p₂. Unlike isBelow, this IS a simple linear ordering with VP_adj between V and v. Fully pattern-matched to avoid BEq reduction issues in proofs.

Equations

Instances For

instance Minimalism.Ellipsis.instDeletionSpineSpinePos :

DeletionSpine SpinePos

Equations

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

structure Minimalism.Ellipsis.EllipsisType :

An ellipsis type is defined by the spine position of the [E]-bearing head. The deletion domain is the complement of that head — everything strictly below it in the spine.

ePosition : SpinePos
The head carrying [E]
name : String
Label for display

Instances For

def Minimalism.Ellipsis.instReprEllipsisType.repr :

EllipsisType → ℕ → Std.Format

Equations

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

Instances For

instance Minimalism.Ellipsis.instReprEllipsisType :

Repr EllipsisType

Equations

Minimalism.Ellipsis.instReprEllipsisType = { reprPrec := Minimalism.Ellipsis.instReprEllipsisType.repr }

def Minimalism.Ellipsis.isInDeletionDomain (c : SpinePos) (e : EllipsisType) :

Is a spine position inside the deletion domain of an ellipsis type? A position is in the deletion domain iff it is strictly below the [E]-bearing head.

Equations

Minimalism.Ellipsis.isInDeletionDomain c e = c.isBelow e.ePosition

Instances For

def Minimalism.Ellipsis.sluicing :

Sluicing: [E] on C, deletes TP. Contains Voice → voice mismatch blocked.

Equations

Minimalism.Ellipsis.sluicing = { ePosition := Minimalism.Ellipsis.SpinePos.C, name := "sluicing" }

Instances For

def Minimalism.Ellipsis.tpEllipsis :

TP ellipsis: [E] on T, deletes VoiceP.

Equations

Minimalism.Ellipsis.tpEllipsis = { ePosition := Minimalism.Ellipsis.SpinePos.T, name := "TP ellipsis" }

Instances For

def Minimalism.Ellipsis.englishVPE :

English VPE: [E] on Voice, deletes vP. Voice is external → voice mismatch tolerated. v is internal → transitivity mismatch blocked.

Equations

Minimalism.Ellipsis.englishVPE = { ePosition := Minimalism.Ellipsis.SpinePos.Voice, name := "English VPE" }

Instances For

def Minimalism.Ellipsis.vVPE :

v-stranding VPE: [E] on v, deletes VP. Both Voice and v are external → voice and transitivity mismatches OK. Attested in Muira Dargwa complex predicates (@cite{kalyakin-2026}).

Equations

Minimalism.Ellipsis.vVPE = { ePosition := Minimalism.Ellipsis.SpinePos.v, name := "v-stranding VPE" }

Instances For

structure Minimalism.Ellipsis.MismatchDimension :

A mismatch dimension: a syntactic feature whose head position determines whether mismatches in that feature are tolerated.

name : String
Label for the dimension
headPosition : SpinePos
The spine position of the head bearing this feature

Instances For

instance Minimalism.Ellipsis.instReprMismatchDimension :

Repr MismatchDimension

Equations

Minimalism.Ellipsis.instReprMismatchDimension = { reprPrec := Minimalism.Ellipsis.instReprMismatchDimension.repr }

def Minimalism.Ellipsis.instReprMismatchDimension.repr :

MismatchDimension → ℕ → Std.Format

Equations

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

Instances For

def Minimalism.Ellipsis.voiceMismatch :

MismatchDimension

Voice mismatch: active vs. passive, determined by Voice head.

Equations

Minimalism.Ellipsis.voiceMismatch = { name := "voice", headPosition := Minimalism.Ellipsis.SpinePos.Voice }

Instances For

def Minimalism.Ellipsis.transitivityMismatch :

MismatchDimension

Transitivity mismatch: transitive v vs. unaccusative v.

Equations

Minimalism.Ellipsis.transitivityMismatch = { name := "transitivity", headPosition := Minimalism.Ellipsis.SpinePos.v }

Instances For

def Minimalism.Ellipsis.lexicalMismatch :

MismatchDimension

Lexical verb mismatch: different V heads.

Equations

Minimalism.Ellipsis.lexicalMismatch = { name := "lexical verb", headPosition := Minimalism.Ellipsis.SpinePos.V }

Instances For

def Minimalism.Ellipsis.dativeAlternation :

MismatchDimension

Dative alternation: double-object vs prepositional dative. Regulated by distinct v heads below Voice (@cite{merchant-2013} §3.3).

Equations

Minimalism.Ellipsis.dativeAlternation = { name := "dative alternation", headPosition := Minimalism.Ellipsis.SpinePos.v }

Instances For

def Minimalism.Ellipsis.prepAlternation :

MismatchDimension

Applicative/prepositional alternation: embroider X with Y vs embroider Y on X. Regulated by applicative v heads below Voice (@cite{merchant-2013} §3.3).

Equations

Minimalism.Ellipsis.prepAlternation = { name := "prepositional alternation", headPosition := Minimalism.Ellipsis.SpinePos.v }

Instances For

def Minimalism.Ellipsis.middleAlternation :

MismatchDimension

Transitive/middle alternation: they market ethanol vs ethanol markets well. Regulated by v heads determining external argument realization (@cite{merchant-2013} §3.3).

Equations

Minimalism.Ellipsis.middleAlternation = { name := "middle alternation", headPosition := Minimalism.Ellipsis.SpinePos.v }

Instances For

def Minimalism.Ellipsis.canMismatch (e : EllipsisType) (d : MismatchDimension) :

A mismatch in dimension d is tolerated by ellipsis type e iff the head bearing the feature is NOT in the deletion domain — i.e., it is at or above the [E]-bearing head.

Equations

Minimalism.Ellipsis.canMismatch e d = !Minimalism.Ellipsis.isInDeletionDomain d.headPosition e

Instances For

theorem Minimalism.Ellipsis.englishVPE_voice_ok :

canMismatch englishVPE voiceMismatch = true

English VPE tolerates voice mismatches: Voice is external to vP.

theorem Minimalism.Ellipsis.englishVPE_transitivity_blocked :

canMismatch englishVPE transitivityMismatch = false

English VPE blocks transitivity mismatches: v is inside vP.

theorem Minimalism.Ellipsis.englishVPE_lexical_blocked :

canMismatch englishVPE lexicalMismatch = false

English VPE blocks lexical verb mismatches: V is inside vP.

theorem Minimalism.Ellipsis.sluicing_voice_blocked :

canMismatch sluicing voiceMismatch = false

Sluicing blocks voice mismatches: Voice is inside TP.

theorem Minimalism.Ellipsis.sluicing_transitivity_blocked :

canMismatch sluicing transitivityMismatch = false

Sluicing blocks transitivity mismatches: v is inside TP.

theorem Minimalism.Ellipsis.vVPE_voice_ok :

canMismatch vVPE voiceMismatch = true

vVPE tolerates voice mismatches: Voice is external to VP.

theorem Minimalism.Ellipsis.vVPE_transitivity_ok :

canMismatch vVPE transitivityMismatch = true

vVPE tolerates transitivity mismatches: v is external to VP.

theorem Minimalism.Ellipsis.vVPE_lexical_blocked :

canMismatch vVPE lexicalMismatch = false

vVPE blocks lexical verb mismatches: V is inside VP.

theorem Minimalism.Ellipsis.mismatch_monotone (d : MismatchDimension) (e₁ e₂ : EllipsisType) (h₁ : canMismatch e₁ d = true) (h₂ : e₂.ePosition.isAtOrBelow e₁.ePosition = true) :

canMismatch e₂ d = true

Monotonicity of mismatch tolerance: if ellipsis type e₁ tolerates a mismatch dimension d, then any ellipsis type e₂ whose [E] position is at or below e₁'s also tolerates d.

def Minimalism.Ellipsis.rootInVVPEDomain :

RootPosition → Bool

Is a root inside the vVPE deletion domain (= VP)? Uses RootPosition from Core.Lexical.RootFeatures (Marantz 2013, @cite{beavers-koontz-garboden-2020}):

.complement roots (change-of-state) are inside VP → deleted
.adjoined roots (manner/activity) are outside VP → survive

Equations

Instances For

theorem Minimalism.Ellipsis.complementRoot_in_vVPE :

rootInVVPEDomain RootPosition.complement = true

Complement roots (change-of-state) are deleted under vVPE.

theorem Minimalism.Ellipsis.adjoinedRoot_outside_vVPE :

rootInVVPEDomain RootPosition.adjoined = false

Adjoined roots (manner/activity) survive vVPE — they are outside the deletion domain. This is why antipassive roots block vVPE in Muira Dargwa: antipassive coerces adjunction (@cite{kalyakin-2026}).

inductive Minimalism.Ellipsis.AgainPosition :

Adjunction position of again, following @cite{merchant-2013} (building on Johnson 2004, von Stechow 1996).

vP_adjunction : AgainPosition
VP_adjunction : AgainPosition

Instances For

instance Minimalism.Ellipsis.instDecidableEqAgainPosition :

DecidableEq AgainPosition

Equations

Minimalism.Ellipsis.instDecidableEqAgainPosition x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Minimalism.Ellipsis.instBEqAgainPosition.beq :

AgainPosition → AgainPosition → Bool

Equations

Minimalism.Ellipsis.instBEqAgainPosition.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

instance Minimalism.Ellipsis.instBEqAgainPosition :

BEq AgainPosition

Equations

Minimalism.Ellipsis.instBEqAgainPosition = { beq := Minimalism.Ellipsis.instBEqAgainPosition.beq }

instance Minimalism.Ellipsis.instReprAgainPosition :

Repr AgainPosition

Equations

Minimalism.Ellipsis.instReprAgainPosition = { reprPrec := Minimalism.Ellipsis.instReprAgainPosition.repr }

def Minimalism.Ellipsis.instReprAgainPosition.repr :

AgainPosition → ℕ → Std.Format

Equations

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

Instances For

def Minimalism.Ellipsis.againSurvives (pos : AgainPosition) (e : EllipsisType) :

Is an again reading available under a given ellipsis type?

Repetitive again adjoins high (vP or VoiceP): modeled at Voice level — outside the deletion domain of both VPE and vVPE.

Restitutive again adjoins to VP — modeled at VP_adj. This is inside vP (deleted under English VPE, [E] on Voice) but NOT inside v's complement (survives vVPE, [E] on v). The distinction between VP_adj and V is crucial: V (the head) is in v's complement, but VP-adjunction is at the complement boundary, outside it.

Equations

Instances For

theorem Minimalism.Ellipsis.englishVPE_again :

againSurvives AgainPosition.vP_adjunction englishVPE = true ∧ againSurvives AgainPosition.VP_adjunction englishVPE = false

Under English VPE, restitutive again is inside the deletion domain (deleted), while repetitive again survives. @cite{merchant-2013}: only repetitive reading available (Johnson 2004 exx. 49a–b).

theorem Minimalism.Ellipsis.vVPE_again :

againSurvives AgainPosition.vP_adjunction vVPE = true ∧ againSurvives AgainPosition.VP_adjunction vVPE = true

Under vVPE, BOTH readings survive: restitutive again (VP-adjoined) is outside v's complement, so it is not deleted. @cite{kalyakin-2026} §4.1 (exx. 52a–b): both repetitive and restitutive ʔibrra 'again' are available under vVPE in Muira Dargwa. This is the key diagnostic proving the deletion domain is VP (smaller than English VPE's vP).

theorem Minimalism.Ellipsis.voice_agreement :

canMismatch englishVPE voiceMismatch = true ∧ canMismatch vVPE voiceMismatch = true

English VPE and vVPE agree on voice: both tolerate voice mismatches.

theorem Minimalism.Ellipsis.transitivity_divergence :

canMismatch englishVPE transitivityMismatch = false ∧ canMismatch vVPE transitivityMismatch = true

English VPE and vVPE diverge on transitivity: English blocks it, vVPE allows it. This is the key prediction that distinguishes the two ellipsis types.

theorem Minimalism.Ellipsis.lexical_blocked_both :

canMismatch englishVPE lexicalMismatch = false ∧ canMismatch vVPE lexicalMismatch = false

Both block lexical verb mismatches: V is inside the deletion domain of both English VPE and vVPE.

structure Minimalism.Ellipsis.VPEProfile :

Extended ellipsis type with cross-linguistic variation parameters. Languages with verb-stranding ellipsis vary in:

deletion domain size (again test: VP vs vP)
whether the Verbal Identity Requirement holds (LV must match)
whether argument-structure alternations are tolerated

ellipsisType : EllipsisType
The core ellipsis type (spine position of [E])
virRequired : Bool
Verbal Identity Requirement (@cite{goldberg-2005}): antecedent and target light verbs must be identical in root and derivational morphology. Active in Persian and Bangla; inactive in Muira Dargwa.
language : String
Language label

Instances For

def Minimalism.Ellipsis.instReprVPEProfile.repr :

VPEProfile → ℕ → Std.Format

Equations

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

Instances For

instance Minimalism.Ellipsis.instReprVPEProfile :

Repr VPEProfile

Equations

Minimalism.Ellipsis.instReprVPEProfile = { reprPrec := Minimalism.Ellipsis.instReprVPEProfile.repr }

def Minimalism.Ellipsis.muiraDargwaVVPE :

Muira Dargwa vVPE: [E] on v, deletion domain = VP. Both again readings survive; arg-structure alternations tolerated; LV mismatches tolerated (@cite{kalyakin-2026} ex. 78).

Equations

Minimalism.Ellipsis.muiraDargwaVVPE = { ellipsisType := Minimalism.Ellipsis.vVPE, virRequired := false, language := "Muira Dargwa" }

Instances For

def Minimalism.Ellipsis.persianVVPE :

Persian vVPE: [E] on v, deletion domain = VP. Both again readings survive (@cite{toosarvandani-2009} ex. 90). But arg-structure alternations blocked (ex. 91) and LV identity required — VIR is active.

Equations

Minimalism.Ellipsis.persianVVPE = { ellipsisType := Minimalism.Ellipsis.vVPE, virRequired := true, language := "Persian" }

Instances For

def Minimalism.Ellipsis.banglaVVPE :

Bangla verb-stranding: deletion domain = vP (NOT VP). Only repetitive again survives (Haldar 2021 ex. 94a–b); adjuncts CAN be interpreted in the ellipsis site (ex. 95). This means the [E] position is Voice (same as English VPE), with the LV evacuating via head movement.

Equations

Minimalism.Ellipsis.banglaVVPE = { ellipsisType := Minimalism.Ellipsis.englishVPE, virRequired := true, language := "Bangla" }

Instances For

def Minimalism.Ellipsis.britishDoVVPE :

British do ellipsis: [E] on v, deletion domain = VP. Tolerates voice mismatches (Silk 2025 ex. 97) and arg-structure alternations (ex. 98), matching Muira Dargwa vVPE.

Equations

Minimalism.Ellipsis.britishDoVVPE = { ellipsisType := Minimalism.Ellipsis.vVPE, virRequired := false, language := "British English" }

Instances For

theorem Minimalism.Ellipsis.dargwa_persian_same_domain :

muiraDargwaVVPE.ellipsisType.ePosition = persianVVPE.ellipsisType.ePosition ∧ muiraDargwaVVPE.virRequired ≠ persianVVPE.virRequired

Muira Dargwa and Persian share the same [E] position but differ on VIR.

theorem Minimalism.Ellipsis.bangla_larger_domain :

banglaVVPE.ellipsisType.ePosition = SpinePos.Voice ∧ muiraDargwaVVPE.ellipsisType.ePosition = SpinePos.v ∧ SpinePos.v.isBelow SpinePos.Voice = true

Bangla has a LARGER deletion domain than Muira Dargwa: [E] on Voice (= English VPE) vs [E] on v. The again test diagnoses this: Bangla deletes restitutive again (Haldar 2021), Muira Dargwa does not.

theorem Minimalism.Ellipsis.again_differentiates_bangla_dargwa :

againSurvives AgainPosition.VP_adjunction banglaVVPE.ellipsisType = false ∧ againSurvives AgainPosition.VP_adjunction muiraDargwaVVPE.ellipsisType = true

The again test correctly differentiates Bangla (vP domain) from Muira Dargwa (VP domain): restitutive again is deleted under Bangla's ellipsis but survives Muira Dargwa's.

inductive Minimalism.Ellipsis.NomSpinePos :

Positions in the nominal spine, ordered from lowest to highest. Parallels the clausal SpinePos for the nominal extended projection N(F0) → n(F1) → Num(F3) → D(F4).

NP_adj parallels clausal VP_adj: the site of prenominal modifiers (adjectives in Spec of functional heads within nP) that are inside nP but NOT in n's complement (NP). This distinction matters for N-stranding NP-ellipsis (@cite{benz-salzmann-2025}): prenominal adjectives survive n[E] (outside NP) but are deleted under Num[E] (inside nP).

Instances For

instance Minimalism.Ellipsis.instDecidableEqNomSpinePos :

DecidableEq NomSpinePos

Equations

Minimalism.Ellipsis.instDecidableEqNomSpinePos x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Minimalism.Ellipsis.instBEqNomSpinePos.beq :

NomSpinePos → NomSpinePos → Bool

Equations

Minimalism.Ellipsis.instBEqNomSpinePos.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

instance Minimalism.Ellipsis.instBEqNomSpinePos :

BEq NomSpinePos

Equations

Minimalism.Ellipsis.instBEqNomSpinePos = { beq := Minimalism.Ellipsis.instBEqNomSpinePos.beq }

instance Minimalism.Ellipsis.instReprNomSpinePos :

Repr NomSpinePos

Equations

Minimalism.Ellipsis.instReprNomSpinePos = { reprPrec := Minimalism.Ellipsis.instReprNomSpinePos.repr }

def Minimalism.Ellipsis.instReprNomSpinePos.repr :

NomSpinePos → ℕ → Std.Format

Equations

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

Instances For

def Minimalism.Ellipsis.NomSpinePos.isBelow :

NomSpinePos → NomSpinePos → Bool

Strict "in deletion domain of" relation on nominal spine positions.

Parallels SpinePos.isBelow with the same complement-vs-adjunction distinction:

N.isBelow .n = true: N is in n's complement (NP)
NP_adj.isBelow .n = false: prenominal modifiers NOT in n's complement
NP_adj.isBelow .Num = true: prenominal modifiers ARE in Num's complement (nP)

Equations

Instances For

def Minimalism.Ellipsis.NomSpinePos.isAtOrBelow :

NomSpinePos → NomSpinePos → Bool

Structural height comparison (non-strict) for nominal spine. Simple linear order: N ≤ NP_adj ≤ n ≤ Num ≤ D.

Equations

Instances For

instance Minimalism.Ellipsis.instDeletionSpineNomSpinePos :

DeletionSpine NomSpinePos

Equations

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

structure Minimalism.Ellipsis.NomEllipsisType :

A nominal ellipsis type: [E] on a head in the nominal spine. The deletion domain is the complement of the [E]-bearing head.

ePosition : NomSpinePos
name : String

Instances For

def Minimalism.Ellipsis.instReprNomEllipsisType.repr :

NomEllipsisType → ℕ → Std.Format

Equations

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

Instances For

instance Minimalism.Ellipsis.instReprNomEllipsisType :

Repr NomEllipsisType

Equations

Minimalism.Ellipsis.instReprNomEllipsisType = { reprPrec := Minimalism.Ellipsis.instReprNomEllipsisType.repr }

def Minimalism.Ellipsis.nomInDeletionDomain (c : NomSpinePos) (e : NomEllipsisType) :

Is a nominal position in the deletion domain?

Equations

Minimalism.Ellipsis.nomInDeletionDomain c e = c.isBelow e.ePosition

Instances For

def Minimalism.Ellipsis.nomSurvives (c : NomSpinePos) (e : NomEllipsisType) :

Does a nominal position survive ellipsis?

Equations

Minimalism.Ellipsis.nomSurvives c e = !Minimalism.Ellipsis.nomInDeletionDomain c e

Instances For

def Minimalism.Ellipsis.numPEllipsis :

NomEllipsisType

NumP-ellipsis: [E] on D, deletes everything below D. Determiner/demonstrative survives; N, adjectives, numerals deleted.

Equations

Minimalism.Ellipsis.numPEllipsis = { ePosition := Minimalism.Ellipsis.NomSpinePos.D, name := "NumP-ellipsis" }

Instances For

def Minimalism.Ellipsis.nPEllipsis :

NomEllipsisType

nP-ellipsis: [E] on Num, deletes nP (complement of Num). Numeral and determiner survive; N, n, and prenominal adjectives deleted. @cite{saab-2026}: Num[E] in Spanish pseudo-partitive/quantificational binominals.

Equations

Minimalism.Ellipsis.nPEllipsis = { ePosition := Minimalism.Ellipsis.NomSpinePos.Num, name := "nP-ellipsis" }

Instances For

def Minimalism.Ellipsis.nStrandingNPE :

NomEllipsisType

N-stranding NP-ellipsis: [E] on n, deletes only NP (complement of n). N survives via N-to-n head movement; prenominal adjectives survive (in nP, not NP). Postnominal dependents of N (PPs, relative clauses, genitive arguments) are in NP and are deleted. @cite{benz-salzmann-2025}: German N-stranding NP-ellipsis.

Equations

Minimalism.Ellipsis.nStrandingNPE = { ePosition := Minimalism.Ellipsis.NomSpinePos.n, name := "N-stranding NP-ellipsis" }

Instances For

theorem Minimalism.Ellipsis.nStranding_deletes_NP :

nomInDeletionDomain NomSpinePos.N nStrandingNPE = true

Under N-stranding, NP-internal material (postnominal PPs, relatives, genitive arguments) is in the deletion domain.

theorem Minimalism.Ellipsis.nStranding_adj_survives :

nomSurvives NomSpinePos.NP_adj nStrandingNPE = true

Under N-stranding, prenominal adjectives survive: they are inside nP but NOT in n's complement (NP). @cite{benz-salzmann-2025} ex. (25): *Ich habe das schönste Auto und du das schönste Motorrad — adjective cannot be deleted.

theorem Minimalism.Ellipsis.nStranding_n_external :

nomSurvives NomSpinePos.n nStrandingNPE = true

Under N-stranding, the n head is external (it bears [E]). N moves here via N-to-n head movement and survives.

theorem Minimalism.Ellipsis.nStranding_num_survives :

nomSurvives NomSpinePos.Num nStrandingNPE = true

Under N-stranding, Num is external (numerals survive). @cite{benz-salzmann-2025} ex. (25b): numeral zwei cannot be deleted under N-stranding.

theorem Minimalism.Ellipsis.nPE_deletes_N :

nomInDeletionDomain NomSpinePos.N nPEllipsis = true

Under nP-ellipsis, N is in the deletion domain (N does not survive).

theorem Minimalism.Ellipsis.nPE_deletes_adj :

nomInDeletionDomain NomSpinePos.NP_adj nPEllipsis = true

Under nP-ellipsis, prenominal adjectives are deleted (inside nP).

theorem Minimalism.Ellipsis.nPE_deletes_n :

nomInDeletionDomain NomSpinePos.n nPEllipsis = true

Under nP-ellipsis, n is deleted.

theorem Minimalism.Ellipsis.nPE_num_survives :

nomSurvives NomSpinePos.Num nPEllipsis = true

Under nP-ellipsis, Num is external (numerals survive). @cite{saab-2026}: the numeral/determiner remnant in Spanish pseudo-partitive ellipsis.

Under NumP-ellipsis, everything below D is deleted.

Nominal monotonicity: N-stranding (n[E]) → nP-ellipsis (Num[E]) → NumP-ellipsis (D[E]) form a chain where lower [E] → smaller domain. Anything deleted under n[E] is also deleted under Num[E] and D[E].

theorem Minimalism.Ellipsis.n_stranding_is_xStranding :

inDomain NomSpinePos.n NomSpinePos.n = false ∧ inDomain NomSpinePos.N NomSpinePos.n = true

N-to-n movement instantiates generic X-stranding: N (base) is below n (landing), so when [E] is on n, N's base position is in the deletion domain but the n head (where N has moved) is external. @cite{benz-salzmann-2025}: German N-stranding NP-ellipsis.

theorem Minimalism.Ellipsis.v_stranding_is_xStranding :

inDomain SpinePos.v SpinePos.v = false ∧ inDomain SpinePos.V SpinePos.v = true

V-to-v movement is the clausal analogue: V (base) is below v (landing), so when [E] is on v, V's base position is deleted but v survives. This is exactly v-stranding VPE (@cite{kalyakin-2026}).

theorem Minimalism.Ellipsis.clausal_nominal_xStranding_parallel :

SpinePos.V.isBelow SpinePos.v = true ∧ NomSpinePos.N.isBelow NomSpinePos.n = true

The clausal and nominal X-stranding patterns are structurally identical: both are instances of the generic xStranding theorem at the F1 (categorizer) level of their respective extended projections. V:v :: N:n — the same abstract relationship.