Ellipsis

Merchant's [E] feature on a head of a spine instructs the phonology not to pronounce the head's complement, under the presupposition that the complement is given. Each kind of ellipsis is an [E] feature on a head: VP-ellipsis puts it on Voice and deletes vP, sluicing puts it on C and deletes TP, and v-stranding VP-ellipsis puts it on v and deletes VP alone. A site of a spine is a head or the adjunction site of the phrase a head projects. [E] deletes the heads of its complement and the adjuncts of the phrases properly inside it, so that the adjuncts of the phrase just below the [E]-bearing head survive. A site outside the deletion domain survives and is invisible to the identity condition, so a mismatch in a feature its head bears is tolerated. Lowering [E] shrinks the domain, so whatever a higher ellipsis tolerates a lower one tolerates too, which is Sailor's generalization. [E]-deletion is one model of Hankamer and Sag's depth: the null sites of a spine are the complements [E] silences and the null pro-forms.

Main definitions

• Minimalist.ClauseSpine.Site: a head of a spine, or the adjunction site of the phrase it projects.
• Minimalist.ClauseSpine.Deletes: the sites [E] on a head deletes.
• Minimalist.Ellipsis: an [E] feature on a head of a spine, with Minimalist.Ellipsis.sluicing, Minimalist.Ellipsis.vpEllipsis, Minimalist.Ellipsis.vStrandingVPE on Minimalist.Ellipsis.clausalSpine, and Minimalist.Ellipsis.nPEllipsis on Minimalist.Ellipsis.nominalSpine.
• Minimalist.Ellipsis.Mismatch: the dimensions in which an elided phrase may differ from its antecedent, each regulated by a head of the spine.
• Minimalist.AgainReading: the two readings of again and their adjunction sites.
• Minimalist.NullSite: a null site of a spine, an [E] deletion domain or a null pro-form, with its Anaphor.DepthModel instance.

Main results

• Minimalist.ClauseSpine.not_deletes_head_self: the [E]-bearing head survives its own ellipsis, the core of X-stranding.
• Minimalist.ClauseSpine.Deletes.of_mem_below, Minimalist.Ellipsis.Tolerates.of_mem_below: Sailor's generalization, what [E] on a head deletes [E] on any higher head deletes too.
• Minimalist.NullSite.not_silences_ePosition: the head bearing [E] lies outside the site it silences.

Implementation notes

The adjunction site of a phrase lies below the head that selects the phrase but outside that head's complement, so restitutive again and manner roots, adjoined to VP, survive v-stranding VP-ellipsis while V does not, and prenominal modifiers, adjoined to NP, survive [E] on n. A null site built from [E] carries a site of its deletion domain, since a head at the bottom of a spine has no complement to silence; that witness is what the surface condition of Anaphor.DepthModel asks for.

References

• [Mer01]
• [Mer13b]
• [Kal26]
• [Sai14]
• [LS14]
• [BS25]
• [HS76]

inductive Minimalist.ClauseSpine.Site : Type

A site of a spine is a head, or the adjunction site of the phrase a head projects, where adjuncts such as again, manner roots and prenominal modifiers attach.

• head (c : Cat) : Site
• adjunct (c : Cat) : Site

@[instance_reducible]

instance Minimalist.ClauseSpine.instDecidableEqSite : DecidableEq Site

Equations

• Minimalist.ClauseSpine.instDecidableEqSite = Minimalist.ClauseSpine.instDecidableEqSite.decEq

def Minimalist.ClauseSpine.instDecidableEqSite.decEq (x✝ x✝¹ : Site) : Decidable (x✝ = x✝¹)

Equations

• Minimalist.ClauseSpine.instDecidableEqSite.decEq (Minimalist.ClauseSpine.Site.head a) (Minimalist.ClauseSpine.Site.head b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Minimalist.ClauseSpine.instDecidableEqSite.decEq (Minimalist.ClauseSpine.Site.head c) (Minimalist.ClauseSpine.Site.adjunct c_1) = isFalse ⋯
• Minimalist.ClauseSpine.instDecidableEqSite.decEq (Minimalist.ClauseSpine.Site.adjunct c) (Minimalist.ClauseSpine.Site.head c_1) = isFalse ⋯
• Minimalist.ClauseSpine.instDecidableEqSite.decEq (Minimalist.ClauseSpine.Site.adjunct a) (Minimalist.ClauseSpine.Site.adjunct b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Minimalist.ClauseSpine.instReprSite : Repr Site

Equations

• Minimalist.ClauseSpine.instReprSite = { reprPrec := Minimalist.ClauseSpine.instReprSite.repr }

def Minimalist.ClauseSpine.instReprSite.repr : Site → ℕ → Std.Format

Equations

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

def Minimalist.ClauseSpine.Deletes (s : ClauseSpine) (p : Cat) : Site → Prop

[E] on p deletes the heads of its complement, and the adjuncts of a phrase that some head of the complement takes in its own complement, so that the adjuncts of the phrase just below p survive.

Equations

• s.Deletes p (Minimalist.ClauseSpine.Site.head d) = (d ∈ s.below p)
• s.Deletes p (Minimalist.ClauseSpine.Site.adjunct d) = ∃ e ∈ s.below p, d ∈ s.below e

@[instance_reducible]

instance Minimalist.ClauseSpine.instDecidableDeletes (s : ClauseSpine) (p : Cat) (x : Site) : Decidable (s.Deletes p x)

Equations

• s.instDecidableDeletes p (Minimalist.ClauseSpine.Site.head d) = { decide := decide (List.elem d (s.below p) = true), reflects_decide := ⋯ }
• s.instDecidableDeletes p (Minimalist.ClauseSpine.Site.adjunct d) = Minimalist.ClauseSpine.instDecidableDeletes._aux_2 s p d

theorem Minimalist.ClauseSpine.not_deletes_head_self (s : ClauseSpine) (p : Cat) : ¬s.Deletes p (Site.head p)

The [E]-bearing head survives its own ellipsis, which is the core of X-stranding: a head that has moved to the [E]-bearing position is pronounced while its base position is deleted.

theorem Minimalist.ClauseSpine.Deletes.of_mem_below {s : ClauseSpine} {p q : Cat} {x : Site} (h : s.Deletes q x) (hq : q ∈ s.below p) : s.Deletes p x

Sailor's generalization. What [E] on a head deletes, [E] on any head above it deletes too.

Ellipsis types

structure Minimalist.Ellipsis (s : ClauseSpine) : Type

An ellipsis is an [E] feature on a head of the spine s; its deletion domain is that head's complement.

• ePosition : Cat

  The head carrying [E].

def Minimalist.instDecidableEqEllipsis.decEq {s✝ : ClauseSpine} (x✝ x✝¹ : Ellipsis s✝) : Decidable (x✝ = x✝¹)

Equations

• Minimalist.instDecidableEqEllipsis.decEq { ePosition := a } { ePosition := b } = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Minimalist.instDecidableEqEllipsis {s✝ : ClauseSpine} : DecidableEq (Ellipsis s✝)

Equations

• Minimalist.instDecidableEqEllipsis = Minimalist.instDecidableEqEllipsis.decEq

def Minimalist.instReprEllipsis.repr {s✝ : ClauseSpine} : Ellipsis s✝ → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Minimalist.instReprEllipsis {s✝ : ClauseSpine} : Repr (Ellipsis s✝)

Equations

• Minimalist.instReprEllipsis = { reprPrec := Minimalist.instReprEllipsis.repr }

def Minimalist.Ellipsis.clausalSpine : ClauseSpine

The clausal spine that ellipsis distinguishes, V, v, Voice, T and C.

Equations

• Minimalist.Ellipsis.clausalSpine = { heads := [Minimalist.Cat.V, Minimalist.Cat.v, Minimalist.Cat.Voice, Minimalist.Cat.T, Minimalist.Cat.C] }

def Minimalist.Ellipsis.nominalSpine : ClauseSpine

The nominal spine, N, the categorizer n, Num and D.

Equations

• Minimalist.Ellipsis.nominalSpine = { heads := [Minimalist.Cat.N, Minimalist.Cat.n, Minimalist.Cat.Num, Minimalist.Cat.D] }

def Minimalist.Ellipsis.Deletes {s : ClauseSpine} (e : Ellipsis s) (x : ClauseSpine.Site) : Prop

e.Deletes x when the site x lies in the deletion domain of e.

Equations

• e.Deletes x = s.Deletes e.ePosition x

@[instance_reducible]

instance Minimalist.Ellipsis.instDecidableDeletes {s : ClauseSpine} {e : Ellipsis s} {x : ClauseSpine.Site} : Decidable (e.Deletes x)

Equations

• Minimalist.Ellipsis.instDecidableDeletes = Minimalist.Ellipsis.instDecidableDeletes._aux_1

def Minimalist.Ellipsis.Spares {s : ClauseSpine} (e : Ellipsis s) (x : ClauseSpine.Site) : Prop

e.Spares x when the site x is external to e and survives it.

Equations

• e.Spares x = ¬e.Deletes x

@[instance_reducible]

instance Minimalist.Ellipsis.instDecidableSpares {s : ClauseSpine} {e : Ellipsis s} {x : ClauseSpine.Site} : Decidable (e.Spares x)

Equations

• Minimalist.Ellipsis.instDecidableSpares = { decide := !decide (e.Deletes x), reflects_decide := ⋯ }

theorem Minimalist.Ellipsis.spares_ePosition {s : ClauseSpine} (e : Ellipsis s) : e.Spares (ClauseSpine.Site.head e.ePosition)

theorem Minimalist.Ellipsis.Spares.of_mem_below {s : ClauseSpine} {e e' : Ellipsis s} {x : ClauseSpine.Site} (h : e.Spares x) (hle : e'.ePosition ∈ s.below e.ePosition) : e'.Spares x

Sailor's generalization. What an ellipsis spares, every ellipsis whose [E] sits lower spares.

def Minimalist.Ellipsis.sluicing : Ellipsis clausalSpine

Sluicing puts [E] on C and deletes TP.

Equations

• Minimalist.Ellipsis.sluicing = { ePosition := Minimalist.Cat.C }

def Minimalist.Ellipsis.vpEllipsis : Ellipsis clausalSpine

VP-ellipsis puts [E] on Voice and deletes vP, so that Voice is external to the ellipsis.

Equations

• Minimalist.Ellipsis.vpEllipsis = { ePosition := Minimalist.Cat.Voice }

def Minimalist.Ellipsis.vStrandingVPE : Ellipsis clausalSpine

v-stranding VP-ellipsis puts [E] on v and deletes VP alone, stranding the light verb.

Equations

• Minimalist.Ellipsis.vStrandingVPE = { ePosition := Minimalist.Cat.v }

def Minimalist.Ellipsis.nPEllipsis : Ellipsis nominalSpine

nP-ellipsis puts [E] on Num and deletes nP, the configuration [LS14] find in Spanish: the noun, the categorizer and prenominal modifiers are all deleted.

Equations

• Minimalist.Ellipsis.nPEllipsis = { ePosition := Minimalist.Cat.Num }

Mismatches

inductive Minimalist.Ellipsis.Mismatch : Type

A dimension in which an elided phrase may differ from its antecedent, each regulated by a head of the spine: voice by Voice, the causative, dative, prepositional and middle alternations by flavours of v, and the lexical verb by V.

• voice : Mismatch
• transitivity : Mismatch
• dative : Mismatch
• prepositional : Mismatch
• middle : Mismatch
• lexical : Mismatch

@[instance_reducible]

instance Minimalist.Ellipsis.instDecidableEqMismatch : DecidableEq Mismatch

Equations

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

def Minimalist.Ellipsis.instReprMismatch.repr : Mismatch → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Minimalist.Ellipsis.instReprMismatch : Repr Mismatch

Equations

• Minimalist.Ellipsis.instReprMismatch = { reprPrec := Minimalist.Ellipsis.instReprMismatch.repr }

def Minimalist.Ellipsis.Mismatch.head : Mismatch → Cat

The head that regulates each dimension.

Equations

• Minimalist.Ellipsis.Mismatch.voice.head = Minimalist.Cat.Voice
• Minimalist.Ellipsis.Mismatch.transitivity.head = Minimalist.Cat.v
• Minimalist.Ellipsis.Mismatch.dative.head = Minimalist.Cat.v
• Minimalist.Ellipsis.Mismatch.prepositional.head = Minimalist.Cat.v
• Minimalist.Ellipsis.Mismatch.middle.head = Minimalist.Cat.v
• Minimalist.Ellipsis.Mismatch.lexical.head = Minimalist.Cat.V

def Minimalist.Ellipsis.Tolerates (e : Ellipsis clausalSpine) (m : Mismatch) : Prop

e.Tolerates m when the head regulating m is external to e, so that a mismatch in m is invisible to the identity condition.

Equations

• e.Tolerates m = e.Spares (Minimalist.ClauseSpine.Site.head m.head)

@[instance_reducible]

instance Minimalist.Ellipsis.instDecidableTolerates (e : Ellipsis clausalSpine) (m : Mismatch) : Decidable (e.Tolerates m)

Equations

• e.instDecidableTolerates m = { decide := !decide (e.Deletes (Minimalist.ClauseSpine.Site.head m.head)), reflects_decide := ⋯ }

theorem Minimalist.Ellipsis.Tolerates.of_mem_below {e e' : Ellipsis clausalSpine} {m : Mismatch} (h : e.Tolerates m) (hle : e'.ePosition ∈ clausalSpine.below e.ePosition) : e'.Tolerates m

Sailor's generalization. A mismatch tolerated by an ellipsis is tolerated by every ellipsis whose [E] sits lower.

Null sites and depth

inductive Minimalist.NullSite (s : ClauseSpine) : Type

A null site of a spine: the complement an [E]-bearing head leaves unpronounced, which must contain some site, or a null pro-form, a head without a complement, such as pro or an empty noun.

• elided {s : ClauseSpine} (e : Ellipsis s) (h : ∃ (x : ClauseSpine.Site), e.Deletes x) : NullSite s
• proform {s : ClauseSpine} (x : ClauseSpine.Site) : NullSite s

def Minimalist.NullSite.depth {s : ClauseSpine} : NullSite s → Anaphor.Depth

[E]-deletion yields a surface anaphor, and a null pro-form a deep one.

Equations

• (Minimalist.NullSite.elided e h).depth = Anaphor.Depth.surface
• (Minimalist.NullSite.proform x_1).depth = Anaphor.Depth.deep

def Minimalist.NullSite.Silences {s : ClauseSpine} : NullSite s → ClauseSpine.Site → Prop

The sites a null site leaves unpronounced, the deletion domain of an [E]-bearing head and none for a pro-form.

Equations

• (Minimalist.NullSite.elided e h).Silences x✝ = e.Deletes x✝
• (Minimalist.NullSite.proform x_2).Silences x✝ = False

@[instance_reducible]

instance Minimalist.NullSite.instDepthModelSite {s : ClauseSpine} : Anaphor.DepthModel (NullSite s) ClauseSpine.Site

[E]-deletion realizes Hankamer and Sag's depth: an [E] site silences its complement, and a null pro-form silences nothing.

Equations

• Minimalist.NullSite.instDepthModelSite = { depth := Minimalist.NullSite.depth, Silences := Minimalist.NullSite.Silences, exists_silences_of_surface := ⋯, not_silences_of_deep := ⋯ }

@[instance_reducible]

instance Minimalist.NullSite.instDecidableSilences {s : ClauseSpine} (n : NullSite s) (x : ClauseSpine.Site) : Decidable (n.Silences x)

Equations

• (Minimalist.NullSite.elided e h).instDecidableSilences x✝ = Minimalist.NullSite.instDecidableSilences._aux_1 e h x✝
• (Minimalist.NullSite.proform x_2).instDecidableSilences x✝ = { decide := false, reflects_decide := ⋯ }

@[simp]

theorem Minimalist.NullSite.silences_elided {s : ClauseSpine} {e : Ellipsis s} {h : ∃ (x : ClauseSpine.Site), e.Deletes x} {x : ClauseSpine.Site} : (elided e h).Silences x ↔ e.Deletes x

theorem Minimalist.NullSite.not_silences_ePosition {s : ClauseSpine} {e : Ellipsis s} (h : ∃ (x : ClauseSpine.Site), e.Deletes x) : ¬(elided e h).Silences (ClauseSpine.Site.head e.ePosition)

The head that bears [E] lies outside the site it silences, which is what lets a head moved there strand.

The two readings of again

inductive Minimalist.AgainReading : Type

The two readings of again and their adjunction sites. Repetitive again adjoins to vP and presupposes an earlier event, restitutive again adjoins to VP and presupposes an earlier result state.

• repetitive : AgainReading
• restitutive : AgainReading

@[instance_reducible]

instance Minimalist.instDecidableEqAgainReading : DecidableEq AgainReading

Equations

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

@[instance_reducible]

instance Minimalist.instReprAgainReading : Repr AgainReading

Equations

• Minimalist.instReprAgainReading = { reprPrec := Minimalist.instReprAgainReading.repr }

def Minimalist.instReprAgainReading.repr : AgainReading → ℕ → Std.Format

Equations

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

def Minimalist.AgainReading.site : AgainReading → ClauseSpine.Site

The adjunction site of each reading.

Equations

• Minimalist.AgainReading.repetitive.site = Minimalist.ClauseSpine.Site.adjunct Minimalist.Cat.v
• Minimalist.AgainReading.restitutive.site = Minimalist.ClauseSpine.Site.adjunct Minimalist.Cat.V