Pesetsky (1995): Zero Syntax

This file formalizes the Cascade account in [Pes95] of the Target/Subject Matter restriction on object-experiencer verbs, the impossibility of expressing a Causer together with a Target or Subject Matter, the article annoyed Bill at the government. The verb's arguments sit in a right-branching Cascade of prepositional projections (Cascade), and the causative reading comes from a zero preposition CAUS, an adjunct-like head situated below the selected arguments, which is an affix and must have reached the verb by phonological form (510). Head movement is successive adjunction to each intervening preposition, and a category headed by a non-affix cannot move on, so CAUS reaches the verb exactly when every preposition above it is affixal (canReachV, canReachV_append). The prepositions at and about that introduce Target and Subject Matter are not affixes, so CAUS is stranded below them (tsm_restriction), whereas nothing intervenes when the stimulus is absent (caus_reaches_without_stimulus); the same mechanism derives Oehrle's observation that the causative reading of give survives in the double object construction, whose zero preposition G is an affix, but not with to (oehrle). Since CAUS starts below the selected arguments, the Causer originates below the Experiencer and raises to subject, which is why object-experiencer verbs show backward binding, the experiencer binding into the reconstructed causer (§6.2.2, experiencer_ccommands_causer). The verb classes of [BR88] from which the book's linking problem starts are recorded with the subject role each predicts (PsychVerbClass, SubjectRole).

Implementation notes

Only the prepositions of the restriction and of the double object alternation are represented. The affixal and prepositional occurrences of CAUS of §6.3, the suppression of the external argument in (522), the semantics of prepositions and mediated θ-selection of the fifth chapter, and the account of heavy shift of the seventh are not formalized.

References

• [Pes95]
• [BR88]

Cascades

structure Pesetsky1995.CascadeHead : Type

A prepositional head of a Cascade: whether it is overt or a zero morpheme, and whether it is an affix that must join the verb.

• overt : Bool
• affixal : Bool

@[instance_reducible]

instance Pesetsky1995.instDecidableEqCascadeHead : DecidableEq CascadeHead

Equations

• Pesetsky1995.instDecidableEqCascadeHead = Pesetsky1995.instDecidableEqCascadeHead.decEq

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

Equations

• Pesetsky1995.instDecidableEqCascadeHead.decEq { overt := a, affixal := a_1 } { overt := b, affixal := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

inductive Pesetsky1995.Phrase : Type

The phrases a Cascade positions.

• experiencer : Phrase
• target : Phrase
• subjectMatter : Phrase
• causer : Phrase
• theme : Phrase
• goal : Phrase

@[instance_reducible]

instance Pesetsky1995.instDecidableEqPhrase : DecidableEq Phrase

Equations

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

inductive Pesetsky1995.Cascade : Type

A Cascade: the right-branching spine of prepositional projections below a verb, each layer a head with the phrase in its specifier, ending in the complement of the lowest head.

• complement (phrase : Phrase) : Cascade
• layer (head : CascadeHead) (spec : Phrase) (rest : Cascade) : Cascade

def Pesetsky1995.Cascade.spine : Cascade → List CascadeHead

The heads from the verb downward.

Equations

• (Pesetsky1995.Cascade.complement phrase).spine = []
• (Pesetsky1995.Cascade.layer h spec rest).spine = h :: rest.spine

def Pesetsky1995.Cascade.position : Cascade → Phrase → Option ℕ

The position of a phrase, counted from the top, the final complement one below the last layer.

Equations

• (Pesetsky1995.Cascade.complement p).position x✝ = if p = x✝ then some 0 else none
• (Pesetsky1995.Cascade.layer head spec rest).position x✝ = if spec = x✝ then some 0 else Option.map (fun (x : ℕ) => x + 1) (rest.position x✝)

def Pesetsky1995.Cascade.CCommands (c : Cascade) (p q : Phrase) : Prop

A phrase c-commands another when it sits in a higher layer.

Equations

• c.CCommands p q = ∃ (i : ℕ), ∃ (j : ℕ), c.position p = some i ∧ c.position q = some j ∧ i < j

def Pesetsky1995.canReachV (spine : List CascadeHead) (i : ℕ) : Prop

The head at position i of a spine can reach the verb by successive adjunction exactly when every head above it is affixal: adjunction to a non-affix yields a category that cannot move on, the Head Movement Constraint.

Equations

• Pesetsky1995.canReachV spine i = ∀ (h : Pesetsky1995.CascadeHead), h ∈ List.take i spine → h.affixal = true

@[instance_reducible]

instance Pesetsky1995.instDecidableCanReachV (spine : List CascadeHead) (i : ℕ) : Decidable (canReachV spine i)

Equations

• Pesetsky1995.instDecidableCanReachV spine i = Pesetsky1995.instDecidableCanReachV._aux_1 spine i

theorem Pesetsky1995.canReachV_append (above : List CascadeHead) (h : CascadeHead) (below : List CascadeHead) : canReachV (above ++ h :: below) above.length ↔ ∀ (h' : CascadeHead), h' ∈ above → h'.affixal = true

A head below a given stretch of the spine reaches the verb iff that stretch is affixal throughout.

def Pesetsky1995.caus : CascadeHead

CAUS: the zero causative preposition, an affix (510).

Equations

• Pesetsky1995.caus = { overt := false, affixal := true }

def Pesetsky1995.headG : CascadeHead

G: the zero preposition of the double object construction, an affix.

Equations

• Pesetsky1995.headG = { overt := false, affixal := true }

def Pesetsky1995.headAt : CascadeHead

at, introducing a Target: overt and not an affix.

Equations

• Pesetsky1995.headAt = { overt := true, affixal := false }

def Pesetsky1995.headAbout : CascadeHead

about, introducing a Subject Matter: overt and not an affix.

Equations

• Pesetsky1995.headAbout = { overt := true, affixal := false }

def Pesetsky1995.headTo : CascadeHead

to of the dative construction: overt and not an affix.

Equations

• Pesetsky1995.headTo = { overt := true, affixal := false }

The Target/Subject Matter restriction (§6.2.1)

inductive Pesetsky1995.StimulusType : Type

The two roles into which the book divides the object of an emotion: the Target the emotion is directed at, as in angry at the government, and the Subject Matter it is about, as in worried about the television set.

• target : StimulusType
• subjectMatter : StimulusType

@[instance_reducible]

instance Pesetsky1995.instDecidableEqStimulusType : DecidableEq StimulusType

Equations

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

@[instance_reducible]

instance Pesetsky1995.instReprStimulusType : Repr StimulusType

Equations

• Pesetsky1995.instReprStimulusType = { reprPrec := Pesetsky1995.instReprStimulusType.repr }

def Pesetsky1995.instReprStimulusType.repr : StimulusType → ℕ → Std.Format

Equations

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

def Pesetsky1995.stimulusHead : StimulusType → CascadeHead

The preposition that introduces each stimulus type.

Equations

• Pesetsky1995.stimulusHead Pesetsky1995.StimulusType.target = Pesetsky1995.headAt
• Pesetsky1995.stimulusHead Pesetsky1995.StimulusType.subjectMatter = Pesetsky1995.headAbout

def Pesetsky1995.stimulusPhrase : StimulusType → Phrase

The phrase of each stimulus type.

Equations

• Pesetsky1995.stimulusPhrase Pesetsky1995.StimulusType.target = Pesetsky1995.Phrase.target
• Pesetsky1995.stimulusPhrase Pesetsky1995.StimulusType.subjectMatter = Pesetsky1995.Phrase.subjectMatter

def Pesetsky1995.stimulusCascade (s : StimulusType) : Cascade

(513): the Experiencer in the specifier of the stimulus preposition, the stimulus in the specifier of CAUS, and the Causer as CAUS's complement.

Equations

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

def Pesetsky1995.plainCascade : Cascade

(514): the Experiencer in the specifier of CAUS, with no stimulus.

Equations

• Pesetsky1995.plainCascade = Pesetsky1995.Cascade.layer Pesetsky1995.caus Pesetsky1995.Phrase.experiencer (Pesetsky1995.Cascade.complement Pesetsky1995.Phrase.causer)

theorem Pesetsky1995.stimulusHead_nonaffixal (s : StimulusType) : (stimulusHead s).affixal = false

Both stimulus prepositions are non-affixes, so Target and Subject Matter block alike.

theorem Pesetsky1995.tsm_restriction (s : StimulusType) : ¬canReachV (stimulusCascade s).spine 1

The restriction: with a Target or Subject Matter present, CAUS cannot reach the verb.

theorem Pesetsky1995.caus_reaches_without_stimulus : canReachV plainCascade.spine 0

Without a stimulus nothing intervenes and CAUS reaches the verb.

Oehrle's observation (§6.2.1)

def Pesetsky1995.doubleObjectCascade : Cascade

(511): the double object construction with a causative reading, G above CAUS.

Equations

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

def Pesetsky1995.toCascade : Cascade

(512): the to-dative with CAUS below to.

Equations

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

theorem Pesetsky1995.oehrle : canReachV doubleObjectCascade.spine 1 ∧ ¬canReachV toCascade.spine 1

The causative reading of give, the war years gave Mailer his first big success, survives in the double object construction, whose G is an affix, and not with to.

Backward binding (§6.2.2)

theorem Pesetsky1995.experiencer_ccommands_causer (s : StimulusType) : (stimulusCascade s).CCommands Phrase.experiencer Phrase.causer ∧ plainCascade.CCommands Phrase.experiencer Phrase.causer

The Experiencer c-commands the Causer's base position with or without a stimulus: the Causer is a derived subject, raised from below the Experiencer, and reconstructs there, so the Experiencer can bind into it.

The classes of Belletti and Rizzi

inductive Pesetsky1995.PsychVerbClass : Type

The classes of [BR88] from which the linking problem starts: experiencer-subject verbs, object-experiencer verbs, and the dative-experiencer verbs of Italian.

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

@[instance_reducible]

instance Pesetsky1995.instDecidableEqPsychVerbClass : DecidableEq PsychVerbClass

Equations

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

inductive Pesetsky1995.SubjectRole : Type

The role of the surface subject.

• experiencer : SubjectRole
• stimulus : SubjectRole

@[instance_reducible]

instance Pesetsky1995.instDecidableEqSubjectRole : DecidableEq SubjectRole

Equations

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

def Pesetsky1995.PsychVerbClass.expectedSubjectRole : PsychVerbClass → Option SubjectRole

The subject role each class predicts; the dative-experiencer class has no nominative subject among its two arguments.

Equations

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