Pollock's Verb Movement Diagnostics

[Pol89]

Connects the Minimalist verb movement parameter (Syntax/Minimalist/VerbMovementParameter.lean) to Pollock's French/English diagnostic paradigm (Data/Examples/Pollock1989.json).

Main declarations

• paramOf, diagOf: adapters reading a row's language and paperFeatures into VMovementParam and VDiagnostic
• acceptable_iff_order_predicted: a row is acceptable iff the theory's predicted V/diagnostic order matches the row's attested surface order
• all_diagnostics_converge: all four diagnostics agree for any parameter setting
• doSupport_iff_no_raising: do-support anticorrelates with V-raising

def Pollock1989.paramOf (row : Data.Examples.LinguisticExample) : Option Minimalist.VMovementParam

Movement-parameter adapter: French lexical verbs raise, English lexical verbs stay in situ, English auxiliaries raise.

Equations

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

def Pollock1989.diagOf (row : Data.Examples.LinguisticExample) : Option Minimalist.VDiagnostic

Diagnostic adapter: the row's diagnostic feature as a VDiagnostic.

Equations

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

def Pollock1989.predictedOrder (row : Data.Examples.LinguisticExample) : Option Bool

The theory's predicted surface order: does the verb precede the diagnostic element?

Equations

• Pollock1989.predictedOrder row = do let __do_lift ← Pollock1989.paramOf row let __do_lift_1 ← Pollock1989.diagOf row pure (Minimalist.verbPrecedesDiagnostic __do_lift __do_lift_1)

def Pollock1989.surfaceOrder (row : Data.Examples.LinguisticExample) : Option Bool

The attested surface order recorded in the row's v_precedes_diagnostic feature.

Equations

• Pollock1989.surfaceOrder row = Option.map (fun (x : String) => x == "true") (row.feature? "v_precedes_diagnostic")

theorem Pollock1989.acceptable_iff_order_predicted (row : Data.Examples.LinguisticExample) : row ∈ Examples.all → (row.judgment = Features.Judgment.acceptable ↔ predictedOrder row = surfaceOrder row)

Transfer equation: a Pollock row is acceptable iff the verb movement parameter predicts exactly the attested surface order. The marginal row (ex_p12, "John often has eaten pizza") sits on the not-acceptable side: the auxiliary should raise, so the Adv > Aux order mismatches the prediction.

All four diagnostics agree for any parameter setting. This is the core of Pollock's argument: the four tests are not independent observations but consequences of a single parameter (V-raises vs. V-in-situ).

theorem Pollock1989.all_diagnostics_converge (p : Minimalist.VMovementParam) (d₁ d₂ : Minimalist.VDiagnostic) : Minimalist.verbPrecedesDiagnostic p d₁ = Minimalist.verbPrecedesDiagnostic p d₂

For any parameter setting, all four diagnostics give the same answer.

Do-support and verb raising are complementary: a parameter setting that raises V never needs do-support, and a setting that keeps V in situ always needs it. This follows from the theory: do-support exists because V cannot raise.

theorem Pollock1989.doSupport_iff_no_raising (p : Minimalist.VMovementParam) (ctx : Minimalist.TenseSupportContext) : Minimalist.needsDoSupport p ctx = !Minimalist.verbPrecedesDiagnostic p Minimalist.VDiagnostic.negation

Do-support is needed iff V does not raise past negation.