Cinque (2020): a unified double-Headed analysis of relative clauses

[Cin20]

Formalizes the core of [Cin20]: all attested relative-clause types derive from a single double-Headed structure — an internal Head and an external Head (both indefinite dPs, smaller than DP), with the relative clause merged pre-nominally — via two derivation routes (§1.5):

• Raising — the internal Head raises to Spec,CP and is the overt Head, licensing deletion of the external Head ([Kay94] ch. 8). Reconstruction / island effects are detectable: the overt Head is in a chain with the RC-internal position.
• Matching — the external Head raises and is overt, licensing deletion of the internal Head. Reconstruction is not detectable.

Deletion of the internal Head is licit only when it exactly matches the external Head (both indefinite dP); when the relativized internal Head is bigger — a DP/KP, or a DP/KP inside a PP (an oblique) — no deletion is possible and the internal Head is realized by a wh-pronoun or a resumptive (§1.5).

The different RC types merge at different heights of the nominal extended projection (§3.5): non-restrictives attach above DP (external Head includes strong determiners), restrictives lower (external Head = weak determiners only), participials lower still. The internal-Head realization "strategies" (ch. 4) are gap + invariant relativizer, gap + relative pronoun, resumptive, PRO, non-reduction, and verb-coding.

This is the genuine syntactic treatment that computes a RelativeClause.Realization from the reified derivation — the consumer the substrate's projection hook was built for. [dV18] surveys the framework-neutral typology this single structure is meant to cover.

Main declarations

• Cinque2020.RC — the reified double-Headed relative clause.
• Cinque2020.RC.realization — its computed projection onto RelativeClause.Realization.
• Cinque2020.RC.WellFormed — the deletion-licensing condition.

Implementation notes

The reification stays at the level §1.5 states explicitly (two Heads, derivation route, internal-Head category and strategy, merge height); the tree geometry (Spec,CP, the dP/DP cartography) is below this level and not modelled. PRO and the verb-coding strategy have no exact RelativeClause.NPRelType counterpart in the Keenan-Comrie/WALS inventory the substrate was built from and are approximated when projecting.

The two derivations from the single double-Headed structure

inductive Cinque2020.Derivation : Type

The derivation route ([Cin20] §1.5).

• raising : Derivation

  The internal Head raises to Spec,CP and is overt; the external Head is deleted ([Kay94]).

• matching : Derivation

  The external Head is overt; the internal Head is deleted / a proform.

@[implicit_reducible]

instance Cinque2020.instDecidableEqDerivation : DecidableEq Derivation

Equations

• Cinque2020.instDecidableEqDerivation x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Cinque2020.instReprDerivation : Repr Derivation

Equations

• Cinque2020.instReprDerivation = { reprPrec := Cinque2020.instReprDerivation.repr }

def Cinque2020.instReprDerivation.repr : Derivation → ℕ → Std.Format

Equations

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

inductive Cinque2020.HeadChoice : Type

Which of the two Heads surfaces overtly.

• internal : HeadChoice
• external : HeadChoice

@[implicit_reducible]

instance Cinque2020.instDecidableEqHeadChoice : DecidableEq HeadChoice

Equations

• Cinque2020.instDecidableEqHeadChoice x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Cinque2020.instReprHeadChoice : Repr HeadChoice

Equations

• Cinque2020.instReprHeadChoice = { reprPrec := Cinque2020.instReprHeadChoice.repr }

def Cinque2020.instReprHeadChoice.repr : HeadChoice → ℕ → Std.Format

Equations

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

def Cinque2020.Derivation.overtHead : Derivation → HeadChoice

The overt Head is fixed by the derivation, not stipulated separately.

Equations

• Cinque2020.Derivation.raising.overtHead = Cinque2020.HeadChoice.internal
• Cinque2020.Derivation.matching.overtHead = Cinque2020.HeadChoice.external

The internal Head and its realization strategy

inductive Cinque2020.InternalHeadCategory : Type

Category of the relativized internal Head ([Cin20] §1.5). Deletion under identity with the external Head turns on this: only an indefinite dP exactly matches the (indefinite dP) external Head.

• indefiniteDP : InternalHeadCategory

  An indefinite dP exactly matching the external Head — deletion licit.

• biggerDPKP : InternalHeadCategory

  A DP/KP, or a DP/KP inside a PP (oblique) — bigger than dP, no deletion.

@[implicit_reducible]

instance Cinque2020.instDecidableEqInternalHeadCategory : DecidableEq InternalHeadCategory

Equations

• Cinque2020.instDecidableEqInternalHeadCategory x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Cinque2020.instReprInternalHeadCategory.repr : InternalHeadCategory → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Cinque2020.instReprInternalHeadCategory : Repr InternalHeadCategory

Equations

• Cinque2020.instReprInternalHeadCategory = { reprPrec := Cinque2020.instReprInternalHeadCategory.repr }

inductive Cinque2020.Strategy : Type

Strategies for realizing the internal Head ([Cin20] ch. 4).

• invariantRelativizer : Strategy

  Gap + invariant relativizer (English that, Italian che).

• relativePronoun : Strategy

  Gap + relative pronoun / adjective (who/which, Italian cui).

• resumptive : Strategy

  Resumptive pronoun / epithet.

• pro : Strategy

  PRO (participial relative clauses).

• nonReduction : Strategy

  Full repetition of the Head (non-reduction).

• verbCoding : Strategy

  The verb-coding strategy.

@[implicit_reducible]

instance Cinque2020.instDecidableEqStrategy : DecidableEq Strategy

Equations

• Cinque2020.instDecidableEqStrategy x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Cinque2020.instReprStrategy.repr : Strategy → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Cinque2020.instReprStrategy.repr Cinque2020.Strategy.pro prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Cinque2020.Strategy.pro")).group prec✝

@[implicit_reducible]

instance Cinque2020.instReprStrategy : Repr Strategy

Equations

• Cinque2020.instReprStrategy = { reprPrec := Cinque2020.instReprStrategy.repr }

def Cinque2020.Strategy.DeletesInternalHead (s : Strategy) : Prop

Does this strategy realize the internal Head by deleting it under identity with the external Head (the gap + invariant-relativizer case)? Only the invariant-relativizer strategy does. PRO is a null proform, not deletion: [Cin20] keeps deletion / non-pronunciation distinct from proform-replacement, so PRO is not subject to the exact-match licensing.

Equations

• s.DeletesInternalHead = (s = Cinque2020.Strategy.invariantRelativizer)

@[implicit_reducible]

instance Cinque2020.instDecidableDeletesInternalHead (s : Strategy) : Decidable s.DeletesInternalHead

Equations

• Cinque2020.instDecidableDeletesInternalHead s = id inferInstance

def Cinque2020.Strategy.toNPRelType : Strategy → RelativeClause.NPRelType

Project a Cinque strategy onto the substrate NPRelType. PRO and verb-coding have no exact counterpart in the substrate inventory and are approximated (PRO ≈ a silent gap; verb-coding ≈ non-reduction).

Equations

• Cinque2020.Strategy.invariantRelativizer.toNPRelType = RelativeClause.NPRelType.gap
• Cinque2020.Strategy.relativePronoun.toNPRelType = RelativeClause.NPRelType.relPronoun
• Cinque2020.Strategy.resumptive.toNPRelType = RelativeClause.NPRelType.resumptive
• Cinque2020.Strategy.pro.toNPRelType = RelativeClause.NPRelType.gap
• Cinque2020.Strategy.nonReduction.toNPRelType = RelativeClause.NPRelType.nonReduction
• Cinque2020.Strategy.verbCoding.toNPRelType = RelativeClause.NPRelType.nonReduction

Relative-clause types and merge height

inductive Cinque2020.RCType : Type

RC types, by increasing height of external merge in the nominal extended projection ([Cin20] §3.5): a bigger external Head merges higher.

• participial : RCType
• restrictive : RCType
• maximalizing : RCType
• kindDefining : RCType
• nonRestrictive : RCType

@[implicit_reducible]

instance Cinque2020.instDecidableEqRCType : DecidableEq RCType

Equations

• Cinque2020.instDecidableEqRCType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Cinque2020.instReprRCType : Repr RCType

Equations

• Cinque2020.instReprRCType = { reprPrec := Cinque2020.instReprRCType.repr }

def Cinque2020.instReprRCType.repr : RCType → ℕ → Std.Format

Equations

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

def Cinque2020.RCType.mergeHeight : RCType → ℕ

Relative merge height (bigger external Head = higher), per [Cin20] §3.5: participials lowest (smallest external Head); amount/maximalizing below ordinary restrictives (§3.5.5, presented as a tentative refinement of the §1.5 simplification that they merge alike); kind-defining between restrictives and non-restrictives (§3.5.3); non-restrictives highest (above DP).

Equations

• Cinque2020.RCType.participial.mergeHeight = 0
• Cinque2020.RCType.maximalizing.mergeHeight = 1
• Cinque2020.RCType.restrictive.mergeHeight = 2
• Cinque2020.RCType.kindDefining.mergeHeight = 3
• Cinque2020.RCType.nonRestrictive.mergeHeight = 4

The reified relative clause

structure Cinque2020.RC : Type

A relative clause in [Cin20]'s unified analysis: the single double-Headed structure (both Heads present by construction), a derivation route, the internal-Head category and realization strategy, the relativized AH position, and the position of the RC w.r.t. the Head.

• rcType : RCType
• derivation : Derivation
• internalHeadCategory : InternalHeadCategory
• strategy : Strategy
• position : RelativeClause.AHPosition
• rcPosition : RelativeClause.RCPosition

def Cinque2020.instReprRC.repr : RC → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Cinque2020.instReprRC : Repr RC

Equations

• Cinque2020.instReprRC = { reprPrec := Cinque2020.instReprRC.repr }

def Cinque2020.RC.overtHead (r : RC) : HeadChoice

The overt Head of an RC, determined by its derivation.

Equations

• r.overtHead = r.derivation.overtHead

def Cinque2020.RC.Reconstructs (r : RC) : Prop

Reconstruction / island effects are detectable iff the overt Head is the internal one (raising) — it is then in a chain with the RC-internal position ([Cin20] §1.5).

Equations

• r.Reconstructs = (r.derivation = Cinque2020.Derivation.raising)

@[implicit_reducible]

instance Cinque2020.instDecidableReconstructs (r : RC) : Decidable r.Reconstructs

Equations

• Cinque2020.instDecidableReconstructs r = id inferInstance

def Cinque2020.RC.WellFormed (r : RC) : Prop

[Cin20]'s deletion-licensing condition: the internal Head may be deleted (the gap + invariant-relativizer strategy) only when it exactly matches the external Head (an indefinite dP). A bigger internal Head (oblique DP/KP, or DP/KP in a PP) must be spelled out — a relative pronoun or a resumptive.

Equations

• r.WellFormed = (r.strategy.DeletesInternalHead → r.internalHeadCategory = Cinque2020.InternalHeadCategory.indefiniteDP)

@[implicit_reducible]

instance Cinque2020.instDecidableWellFormed (r : RC) : Decidable r.WellFormed

Equations

• Cinque2020.instDecidableWellFormed r = id inferInstance

def Cinque2020.RC.realization (r : RC) : RelativeClause.Realization

The framework-neutral RelativeClause.Realization this derivation projects to — computed from the reified structure (the relativized position and the NP_rel type the internal-Head strategy yields), not stipulated. The hook by which Cinque's analysis connects to the relativization substrate.

Equations

• r.realization = { position := r.position, npRel := r.strategy.toNPRelType }

Consequences

theorem Cinque2020.matching_not_reconstructs (r : RC) (h : r.derivation = Derivation.matching) : ¬r.Reconstructs

A matching derivation shows no reconstruction ([Cin20] §1.5).

theorem Cinque2020.bigger_head_no_gap_deletion (r : RC) (h : r.WellFormed) (hbig : r.internalHeadCategory = InternalHeadCategory.biggerDPKP) : r.strategy ≠ Strategy.invariantRelativizer

Deletion licensing. A well-formed RC whose relativized internal Head is bigger than an indefinite dP cannot use the gap-deletion (invariant relativizer) strategy — it must spell the internal Head out.

theorem Cinque2020.nonRestrictive_above_restrictive : RCType.restrictive.mergeHeight < RCType.nonRestrictive.mergeHeight

Non-restrictive RCs merge higher than restrictives ([Cin20] §3.5).

theorem Cinque2020.participial_lowest (t : RCType) : RCType.participial.mergeHeight ≤ t.mergeHeight

Participial RCs have the lowest external merge.

theorem Cinque2020.maximalizing_below_restrictive : RCType.maximalizing.mergeHeight < RCType.restrictive.mergeHeight

Amount/maximalizing RCs merge lower (closer to the Head) than ordinary restrictives — [Cin20] §3.5.5, presented there as a tentative refinement of the §1.5 simplification that they merge in the same position.

Worked examples

def Cinque2020.englishThatObject : RC

English "the book that John read ___": matching, internal Head exactly matches the external (indefinite dP), gap via the invariant relativizer that; object relative.

Equations

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

theorem Cinque2020.englishThatObject_realization : englishThatObject.realization = { position := RelativeClause.AHPosition.directObject, npRel := RelativeClause.NPRelType.gap }

It computes to the substrate realization (directObject, gap) — from Cinque's derivation rather than stipulated.

def Cinque2020.englishWhomOblique : RC

"the man to whom I spoke": oblique relativization. The internal Head is bigger than dP (a PP-internal DP/KP), so deletion is barred and a relative pronoun is used.

Equations

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

theorem Cinque2020.oblique_gap_deletion_illFormed : ¬{ rcType := RCType.restrictive, derivation := Derivation.matching, internalHeadCategory := InternalHeadCategory.biggerDPKP, strategy := Strategy.invariantRelativizer, position := RelativeClause.AHPosition.oblique, rcPosition := RelativeClause.RCPosition.postNominal }.WellFormed

The deletion-licensing bite: an oblique (bigger) internal Head cannot be deleted via the invariant relativizer — that derivation is ill-formed.

def Cinque2020.hebrewResumptiveGenitive : RC

Hebrew resumptive relativization at the genitive: matching, internal Head spelled out as a resumptive pronoun.

Equations

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

def Cinque2020.englishRaisingObject : RC

A raising derivation (overt Head = internal Head) shows reconstruction.

Equations

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