Cascade Structures (@cite{pesetsky-1995})

@cite{pesetsky-1995}

Binary-branching PP spines where each node is a preposition (possibly phonologically null) that θ-selects its specifier. Cascade structures provide the geometry for:

1. T/SM restriction (Ch. 6): CAUS movement blocked by nonaffixal P
2. Backward binding (§6.2.2): CAUS starts lower than experiencer
3. Double object alternation (Ch. 5): G as zero preposition for Theme
4. Heavy shift (§7.2): rightward adjunction constrained by Cascades

Architecture

A Cascade is a recursive PP spine. Each layer has a preposition head (with an affixality feature) and a specifier DP. The complement of each layer is another layer or a terminal:

V'
├── V
└── PP₁ (head: P₁, spec: DP₁)
    └── PP₂ (head: P₂, spec: DP₂)
        └── PP₃ (head: P₃, spec: DP₃)

The Head Movement Constraint (HMC) determines whether a zero morpheme head (like CAUS) can incorporate into V by successive head adjunction through the spine. Movement is blocked if any intervening head is nonaffixal.

CAUS ≠ vCAUSE

Pesetsky's CAUS is a syntactic zero morpheme — a phonologically null P head that creates causative verbs by incorporating into V. This is distinct from @cite{cuervo-2003}'s VerbHead.vCAUSE, which is an event-structural head present in both causative and anticausative decompositions.

	Pesetsky CAUS	Cuervo vCAUSE
Nature	Syntactic head (P⁰)	Event-structural head
Phonology	Zero morpheme	Not a morpheme
Present in anticausative	No	Yes
Movement	Incorporates into V via HMC	No movement
Effect	Suppresses external θ-role	Relates subevents

structure Minimalist.CascadeHead : Type

A preposition head in a Cascade structure.

Each head has:

• label: identifies the head (e.g., "CAUS", "G", "at", "about")
• overt: whether the head is phonologically realized
• affixal: whether the head permits head adjunction passthrough

Affixality determines HMC behavior: when a lower head Z adjoins to this head Y, the resulting complex [Z+Y] is headed by Y. If Y is affixal, [Z+Y] can continue moving upward. If Y is nonaffixal, [Z+Y] is stuck — the complex cannot move further.

• label : String
• overt : Bool
• affixal : Bool

def Minimalist.instDecidableEqCascadeHead.decEq (x✝ x✝¹ : CascadeHead) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance Minimalist.instDecidableEqCascadeHead : DecidableEq CascadeHead

Equations

• Minimalist.instDecidableEqCascadeHead = Minimalist.instDecidableEqCascadeHead.decEq

def Minimalist.instReprCascadeHead.repr : CascadeHead → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Minimalist.instReprCascadeHead : Repr CascadeHead

Equations

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

def Minimalist.CascadeHead.isZero (h : CascadeHead) : Bool

Is this a zero morpheme (phonologically unrealized)?

Equations

• h.isZero = !h.overt

inductive Minimalist.Cascade : Type

A Cascade structure: binary-branching recursive PP spine.

Each layer consists of a P head, its specifier (a DP argument identified by a label), and its complement (another layer or a terminal). The outermost layer is V's complement.

• terminal : Cascade

  Base: bottom of the cascade (no more PP layers).

• layer : CascadeHead → String → Cascade → Cascade

  PP layer: head P, specifier DP label, complement.

@[implicit_reducible]

instance Minimalist.instReprCascade : Repr Cascade

Equations

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

def Minimalist.instReprCascade.repr : Cascade → ℕ → Std.Format

Equations

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

def Minimalist.Cascade.spine : Cascade → List CascadeHead

Extract the spine of P heads, ordered from closest-to-V (index 0) to deepest.

Equations

• Minimalist.Cascade.terminal.spine = []
• (Minimalist.Cascade.layer a a_1 a_2).spine = a :: a_2.spine

def Minimalist.Cascade.arguments : Cascade → List String

The argument labels, ordered from closest-to-V to deepest.

Equations

• Minimalist.Cascade.terminal.arguments = []
• (Minimalist.Cascade.layer a a_1 a_2).arguments = a_1 :: a_2.arguments

def Minimalist.Cascade.depth : Cascade → ℕ

Number of PP layers.

Equations

• Minimalist.Cascade.terminal.depth = 0
• (Minimalist.Cascade.layer a a_1 a_2).depth = 1 + a_2.depth

theorem Minimalist.spine_length_eq_depth (c : Cascade) : c.spine.length = c.depth

def Minimalist.canReachV (spine : List CascadeHead) (idx : ℕ) : Bool

Can a head at position idx in the spine reach V via successive head adjunction?

A head at position idx must adjoin to each intermediate head (positions idx−1, idx−2, …, 0) before reaching V. Movement is blocked if any intermediate head is nonaffixal, because the resulting complex is headed by the nonaffixal host, which cannot itself move. @cite{pesetsky-1995} §6.2.

Formally: all heads at positions 0 … idx−1 must be affixal.

Equations

• Minimalist.canReachV spine idx = (List.take idx spine).all fun (x : Minimalist.CascadeHead) => x.affixal

def Minimalist.findInSpine (spine : List CascadeHead) (label : String) : Option ℕ

Does the spine contain a head with the given label? Returns its index if found.

Equations

• Minimalist.findInSpine spine label = Minimalist.findInSpine.go label spine 0

def Minimalist.findInSpine.go (label : String) : List CascadeHead → ℕ → Option ℕ

Equations

• Minimalist.findInSpine.go label [] a✝ = none
• Minimalist.findInSpine.go label (h :: rest) a✝ = if (h.label == label) = true then some a✝ else Minimalist.findInSpine.go label rest (a✝ + 1)

def Minimalist.Cascade.headCanReachV (c : Cascade) (label : String) : Option Bool

Can a head with the given label reach V in this cascade?

Equations

• c.headCanReachV label = Option.map (fun (x : ℕ) => Minimalist.canReachV c.spine x) (Minimalist.findInSpine c.spine label)

def Minimalist.Cascade.hasHead (c : Cascade) (label : String) : Bool

Does this cascade contain a head with the given label?

Equations

• c.hasHead label = c.spine.any fun (x : Minimalist.CascadeHead) => x.label == label

def Minimalist.caus : CascadeHead

CAUS: zero causative morpheme. Decomposes Class II psych verbs as √root + CAUS. Affixal: must incorporate into V via HMC.

Equations

• Minimalist.caus = { label := "CAUS", overt := false, affixal := true }

def Minimalist.headG : CascadeHead

G: zero preposition for Theme/Patient. Mediates Theme θ-selection in double object constructions (§5.3). Affixal.

Equations

• Minimalist.headG = { label := "G", overt := false, affixal := true }

def Minimalist.headTEMP : CascadeHead

TEMP: zero temporal preposition (§7.1.5). Heads temporal adjunct PPs in Cascade structures. Affixal.

Equations

• Minimalist.headTEMP = { label := "TEMP", overt := false, affixal := true }

def Minimalist.headSUG : CascadeHead

SUG: zero Suggestor morpheme (§6.2.3). Parallel to CAUS for adjectives: assigns Suggestor role to AP's external argument (e.g., "his manner was angry"). Affixal.

Equations

• Minimalist.headSUG = { label := "SUG", overt := false, affixal := true }

def Minimalist.headAt : CascadeHead

Overt "at" — introduces Target stimulus in psych verbs. Nonaffixal: blocks CAUS movement through it.

Equations

• Minimalist.headAt = { label := "at", affixal := false }

def Minimalist.headAbout : CascadeHead

Overt "about" — introduces Subject Matter stimulus. Nonaffixal.

Equations

• Minimalist.headAbout = { label := "about", affixal := false }

def Minimalist.headTo : CascadeHead

Overt "to" — dative/goal preposition. Nonaffixal.

Equations

• Minimalist.headTo = { label := "to", affixal := false }

def Minimalist.headOf : CascadeHead

Overt "of" — partitive/possessive. Nonaffixal.

Equations

• Minimalist.headOf = { label := "of", affixal := false }

def Minimalist.thetaSuppressed (causAffixed rootHasExtArg : Bool) : Bool

@cite{pesetsky-1995} (522): Suppression of external argument.

Only affixation of a semantically contentful morpheme to a verb with an external argument α allows α to be unexpressed. When CAUS affixes to √annoy, the A-Causer (CAUS's object) surfaces as subject, and √annoy's original Agent role is suppressed.

This distinguishes CAUS from semantically vacuous affixes (e.g., anticausative SE), which do not suppress external arguments.

Equations

• Minimalist.thetaSuppressed causAffixed rootHasExtArg = (causAffixed && rootHasExtArg)

inductive Minimalist.CausVariant : Type

Two occurrences of CAUS in Experiencer predicate structures (@cite{pesetsky-1995} §6.2.2, p. 208):

• affixal (CAUS_aff): starts affixed to V in the lexicon; bears strong features that must be discharged at PF
• prepositional (CAUS_p): an independent P head in the Cascade; its features are discharged when V+CAUS_aff adjoins

• affixal : CausVariant
• prepositional : CausVariant

@[implicit_reducible]

instance Minimalist.instDecidableEqCausVariant : DecidableEq CausVariant

Equations

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

@[implicit_reducible]

instance Minimalist.instReprCausVariant : Repr CausVariant

Equations

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

def Minimalist.instReprCausVariant.repr : CausVariant → ℕ → Std.Format

Equations

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

def Minimalist.CausVariant.hasStrongFeatures : CausVariant → Bool

CAUS_aff bears strong features that must be discharged at PF.

Equations

• Minimalist.CausVariant.affixal.hasStrongFeatures = true
• Minimalist.CausVariant.prepositional.hasStrongFeatures = false

inductive Minimalist.CausStrength : Type

Three types of semantically causative verbs, classified by their relationship to CAUS (@cite{pesetsky-1995} §6.3, p. 217):

1. strong: A-Causer suppressed by CAUS_aff (ObjExp psych verbs, causative give). Subject = A-Causer, not Agent.
2. weak: CAUS adds a causal clause without suppressing any θ-role (causative break, grow).
3. absent: no CAUS at all (run, sleep).

• strong : CausStrength
• weak : CausStrength
• absent : CausStrength

@[implicit_reducible]

instance Minimalist.instDecidableEqCausStrength : DecidableEq CausStrength

Equations

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

def Minimalist.instReprCausStrength.repr : CausStrength → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Minimalist.instReprCausStrength : Repr CausStrength

Equations

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

def Minimalist.Cascade.causStrength (c : Cascade) : CausStrength

Derive CAUS strength from cascade structure. A cascade containing CAUS has strong causation; one without has absent. (Weak CAUS — causative break/grow — requires additional verbal decomposition beyond cascade presence alone.)

Equations

• c.causStrength = if c.hasHead "CAUS" = true then Minimalist.CausStrength.strong else Minimalist.CausStrength.absent

def Minimalist.Cascade.argPosition : Cascade → String → Option ℕ

Position of an argument label in the cascade (0 = closest to V, i.e., outermost PP = structurally highest).

Equations

• Minimalist.Cascade.terminal.argPosition x✝ = none
• (Minimalist.Cascade.layer a arg rest).argPosition x✝ = if (arg == x✝) = true then some 0 else Option.map (fun (x : ℕ) => x + 1) (rest.argPosition x✝)

def Minimalist.Cascade.specCCommands (c : Cascade) (commander commanded : String) : Bool

In a Cascade, spec of position i c-commands spec of position j when i < j (outer spec c-commands inner specs).

Position 0 = outermost PP (closest to V) = structurally highest. This follows from X-bar c-command: spec of PP₀ c-commands the complement of PP₀, which contains PP₁ and its spec.

Equations

• c.specCCommands commander commanded = match c.argPosition commander, c.argPosition commanded with | some i, some j => decide (i < j) | x, x_1 => false

def Minimalist.Cascade.shiftSites (c : Cascade) : ℕ

Number of potential heavy NP shift landing sites in a cascade. Each cascade layer provides one rightward adjunction site. @cite{pesetsky-1995} Ch. 7 derives HNPS from cascade geometry: shifted phrases adjoin to cascade nodes, so cascade depth determines how many landing sites are available.

Equations

• c.shiftSites = c.depth

theorem Minimalist.caus_is_zero : caus.isZero = true

Zero morphemes are phonologically unrealized.

theorem Minimalist.g_is_zero : headG.isZero = true

theorem Minimalist.temp_is_zero : headTEMP.isZero = true

theorem Minimalist.sug_is_zero : headSUG.isZero = true

theorem Minimalist.at_is_overt : headAt.isZero = false

Overt prepositions are phonologically realized.

theorem Minimalist.about_is_overt : headAbout.isZero = false

theorem Minimalist.caus_affixal : caus.affixal = true

Zero morphemes are affixal; T/SM prepositions are nonaffixal.

theorem Minimalist.g_affixal : headG.affixal = true

theorem Minimalist.at_nonaffixal : headAt.affixal = false

theorem Minimalist.about_nonaffixal : headAbout.affixal = false

theorem Minimalist.to_nonaffixal : headTo.affixal = false

theorem Minimalist.position_zero_reachable (spine : List CascadeHead) : canReachV spine 0 = true

A head at position 0 (immediately below V) can always reach V: no intervening heads.

theorem Minimalist.all_affixal_reachable (spine : List CascadeHead) (idx : ℕ) (h : (spine.all fun (x : CascadeHead) => x.affixal) = true) : canReachV spine idx = true

theorem Minimalist.nonaffixal_blocks (h : CascadeHead) (rest : List CascadeHead) (idx : ℕ) (hna : h.affixal = false) (hidx : idx > 0) : canReachV (h :: rest) idx = false

A nonaffixal head at position 0 blocks anything below it.

theorem Minimalist.terminal_spine : Cascade.terminal.spine = []

Spine of a terminal cascade is empty.

theorem Minimalist.single_layer_spine (h : CascadeHead) (arg : String) : (Cascade.layer h arg Cascade.terminal).spine = [h]

Spine of a single-layer cascade is a singleton.

theorem Minimalist.two_layer_spine (h₁ h₂ : CascadeHead) (a₁ a₂ : String) : (Cascade.layer h₁ a₁ (Cascade.layer h₂ a₂ Cascade.terminal)).spine = [h₁, h₂]

A two-layer cascade spine lists heads from top to bottom.

theorem Minimalist.vcause_in_anticausative_but_not_caus : isAnticausative [VerbHead.vCAUSE, VerbHead.vGO, VerbHead.vBE] = true

Pesetsky's CAUS is distinct from event-structural vCAUSE.

VerbHead.vCAUSE (from @cite{cuervo-2003}) is present in both causative and anticausative decompositions — it encodes the causal relation between subevents, independent of Voice.

Pesetsky's caus is a syntactic zero morpheme — a P⁰ head that creates causative verbs by incorporating into V, and is present ONLY in causative structures. The anticausative "the door opened" has vCAUSE (causal relation exists) but no CAUS (no zero morpheme creating a derived causative).

This theorem witnesses the structural distinction: vCAUSE can appear without external cause (anticausative), while CAUS always requires a Causer argument as its specifier in the Cascade.