Psych Verb Data (@cite{belletti-rizzi-1988}, @cite{kim-2024})

@cite{belletti-rizzi-1988} @cite{kim-2024}

Theory-neutral empirical data on psych verbs from @cite{belletti-rizzi-1988} and @cite{kim-2024}.

@cite{belletti-rizzi-1988} classification

Class	Subject	Object	Example
I	experiencer	theme	"Mary enjoys jazz" / It. temere
II	stimulus/cause	experiencer	"Jazz interests Mary" / It. preoccupare
III	(dative experiencer)		It. "A Gianni piace la musica"

B&R syntactic diagnostics (§§1–2)

The Class I/II split is diagnosed by five syntactic tests:

1. Anaphoric cliticization (§1.1): Class II allows partitive ne from subject; Class I does not
2. Arbitrary pro (§1.2): Class I allows arb pro subject; Class II does not
3. Causative fare (§1.3): Class I embeds under fare infinitive; Class II does not (but see caveat: preoccupare-class verbs embed under fare due to independent unaccusative representation, B&R ex. 37)
4. Backward binding (§2.1): Class II allows object-to-subject binding; Class I does not
5. Passive type (§1.5): Class II passive is adjectival; Class I is verbal

@cite{kim-2024} diagnostics

Kim extends B&R with two further diagnostics on the within-Class II split: 5. Intensionality (Ch. 4): Stative Class II verbs create intensional subject positions; eventive Class II verbs do not 6. T/SM restriction (Ch. 5): Cause and Subject Matter cannot cooccur

inductive Phenomena.PsychVerbs.Data.PsychVerbClass : Type

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

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

instance Phenomena.PsychVerbs.Data.instDecidableEqPsychVerbClass : DecidableEq PsychVerbClass

Equations

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

def Phenomena.PsychVerbs.Data.instReprPsychVerbClass.repr : PsychVerbClass → Nat → Std.Format

Equations

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

instance Phenomena.PsychVerbs.Data.instReprPsychVerbClass : Repr PsychVerbClass

Equations

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

def Phenomena.PsychVerbs.Data.instBEqPsychVerbClass.beq : PsychVerbClass → PsychVerbClass → Bool

Equations

• Phenomena.PsychVerbs.Data.instBEqPsychVerbClass.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.PsychVerbs.Data.instBEqPsychVerbClass : BEq PsychVerbClass

Equations

• Phenomena.PsychVerbs.Data.instBEqPsychVerbClass = { beq := Phenomena.PsychVerbs.Data.instBEqPsychVerbClass.beq }

inductive Phenomena.PsychVerbs.Data.ClassIIReading : Type

Aspectual reading of a Class II psych verb.

• eventive : ClassIIReading
• stative : ClassIIReading

instance Phenomena.PsychVerbs.Data.instDecidableEqClassIIReading : DecidableEq ClassIIReading

Equations

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

instance Phenomena.PsychVerbs.Data.instReprClassIIReading : Repr ClassIIReading

Equations

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

def Phenomena.PsychVerbs.Data.instReprClassIIReading.repr : ClassIIReading → Nat → Std.Format

Equations

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

instance Phenomena.PsychVerbs.Data.instBEqClassIIReading : BEq ClassIIReading

Equations

• Phenomena.PsychVerbs.Data.instBEqClassIIReading = { beq := Phenomena.PsychVerbs.Data.instBEqClassIIReading.beq }

def Phenomena.PsychVerbs.Data.instBEqClassIIReading.beq : ClassIIReading → ClassIIReading → Bool

Equations

• Phenomena.PsychVerbs.Data.instBEqClassIIReading.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

inductive Phenomena.PsychVerbs.Data.BRDiagnostic : Type

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

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

instance Phenomena.PsychVerbs.Data.instDecidableEqBRDiagnostic : DecidableEq BRDiagnostic

Equations

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

instance Phenomena.PsychVerbs.Data.instReprBRDiagnostic : Repr BRDiagnostic

Equations

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

def Phenomena.PsychVerbs.Data.instReprBRDiagnostic.repr : BRDiagnostic → Nat → Std.Format

Equations

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

instance Phenomena.PsychVerbs.Data.instBEqBRDiagnostic : BEq BRDiagnostic

Equations

• Phenomena.PsychVerbs.Data.instBEqBRDiagnostic = { beq := Phenomena.PsychVerbs.Data.instBEqBRDiagnostic.beq }

def Phenomena.PsychVerbs.Data.instBEqBRDiagnostic.beq : BRDiagnostic → BRDiagnostic → Bool

Equations

• Phenomena.PsychVerbs.Data.instBEqBRDiagnostic.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

structure Phenomena.PsychVerbs.Data.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

instance Phenomena.PsychVerbs.Data.instReprBRDiagnosticResult : Repr BRDiagnosticResult

Equations

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

def Phenomena.PsychVerbs.Data.instReprBRDiagnosticResult.repr : BRDiagnosticResult → Nat → Std.Format

Equations

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

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

Equations

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

instance Phenomena.PsychVerbs.Data.instBEqBRDiagnosticResult : BEq BRDiagnosticResult

Equations

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

def Phenomena.PsychVerbs.Data.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.Data.br_diagnostics_discriminate : (brDiagnosticData.all fun (d : BRDiagnosticResult) => d.classI != d.classII) = true

Every B&R diagnostic discriminates Class I from Class II: the two classes never give the same result on any test.

theorem Phenomena.PsychVerbs.Data.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.Data.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: passes ne-cliticization, backward binding, and adjectival passive; fails arb-pro and causative-fare.

inductive Phenomena.PsychVerbs.Data.SubjectRole : Type

The Class I/II distinction is characterized by theta-role reversal: Class I maps experiencer to subject, Class II maps experiencer to object.

Position	Class I	Class II
Subject	experiencer	stimulus
Object	stimulus/theme	experiencer

• experiencer : SubjectRole
• stimulus : SubjectRole

instance Phenomena.PsychVerbs.Data.instDecidableEqSubjectRole : DecidableEq SubjectRole

Equations

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

def Phenomena.PsychVerbs.Data.instReprSubjectRole.repr : SubjectRole → Nat → Std.Format

Equations

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

instance Phenomena.PsychVerbs.Data.instReprSubjectRole : Repr SubjectRole

Equations

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

instance Phenomena.PsychVerbs.Data.instBEqSubjectRole : BEq SubjectRole

Equations

• Phenomena.PsychVerbs.Data.instBEqSubjectRole = { beq := Phenomena.PsychVerbs.Data.instBEqSubjectRole.beq }

def Phenomena.PsychVerbs.Data.instBEqSubjectRole.beq : SubjectRole → SubjectRole → Bool

Equations

• Phenomena.PsychVerbs.Data.instBEqSubjectRole.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

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

Map from B&R class to expected subject role.

Equations

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

structure Phenomena.PsychVerbs.Data.IntensionalityDatum : Type

Intensionality datum: does substitution of co-referential terms fail in subject position?

• Stative "concern": "Cicero concerns Mary" ≠ "Tully concerns Mary" (can differ in truth value — substitution fails)
• Eventive "frighten": "Cicero frightened Mary" = "Tully frightened Mary" (same truth value — substitution succeeds)

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

instance Phenomena.PsychVerbs.Data.instReprIntensionalityDatum : Repr IntensionalityDatum

Equations

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

def Phenomena.PsychVerbs.Data.instReprIntensionalityDatum.repr : IntensionalityDatum → Nat → Std.Format

Equations

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

instance Phenomena.PsychVerbs.Data.instBEqIntensionalityDatum : BEq IntensionalityDatum

Equations

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

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

Equations

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

def Phenomena.PsychVerbs.Data.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.Data.TSMRestriction : Type

The T/SM restriction: Cause and Subject Matter cannot cooccur.

*"The noise about the deadline concerned John" — both "the noise" (Cause) and "about the deadline" (SM) present → ill-formed.

This follows from the Onset Condition: both map to the onset position of the causal chain, but only one slot is available.

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

def Phenomena.PsychVerbs.Data.instReprTSMRestriction.repr : TSMRestriction → Nat → Std.Format

Equations

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

instance Phenomena.PsychVerbs.Data.instReprTSMRestriction : Repr TSMRestriction

Equations

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

instance Phenomena.PsychVerbs.Data.instBEqTSMRestriction : BEq TSMRestriction

Equations

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

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

Equations

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

def Phenomena.PsychVerbs.Data.tsmData : List TSMRestriction

Cause and SM cannot cooccur.

Equations

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

theorem Phenomena.PsychVerbs.Data.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.Data.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.Data.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.