Westergaard (2009): Micro-Cues, Information Structure, and Economy

@cite{westergaard-2009}

Marit Westergaard. The Acquisition of Word Order: Micro-Cues, Information Structure, and Economy. Linguistik Aktuell/Linguistics Today 145. John Benjamins, 2009.

Core Claim

V2 is not a single parameter. It decomposes into micro-parameters: one per clause-type head in a split-CP (ForceP) domain. Each micro-parameter is independently settable to + (verb movement to that head) or − (no verb movement). Different Germanic languages and dialects are characterized by different profiles of + and − across these heads.

The book distinguishes two levels:

• Micro-parameters (Table 3.1): settings in the adult grammar
• Micro-cues (Ch. 3 §4, Ch. 10 §3): observable input patterns that trigger each parameter setting in acquisition

Formalization

1. ForceHead: the seven clause-type heads (theory layer)
2. V2Profile: a function ForceHead → Bool (theory layer)
3. Language profiles: per-language Fragment files
4. MicroCue: syntactic templates from Ch. 3 §4
5. Bridge theorems to SAI data, V2 data, and GermanicV2
6. Information Structure: [±FOC] conditioning of "optional" V2

The Split-ForceP Model

@cite{westergaard-2009} splits @cite{rizzi-1997}'s ForceP into clause-type-specific projections. All seven heads are in the CP domain (above FinP). Crucially, the distinctions among Decl°, Int°, Pol°, Excl°, Imp° are finer than @cite{rizzi-1997}'s inventory — they are all "flavors of Force" that the existing Cat enum does not distinguish.

Fin° and Wh° do correspond to existing Cat heads (.Fin and .C respectively), but the five Force-level heads (Decl°, Int°, Pol°, Excl°, Imp°) are all at the Force level. Note: @cite{westergaard-2009}'s Pol° is a CP-domain head for yes/no-questions, NOT @cite{laka-1990}'s ΣP (which is Cat.Pol in linglib at F-value 2).

def V2Data.toProfile (d : V2Data) : Minimalism.V2Profile

Map theory-neutral V2 observations to's split-ForceP micro-parameter representation. The mapping:

• declV2 → Decl° (verb movement in declaratives)
• whQV2 → Int° (verb movement in wh-questions)
• ynQV2 → Pol° (verb movement in yes/no-questions)
• exclV2 → Excl° (verb movement in exclamatives)
• impV2 → Imp° (verb movement in imperatives)
• embFinV2 → Fin° (V-to-I in embedded finite clauses)
• embQV2 → Wh° (verb movement in embedded questions)

Equations

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

Shared types for describing V2 word order variation.

inductive Phenomena.WordOrder.Studies.Westergaard2009.ClauseType : Type

Clause types relevant to V2 variation.

• declarative : ClauseType
• whQuestion : ClauseType
• yesNoQuestion : ClauseType
• exclamative : ClauseType
• imperative : ClauseType
• embeddedDecl : ClauseType
• embeddedQuestion : ClauseType

instance Phenomena.WordOrder.Studies.Westergaard2009.instDecidableEqClauseType : DecidableEq ClauseType

Equations

• Phenomena.WordOrder.Studies.Westergaard2009.instDecidableEqClauseType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Phenomena.WordOrder.Studies.Westergaard2009.instReprClauseType : Repr ClauseType

Equations

• Phenomena.WordOrder.Studies.Westergaard2009.instReprClauseType = { reprPrec := Phenomena.WordOrder.Studies.Westergaard2009.instReprClauseType.repr }

def Phenomena.WordOrder.Studies.Westergaard2009.instReprClauseType.repr : ClauseType → ℕ → Std.Format

Equations

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

def Phenomena.WordOrder.Studies.Westergaard2009.instBEqClauseType.beq : ClauseType → ClauseType → Bool

Equations

• Phenomena.WordOrder.Studies.Westergaard2009.instBEqClauseType.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.WordOrder.Studies.Westergaard2009.instBEqClauseType : BEq ClauseType

Equations

• Phenomena.WordOrder.Studies.Westergaard2009.instBEqClauseType = { beq := Phenomena.WordOrder.Studies.Westergaard2009.instBEqClauseType.beq }

inductive Phenomena.WordOrder.Studies.Westergaard2009.V2Status : Type

V2 status of a clause type in a given language/dialect.

• obligatory : V2Status

  V2 is obligatory

• impossible : V2Status

  V2 is impossible (verb stays low or appears finally)

• optional : V2Status

  V2 alternates with non-V2, conditioned by other factors

instance Phenomena.WordOrder.Studies.Westergaard2009.instDecidableEqV2Status : DecidableEq V2Status

Equations

• Phenomena.WordOrder.Studies.Westergaard2009.instDecidableEqV2Status x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Phenomena.WordOrder.Studies.Westergaard2009.instReprV2Status : Repr V2Status

Equations

• Phenomena.WordOrder.Studies.Westergaard2009.instReprV2Status = { reprPrec := Phenomena.WordOrder.Studies.Westergaard2009.instReprV2Status.repr }

def Phenomena.WordOrder.Studies.Westergaard2009.instReprV2Status.repr : V2Status → ℕ → Std.Format

Equations

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

def Phenomena.WordOrder.Studies.Westergaard2009.instBEqV2Status.beq : V2Status → V2Status → Bool

Equations

• Phenomena.WordOrder.Studies.Westergaard2009.instBEqV2Status.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.WordOrder.Studies.Westergaard2009.instBEqV2Status : BEq V2Status

Equations

• Phenomena.WordOrder.Studies.Westergaard2009.instBEqV2Status = { beq := Phenomena.WordOrder.Studies.Westergaard2009.instBEqV2Status.beq }

structure Phenomena.WordOrder.Studies.Westergaard2009.V2Datum : Type

A single V2 observation: what happens in a given clause type.

• sentence : String
• language : String
• clauseType : ClauseType
• v2Status : V2Status
• description : String
• citation : String

instance Phenomena.WordOrder.Studies.Westergaard2009.instReprV2Datum : Repr V2Datum

Equations

• Phenomena.WordOrder.Studies.Westergaard2009.instReprV2Datum = { reprPrec := Phenomena.WordOrder.Studies.Westergaard2009.instReprV2Datum.repr }

def Phenomena.WordOrder.Studies.Westergaard2009.instReprV2Datum.repr : V2Datum → ℕ → Std.Format

Equations

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

def Phenomena.WordOrder.Studies.Westergaard2009.instBEqV2Datum.beq : V2Datum → V2Datum → Bool

Equations

• One or more equations did not get rendered due to their size.
• Phenomena.WordOrder.Studies.Westergaard2009.instBEqV2Datum.beq x✝¹ x✝ = false

instance Phenomena.WordOrder.Studies.Westergaard2009.instBEqV2Datum : BEq V2Datum

Equations

• Phenomena.WordOrder.Studies.Westergaard2009.instBEqV2Datum = { beq := Phenomena.WordOrder.Studies.Westergaard2009.instBEqV2Datum.beq }

Table 3.1 (p. 41) has exactly 6 language varieties. Every cell (6 × 7 = 42) is verified, so changing a single field in a Fragment file breaks exactly one guard.

Ch. 3 §4 introduces the cues — the syntactic templates in the input that trigger each micro-parameter. A micro-cue is a piece of I-language structure that children produce on exposure to the relevant input. Ch. 10 §3 (34)–(37) gives the final formulations.

The distinction from Table 3.1: micro-parameters are the *grammar's*
settings; micro-cues are the *observable evidence* in the input that
leads children to set each parameter.

Final micro-cue formulations (Ch. 10 (34)–(37)):
- (34) DeclP[XP Decl°[+V] ...] — V2 in declaratives
- (35) IntP[wh Int°[+V] ...] — V2 in wh-questions (wh-phrase in SpecIntP)
- (36) IntP[wh[Int°] ...] — non-V2 in wh-questions (wh-head *in* Int°)
- (37) TopP[DP[−FOC] Top° IntP[wh[Int°] ...]] — given subject → non-V2

NOTE: (36) and (37) are the two key innovations. (36) captures the
wh-head/phrase distinction: monosyllabic wh-words are heads that
occupy Int° directly, blocking verb movement. (37) captures the
TopP/[±FOC] mechanism: given subjects ([−FOC]) move to SpecTopP,
which is the structural basis for the information-structure
conditioning of V2 in § 10 below. 

structure Phenomena.WordOrder.Studies.Westergaard2009.MicroCue : Type

A micro-cue: a syntactic template that serves as evidence for a particular micro-parameter setting in acquisition.

• target : Minimalism.ForceHead

  Which head this cue is evidence for

• template : String

  The syntactic template (schematic notation)

• description : String

  Description of the cue

def Phenomena.WordOrder.Studies.Westergaard2009.instReprMicroCue.repr : MicroCue → ℕ → Std.Format

Equations

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

instance Phenomena.WordOrder.Studies.Westergaard2009.instReprMicroCue : Repr MicroCue

Equations

• Phenomena.WordOrder.Studies.Westergaard2009.instReprMicroCue = { reprPrec := Phenomena.WordOrder.Studies.Westergaard2009.instReprMicroCue.repr }

def Phenomena.WordOrder.Studies.Westergaard2009.instBEqMicroCue.beq : MicroCue → MicroCue → Bool

Equations

• One or more equations did not get rendered due to their size.
• Phenomena.WordOrder.Studies.Westergaard2009.instBEqMicroCue.beq x✝¹ x✝ = false

instance Phenomena.WordOrder.Studies.Westergaard2009.instBEqMicroCue : BEq MicroCue

Equations

• Phenomena.WordOrder.Studies.Westergaard2009.instBEqMicroCue = { beq := Phenomena.WordOrder.Studies.Westergaard2009.instBEqMicroCue.beq }

def Phenomena.WordOrder.Studies.Westergaard2009.cueIntV2 : MicroCue

Cue for V2 in wh-questions.

Equations

• Phenomena.WordOrder.Studies.Westergaard2009.cueIntV2 = { target := Minimalism.ForceHead.Int, template := "IntP[wh Int°V]", description := "Wh-element in SpecIntP, finite verb raised to Int°" }

def Phenomena.WordOrder.Studies.Westergaard2009.cueDeclV2 : MicroCue

Cue for V2 in declaratives.

Equations

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

def Phenomena.WordOrder.Studies.Westergaard2009.cueExclV2 : MicroCue

Cue for V2 in exclamatives.

Equations

• Phenomena.WordOrder.Studies.Westergaard2009.cueExclV2 = { target := Minimalism.ForceHead.Excl, template := "ExclP[wh Excl°V]", description := "Wh-exclamative with finite verb raised to Excl°" }

def Phenomena.WordOrder.Studies.Westergaard2009.cueWhV2 : MicroCue

Cue for V2 in embedded questions.

Equations

• Phenomena.WordOrder.Studies.Westergaard2009.cueWhV2 = { target := Minimalism.ForceHead.Wh, template := "WhP[wh Wh°V]", description := "Embedded question with finite verb raised to Wh°" }

def Phenomena.WordOrder.Studies.Westergaard2009.cueExclNonV2 : MicroCue

Cue for non-V2 in exclamatives.

Equations

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

def Phenomena.WordOrder.Studies.Westergaard2009.cueWhNonV2 : MicroCue

Cue for non-V2 in embedded questions.

Equations

• Phenomena.WordOrder.Studies.Westergaard2009.cueWhNonV2 = { target := Minimalism.ForceHead.Wh, template := "WhP[wh ... VP[V]]", description := "Embedded question with verb remaining in VP" }

def Phenomena.WordOrder.Studies.Westergaard2009.cuePolV2 : MicroCue

Cue for V2 in yes/no-questions.

Equations

• Phenomena.WordOrder.Studies.Westergaard2009.cuePolV2 = { target := Minimalism.ForceHead.Pol, template := "PolP[Pol°V ...]", description := "Finite verb raised to Pol° in yes/no-questions" }

def Phenomena.WordOrder.Studies.Westergaard2009.cueImpV2 : MicroCue

Cue for V2 in imperatives.

Equations

• Phenomena.WordOrder.Studies.Westergaard2009.cueImpV2 = { target := Minimalism.ForceHead.Imp, template := "ImpP[Imp°V ...]", description := "Finite verb raised to Imp° in imperatives" }

def Phenomena.WordOrder.Studies.Westergaard2009.cueWhHeadInInt : MicroCue

Cue for wh-head-in-Int° (non-V2 in wh-questions). Ch. 10 (36): IntP[wh[Int°] ...] — the monosyllabic wh-word occupies Int° itself, blocking verb movement to that position.

Equations

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

def Phenomena.WordOrder.Studies.Westergaard2009.cueExpressed (lang : V2Data) (c : MicroCue) : Bool

Whether a cue is expressed (+) in a given language's input. Children exposed to a + cue will set the corresponding parameter.

Equations

• Phenomena.WordOrder.Studies.Westergaard2009.cueExpressed lang c = lang.toProfile.verbMovement c.target

V2 observations from across the book, organized by language.

def Phenomena.WordOrder.Studies.Westergaard2009.no_decl_nonsubj : V2Datum

Non-subject-initial declaratives: V2 obligatory.

Equations

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

def Phenomena.WordOrder.Studies.Westergaard2009.no_yesno : V2Datum

Yes/no-questions: V2 obligatory.

Equations

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

def Phenomena.WordOrder.Studies.Westergaard2009.no_wh_long : V2Datum

Wh-questions with long (polysyllabic) wh-phrases: V2 obligatory.

Equations

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

def Phenomena.WordOrder.Studies.Westergaard2009.no_wh_short : V2Datum

Wh-questions with short (monosyllabic) wh-words: V2 optional, conditioned by information structure.

Equations

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

def Phenomena.WordOrder.Studies.Westergaard2009.no_excl : V2Datum

Exclamatives: non-V2 obligatory.

Equations

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

def Phenomena.WordOrder.Studies.Westergaard2009.no_emb_decl : V2Datum

Embedded declaratives: non-V2 (mostly).

Equations

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

def Phenomena.WordOrder.Studies.Westergaard2009.en_decl : V2Datum

Standard English: no V2 in declaratives (SVO base order).

Equations

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

def Phenomena.WordOrder.Studies.Westergaard2009.en_wh : V2Datum

Standard English: V2 in wh-questions (via SAI).

Equations

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

def Phenomena.WordOrder.Studies.Westergaard2009.belfast_emb_q : V2Datum

Belfast English: V2 in embedded questions too.

Equations

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

def Phenomena.WordOrder.Studies.Westergaard2009.da_excl : V2Datum

Danish: V2 in exclamatives (unlike Norwegian and English).

Equations

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

def Phenomena.WordOrder.Studies.Westergaard2009.de_decl : V2Datum

German root declaratives: V2 obligatory.

Equations

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

def Phenomena.WordOrder.Studies.Westergaard2009.de_emb : V2Datum

German embedded clauses with complementizer: verb-final (no V2). The verb raises to I/Fin (hence +Fin° in Table 3.1) but not to C, so it appears clause-finally due to SOV base order.

Equations

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

theorem Phenomena.WordOrder.Studies.Westergaard2009.no_en_differ_only_on_decl : Fragments.Norwegian.stdNorwegian.toProfile.verbMovement Minimalism.ForceHead.Int = Fragments.English.stdEnglish.toProfile.verbMovement Minimalism.ForceHead.Int ∧ Fragments.Norwegian.stdNorwegian.toProfile.verbMovement Minimalism.ForceHead.Pol = Fragments.English.stdEnglish.toProfile.verbMovement Minimalism.ForceHead.Pol ∧ Fragments.Norwegian.stdNorwegian.toProfile.verbMovement Minimalism.ForceHead.Excl = Fragments.English.stdEnglish.toProfile.verbMovement Minimalism.ForceHead.Excl ∧ Fragments.Norwegian.stdNorwegian.toProfile.verbMovement Minimalism.ForceHead.Imp = Fragments.English.stdEnglish.toProfile.verbMovement Minimalism.ForceHead.Imp ∧ Fragments.Norwegian.stdNorwegian.toProfile.verbMovement Minimalism.ForceHead.Fin = Fragments.English.stdEnglish.toProfile.verbMovement Minimalism.ForceHead.Fin ∧ Fragments.Norwegian.stdNorwegian.toProfile.verbMovement Minimalism.ForceHead.Wh = Fragments.English.stdEnglish.toProfile.verbMovement Minimalism.ForceHead.Wh ∧ Fragments.Norwegian.stdNorwegian.toProfile.verbMovement Minimalism.ForceHead.Decl ≠ Fragments.English.stdEnglish.toProfile.verbMovement Minimalism.ForceHead.Decl

Standard Norwegian and Standard English differ only on Decl°. This captures the classic observation that English lost V2 in declaratives but retained it in questions.

theorem Phenomena.WordOrder.Studies.Westergaard2009.nordmore_en_mirror_decl_int : Fragments.Norwegian.nordmoreNorwegian.toProfile.verbMovement Minimalism.ForceHead.Decl = true ∧ Fragments.Norwegian.nordmoreNorwegian.toProfile.verbMovement Minimalism.ForceHead.Int = false ∧ Fragments.English.stdEnglish.toProfile.verbMovement Minimalism.ForceHead.Decl = false ∧ Fragments.English.stdEnglish.toProfile.verbMovement Minimalism.ForceHead.Int = true

Nordmøre Norwegian is the mirror image of English on Decl° vs. Int°: Nordmøre has +Decl° −Int°, English has −Decl° +Int°.

theorem Phenomena.WordOrder.Studies.Westergaard2009.danish_no_differ_only_on_excl : Fragments.Danish.danish.toProfile.verbMovement Minimalism.ForceHead.Decl = Fragments.Norwegian.stdNorwegian.toProfile.verbMovement Minimalism.ForceHead.Decl ∧ Fragments.Danish.danish.toProfile.verbMovement Minimalism.ForceHead.Int = Fragments.Norwegian.stdNorwegian.toProfile.verbMovement Minimalism.ForceHead.Int ∧ Fragments.Danish.danish.toProfile.verbMovement Minimalism.ForceHead.Pol = Fragments.Norwegian.stdNorwegian.toProfile.verbMovement Minimalism.ForceHead.Pol ∧ Fragments.Danish.danish.toProfile.verbMovement Minimalism.ForceHead.Imp = Fragments.Norwegian.stdNorwegian.toProfile.verbMovement Minimalism.ForceHead.Imp ∧ Fragments.Danish.danish.toProfile.verbMovement Minimalism.ForceHead.Fin = Fragments.Norwegian.stdNorwegian.toProfile.verbMovement Minimalism.ForceHead.Fin ∧ Fragments.Danish.danish.toProfile.verbMovement Minimalism.ForceHead.Wh = Fragments.Norwegian.stdNorwegian.toProfile.verbMovement Minimalism.ForceHead.Wh ∧ Fragments.Danish.danish.toProfile.verbMovement Minimalism.ForceHead.Excl ≠ Fragments.Norwegian.stdNorwegian.toProfile.verbMovement Minimalism.ForceHead.Excl

Danish differs from Standard Norwegian only on Excl°.

theorem Phenomena.WordOrder.Studies.Westergaard2009.pol_universal : Fragments.Norwegian.stdNorwegian.toProfile.verbMovement Minimalism.ForceHead.Pol = true ∧ Fragments.English.stdEnglish.toProfile.verbMovement Minimalism.ForceHead.Pol = true ∧ Fragments.Norwegian.nordmoreNorwegian.toProfile.verbMovement Minimalism.ForceHead.Pol = true ∧ Fragments.English.belfastEnglish.toProfile.verbMovement Minimalism.ForceHead.Pol = true ∧ Fragments.German.german.toProfile.verbMovement Minimalism.ForceHead.Pol = true ∧ Fragments.Danish.danish.toProfile.verbMovement Minimalism.ForceHead.Pol = true

All six Table 3.1 languages agree on +Pol° (V2 in yes/no-questions is universal across these Germanic varieties).

theorem Phenomena.WordOrder.Studies.Westergaard2009.fin_only_german : Fragments.German.german.toProfile.verbMovement Minimalism.ForceHead.Fin = true ∧ Fragments.Norwegian.stdNorwegian.toProfile.verbMovement Minimalism.ForceHead.Fin = false ∧ Fragments.English.stdEnglish.toProfile.verbMovement Minimalism.ForceHead.Fin = false ∧ Fragments.Norwegian.nordmoreNorwegian.toProfile.verbMovement Minimalism.ForceHead.Fin = false ∧ Fragments.English.belfastEnglish.toProfile.verbMovement Minimalism.ForceHead.Fin = false ∧ Fragments.Danish.danish.toProfile.verbMovement Minimalism.ForceHead.Fin = false

German is the only Table 3.1 language with +Fin° (V-to-I in embedded clauses).

theorem Phenomena.WordOrder.Studies.Westergaard2009.active_count_ordering : Fragments.English.stdEnglish.toProfile.activeCount ≤ Fragments.Norwegian.nordmoreNorwegian.toProfile.activeCount ∧ Fragments.Norwegian.nordmoreNorwegian.toProfile.activeCount ≤ Fragments.Norwegian.stdNorwegian.toProfile.activeCount ∧ Fragments.Norwegian.stdNorwegian.toProfile.activeCount ≤ Fragments.German.german.toProfile.activeCount ∧ Fragments.German.german.toProfile.activeCount ≤ Fragments.Danish.danish.toProfile.activeCount

Active parameter counts form a monotone chain from English (fewest) to Danish (most) among the Table 3.1 languages.

Ch. 7 argues that monosyllabic wh-words are syntactic heads (X°) while polysyllabic wh-constituents are phrases (XP). When a wh-head occupies Int°, it blocks verb movement, making non-V2 possible. When a wh-phrase is in SpecIntP, Int° is free for the verb → V2 obligatory.

Tromsø Norwegian wh-words:
- Monosyllabic (heads): *ka* 'what' (1σ), *kem* 'who' (1σ),
  *kor* 'where' (1σ)
- Polysyllabic (phrases): *korfor* 'why' (2σ), *korsen* 'how' (2σ),
  *katti* 'when' (2σ) 

def Phenomena.WordOrder.Studies.Westergaard2009.tromsøWhWords : List (String × String × ℕ)

Tromsø wh-word data: (form, gloss, syllable count).

Equations

• Phenomena.WordOrder.Studies.Westergaard2009.tromsøWhWords = [("ka", "what", 1), ("kem", "who", 1), ("kor", "where", 1), ("korfor", "why", 2), ("korsen", "how", 2), ("katti", "when", 2)]

theorem Phenomena.WordOrder.Studies.Westergaard2009.tromsø_mono_are_heads : ((List.filter (fun (x : String × String × ℕ) => decide (x.2.2 ≤ 1)) tromsøWhWords).all fun (x : String × String × ℕ) => Minimalism.WhElementStatus.fromSyllableCount x.2.2 == Minimalism.WhElementStatus.head) = true

All monosyllabic Tromsø wh-words classify as heads.

theorem Phenomena.WordOrder.Studies.Westergaard2009.tromsø_poly_are_phrases : ((List.filter (fun (x : String × String × ℕ) => decide (x.2.2 > 1)) tromsøWhWords).all fun (x : String × String × ℕ) => Minimalism.WhElementStatus.fromSyllableCount x.2.2 == Minimalism.WhElementStatus.phrase) = true

All polysyllabic Tromsø wh-words classify as phrases.

theorem Phenomena.WordOrder.Studies.Westergaard2009.wh_blocking : Minimalism.whBlocksVerbMovement Minimalism.WhElementStatus.head = true ∧ Minimalism.whBlocksVerbMovement Minimalism.WhElementStatus.phrase = false

Head wh-words block verb movement; phrase wh-words do not.

English SAI (from SubjectAuxInversion.lean) is exactly the surface reflex of +Int° and +Pol° in the English V2 profile.

theorem Phenomena.WordOrder.Studies.Westergaard2009.english_wh_sai_consistent : SubjectAuxInversion.ex01.inverted = true ∧ SubjectAuxInversion.ex01.acceptability = SubjectAuxInversion.Acceptability.grammatical ∧ Fragments.English.stdEnglish.toProfile.verbMovement Minimalism.ForceHead.Int = true

English matrix wh-questions require inversion (ex01) and the profile marks Int° as + — consistent.

theorem Phenomena.WordOrder.Studies.Westergaard2009.english_yn_sai_consistent : SubjectAuxInversion.ex04.inverted = true ∧ SubjectAuxInversion.ex04.acceptability = SubjectAuxInversion.Acceptability.grammatical ∧ Fragments.English.stdEnglish.toProfile.verbMovement Minimalism.ForceHead.Pol = true

English matrix yes/no-questions require inversion (ex04) and the profile marks Pol° as + — consistent.

theorem Phenomena.WordOrder.Studies.Westergaard2009.english_decl_no_v2_consistent : Fragments.English.stdEnglish.toProfile.verbMovement Minimalism.ForceHead.Decl = false

English declaratives lack V2 — consistent with −Decl°.

theorem Phenomena.WordOrder.Studies.Westergaard2009.belfast_embedded_inv_consistent : SubjectAuxInversion.ex23.acceptability = SubjectAuxInversion.Acceptability.dialectal ∧ SubjectAuxInversion.ex24.acceptability = SubjectAuxInversion.Acceptability.dialectal ∧ Fragments.English.belfastEnglish.toProfile.verbMovement Minimalism.ForceHead.Wh = true

Belfast English embedded inversion (ex23, ex24) is consistent with +Wh°.

theorem Phenomena.WordOrder.Studies.Westergaard2009.no_yesno_consistent : no_yesno.v2Status = V2Status.obligatory ∧ Fragments.Norwegian.stdNorwegian.toProfile.verbMovement Minimalism.ForceHead.Pol = true

Norwegian yes/no-questions are obligatorily V2, consistent with +Pol°.

theorem Phenomena.WordOrder.Studies.Westergaard2009.no_excl_consistent : no_excl.v2Status = V2Status.impossible ∧ Fragments.Norwegian.stdNorwegian.toProfile.verbMovement Minimalism.ForceHead.Excl = false

Norwegian exclamatives are non-V2, consistent with −Excl°.

theorem Phenomena.WordOrder.Studies.Westergaard2009.da_excl_consistent : da_excl.v2Status = V2Status.obligatory ∧ Fragments.Danish.danish.toProfile.verbMovement Minimalism.ForceHead.Excl = true

Danish exclamatives are V2, consistent with +Excl°.

theorem Phenomena.WordOrder.Studies.Westergaard2009.de_emb_no_v2 : de_emb.v2Status = V2Status.impossible ∧ Fragments.German.german.toProfile.verbMovement Minimalism.ForceHead.Wh = false

German embedded clauses are verb-final (no V2), even though German has +Fin° (V-to-I). V2 = verb-to-C, which requires +Decl°/+Int° etc. Verb-final is consistent with −Wh° (no V-to-C in embedded contexts).

GermanicV2.lean proves that German V2 involves head-to-head movement of V to C, skipping T (HMC violation). This is the structural realization of +Decl° in profile: verb movement targets the Decl° head in the CP domain.

The bridge: German has +Decl° (our profile) AND the syntactic analysis
shows V moves to C in root declaratives (GermanicV2). 

theorem Phenomena.WordOrder.Studies.Westergaard2009.german_decl_v2_bridge : Fragments.German.german.toProfile.verbMovement Minimalism.ForceHead.Decl = true

German +Decl° is consistent with the V-to-C movement formalized in GermanicV2.lean: the verb moves to C (= the Decl° position in split-ForceP).

The GermanicV2 file shows:

• V2 is head-to-head movement (v2_mover_stays_minimal)
• V skips T to reach C (t_intervenes_in_v2)
• The mover was a head in the target (verb_was_head_in_target)

WALS classifies German as having "no dominant order" (Typology.lean). Westergaard's micro-parameters explain why: German has +Decl° (V2 in root declaratives) but also +Fin° (V-to-I in embedded clauses, yielding verb-final surface order due to SOV base). This split makes the "basic" order indeterminate — SVO on the surface in root clauses, SOV underlyingly and in embedded clauses.

theorem Phenomena.WordOrder.Studies.Westergaard2009.german_noDominant_explained : Typology.germanV2.basicOrder = Typology.BasicOrder.noDominant ∧ Fragments.German.german.toProfile.verbMovement Minimalism.ForceHead.Decl = true ∧ Fragments.German.german.toProfile.verbMovement Minimalism.ForceHead.Fin = true

German's "no dominant order" classification in WALS is consistent with a micro-parameter profile that has BOTH +Decl° (V2 in roots → surface SVO) AND +Fin° (V-to-I in embedded → surface SOV).

theorem Phenomena.WordOrder.Studies.Westergaard2009.english_svo_explained : Typology.english.basicOrder = Typology.BasicOrder.svo ∧ Fragments.English.stdEnglish.toProfile.verbMovement Minimalism.ForceHead.Decl = false ∧ Fragments.English.stdEnglish.toProfile.verbMovement Minimalism.ForceHead.Fin = false

English is classified as SVO in WALS. This is consistent with −Decl° (no verb movement in declaratives → surface SVO with SVO base order) and −Fin° (no V-to-I in embedded clauses → embedded order also SVO).

In Tromsø wh-questions with monosyllabic wh-words, V2 vs. non-V2 correlates with the discourse status of the subject:

- **[−FOC] / given subject** (pronoun) → non-V2 preferred.
  Subject moves to SpecTopP; verb stays low.
- **[+FOC] / new subject** (full DP) → V2 preferred.
  Subject stays in SpecIP; verb moves to Top° to check [−FOC].

The book *derives* this from TopP structure (pp. 46–47): given subjects
carry [−FOC], which triggers movement to SpecTopP, leaving Int° empty
(verb stays low). New subjects lack [−FOC], so they stay in SpecIP and
the verb moves to Top°/Int° → V2. The [±FOC] feature already exists in
`Features.lean` (`foc : Bool → FeatureVal`) but is not yet connected
to an Agree-based derivation.

TODO: Replace this stipulative pattern match with a derivation from
[±FOC] feature checking on subjects + TopP Agree/movement. The
current version captures the correct *empirical mapping* but does not
explain *why* the mapping holds — the TopP mechanism does. 

def Phenomena.WordOrder.Studies.Westergaard2009.tromsøWhV2Preference : Core.InformationStructure.DiscourseStatus → V2Status

Preferred V2 status given subject discourse status in Tromsø monosyllabic wh-questions.

STIPULATIVE: this pattern-matches on discourse status directly. The book derives this from [±FOC]/TopP (see § 10 docstring).

Equations

• Phenomena.WordOrder.Studies.Westergaard2009.tromsøWhV2Preference Core.InformationStructure.DiscourseStatus.given = Phenomena.WordOrder.Studies.Westergaard2009.V2Status.impossible
• Phenomena.WordOrder.Studies.Westergaard2009.tromsøWhV2Preference Core.InformationStructure.DiscourseStatus.new = Phenomena.WordOrder.Studies.Westergaard2009.V2Status.obligatory
• Phenomena.WordOrder.Studies.Westergaard2009.tromsøWhV2Preference Core.InformationStructure.DiscourseStatus.focused = Phenomena.WordOrder.Studies.Westergaard2009.V2Status.obligatory

theorem Phenomena.WordOrder.Studies.Westergaard2009.given_predicts_nonV2 : tromsøWhV2Preference Core.InformationStructure.DiscourseStatus.given = V2Status.impossible

Given subjects predict non-V2 in Tromsø short wh-questions.

theorem Phenomena.WordOrder.Studies.Westergaard2009.new_predicts_V2 : tromsøWhV2Preference Core.InformationStructure.DiscourseStatus.new = V2Status.obligatory

New subjects predict V2 in Tromsø short wh-questions.

structural economy (p. 4):

(9a) Only build as much structure as there is evidence for in the input.
(9b) Only move elements as far as there is evidence for in the input.

These principles constrain *children's grammars*: children build minimal
structure, adding projections only when input evidence forces them.

The following theorems derive a corollary: languages with fewer active
micro-parameters require less structure to be built. This is our own
formalization of a consequence of (9a), not a claim directly stated in
the book. 

theorem Phenomena.WordOrder.Studies.Westergaard2009.english_fewer_active : Fragments.English.stdEnglish.toProfile.activeCount < Fragments.Norwegian.stdNorwegian.toProfile.activeCount

English activates fewer micro-parameters than Standard Norwegian.

theorem Phenomena.WordOrder.Studies.Westergaard2009.nordmore_fewer_active : Fragments.Norwegian.nordmoreNorwegian.toProfile.activeCount < Fragments.Norwegian.stdNorwegian.toProfile.activeCount

Nordmøre activates fewer micro-parameters than Standard Norwegian.