Pollock (1989): Verb Movement, Universal Grammar, and the Structure of IP

This file formalizes Pollock's account of the placement of French and English verbs relative to negation, adverbs, floating quantifiers, and the subject. The clause is [TP T [NegP Neg [AgrP Agr [VP Adv V]]]], and a verb moves head to head: to Agr, the short movement that carries it past an adverb, and from Agr to T, the long movement that carries it past negation and lets it invert with the subject. A head that is opaque to θ-role assignment blocks the movement of a verb with θ-roles to assign, since the raised verb could no longer assign them, and only a verb with none, the auxiliaries be and have, may pass. English Agr is opaque and French Agr transparent; nonfinite T is opaque in both languages. Finite T is an operator that must bind a verb trace, so in a finite clause a verb rises as high as it can, and when it cannot rise at all the tense affix lowers onto it and do supports it under negation.

The heights a verb can reach are Reaches; from it follow the paper's generalizations: long movement passes through short movement, auxiliaries reach T in every clause, no lexical verb reaches nonfinite T in either language, lexical verbs move at all exactly in French, and do-support arises exactly in English finite clauses with a lexical verb (reaches_tense_imp_agr, auxiliary_reaches_tense, lexical_not_reaches_nonfinite_tense, lexical_reaches_agr_iff, needsDo_iff). The paradigm of examples (2) to (39), forty rows over finite and nonfinite clauses of both languages, is accounted for row by row: a row is excluded exactly when no admissible height puts the verb where the row puts it (paradigm).

Implementation notes

The θ-theoretic mechanism is represented by its effect, which head hosts which verb, not by θ-grids and chains; the ban on vacuous quantification likewise by the obligatoriness of the highest reachable position in finite clauses. Marginal rows are counted as admitted, as the paper treats their degradation as stylistic. The structure of TP with do, imperatives, gerunds, and the ECP account of why not alone blocks affix lowering are not formalized.

References

• [Pol89]

Heads, verbs, and reachability

inductive Pollock1989.Height : Type

A verb occupies its position in VP, Agr after short movement, or T after long movement.

• vp : Height
• agr : Height
• tense : Height

@[instance_reducible]

instance Pollock1989.instDecidableEqHeight : DecidableEq Height

Equations

• Pollock1989.instDecidableEqHeight x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Pollock1989.instReprHeight : Repr Height

Equations

• Pollock1989.instReprHeight = { reprPrec := Pollock1989.instReprHeight.repr }

def Pollock1989.instReprHeight.repr : Height → ℕ → Std.Format

Equations

• Pollock1989.instReprHeight.repr Pollock1989.Height.vp prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Pollock1989.Height.vp")).group prec✝
• Pollock1989.instReprHeight.repr Pollock1989.Height.agr prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Pollock1989.Height.agr")).group prec✝
• Pollock1989.instReprHeight.repr Pollock1989.Height.tense prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Pollock1989.Height.tense")).group prec✝

@[instance_reducible]

instance Pollock1989.instFintypeHeight : Fintype Height

Equations

• Pollock1989.instFintypeHeight = { elems := { val := ↑Pollock1989.Height.enumList, nodup := Pollock1989.Height.enumList_nodup }, complete := Pollock1989.instFintypeHeight._proof_1 }

def Pollock1989.Height.rank : Height → ℕ

Height as the number of heads climbed.

Equations

• Pollock1989.Height.vp.rank = 0
• Pollock1989.Height.agr.rank = 1
• Pollock1989.Height.tense.rank = 2

@[instance_reducible]

instance Pollock1989.instLinearOrderHeight : LinearOrder Height

Equations

• Pollock1989.instLinearOrderHeight = LinearOrder.lift' Pollock1989.Height.rank Pollock1989.instLinearOrderHeight._proof_1

inductive Pollock1989.Verb : Type

A verb with θ-roles to assign, or an auxiliary with none.

• lexical : Verb
• auxiliary : Verb

@[instance_reducible]

instance Pollock1989.instDecidableEqVerb : DecidableEq Verb

Equations

• Pollock1989.instDecidableEqVerb x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Pollock1989.instReprVerb : Repr Verb

Equations

• Pollock1989.instReprVerb = { reprPrec := Pollock1989.instReprVerb.repr }

def Pollock1989.instReprVerb.repr : Verb → ℕ → Std.Format

Equations

• Pollock1989.instReprVerb.repr Pollock1989.Verb.lexical prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Pollock1989.Verb.lexical")).group prec✝
• Pollock1989.instReprVerb.repr Pollock1989.Verb.auxiliary prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Pollock1989.Verb.auxiliary")).group prec✝

@[instance_reducible]

instance Pollock1989.instFintypeVerb : Fintype Verb

Equations

• Pollock1989.instFintypeVerb = { elems := { val := ↑Pollock1989.Verb.enumList, nodup := Pollock1989.Verb.enumList_nodup }, complete := Pollock1989.instFintypeVerb._proof_1 }

inductive Pollock1989.Language : Type

The two languages compared.

• french : Language
• english : Language

@[instance_reducible]

instance Pollock1989.instDecidableEqLanguage : DecidableEq Language

Equations

• Pollock1989.instDecidableEqLanguage x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Pollock1989.instReprLanguage : Repr Language

Equations

• Pollock1989.instReprLanguage = { reprPrec := Pollock1989.instReprLanguage.repr }

def Pollock1989.instReprLanguage.repr : Language → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Pollock1989.instFintypeLanguage : Fintype Language

Equations

• Pollock1989.instFintypeLanguage = { elems := { val := ↑Pollock1989.Language.enumList, nodup := Pollock1989.Language.enumList_nodup }, complete := Pollock1989.instFintypeLanguage._proof_1 }

structure Pollock1989.Clause : Type

A clause type is a language with the finiteness of its T.

• language : Language
• finite : Bool

def Pollock1989.instDecidableEqClause.decEq (x✝ x✝¹ : Clause) : Decidable (x✝ = x✝¹)

Equations

• Pollock1989.instDecidableEqClause.decEq { language := a, finite := a_1 } { language := b, finite := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

@[instance_reducible]

instance Pollock1989.instDecidableEqClause : DecidableEq Clause

Equations

• Pollock1989.instDecidableEqClause = Pollock1989.instDecidableEqClause.decEq

@[instance_reducible]

instance Pollock1989.instReprClause : Repr Clause

Equations

• Pollock1989.instReprClause = { reprPrec := Pollock1989.instReprClause.repr }

def Pollock1989.instReprClause.repr : Clause → ℕ → Std.Format

Equations

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

def Pollock1989.Clause.AgrOpaque (c : Clause) : Prop

English Agr is too poor morphologically to transmit θ-roles.

Equations

• c.AgrOpaque = (c.language = Pollock1989.Language.english)

def Pollock1989.Clause.TenseOpaque (c : Clause) : Prop

Nonfinite T is opaque to θ-role assignment in both languages.

Equations

• c.TenseOpaque = (c.finite = false)

def Pollock1989.Hosts (isOpaque : Prop) (v : Verb) : Prop

A head hosts a verb unless it is opaque and the verb has θ-roles to assign.

Equations

• Pollock1989.Hosts isOpaque v = (¬isOpaque ∨ v = Pollock1989.Verb.auxiliary)

def Pollock1989.Reaches (c : Clause) (v : Verb) : Height → Prop

A verb reaches the heights of a clause head by head, Agr if Agr hosts it and T if moreover T hosts it.

Equations

• Pollock1989.Reaches c v Pollock1989.Height.vp = True
• Pollock1989.Reaches c v Pollock1989.Height.agr = Pollock1989.Hosts c.AgrOpaque v
• Pollock1989.Reaches c v Pollock1989.Height.tense = (Pollock1989.Hosts c.AgrOpaque v ∧ Pollock1989.Hosts c.TenseOpaque v)

@[instance_reducible]

instance Pollock1989.instDecidablePredHeightReaches (c : Clause) (v : Verb) : DecidablePred (Reaches c v)

Equations

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

theorem Pollock1989.reaches_tense_imp_agr {c : Clause} {v : Verb} (h : Reaches c v Height.tense) : Reaches c v Height.agr

Long movement is short movement continued (the Head Movement Constraint).

theorem Pollock1989.reaches_of_le {c : Clause} {v : Verb} {h h' : Height} (hle : h' ≤ h) (hr : Reaches c v h) : Reaches c v h'

Reachability is downward closed.

theorem Pollock1989.auxiliary_reaches_tense (c : Clause) : Reaches c Verb.auxiliary Height.tense

Be and have reach T in every clause of both languages.

theorem Pollock1989.lexical_not_reaches_nonfinite_tense (l : Language) : ¬Reaches { language := l, finite := false } Verb.lexical Height.tense

No lexical verb reaches nonfinite T, in French as in English: the restriction is not an English idiosyncrasy.

theorem Pollock1989.lexical_reaches_agr_iff (c : Clause) : Reaches c Verb.lexical Height.agr ↔ c.language = Language.french

A lexical verb moves at all exactly in French: the lexical restrictions on short movement in infinitives and on long movement in finite clauses are the same restriction.

Finiteness and do-support

def Pollock1989.top (c : Clause) (v : Verb) : Height

The highest position a verb reaches.

Equations

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

def Pollock1989.Admits (c : Clause) (v : Verb) (h : Height) : Prop

A verb may surface only in its highest position in a finite clause, where T is an operator that must bind the verb's trace, and in any position it reaches in a nonfinite clause.

Equations

• Pollock1989.Admits c v h = if c.finite = true then h = Pollock1989.top c v else Pollock1989.Reaches c v h

@[instance_reducible]

instance Pollock1989.instDecidableAdmits (c : Clause) (v : Verb) (h : Height) : Decidable (Admits c v h)

Equations

• Pollock1989.instDecidableAdmits c v h = id inferInstance

def Pollock1989.NeedsDo (c : Clause) (v : Verb) : Prop

The tense affix must lower onto a verb that cannot rise at all, and do supports it when negation blocks the lowering.

Equations

• Pollock1989.NeedsDo c v = (c.finite = true ∧ Pollock1989.top c v = Pollock1989.Height.vp)

@[instance_reducible]

instance Pollock1989.instDecidableNeedsDo (c : Clause) (v : Verb) : Decidable (NeedsDo c v)

Equations

• Pollock1989.instDecidableNeedsDo c v = id inferInstance

theorem Pollock1989.needsDo_iff (c : Clause) (v : Verb) : NeedsDo c v ↔ c = { language := Language.english, finite := true } ∧ v = Verb.lexical

Do-support arises exactly in English finite clauses with a lexical verb.

The paradigm

inductive Pollock1989.Diagnostic : Type

The four diagnostics of the verb's position.

• negation : Diagnostic
• adverb : Diagnostic
• floatingQ : Diagnostic
• inversion : Diagnostic

@[instance_reducible]

instance Pollock1989.instDecidableEqDiagnostic : DecidableEq Diagnostic

Equations

• Pollock1989.instDecidableEqDiagnostic x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Pollock1989.instReprDiagnostic.repr : Diagnostic → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Pollock1989.instReprDiagnostic : Repr Diagnostic

Equations

• Pollock1989.instReprDiagnostic = { reprPrec := Pollock1989.instReprDiagnostic.repr }

@[instance_reducible]

instance Pollock1989.instFintypeDiagnostic : Fintype Diagnostic

Equations

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

def Pollock1989.precedes (h : Height) : Diagnostic → Bool

A verb precedes negation and the inverted subject from T, and an adverb or floating quantifier in the VP-initial position from Agr or T.

Equations

• Pollock1989.precedes h Pollock1989.Diagnostic.negation = decide (h = Pollock1989.Height.tense)
• Pollock1989.precedes h Pollock1989.Diagnostic.inversion = decide (h = Pollock1989.Height.tense)
• Pollock1989.precedes h Pollock1989.Diagnostic.adverb = decide (h ≠ Pollock1989.Height.vp)
• Pollock1989.precedes h Pollock1989.Diagnostic.floatingQ = decide (h ≠ Pollock1989.Height.vp)

theorem Pollock1989.precedes_adverb_floatingQ (h : Height) : precedes h Diagnostic.adverb = precedes h Diagnostic.floatingQ ∧ precedes h Diagnostic.negation = precedes h Diagnostic.inversion

The adverb and floating-quantifier diagnostics agree at every height, and negation and inversion agree at every height.

def Pollock1989.interpret (r : Datum) : Option (Clause × Verb × Diagnostic × Bool)

A row's clause type, verb, diagnostic, and attested order, read from its features.

Equations

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

def Pollock1989.Predicted (r : Datum) : Prop

A row is predicted when it is excluded exactly where no admitted height puts the verb on the attested side of the diagnostic element.

Equations

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

@[instance_reducible]

instance Pollock1989.instDecidablePredicted (r : Datum) : Decidable (Predicted r)

Equations

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

theorem Pollock1989.paradigm (r : Datum) : r ∈ Examples.all → Predicted r

Every row of the paradigm (2) to (39) is predicted.