Head Movement in Bulgarian LHM and Germanic V2

[HG19]

Connects the Minimalist analysis of head movement to empirical verb position data.

Bulgarian Long Head Movement

[Lam04] (cited in [HG19] examples (29), (48), (52)): both word orders are grammatical with the same meaning.

Order A (participle before auxiliary): Pročeli bjaha studentite statijata. read be.3p.pst the.students the.article 'The students had read the article.'

Order B (auxiliary before participle): Studentite bjaha pročeli statijata. the.students be.3p.pst read the.article 'The students had read the article.'

Germanic V2

• models_root_v2: German root declaratives are V2 (consistent with V-to-C)
• models_embedded_verb_final: German embedded clauses are verb-final

Disputed: V-to-I in German embedded clauses

[HG19] (§5.1.2) and [Wes09] (Table 3.1) make incompatible claims about whether the finite verb raises to I/T/Fin in German embedded finite clauses.

• [HG19], with [Hai10] as the strongest contemporary German-internal anchor: V does NOT raise to T in embedded non-V2 clauses — it "stays below adverbs/negation." The only V-movement step in German is the V-to-C step in matrix V2 contexts. (Quoted in GermanicV2.lean.)
• [Wes09]: German is +Fin° in Table 3.1. Combined with OV base order, +Fin° derives the verb-final embedded surface order via raising to Fin (rather than via the verb staying in V).

The empirical diagnostic — [Rob93]'s V-to-I diagnostic kit — is the position of the embedded finite verb relative to sentence adverbs (e.g. oft, wahrscheinlich) and negation. Both analyses derive verb-final surface order; they disagree about whether V crosses I on the way there. The codebase records Westergaard's positive claim via German.german's .Fin membership; [HG19]'s denial lives in prose ("no V-to-I" is not a positive Lean witness), but the contradiction with Westergaard is formalized as a refutation theorem below via the westergaardToMovementParam projection.

theorem HarizanovGribanova2019.models_root_v2 : Westergaard2009.de_decl.v2Status = Westergaard2009.V2Status.obligatory

German root declaratives are V2 — consistent with V-to-C head movement.

theorem HarizanovGribanova2019.models_embedded_verb_final : Westergaard2009.de_emb.v2Status = Westergaard2009.V2Status.impossible

German embedded clauses are verb-final — no V-to-C in the presence of an overt complementizer.

theorem HarizanovGribanova2019.root_sentence : Westergaard2009.de_decl.sentence = "Diesen Film haben die Kinder gesehen"

The root-clause sentence from [Vik95].

theorem HarizanovGribanova2019.westergaard_german_plus_fin : Minimalist.ForceHead.Fin ∈ German.german

[Wes09]'s positive claim: German embedded clauses have V-to-I (= +Fin°). [HG19] disputes this analytically (no V-to-I; verb stays in V). Re-exported from Westergaard2009.fin_only_german so this file's H&G-vs-Westergaard section has the witness in scope; the actual decide lives in Westergaard2009. The H&G "no V-to-I" denial is encoded as a refutation theorem below via the westergaardToMovementParam projection.

def HarizanovGribanova2019.westergaardToMovementParam (p : Minimalist.V2Profile) [Decidable (Minimalist.ForceHead.Fin ∈ p)] : Minimalist.VMovementParam

Project [Wes09]'s V2 micro-parameter profile into [Pol89]'s V-movement parameter: the +Fin° micro-parameter (V-to-Fin / V-to-I) in the V2 profile corresponds to .raises in VMovementParam; its absence corresponds to .inSitu. Lets the otherwise-incompatible Westergaard and H&G accounts contradict each other on a common Lean object.

Equations

• HarizanovGribanova2019.westergaardToMovementParam p = if Minimalist.ForceHead.Fin ∈ p then Minimalist.VMovementParam.raises else Minimalist.VMovementParam.inSitu

def HarizanovGribanova2019.germanHG : Minimalist.VMovementParam

[HG19]'s prediction for German embedded finite clauses: V stays in V — no V-to-I, no V-to-T.

Equations

• HarizanovGribanova2019.germanHG = Minimalist.VMovementParam.inSitu

theorem HarizanovGribanova2019.hg_westergaard_german_disagree : germanHG ≠ westergaardToMovementParam German.german

[HG19] predicts .inSitu for German embedded clauses; [Wes09]'s V2 profile, projected via westergaardToMovementParam, predicts .raises. The two frameworks make contradictory predictions about a single Lean object — formalizing the long-standing Vikner-vs.-Haider / Westergaard-vs.-H&G dispute about V-to-I in German.