Verb Movement Parameter

@cite{chomsky-1995} @cite{pollock-1989}

@cite{pollock-1989} established that languages differ parametrically in whether lexical verbs raise to T (Inflection). French lexical verbs obligatorily raise past negation, adverbs, and floating quantifiers; English lexical verbs remain in situ. English auxiliaries, however, do raise — patterning with French lexical verbs rather than English lexical verbs.

This asymmetry explains do-support: when T must be realized high (in C for questions, above negation) but the lexical verb cannot raise, a dummy 'do' is inserted to host tense features.

The Four Diagnostics

Pollock identifies four positions that diagnose V-raising:

1. Negation: V > Neg (French) vs. *V > Neg (English)
2. Adverbs: V > Adv (French) vs. *V > Adv (English)
3. Floating quantifiers: V > FQ (French) vs. *V > FQ (English)
4. Subject inversion: V-Subj (French) vs. *V-Subj (English lexical V)

All four converge: a language either raises V past all four, or past none.

inductive Minimalism.VMovementParam : Type

The verb movement parameter: does V raise to T?

• raises : VMovementParam

  V raises to T (French lexical verbs, English auxiliaries)

• inSitu : VMovementParam

  V stays in situ below T (English lexical verbs)

instance Minimalism.instDecidableEqVMovementParam : DecidableEq VMovementParam

Equations

• Minimalism.instDecidableEqVMovementParam x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Minimalism.instReprVMovementParam : Repr VMovementParam

Equations

• Minimalism.instReprVMovementParam = { reprPrec := Minimalism.instReprVMovementParam.repr }

def Minimalism.instReprVMovementParam.repr : VMovementParam → ℕ → Std.Format

Equations

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

def Minimalism.instBEqVMovementParam.beq : VMovementParam → VMovementParam → Bool

Equations

• Minimalism.instBEqVMovementParam.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Minimalism.instBEqVMovementParam : BEq VMovementParam

Equations

• Minimalism.instBEqVMovementParam = { beq := Minimalism.instBEqVMovementParam.beq }

inductive Minimalism.VDiagnostic : Type

Pollock's four diagnostics for verb position relative to T.

• negation : VDiagnostic

  Does V precede sentential negation?

• adverb : VDiagnostic

  Does V precede VP-adverbs (e.g., 'often', 'souvent')?

• floatingQ : VDiagnostic

  Does V precede floating quantifiers (e.g., 'all', 'tous')?

• inversion : VDiagnostic

  Can V invert with the subject (V-to-C via T)?

instance Minimalism.instDecidableEqVDiagnostic : DecidableEq VDiagnostic

Equations

• Minimalism.instDecidableEqVDiagnostic x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Minimalism.instReprVDiagnostic.repr : VDiagnostic → ℕ → Std.Format

Equations

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

instance Minimalism.instReprVDiagnostic : Repr VDiagnostic

Equations

• Minimalism.instReprVDiagnostic = { reprPrec := Minimalism.instReprVDiagnostic.repr }

instance Minimalism.instBEqVDiagnostic : BEq VDiagnostic

Equations

• Minimalism.instBEqVDiagnostic = { beq := Minimalism.instBEqVDiagnostic.beq }

def Minimalism.instBEqVDiagnostic.beq : VDiagnostic → VDiagnostic → Bool

Equations

• Minimalism.instBEqVDiagnostic.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Minimalism.instInhabitedVDiagnostic : Inhabited VDiagnostic

Equations

• Minimalism.instInhabitedVDiagnostic = { default := Minimalism.instInhabitedVDiagnostic.default }

def Minimalism.instInhabitedVDiagnostic.default : VDiagnostic

Equations

• Minimalism.instInhabitedVDiagnostic.default = Minimalism.VDiagnostic.negation

def Minimalism.verbPrecedesDiagnostic (p : VMovementParam) : VDiagnostic → Bool

Prediction: does V precede the diagnostic position?

If V raises to T, it precedes all four diagnostic positions (negation, adverbs, floating quantifiers, and can reach C for inversion). If V stays in situ, it follows all four.

Equations

• Minimalism.verbPrecedesDiagnostic Minimalism.VMovementParam.raises x✝ = true
• Minimalism.verbPrecedesDiagnostic Minimalism.VMovementParam.inSitu x✝ = false

inductive Minimalism.TenseSupportContext : Type

Contexts where tense features need overt support in T/C position.

When V cannot raise to T (English lexical verbs), these contexts require do-insertion because tense must be realized above VP.

• negation : TenseSupportContext

  Sentential negation: "Sue does not eat fish"

• question : TenseSupportContext

  Questions (SAI requires T-to-C): "Does she eat fish?"

• verumFocus : TenseSupportContext

  Verum focus (stressed T): "She DOES eat fish"

• tagQuestion : TenseSupportContext

  Tag questions: "She likes him, doesn't she?"

• vpEllipsis : TenseSupportContext

  VP ellipsis (stranded T): "She runs faster than he does"

instance Minimalism.instDecidableEqTenseSupportContext : DecidableEq TenseSupportContext

Equations

• Minimalism.instDecidableEqTenseSupportContext x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Minimalism.instReprTenseSupportContext.repr : TenseSupportContext → ℕ → Std.Format

Equations

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

instance Minimalism.instReprTenseSupportContext : Repr TenseSupportContext

Equations

• Minimalism.instReprTenseSupportContext = { reprPrec := Minimalism.instReprTenseSupportContext.repr }

def Minimalism.instBEqTenseSupportContext.beq : TenseSupportContext → TenseSupportContext → Bool

Equations

• Minimalism.instBEqTenseSupportContext.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Minimalism.instBEqTenseSupportContext : BEq TenseSupportContext

Equations

• Minimalism.instBEqTenseSupportContext = { beq := Minimalism.instBEqTenseSupportContext.beq }

instance Minimalism.instInhabitedTenseSupportContext : Inhabited TenseSupportContext

Equations

• Minimalism.instInhabitedTenseSupportContext = { default := Minimalism.instInhabitedTenseSupportContext.default }

def Minimalism.instInhabitedTenseSupportContext.default : TenseSupportContext

Equations

• Minimalism.instInhabitedTenseSupportContext.default = Minimalism.TenseSupportContext.negation

def Minimalism.needsDoSupport (p : VMovementParam) : TenseSupportContext → Bool

Does this parameter setting require do-support in the given context?

Do-support is needed exactly when V is in situ: T cannot lower to V (blocked by the intervening material), so a dummy 'do' hosts tense.

Equations

• Minimalism.needsDoSupport Minimalism.VMovementParam.raises x✝ = false
• Minimalism.needsDoSupport Minimalism.VMovementParam.inSitu x✝ = true

def Minimalism.french : VMovementParam

French lexical verbs raise to T.

Equations

• Minimalism.french = Minimalism.VMovementParam.raises

def Minimalism.englishLexical : VMovementParam

English lexical verbs stay in situ.

Equations

• Minimalism.englishLexical = Minimalism.VMovementParam.inSitu

def Minimalism.englishAux : VMovementParam

English auxiliaries raise to T — patterning with French, not with English lexical verbs. This is Pollock's key observation.

Equations

• Minimalism.englishAux = Minimalism.VMovementParam.raises

theorem Minimalism.raises_verb_precedes_all (d : VDiagnostic) : verbPrecedesDiagnostic VMovementParam.raises d = true

V-raising languages: V precedes all four diagnostic positions.

theorem Minimalism.inSitu_verb_follows_all (d : VDiagnostic) : verbPrecedesDiagnostic VMovementParam.inSitu d = false

V-in-situ languages: V follows all four diagnostic positions.

theorem Minimalism.english_aux_patterns_with_french : englishAux = french

English auxiliaries have the same movement parameter as French lexical verbs. This is Pollock's central observation: the aux/lexical split in English mirrors the English/French split.

theorem Minimalism.raises_never_needs_do (ctx : TenseSupportContext) : needsDoSupport VMovementParam.raises ctx = false

V-raising languages never need do-support.

theorem Minimalism.inSitu_always_needs_do (ctx : TenseSupportContext) : needsDoSupport VMovementParam.inSitu ctx = true

V-in-situ languages always need do-support.

theorem Minimalism.diagnostics_converge (p : VMovementParam) (d₁ d₂ : VDiagnostic) : verbPrecedesDiagnostic p d₁ = verbPrecedesDiagnostic p d₂

All four diagnostics converge for any parameter setting: they either all return true (raises) or all return false (inSitu).

theorem Minimalism.doSupport_anticorrelates_raising (p : VMovementParam) (ctx : TenseSupportContext) : needsDoSupport p ctx = !verbPrecedesDiagnostic p VDiagnostic.negation

Do-support and verb raising are perfectly anticorrelated: do-support is needed iff V does not precede negation.