Zero Syntax: Experiencers and Cascades

[Pes95]

Cascade-based analysis of Class II psych verbs. The T/SM restriction (Cause and Subject Matter cannot cooccur) is derived from the Head Movement Constraint: CAUS must incorporate into V by successive head adjunction through the Cascade spine, and nonaffixal overt prepositions (T/SM heads like at and about) block this movement.

Key results

1. T/SM restriction from HMC (§ 2): CAUS is blocked by nonaffixal P
2. T/SM mutual exclusivity (§ 2): each cascade has at most one stimulus slot
3. Backward binding as derived-subject diagnostic (§ 3): A-Causer originates inside VP (spec of CAUS in cascade complement), must raise to subject — reconstruction enables backward binding
4. Double object alternation (§ 4): G (zero P) vs to cascades
5. θ-suppression (§ 5): CAUS affixation suppresses external argument
6. CAUS strength derived from cascade geometry (§ 6)
7. Symmetric T/SM blocking (§ 7): both at and about are nonaffixal, so both block CAUS movement equally via HMC
8. Natural vs arbitrary predicates (§ 9): Target-selecting predicates are "natural," SM-selecting predicates are "arbitrary"
9. HNPS from cascade geometry (§ 10): cascade depth determines available landing sites for heavy NP shift
10. End-to-end per-verb derivation (§ 9): full cascade chain for all 24 Class II psych verbs, derived from causalSource

Cascade structures ([Pes95])

Binary-branching PP spines where each node is a (possibly null) preposition that θ-selects its specifier — the geometry behind the T/SM restriction (Ch. 6), backward binding (§6.2.2), the dative alternation (Ch. 5), and heavy NP shift (§7.2). Formerly Syntax/Minimalist/Cascade.lean, dissolved here as this paper's apparatus.

CAUS ≠ vCAUSE. Pesetsky's caus is a syntactic zero morpheme (a null P⁰ that creates causatives by incorporating into V via the HMC); distinct from [Cue03]'s event- structural VerbHead.vCAUSE (present in both causative and anticausative).

structure Minimalist.CascadeHead : Type

A preposition head in a Cascade. affixal determines HMC passthrough: when a lower head Z adjoins to this head Y, the complex [Z+Y] can move on only if Y is affixal.

• 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

@[implicit_reducible]

instance Minimalist.instReprCascadeHead : Repr CascadeHead

Equations

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

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

Equations

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

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: a binary-branching recursive PP spine. Each layer is a P head, its specifier-DP label, and a complement (another layer or the terminal).

• terminal : Cascade
• layer : CascadeHead → String → Cascade → Cascade

@[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

The spine of P heads, 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, 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 spine position idx reach V via successive head adjunction? It must adjoin to each intermediate head (positions idx−1 … 0); blocked if any is nonaffixal ([Pes95] §6.2).

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 ℕ

Index of the head with the given label, if present.

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; affixal, incorporates into V via the HMC.

Equations

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

def Minimalist.headG : CascadeHead

G: zero preposition for Theme/Patient in double object constructions (§5.3); affixal.

Equations

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

def Minimalist.headAt : CascadeHead

Overt "at" — Target stimulus; nonaffixal (blocks CAUS movement through it).

Equations

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

def Minimalist.headAbout : CascadeHead

Overt "about" — Subject Matter stimulus; nonaffixal.

Equations

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

def Minimalist.headTo : CascadeHead

Overt "to" — dative/goal; 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

[Pes95] (522): only affixation of a semantically contentful morpheme to a verb with an external argument lets that argument go unexpressed (CAUS suppresses √annoy's Agent; vacuous affixes like anticausative SE do not).

Equations

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

inductive Minimalist.CausVariant : Type

The two occurrences of CAUS in Experiencer predicates ([Pes95] §6.2.2): affixal (CAUS_aff, strong features) vs prepositional (CAUS_p, independent P).

• 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 ⋯

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

Equations

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

@[implicit_reducible]

instance Minimalist.instReprCausVariant : Repr CausVariant

Equations

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

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

Causative-verb classification by relation to CAUS ([Pes95] §6.3): strong (A-Causer suppressed), weak (CAUS, no suppression), absent.

• 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

Strong causation iff the cascade contains CAUS; else absent. (Weak CAUS needs further verbal decomposition beyond cascade presence.)

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 (0 = 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

Spec of position i c-commands spec of position j iff i < j (outer c-commands inner).

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) : ℕ

Heavy-NP-shift landing sites: one per cascade layer ([Pes95] Ch. 7).

Equations

• c.shiftSites = c.depth

theorem Minimalist.caus_is_zero : caus.isZero = true

theorem Minimalist.g_is_zero : headG.isZero = true

theorem Minimalist.at_is_overt : headAt.isZero = false

theorem Minimalist.about_is_overt : headAbout.isZero = false

theorem Minimalist.caus_affixal : caus.affixal = true

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 always reaches V.

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

If every spine head is affixal, any position reaches V.

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 = []

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

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

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

CAUS is a syntactic zero morpheme present only in causatives; [Cue03]'s event-structural vCAUSE appears in anticausatives too — they are distinct.

inductive Pesetsky1995.PsychVerbs.PsychVerbClass : Type

[BR88] classification of psych verbs.

• classI : PsychVerbClass
• classII : PsychVerbClass
• classIII : PsychVerbClass

@[implicit_reducible]

instance Pesetsky1995.PsychVerbs.instDecidableEqPsychVerbClass : DecidableEq PsychVerbClass

Equations

• Pesetsky1995.PsychVerbs.instDecidableEqPsychVerbClass x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Pesetsky1995.PsychVerbs.instReprPsychVerbClass : Repr PsychVerbClass

Equations

• Pesetsky1995.PsychVerbs.instReprPsychVerbClass = { reprPrec := Pesetsky1995.PsychVerbs.instReprPsychVerbClass.repr }

def Pesetsky1995.PsychVerbs.instReprPsychVerbClass.repr : PsychVerbClass → ℕ → Std.Format

Equations

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

inductive Pesetsky1995.PsychVerbs.ClassIIReading : Type

Aspectual reading of a Class II psych verb.

• eventive : ClassIIReading
• stative : ClassIIReading

@[implicit_reducible]

instance Pesetsky1995.PsychVerbs.instDecidableEqClassIIReading : DecidableEq ClassIIReading

Equations

• Pesetsky1995.PsychVerbs.instDecidableEqClassIIReading x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Pesetsky1995.PsychVerbs.instReprClassIIReading.repr : ClassIIReading → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Pesetsky1995.PsychVerbs.instReprClassIIReading : Repr ClassIIReading

Equations

• Pesetsky1995.PsychVerbs.instReprClassIIReading = { reprPrec := Pesetsky1995.PsychVerbs.instReprClassIIReading.repr }

inductive Pesetsky1995.PsychVerbs.BRDiagnostic : Type

B&R syntactic diagnostic for discriminating psych verb classes (§§1–2).

• anaphoricCliticization : BRDiagnostic
• arbitraryPro : BRDiagnostic
• causativeFare : BRDiagnostic
• backwardBinding : BRDiagnostic
• adjectivalPassive : BRDiagnostic

@[implicit_reducible]

instance Pesetsky1995.PsychVerbs.instDecidableEqBRDiagnostic : DecidableEq BRDiagnostic

Equations

• Pesetsky1995.PsychVerbs.instDecidableEqBRDiagnostic x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Pesetsky1995.PsychVerbs.instReprBRDiagnostic : Repr BRDiagnostic

Equations

• Pesetsky1995.PsychVerbs.instReprBRDiagnostic = { reprPrec := Pesetsky1995.PsychVerbs.instReprBRDiagnostic.repr }

def Pesetsky1995.PsychVerbs.instReprBRDiagnostic.repr : BRDiagnostic → ℕ → Std.Format

Equations

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

structure Pesetsky1995.PsychVerbs.BRDiagnosticResult : Type

Result of a B&R diagnostic applied to each class. classI/classII record whether the class passes the test.

• diagnostic : BRDiagnostic
• classI : Bool
• classII : Bool

@[implicit_reducible]

instance Pesetsky1995.PsychVerbs.instReprBRDiagnosticResult : Repr BRDiagnosticResult

Equations

• Pesetsky1995.PsychVerbs.instReprBRDiagnosticResult = { reprPrec := Pesetsky1995.PsychVerbs.instReprBRDiagnosticResult.repr }

def Pesetsky1995.PsychVerbs.instReprBRDiagnosticResult.repr : BRDiagnosticResult → ℕ → Std.Format

Equations

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

def Pesetsky1995.PsychVerbs.instBEqBRDiagnosticResult.beq : BRDiagnosticResult → BRDiagnosticResult → Bool

Equations

• One or more equations did not get rendered due to their size.
• Pesetsky1995.PsychVerbs.instBEqBRDiagnosticResult.beq x✝¹ x✝ = false

@[implicit_reducible]

instance Pesetsky1995.PsychVerbs.instBEqBRDiagnosticResult : BEq BRDiagnosticResult

Equations

• Pesetsky1995.PsychVerbs.instBEqBRDiagnosticResult = { beq := Pesetsky1995.PsychVerbs.instBEqBRDiagnosticResult.beq }

def Pesetsky1995.PsychVerbs.brDiagnosticData : List BRDiagnosticResult

[BR88] diagnostic data.

Diagnostic	Class I (temere)	Class II (preoccupare)
Anaphoric clitic ne (§1.1)	✗	✓ (11a)
Arbitrary pro (§1.2)	✓ (24a)	✗ (24b)
Causative fare (§1.3)	✓ (35)	✗ (36)
Backward binding (§2.1)	✗	✓ (57a)
Adjectival passive (§1.5)	✗	✓ (47)

Equations

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

theorem Pesetsky1995.PsychVerbs.br_diagnostics_discriminate : (brDiagnosticData.all fun (d : BRDiagnosticResult) => d.classI != d.classII) = true

Every B&R diagnostic discriminates Class I from Class II.

theorem Pesetsky1995.PsychVerbs.classI_pattern : (brDiagnosticData.all fun (d : BRDiagnosticResult) => match d.diagnostic with | BRDiagnostic.anaphoricCliticization => d.classI == false | BRDiagnostic.arbitraryPro => d.classI == true | BRDiagnostic.causativeFare => d.classI == true | BRDiagnostic.backwardBinding => d.classI == false | BRDiagnostic.adjectivalPassive => d.classI == false) = true

Class I passes arb-pro and causative-fare but fails the other three.

theorem Pesetsky1995.PsychVerbs.classII_pattern : (brDiagnosticData.all fun (d : BRDiagnosticResult) => match d.diagnostic with | BRDiagnostic.anaphoricCliticization => d.classII == true | BRDiagnostic.arbitraryPro => d.classII == false | BRDiagnostic.causativeFare => d.classII == false | BRDiagnostic.backwardBinding => d.classII == true | BRDiagnostic.adjectivalPassive => d.classII == true) = true

Class II shows the mirror pattern.

inductive Pesetsky1995.PsychVerbs.SubjectRole : Type

The Class I/II distinction is characterized by theta-role reversal.

• experiencer : SubjectRole
• stimulus : SubjectRole

@[implicit_reducible]

instance Pesetsky1995.PsychVerbs.instDecidableEqSubjectRole : DecidableEq SubjectRole

Equations

• Pesetsky1995.PsychVerbs.instDecidableEqSubjectRole x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Pesetsky1995.PsychVerbs.instReprSubjectRole : Repr SubjectRole

Equations

• Pesetsky1995.PsychVerbs.instReprSubjectRole = { reprPrec := Pesetsky1995.PsychVerbs.instReprSubjectRole.repr }

def Pesetsky1995.PsychVerbs.instReprSubjectRole.repr : SubjectRole → ℕ → Std.Format

Equations

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

def Pesetsky1995.PsychVerbs.PsychVerbClass.expectedSubjectRole : PsychVerbClass → Option SubjectRole

Map from B&R class to expected subject role.

Equations

• Pesetsky1995.PsychVerbs.PsychVerbClass.classI.expectedSubjectRole = some Pesetsky1995.PsychVerbs.SubjectRole.experiencer
• Pesetsky1995.PsychVerbs.PsychVerbClass.classII.expectedSubjectRole = some Pesetsky1995.PsychVerbs.SubjectRole.stimulus
• Pesetsky1995.PsychVerbs.PsychVerbClass.classIII.expectedSubjectRole = none

structure Pesetsky1995.PsychVerbs.IntensionalityDatum : Type

Intensionality datum ([Kim24] Ch. 4): does substitution of co-referential terms fail in subject position?

• verb : String
• reading : ClassIIReading
• substitutionFails : Bool

@[implicit_reducible]

instance Pesetsky1995.PsychVerbs.instReprIntensionalityDatum : Repr IntensionalityDatum

Equations

• Pesetsky1995.PsychVerbs.instReprIntensionalityDatum = { reprPrec := Pesetsky1995.PsychVerbs.instReprIntensionalityDatum.repr }

def Pesetsky1995.PsychVerbs.instReprIntensionalityDatum.repr : IntensionalityDatum → ℕ → Std.Format

Equations

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

def Pesetsky1995.PsychVerbs.instBEqIntensionalityDatum.beq : IntensionalityDatum → IntensionalityDatum → Bool

Equations

• One or more equations did not get rendered due to their size.
• Pesetsky1995.PsychVerbs.instBEqIntensionalityDatum.beq x✝¹ x✝ = false

@[implicit_reducible]

instance Pesetsky1995.PsychVerbs.instBEqIntensionalityDatum : BEq IntensionalityDatum

Equations

• Pesetsky1995.PsychVerbs.instBEqIntensionalityDatum = { beq := Pesetsky1995.PsychVerbs.instBEqIntensionalityDatum.beq }

def Pesetsky1995.PsychVerbs.intensionalityData : List IntensionalityDatum

Empirical intensionality data from [Kim24].

Equations

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

structure Pesetsky1995.PsychVerbs.TSMRestriction : Type

The T/SM restriction ([Kim24] Ch. 5): Cause and Subject Matter cannot cooccur.

• causePresent : Bool
• smPresent : Bool
• wellFormed : Bool

@[implicit_reducible]

instance Pesetsky1995.PsychVerbs.instReprTSMRestriction : Repr TSMRestriction

Equations

• Pesetsky1995.PsychVerbs.instReprTSMRestriction = { reprPrec := Pesetsky1995.PsychVerbs.instReprTSMRestriction.repr }

def Pesetsky1995.PsychVerbs.instReprTSMRestriction.repr : TSMRestriction → ℕ → Std.Format

Equations

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

def Pesetsky1995.PsychVerbs.instBEqTSMRestriction.beq : TSMRestriction → TSMRestriction → Bool

Equations

• One or more equations did not get rendered due to their size.
• Pesetsky1995.PsychVerbs.instBEqTSMRestriction.beq x✝¹ x✝ = false

@[implicit_reducible]

instance Pesetsky1995.PsychVerbs.instBEqTSMRestriction : BEq TSMRestriction

Equations

• Pesetsky1995.PsychVerbs.instBEqTSMRestriction = { beq := Pesetsky1995.PsychVerbs.instBEqTSMRestriction.beq }

def Pesetsky1995.PsychVerbs.tsmData : List TSMRestriction

Cause and SM cannot cooccur.

Equations

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

theorem Pesetsky1995.PsychVerbs.stative_substitution_fails : ((List.filter (fun (x : IntensionalityDatum) => x.reading == ClassIIReading.stative) intensionalityData).all fun (x : IntensionalityDatum) => x.substitutionFails) = true

Stative Class II verbs create intensional subject positions.

theorem Pesetsky1995.PsychVerbs.eventive_substitution_succeeds : ((List.filter (fun (x : IntensionalityDatum) => x.reading == ClassIIReading.eventive) intensionalityData).all fun (x : IntensionalityDatum) => !x.substitutionFails) = true

Eventive Class II verbs have extensional subject positions.

theorem Pesetsky1995.PsychVerbs.cause_sm_cooccurrence_illformed : ((List.filter (fun (d : TSMRestriction) => d.causePresent && d.smPresent) tsmData).all fun (x : TSMRestriction) => !x.wellFormed) = true

Cause + SM cooccurrence is always ill-formed.

def Pesetsky1995.cascadeTarget : Minimalist.Cascade

Class II psych verb with Target stimulus via at.

V'
├── V (annoy, frighten, ...)
└── PP_CAUS (head: CAUS, spec: A-Causer)
    └── PP_at (head: at, spec: Experiencer)
        └── terminal

CAUS is closest to V (position 0), then at (position 1). The A-Causer is the specifier of CAUS; the Experiencer is the specifier of at.

Equations

• Pesetsky1995.cascadeTarget = Minimalist.Cascade.layer Minimalist.caus "A-Causer" (Minimalist.Cascade.layer Minimalist.headAt "Experiencer" Minimalist.Cascade.terminal)

def Pesetsky1995.cascadeSM : Minimalist.Cascade

Class II psych verb with Subject Matter stimulus via about.

Same geometry as Target, but with about instead of at. Both are nonaffixal, so both block CAUS equally.

Equations

• Pesetsky1995.cascadeSM = Minimalist.Cascade.layer Minimalist.caus "A-Causer" (Minimalist.Cascade.layer Minimalist.headAbout "Experiencer" Minimalist.Cascade.terminal)

def Pesetsky1995.cascadeCausePlusStimulus : Minimalist.Cascade

Class II psych verb with BOTH Cause and T/SM stimulus.

V'
├── V
└── PP_CAUS (head: CAUS, spec: A-Causer)
    └── PP_at (head: at, spec: Target)
        └── PP_about (head: about, spec: SM)
            └── terminal

The ill-formed structure that the T/SM restriction rules out.

Equations

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

def Pesetsky1995.cascadeDOC : Minimalist.Cascade

Double object construction with zero G preposition.

V'
├── V (give)
└── PP_G (head: G, spec: Theme)
    └── PP_to (head: to, spec: Goal)
        └── terminal

G is a zero preposition that mediates Theme θ-selection in double object constructions.

Equations

• Pesetsky1995.cascadeDOC = Minimalist.Cascade.layer Minimalist.headG "Theme" (Minimalist.Cascade.layer Minimalist.headTo "Goal" Minimalist.Cascade.terminal)

def Pesetsky1995.cascadeDative : Minimalist.Cascade

Dative alternant: single to-PP.

V'
├── V (give)
└── PP_to (head: to, spec: Goal)
    └── terminal

Equations

• Pesetsky1995.cascadeDative = Minimalist.Cascade.layer Minimalist.headTo "Goal" Minimalist.Cascade.terminal

def Pesetsky1995.cascadeForSource : Causation.Psych.CausalSource → Minimalist.Cascade

Derive the appropriate cascade from a verb's causal source. External cause → Target cascade (with at); internal cause → SM cascade (with about).

Equations

• Pesetsky1995.cascadeForSource Causation.Psych.CausalSource.external = Pesetsky1995.cascadeTarget
• Pesetsky1995.cascadeForSource Causation.Psych.CausalSource.internal = Pesetsky1995.cascadeSM

The T/SM restriction follows from the HMC: CAUS at position 0 must incorporate into V, but any nonaffixal head between CAUS and V blocks movement. In the Target/SM cascades, CAUS IS at position 0 (closest to V), so it CAN reach V — there are no intervening heads.

The restriction arises in a different configuration: when an OVERT
Cause argument occupies the specifier of CAUS, the T/SM stimulus
cannot also be expressed, because the Cascade geometry doesn't have
room for both an independent Cause and a T/SM stimulus while keeping
CAUS in a position that can incorporate.

More precisely: in Pesetsky's actual account, the restriction comes
from the fact that CAUS_aff (on V) must DISCHARGE its strong features
by adjoining to CAUS_p (in the Cascade). If a nonaffixal head
intervenes between CAUS_p and the stimulus head, the Cascade
geometry is ill-formed. 

theorem Pesetsky1995.target_spine : cascadeTarget.spine = [Minimalist.caus, Minimalist.headAt]

Target cascade spine: [CAUS, at].

theorem Pesetsky1995.sm_spine : cascadeSM.spine = [Minimalist.caus, Minimalist.headAbout]

SM cascade spine: [CAUS, about].

theorem Pesetsky1995.caus_reachable_in_target : cascadeTarget.headCanReachV "CAUS" = some true

CAUS is at position 0 in the Target cascade. Position 0 can always reach V (no interveners).

theorem Pesetsky1995.caus_reachable_in_sm : cascadeSM.headCanReachV "CAUS" = some true

CAUS is at position 0 in the SM cascade. Position 0 can always reach V (no interveners).

theorem Pesetsky1995.at_blocks_below : Minimalist.canReachV cascadeCausePlusStimulus.spine 2 = false

The nonaffixal at head blocks anything below it. In the Cause+Stimulus cascade, at at position 1 blocks position 2+.

theorem Pesetsky1995.about_blocks_in_extended : Minimalist.canReachV [Minimalist.caus, Minimalist.headAbout, Minimalist.headAt] 2 = false

The nonaffixal about head also blocks anything below it.

theorem Pesetsky1995.tsm_restriction_via_hmc : Minimalist.canReachV cascadeCausePlusStimulus.spine 0 = true ∧ Minimalist.canReachV cascadeCausePlusStimulus.spine 2 = false ∧ Minimalist.canReachV cascadeCausePlusStimulus.spine 3 = false

Core T/SM restriction theorem: in the Cause+Stimulus cascade, the CAUS head can reach V (it's at position 0), but any head at position 2 or deeper cannot — blocked by the nonaffixal at at position 1.

theorem Pesetsky1995.t_sm_exclusive_in_target : cascadeTarget.hasHead "at" = true ∧ cascadeTarget.hasHead "about" = false

T/SM mutual exclusivity (Target cascade): the Target cascade contains at but not about. A single cascade geometry admits at most one stimulus type, so T and SM cannot cooccur within a single verb's cascade complement.

theorem Pesetsky1995.t_sm_exclusive_in_sm : cascadeSM.hasHead "about" = true ∧ cascadeSM.hasHead "at" = false

T/SM mutual exclusivity (SM cascade): the SM cascade contains about but not at.

theorem Pesetsky1995.source_determines_unique_stimulus : (cascadeForSource Causation.Psych.CausalSource.external).hasHead "at" = true ∧ (cascadeForSource Causation.Psych.CausalSource.external).hasHead "about" = false ∧ (cascadeForSource Causation.Psych.CausalSource.internal).hasHead "about" = true ∧ (cascadeForSource Causation.Psych.CausalSource.internal).hasHead "at" = false

The cascade assigned to a verb is determined by its causal source, so a verb with a single source gets exactly one stimulus type. External source → cascade with at (Target), no about (SM). Internal source → cascade with about (SM), no at (Target).

Backward binding in Class II psych verbs ("Stories about each other_i worried the boys_i") is diagnosed by B&R as a Class II property.

Pesetsky's cascade geometry explains this: the A-Causer originates
INSIDE the cascade complement of V (spec of CAUS at position 0),
making it a VP-internal argument. It must RAISE to subject position
(Spec,IP) to receive Case. This derived-subject status enables
backward binding via reconstruction: at LF, the raised subject
reconstructs to its base position inside the cascade, where the
experiencer (in the higher position within the VP) c-commands it.

In the base cascade, A-Causer (position 0, outermost) actually
c-commands the Experiencer (position 1, inner). The binding reversal
comes from movement + reconstruction, not from the base geometry. 

theorem Pesetsky1995.causer_is_cascade_internal : cascadeTarget.argPosition "A-Causer" = some 0 ∧ cascadeSM.argPosition "A-Causer" = some 0

A-Causer originates inside the cascade at position 0 (spec of CAUS). This VP-internal base position means the surface subject is DERIVED — the key structural prerequisite for backward binding.

theorem Pesetsky1995.causer_ccommands_experiencer_base : cascadeTarget.specCCommands "A-Causer" "Experiencer" = true ∧ cascadeSM.specCCommands "A-Causer" "Experiencer" = true

In the base cascade, A-Causer (outer, position 0) c-commands Experiencer (inner, position 1) — the standard direction.

theorem Pesetsky1995.experiencer_does_not_ccommand_causer_base : cascadeTarget.specCCommands "Experiencer" "A-Causer" = false ∧ cascadeSM.specCCommands "Experiencer" "A-Causer" = false

The experiencer does NOT c-command the A-Causer in the base cascade. Backward binding requires A-Causer to raise to subject, then reconstruct — the experiencer binds the reconstructed copy.

theorem Pesetsky1995.backward_binding_br_match : ((List.filter (fun (x : PsychVerbs.BRDiagnosticResult) => x.diagnostic == PsychVerbs.BRDiagnostic.backwardBinding) PsychVerbs.brDiagnosticData).all fun (x : PsychVerbs.BRDiagnosticResult) => x.classII) = true

Backward binding diagnostic matches Cascade prediction. B&R diagnostic: Class II allows backward binding (Data.lean).

theorem Pesetsky1995.doc_spine : cascadeDOC.spine = [Minimalist.headG, Minimalist.headTo]

DOC cascade has zero G (affixal) and overt to (nonaffixal).

theorem Pesetsky1995.g_reaches_v : cascadeDOC.headCanReachV "G" = some true

G can reach V because it's at position 0 (zero affixal P).

theorem Pesetsky1995.doc_arguments : cascadeDOC.arguments = ["Theme", "Goal"]

DOC argument order: Theme (spec of G) then Goal (spec of to).

theorem Pesetsky1995.dative_spine : cascadeDative.spine = [Minimalist.headTo]

Dative alternant has only to (nonaffixal).

theorem Pesetsky1995.doc_vs_dative_depth : cascadeDOC.depth = 2 ∧ cascadeDative.depth = 1

DOC vs dative: different cascade geometries.

theorem Pesetsky1995.caus_aff_suppresses : Minimalist.CausVariant.affixal.hasStrongFeatures = true ∧ Minimalist.thetaSuppressed true true = true

Strong CAUS (affixal variant) suppresses root's external θ-role.

When CAUS_aff is affixed to √annoy, the agent role of the root is suppressed. The A-Causer (CAUS's own specifier) surfaces as the derived subject instead.

theorem Pesetsky1995.caus_p_no_strong_features : Minimalist.CausVariant.prepositional.hasStrongFeatures = false

Prepositional CAUS does NOT have strong features.

theorem Pesetsky1995.no_caus_no_suppression : Minimalist.thetaSuppressed false true = false

Without CAUS affixation, no suppression occurs.

theorem Pesetsky1995.no_ext_arg_no_suppression : Minimalist.thetaSuppressed true false = false

Without an external argument, there's nothing to suppress.

theorem Pesetsky1995.classII_has_strong_caus : cascadeTarget.causStrength = Minimalist.CausStrength.strong ∧ cascadeSM.causStrength = Minimalist.CausStrength.strong

Target and SM cascades both contain CAUS → strong causation.

theorem Pesetsky1995.classI_no_caus : Minimalist.Cascade.terminal.causStrength = Minimalist.CausStrength.absent

A terminal cascade (no CAUS) → absent causation (Class I).

theorem Pesetsky1995.caus_strength_uniform_across_classII : (cascadeForSource Causation.Psych.CausalSource.external).causStrength = Minimalist.CausStrength.strong ∧ (cascadeForSource Causation.Psych.CausalSource.internal).causStrength = Minimalist.CausStrength.strong

CAUS strength is uniform across Class II: both eventive (external source) and stative (internal source) cascades derive strong CAUS.

The HMC predicts that BOTH Target (at) and Subject Matter (about) block CAUS movement equally, because both are nonaffixal P heads. This symmetric prediction is internal to [Pes95]'s account — both stimulus subtypes produce the same HMC configuration.

The bridge to semantic accounts of the T/SM restriction (which may
make asymmetric predictions) is in `Kim2024_UPH.lean`. 

theorem Pesetsky1995.symmetric_blocking : Minimalist.headAt.affixal = false ∧ Minimalist.headAbout.affixal = false

Both at and about are nonaffixal: both block CAUS movement through the cascade spine equally.

theorem Pesetsky1995.hmc_predicts_tsm_data : Minimalist.canReachV cascadeCausePlusStimulus.spine 2 = false ∧ ((List.filter (fun (d : PsychVerbs.TSMRestriction) => d.causePresent && d.smPresent) PsychVerbs.tsmData).all fun (x : PsychVerbs.TSMRestriction) => !x.wellFormed) = true

The HMC prediction matches the empirical T/SM data: Cause + SM cooccurrence is ill-formed, as predicted by nonaffixal blocking.

theorem Pesetsky1995.caus_zero_morpheme : Minimalist.caus.isZero = true

CAUS is a zero morpheme (not phonologically realized).

theorem Pesetsky1995.caus_is_affixal : Minimalist.caus.affixal = true

CAUS is affixal (can incorporate into V).

theorem Pesetsky1995.vcause_not_caus : Minimalist.isAnticausative [Minimalist.VerbHead.vCAUSE, Minimalist.VerbHead.vGO, Minimalist.VerbHead.vBE] = true ∧ Minimalist.Cascade.terminal.hasHead "CAUS" = false

vCAUSE is present in anticausatives; CAUS is not.

The full argumentation chain for each Class II psych verb, derived from a single lexical field (causalSource in the Fragment):

```
Fragment: v.causalSource = some src
  → Cascade:  cascadeForSource src        (Target or SM cascade)
    → HMC:    headCanReachV "CAUS"        (CAUS can incorporate)
      → Stim: CausalSource.toStimulusType (Target or SubjectMatter)
        → Nat: isNaturalPredicate         (natural or arbitrary)
          → Str: Cascade.causStrength     (strong CAUS)
```

Each per-verb theorem is a single breakable unit: change any verb's
`causalSource` field in the Fragment and exactly one theorem fails.

[pesetsky-1995] Ch. 4 distinguishes **natural** predicates
(Target-selecting, PP *of*: "afraid OF dogs") from **arbitrary**
predicates (SM-selecting, PP *about*: "worried ABOUT the exam").
This is derived from the causal source: external → natural,
internal → arbitrary. 

def Pesetsky1995.isNaturalPredicate : Causation.Psych.StimulusType → Prop

Natural predicates select Target stimulus (PP of); arbitrary predicates select Subject Matter (PP about).

Equations

• Pesetsky1995.isNaturalPredicate Causation.Psych.StimulusType.target = True
• Pesetsky1995.isNaturalPredicate Causation.Psych.StimulusType.subjectMatter = False

@[implicit_reducible]

instance Pesetsky1995.instDecidablePredStimulusTypeIsNaturalPredicate : DecidablePred isNaturalPredicate

Equations

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

def Pesetsky1995.cascadeChain (v : English.Predicates.Verbal.VerbEntry) (src : Causation.Psych.CausalSource) : Prop

End-to-end cascade derivation chain for a Class II psych verb. From a verb's causalSource, derives: cascade assignment (via cascadeForSource), HMC reachability, stimulus type, natural/ arbitrary classification, and CAUS strength. All from one field.

Equations

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

theorem Pesetsky1995.annoy_chain : cascadeChain English.Predicates.Verbal.annoy Causation.Psych.CausalSource.external

theorem Pesetsky1995.frighten_chain : cascadeChain English.Predicates.Verbal.frighten Causation.Psych.CausalSource.external

theorem Pesetsky1995.amuse_chain : cascadeChain English.Predicates.Verbal.amuse Causation.Psych.CausalSource.external

theorem Pesetsky1995.fascinate_chain : cascadeChain English.Predicates.Verbal.fascinate Causation.Psych.CausalSource.external

theorem Pesetsky1995.irritate_chain : cascadeChain English.Predicates.Verbal.irritate Causation.Psych.CausalSource.external

theorem Pesetsky1995.bore_chain : cascadeChain English.Predicates.Verbal.bore Causation.Psych.CausalSource.external

theorem Pesetsky1995.charm_chain : cascadeChain English.Predicates.Verbal.charm Causation.Psych.CausalSource.external

theorem Pesetsky1995.impress_chain : cascadeChain English.Predicates.Verbal.impress Causation.Psych.CausalSource.external

theorem Pesetsky1995.surprise_chain : cascadeChain English.Predicates.Verbal.surprise Causation.Psych.CausalSource.external

theorem Pesetsky1995.scare_chain : cascadeChain English.Predicates.Verbal.scare Causation.Psych.CausalSource.external

theorem Pesetsky1995.delight_chain : cascadeChain English.Predicates.Verbal.delight Causation.Psych.CausalSource.external

theorem Pesetsky1995.embarrass_chain : cascadeChain English.Predicates.Verbal.embarrass Causation.Psych.CausalSource.external

theorem Pesetsky1995.upset_chain : cascadeChain English.Predicates.Verbal.upset_psych Causation.Psych.CausalSource.external

theorem Pesetsky1995.disgust_chain : cascadeChain English.Predicates.Verbal.disgust Causation.Psych.CausalSource.external

theorem Pesetsky1995.shock_chain : cascadeChain English.Predicates.Verbal.shock Causation.Psych.CausalSource.external

theorem Pesetsky1995.confuse_chain : cascadeChain English.Predicates.Verbal.confuse Causation.Psych.CausalSource.external

theorem Pesetsky1995.disappoint_chain : cascadeChain English.Predicates.Verbal.disappoint Causation.Psych.CausalSource.external

theorem Pesetsky1995.worry_ev_chain : cascadeChain English.Predicates.Verbal.worry_eventive Causation.Psych.CausalSource.external

theorem Pesetsky1995.concern_chain : cascadeChain English.Predicates.Verbal.concern Causation.Psych.CausalSource.internal

theorem Pesetsky1995.interest_chain : cascadeChain English.Predicates.Verbal.interest Causation.Psych.CausalSource.internal

theorem Pesetsky1995.worry_st_chain : cascadeChain English.Predicates.Verbal.worry_stative Causation.Psych.CausalSource.internal

theorem Pesetsky1995.please_chain : cascadeChain English.Predicates.Verbal.please_psych Causation.Psych.CausalSource.internal

theorem Pesetsky1995.trouble_chain : cascadeChain English.Predicates.Verbal.trouble Causation.Psych.CausalSource.internal

theorem Pesetsky1995.puzzle_chain : cascadeChain English.Predicates.Verbal.puzzle Causation.Psych.CausalSource.internal

[Pes95] Ch. 7 extends the Cascade Hypothesis to derive heavy NP shift (HNPS) from cascade geometry. Shifted phrases adjoin to cascade nodes; cascade depth determines how many potential landing sites exist for rightward-shifted heavy NPs.

The cascade-based HNPS account provides a *syntactic* mechanism for
weight effects: the verb's argument structure — determined by its
cascade complement — constrains where shifted phrases can land. This
predicts structural constraints on shift targets, not just statistical
preference for heavy-last ordering. 

theorem Pesetsky1995.psych_cascade_deeper_than_dative : cascadeTarget.shiftSites > cascadeDative.shiftSites

Psych verb cascades (depth 2) provide more shift sites than simple dative cascades (depth 1).

theorem Pesetsky1995.doc_same_depth_as_psych : cascadeDOC.shiftSites = cascadeTarget.shiftSites

The DOC cascade and psych verb cascades have equal depth.

theorem Pesetsky1995.terminal_no_shift_sites : Minimalist.Cascade.terminal.shiftSites = 0

Terminal cascades (intransitive verbs) provide no shift sites.

theorem Pesetsky1995.shift_site_hierarchy : Minimalist.Cascade.terminal.shiftSites < cascadeDative.shiftSites ∧ cascadeDative.shiftSites < cascadeTarget.shiftSites ∧ cascadeTarget.shiftSites < cascadeCausePlusStimulus.shiftSites

Cascade depth predicts a hierarchy of HNPS availability: intransitive (0) < simple dative (1) < psych/DOC (2) < extended (3).