Documentation

Linglib.Syntax.Minimalist.Ellipsis

Ellipsis: [E] Features and Deletion Domains #

[Mer01] [Mer13] [BS25]

The [E] feature on a functional head triggers PF-deletion of the head's complement and presupposes e-GIVENness ([Mer01]). 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 ([LS14]): 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 ([Mer13]) #

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 ([Kal26])

Nominal Ellipsis ([BS25]) #

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 ([Sai14]'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 Minimalist.Ellipsis.DeletionSpine (α : Type u_1) :

Type u_1

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 [Mer01]'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. A Bool decision procedure; the Prop predicate layer (inDomain/canMismatch) is built on top.
isAtOrBelow : α → α → Bool
isAtOrBelow p₁ p₂ = true iff p₁ is structurally at or below p₂. A simple linear ordering used for monotonicity reasoning. (A mathlib LinearOrder upgrade of this is a planned follow-up.)
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 [Sai14]'s monotonicity generalization.

Instances

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

Generic: is position c in the deletion domain of [E] at ePos? A Prop predicate; the underlying isBelow stays a Bool decision procedure (the Nat.ble-style computational core).

Equations

Minimalist.Ellipsis.inDomain c ePos = (Minimalist.Ellipsis.DeletionSpine.isBelow c ePos = true)

Instances For

@[implicit_reducible]

instance Minimalist.Ellipsis.instDecidableInDomain {α : Type u_1} [DeletionSpine α] (c ePos : α) :

Decidable (inDomain c ePos)

Equations

Minimalist.Ellipsis.instDecidableInDomain c ePos = id inferInstance

theorem Minimalist.Ellipsis.xStranding {α : Type u_1} [DeletionSpine α] (ePos base : α) (h_base_in_domain : inDomain base ePos) :

¬inDomain ePos ePos ∧ inDomain base ePos

X-stranding ([LS14]): 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 Minimalist.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 ([Kal26]): 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

@[implicit_reducible]

instance Minimalist.Ellipsis.instDecidableEqSpinePos :

DecidableEq SpinePos

Equations

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

@[implicit_reducible]

instance Minimalist.Ellipsis.instReprSpinePos :

Equations

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

def Minimalist.Ellipsis.instReprSpinePos.repr :

SpinePos → ℕ → Std.Format

Equations

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

Instances For

def Minimalist.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 ([Kal26]) predict both again readings survive: restitutive again (VP-adjoined) is outside the complement of v but inside vP.

Equations

Instances For

def Minimalist.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

@[implicit_reducible]

instance Minimalist.Ellipsis.instDeletionSpineSpinePos :

DeletionSpine SpinePos

Equations

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

structure Minimalist.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 Minimalist.Ellipsis.instReprEllipsisType.repr :

EllipsisType → ℕ → Std.Format

Equations

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

Instances For

@[implicit_reducible]

instance Minimalist.Ellipsis.instReprEllipsisType :

Repr EllipsisType

Equations

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

@[implicit_reducible]

instance Minimalist.Ellipsis.instHasDepthEllipsisType :

Anaphor.HasDepth EllipsisType

Every ellipsis type is a Hankamer–Sag surface anaphor ([HS76]): PF-deletion under identity leaves full internal structure in place. So EllipsisType is an Anaphor.HasDepth carrier (depth .surface throughout) — the depth-axis analogue of a Bound pronoun.

Equations

Minimalist.Ellipsis.instHasDepthEllipsisType = { depth := fun (x : Minimalist.Ellipsis.EllipsisType) => Anaphor.Depth.surface }

theorem Minimalist.Ellipsis.isSurface (e : EllipsisType) :

Anaphor.HasDepth.IsSurface e

Witness: every ellipsis type is surface.

def Minimalist.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

Minimalist.Ellipsis.isInDeletionDomain c e = Minimalist.Ellipsis.inDomain c e.ePosition

Instances For

@[implicit_reducible]

instance Minimalist.Ellipsis.instDecidableIsInDeletionDomain (c : SpinePos) (e : EllipsisType) :

Decidable (isInDeletionDomain c e)

Equations

Minimalist.Ellipsis.instDecidableIsInDeletionDomain c e = id inferInstance

def Minimalist.Ellipsis.sluicing :

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

Equations

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

Instances For

def Minimalist.Ellipsis.tpEllipsis :

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

Equations

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

Instances For

def Minimalist.Ellipsis.englishVPE :

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

Equations

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

Instances For

def Minimalist.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 ([Kal26]).

Equations

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

Instances For

structure Minimalist.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

def Minimalist.Ellipsis.instReprMismatchDimension.repr :

MismatchDimension → ℕ → Std.Format

Equations

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

Instances For

@[implicit_reducible]

instance Minimalist.Ellipsis.instReprMismatchDimension :

Repr MismatchDimension

Equations

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

def Minimalist.Ellipsis.voiceMismatch :

MismatchDimension

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

Equations

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

Instances For

def Minimalist.Ellipsis.transitivityMismatch :

MismatchDimension

Transitivity mismatch: transitive v vs. unaccusative v.

Equations

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

Instances For

def Minimalist.Ellipsis.lexicalMismatch :

MismatchDimension

Lexical verb mismatch: different V heads.

Equations

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

Instances For

def Minimalist.Ellipsis.dativeAlternation :

MismatchDimension

Dative alternation: double-object vs prepositional dative. Regulated by distinct v heads below Voice ([Mer13] §3.3).

Equations

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

Instances For

def Minimalist.Ellipsis.prepAlternation :

MismatchDimension

Applicative/prepositional alternation: embroider X with Y vs embroider Y on X. Regulated by applicative v heads below Voice ([Mer13] §3.3).

Equations

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

Instances For

def Minimalist.Ellipsis.middleAlternation :

MismatchDimension

Transitive/middle alternation: they market ethanol vs ethanol markets well. Regulated by v heads determining external argument realization ([Mer13] §3.3).

Equations

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

Instances For

def Minimalist.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

Minimalist.Ellipsis.canMismatch e d = ¬Minimalist.Ellipsis.isInDeletionDomain d.headPosition e

Instances For

@[implicit_reducible]

instance Minimalist.Ellipsis.instDecidableCanMismatch (e : EllipsisType) (d : MismatchDimension) :

Decidable (canMismatch e d)

Equations

Minimalist.Ellipsis.instDecidableCanMismatch e d = id inferInstance

theorem Minimalist.Ellipsis.englishVPE_voice_ok :

canMismatch englishVPE voiceMismatch

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

theorem Minimalist.Ellipsis.englishVPE_transitivity_blocked :

¬canMismatch englishVPE transitivityMismatch

English VPE blocks transitivity mismatches: v is inside vP.

theorem Minimalist.Ellipsis.englishVPE_lexical_blocked :

¬canMismatch englishVPE lexicalMismatch

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

theorem Minimalist.Ellipsis.sluicing_voice_blocked :

¬canMismatch sluicing voiceMismatch

Sluicing blocks voice mismatches: Voice is inside TP.

theorem Minimalist.Ellipsis.sluicing_transitivity_blocked :

¬canMismatch sluicing transitivityMismatch

Sluicing blocks transitivity mismatches: v is inside TP.

theorem Minimalist.Ellipsis.vVPE_voice_ok :

canMismatch vVPE voiceMismatch

vVPE tolerates voice mismatches: Voice is external to VP.

theorem Minimalist.Ellipsis.vVPE_transitivity_ok :

canMismatch vVPE transitivityMismatch

vVPE tolerates transitivity mismatches: v is external to VP.

theorem Minimalist.Ellipsis.vVPE_lexical_blocked :

¬canMismatch vVPE lexicalMismatch

vVPE blocks lexical verb mismatches: V is inside VP.

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

canMismatch e₂ d

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. [Sai14]'s monotonicity: lower [E] → smaller domain → more mismatches tolerated. Routed through the generic class law DeletionSpine.isBelow_mono.

def Minimalist.Ellipsis.rootSpinePos :

Verb.Root.Position → SpinePos

Spine position of a root by its attachment (Root.Position, Semantics/Lexical/Roots/Template.lean; Marantz, [BKG20]): change-of-state .complement roots sit at V (in v's complement), manner/activity .adjoined roots at VP_adj (outside it).

Equations

Instances For

def Minimalist.Ellipsis.rootInVVPEDomain (p : Verb.Root.Position) :

Is a root inside the vVPE deletion domain (= complement of v)? Derived from the spine, not stipulated: a root is deleted under vVPE iff its attachment position is below v.

Equations

Minimalist.Ellipsis.rootInVVPEDomain p = Minimalist.Ellipsis.isInDeletionDomain (Minimalist.Ellipsis.rootSpinePos p) Minimalist.Ellipsis.vVPE

Instances For

@[implicit_reducible]

instance Minimalist.Ellipsis.instDecidableRootInVVPEDomain (p : Verb.Root.Position) :

Decidable (rootInVVPEDomain p)

Equations

Minimalist.Ellipsis.instDecidableRootInVVPEDomain p = id inferInstance

theorem Minimalist.Ellipsis.complementRoot_in_vVPE :

rootInVVPEDomain Verb.Root.Position.complement

Complement roots (change-of-state) are deleted under vVPE: V is in v's complement (follows from the spine, not stipulated).

theorem Minimalist.Ellipsis.adjoinedRoot_outside_vVPE :

¬rootInVVPEDomain Verb.Root.Position.adjoined

Adjoined roots (manner/activity) survive vVPE — VP_adj is outside v's complement. This is why antipassive roots block vVPE in Muira Dargwa: antipassive coerces adjunction ([Kal26]).

inductive Minimalist.Ellipsis.AgainPosition :

Adjunction position of again, following [Mer13] (building on Johnson 2004, von Stechow 1996).

vP_adjunction : AgainPosition
VP_adjunction : AgainPosition

Instances For

@[implicit_reducible]

instance Minimalist.Ellipsis.instDecidableEqAgainPosition :

DecidableEq AgainPosition

Equations

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

@[implicit_reducible]

instance Minimalist.Ellipsis.instReprAgainPosition :

Repr AgainPosition

Equations

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

def Minimalist.Ellipsis.instReprAgainPosition.repr :

AgainPosition → ℕ → Std.Format

Equations

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

Instances For

def Minimalist.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

@[implicit_reducible]

instance Minimalist.Ellipsis.instDecidableAgainSurvives (pos : AgainPosition) (e : EllipsisType) :

Decidable (againSurvives pos e)

Equations

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

theorem Minimalist.Ellipsis.englishVPE_again :

againSurvives AgainPosition.vP_adjunction englishVPE ∧ ¬againSurvives AgainPosition.VP_adjunction englishVPE

Under English VPE, restitutive again is inside the deletion domain (deleted), while repetitive again survives. [Mer13]: only repetitive reading available (Johnson 2004 exx. 49a–b).

theorem Minimalist.Ellipsis.vVPE_again :

againSurvives AgainPosition.vP_adjunction vVPE ∧ againSurvives AgainPosition.VP_adjunction vVPE

Under vVPE, BOTH readings survive: restitutive again (VP-adjoined) is outside v's complement, so it is not deleted. [Kal26] §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 Minimalist.Ellipsis.voice_agreement :

canMismatch englishVPE voiceMismatch ∧ canMismatch vVPE voiceMismatch

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

theorem Minimalist.Ellipsis.transitivity_divergence :

¬canMismatch englishVPE transitivityMismatch ∧ canMismatch vVPE transitivityMismatch

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 Minimalist.Ellipsis.lexical_blocked_both :

¬canMismatch englishVPE lexicalMismatch ∧ ¬canMismatch vVPE lexicalMismatch

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

structure Minimalist.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 ([Gol05]): 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 Minimalist.Ellipsis.instReprVPEProfile.repr :

VPEProfile → ℕ → Std.Format

Equations

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

Instances For

@[implicit_reducible]

instance Minimalist.Ellipsis.instReprVPEProfile :

Repr VPEProfile

Equations

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

def Minimalist.Ellipsis.muiraDargwaVVPE :

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

Equations

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

Instances For

def Minimalist.Ellipsis.persianVVPE :

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

Equations

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

Instances For

def Minimalist.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

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

Instances For

def Minimalist.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

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

Instances For

theorem Minimalist.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 Minimalist.Ellipsis.bangla_larger_domain :

banglaVVPE.ellipsisType.ePosition = SpinePos.Voice ∧ muiraDargwaVVPE.ellipsisType.ePosition = SpinePos.v ∧ inDomain SpinePos.v SpinePos.Voice

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 Minimalist.Ellipsis.again_differentiates_bangla_dargwa :

¬againSurvives AgainPosition.VP_adjunction banglaVVPE.ellipsisType ∧ againSurvives AgainPosition.VP_adjunction muiraDargwaVVPE.ellipsisType

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 Minimalist.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 ([BS25]): prenominal adjectives survive n[E] (outside NP) but are deleted under Num[E] (inside nP).

Instances For

@[implicit_reducible]

instance Minimalist.Ellipsis.instDecidableEqNomSpinePos :

DecidableEq NomSpinePos

Equations

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

@[implicit_reducible]

instance Minimalist.Ellipsis.instReprNomSpinePos :

Repr NomSpinePos

Equations

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

def Minimalist.Ellipsis.instReprNomSpinePos.repr :

NomSpinePos → ℕ → Std.Format

Equations

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

Instances For

def Minimalist.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 Minimalist.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

@[implicit_reducible]

instance Minimalist.Ellipsis.instDeletionSpineNomSpinePos :

DeletionSpine NomSpinePos

Equations

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

structure Minimalist.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

@[implicit_reducible]

instance Minimalist.Ellipsis.instReprNomEllipsisType :

Repr NomEllipsisType

Equations

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

def Minimalist.Ellipsis.instReprNomEllipsisType.repr :

NomEllipsisType → ℕ → Std.Format

Equations

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

Instances For

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

Is a nominal position in the deletion domain?

Equations

Minimalist.Ellipsis.nomInDeletionDomain c e = Minimalist.Ellipsis.inDomain c e.ePosition

Instances For

@[implicit_reducible]

instance Minimalist.Ellipsis.instDecidableNomInDeletionDomain (c : NomSpinePos) (e : NomEllipsisType) :

Decidable (nomInDeletionDomain c e)

Equations

Minimalist.Ellipsis.instDecidableNomInDeletionDomain c e = id inferInstance

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

Does a nominal position survive ellipsis?

Equations

Minimalist.Ellipsis.nomSurvives c e = ¬Minimalist.Ellipsis.nomInDeletionDomain c e

Instances For

@[implicit_reducible]

instance Minimalist.Ellipsis.instDecidableNomSurvives (c : NomSpinePos) (e : NomEllipsisType) :

Decidable (nomSurvives c e)

Equations

Minimalist.Ellipsis.instDecidableNomSurvives c e = id inferInstance

def Minimalist.Ellipsis.numPEllipsis :

NomEllipsisType

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

Equations

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

Instances For

def Minimalist.Ellipsis.nPEllipsis :

NomEllipsisType

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

Equations

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

Instances For

def Minimalist.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. [BS25]: German N-stranding NP-ellipsis.

Equations

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

Instances For

theorem Minimalist.Ellipsis.nStranding_deletes_NP :

nomInDeletionDomain NomSpinePos.N nStrandingNPE

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

theorem Minimalist.Ellipsis.nStranding_adj_survives :

nomSurvives NomSpinePos.NP_adj nStrandingNPE

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

theorem Minimalist.Ellipsis.nStranding_n_external :

nomSurvives NomSpinePos.n nStrandingNPE

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

theorem Minimalist.Ellipsis.nStranding_num_survives :

nomSurvives NomSpinePos.Num nStrandingNPE

Under N-stranding, Num is external (numerals survive). [BS25] ex. (25b): numeral zwei cannot be deleted under N-stranding.

theorem Minimalist.Ellipsis.nPE_deletes_N :

nomInDeletionDomain NomSpinePos.N nPEllipsis

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

theorem Minimalist.Ellipsis.nPE_deletes_adj :

nomInDeletionDomain NomSpinePos.NP_adj nPEllipsis

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

theorem Minimalist.Ellipsis.nPE_deletes_n :

nomInDeletionDomain NomSpinePos.n nPEllipsis

Under nP-ellipsis, n is deleted.

theorem Minimalist.Ellipsis.nPE_num_survives :

nomSurvives NomSpinePos.Num nPEllipsis

Under nP-ellipsis, Num is external (numerals survive). [Saa26]: the numeral/determiner remnant in Spanish pseudo-partitive ellipsis.

theorem Minimalist.Ellipsis.numPE_deletes_all :

nomInDeletionDomain NomSpinePos.N numPEllipsis ∧ nomInDeletionDomain NomSpinePos.NP_adj numPEllipsis ∧ nomInDeletionDomain NomSpinePos.n numPEllipsis ∧ nomInDeletionDomain NomSpinePos.Num numPEllipsis

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 Minimalist.Ellipsis.n_stranding_is_xStranding :

¬inDomain NomSpinePos.n NomSpinePos.n ∧ inDomain NomSpinePos.N NomSpinePos.n

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. [BS25]: German N-stranding NP-ellipsis.

theorem Minimalist.Ellipsis.v_stranding_is_xStranding :

¬inDomain SpinePos.v SpinePos.v ∧ inDomain SpinePos.V SpinePos.v

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 ([Kal26]).

theorem Minimalist.Ellipsis.clausal_nominal_xStranding_parallel :

inDomain SpinePos.V SpinePos.v ∧ inDomain NomSpinePos.N NomSpinePos.n

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.