Zero Syntax: Experiencers and Cascades

@cite{pesetsky-1995}

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

inductive Phenomena.PsychVerbs.PsychVerbClass : Type

@cite{belletti-rizzi-1988} classification of psych verbs.

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

@[implicit_reducible]

instance Phenomena.PsychVerbs.instDecidableEqPsychVerbClass : DecidableEq PsychVerbClass

Equations

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

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

Equations

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

@[implicit_reducible]

instance Phenomena.PsychVerbs.instReprPsychVerbClass : Repr PsychVerbClass

Equations

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

inductive Phenomena.PsychVerbs.ClassIIReading : Type

Aspectual reading of a Class II psych verb.

• eventive : ClassIIReading
• stative : ClassIIReading

@[implicit_reducible]

instance Phenomena.PsychVerbs.instDecidableEqClassIIReading : DecidableEq ClassIIReading

Equations

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

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

Equations

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

@[implicit_reducible]

instance Phenomena.PsychVerbs.instReprClassIIReading : Repr ClassIIReading

Equations

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

inductive Phenomena.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 Phenomena.PsychVerbs.instDecidableEqBRDiagnostic : DecidableEq BRDiagnostic

Equations

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

@[implicit_reducible]

instance Phenomena.PsychVerbs.instReprBRDiagnostic : Repr BRDiagnostic

Equations

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

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

Equations

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

structure Phenomena.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 Phenomena.PsychVerbs.instReprBRDiagnosticResult : Repr BRDiagnosticResult

Equations

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

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

Equations

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

@[implicit_reducible]

instance Phenomena.PsychVerbs.instBEqBRDiagnosticResult : BEq BRDiagnosticResult

Equations

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

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

Equations

• Phenomena.PsychVerbs.instBEqBRDiagnosticResult.beq { diagnostic := a, classI := a_1, classII := a_2 } { diagnostic := b, classI := b_1, classII := b_2 } = (a == b && (a_1 == b_1 && a_2 == b_2))
• Phenomena.PsychVerbs.instBEqBRDiagnosticResult.beq x✝¹ x✝ = false

def Phenomena.PsychVerbs.brDiagnosticData : List BRDiagnosticResult

@cite{belletti-rizzi-1988} 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 Phenomena.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 Phenomena.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 Phenomena.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 Phenomena.PsychVerbs.SubjectRole : Type

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

• experiencer : SubjectRole
• stimulus : SubjectRole

@[implicit_reducible]

instance Phenomena.PsychVerbs.instDecidableEqSubjectRole : DecidableEq SubjectRole

Equations

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

@[implicit_reducible]

instance Phenomena.PsychVerbs.instReprSubjectRole : Repr SubjectRole

Equations

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

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

Equations

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

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

Map from B&R class to expected subject role.

Equations

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

structure Phenomena.PsychVerbs.IntensionalityDatum : Type

Intensionality datum (@cite{kim-2024} Ch. 4): does substitution of co-referential terms fail in subject position?

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

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

Equations

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

@[implicit_reducible]

instance Phenomena.PsychVerbs.instReprIntensionalityDatum : Repr IntensionalityDatum

Equations

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

@[implicit_reducible]

instance Phenomena.PsychVerbs.instBEqIntensionalityDatum : BEq IntensionalityDatum

Equations

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

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

Equations

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

def Phenomena.PsychVerbs.intensionalityData : List IntensionalityDatum

Empirical intensionality data from @cite{kim-2024}.

Equations

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

structure Phenomena.PsychVerbs.TSMRestriction : Type

The T/SM restriction (@cite{kim-2024} Ch. 5): Cause and Subject Matter cannot cooccur.

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

@[implicit_reducible]

instance Phenomena.PsychVerbs.instReprTSMRestriction : Repr TSMRestriction

Equations

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

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

Equations

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

@[implicit_reducible]

instance Phenomena.PsychVerbs.instBEqTSMRestriction : BEq TSMRestriction

Equations

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

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

Equations

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

def Phenomena.PsychVerbs.tsmData : List TSMRestriction

Cause and SM cannot cooccur.

Equations

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

theorem Phenomena.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 Phenomena.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 Phenomena.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 : Semantics.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 Semantics.Causation.Psych.CausalSource.external = Pesetsky1995.cascadeTarget
• Pesetsky1995.cascadeForSource Semantics.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 Semantics.Causation.Psych.CausalSource.external).hasHead "at" = true ∧ (cascadeForSource Semantics.Causation.Psych.CausalSource.external).hasHead "about" = false ∧ (cascadeForSource Semantics.Causation.Psych.CausalSource.internal).hasHead "about" = true ∧ (cascadeForSource Semantics.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 : Phenomena.PsychVerbs.BRDiagnosticResult) => x.diagnostic == Phenomena.PsychVerbs.BRDiagnostic.backwardBinding) Phenomena.PsychVerbs.brDiagnosticData).all fun (x : Phenomena.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 Semantics.Causation.Psych.CausalSource.external).causStrength = Minimalist.CausStrength.strong ∧ (cascadeForSource Semantics.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 @cite{pesetsky-1995}'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 : Phenomena.PsychVerbs.TSMRestriction) => d.causePresent && d.smPresent) Phenomena.PsychVerbs.tsmData).all fun (x : Phenomena.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.

@cite{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 : Semantics.Causation.Psych.StimulusType → Prop

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

Equations

• Pesetsky1995.isNaturalPredicate Semantics.Causation.Psych.StimulusType.target = True
• Pesetsky1995.isNaturalPredicate Semantics.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 : Fragments.English.Predicates.Verbal.VerbEntry) (src : Semantics.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 Fragments.English.Predicates.Verbal.annoy Semantics.Causation.Psych.CausalSource.external

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

@cite{pesetsky-1995} 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).