GenHM and Do-Support

@cite{arregi-pietraszko-2021}

Connects the GenHM formalization to empirical data from SubjectAuxInversion.lean.

Structure

§1 English GenHM chain configurations for A&P's four do-support contexts §2 The bridge table: each contextual datum paired with its GenHM prediction §3 The parallelism theorem: do-support uniformity across all four contexts §4 Deriving VMovementParam from GenHM

Central Result

The parallelism of do-support across A&P's three core contexts (negation, SAI, verum focus) plus VPE is a DERIVED consequence of GenHM chain structure, not a stipulation about the V-movement parameter. The four contexts involve two structurally distinct reasons for chain-splitting — intervention by a [+P] specifier (negation, SAI, verum) and post-syntactic [-P] on V* (VPE) — yet all produce the same do-support outcome because spell-out depends only on WHETHER the chain is split.

A&P unify the three intervention contexts under a single specifier-intervention rule (footnote 30). SAI is intervention by the subject in Spec,TP, NOT "probe displacement"; verum focus is intervention by a covert specifier in Spec,ΣP, NOT a "weak Foc head".

Out of scope

Tag questions (e.g. She likes him, doesn't she?) are not in A&P's paper; their analysis belongs in a future Sailor 2018 study file. A substantive TenseSupportContext → GenHMChain bridge that would connect this file's predictions to Pollock1989.lean's needsDoSupport is deferred to a cross-framework wiring follow-up. Orphan Assignment (the actual do-insertion derivation) and the strong V parameter (A&P's cross-linguistic prediction) are deferred to follow-up substrate work; needsDoSupportGenHM here is a Boolean proxy.

A&P's four do-support contexts as GenHM chains. The four chains involve two distinct split mechanisms:

• Split-by-Intervention (a [+P] specifier intervenes between top of chain and V*): negation, SAI, verum focus.
• Split-by-Deletion (V* marked [-P] post-syntactically): VPE.

def ArregiPietraszko2021.negationChain : Minimalist.GenHMChain

Negation chain: T ... [Spec,ΣP: not] ... V

"Sue does not eat fish" — overt not in Spec,ΣP intervenes. Split-by-Intervention.

Equations

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

def ArregiPietraszko2021.verumChain : Minimalist.GenHMChain

Verum focus chain: T ... [Spec,ΣP: covert verum specifier] ... V

"Sue DOES eat fish" — covert specifier in Spec,ΣP intervenes (cf. A&P fn. 30 — same intervention mechanism as negation). Split-by-Intervention.

Equations

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

def ArregiPietraszko2021.questionChain : Minimalist.GenHMChain

Question chain (SAI): C ← T ... [Spec,TP: subject] ... V

"Where does Sue eat fish?" — the subject in Spec,TP intervenes between T (chained to C) and V*. Crucially this is intervention, NOT "probe displacement" — see A&P, where GenHM is taken to relate V, T, and C across the subject specifier. Split-by-Intervention.

Equations

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

def ArregiPietraszko2021.vpEllipsisChain : Minimalist.GenHMChain

VP ellipsis chain: T ... V (with V* marked [-P] post-syntactically)

"She runs faster than he does" — V is present and chained to T; VPE marks V* with [-P], blocking lowered Vocabulary Insertion. Split-by-Deletion (NOT goal-absence — A&P's analysis crucially has GenHM still applying).

Equations

• ArregiPietraszko2021.vpEllipsisChain = { probeCat := Minimalist.Cat.T, goalCat := Minimalist.Cat.V, splitReason := some Minimalist.ChainSplitReason.deletion }

def ArregiPietraszko2021.declarativeChain : Minimalist.GenHMChain

A declarative chain with no split: T ... V

"Sue eats fish" — clear chain, M-value lowers to V (affix hopping).

Equations

• ArregiPietraszko2021.declarativeChain = { probeCat := Minimalist.Cat.T, goalCat := Minimalist.Cat.V, splitReason := none }

@[simp]

theorem ArregiPietraszko2021.declarative_lowers : Minimalist.spellOutTarget declarativeChain = Minimalist.SpellOutTarget.onGoal

Behavioral fact about declaratives: M-value lowers (affix hopping).

@[simp]

theorem ArregiPietraszko2021.declarative_no_doSupport : Minimalist.needsDoSupportGenHM declarativeChain false = false

Behavioral fact about declaratives with lexical V: no do-support.

def ArregiPietraszko2021.doSupportTable : List (Phenomena.WordOrder.SubjectAuxInversion.SAIDatum × Minimalist.GenHMChain × Bool × Bool)

A&P's do-support paradigm as a bridge table.

Each row pairs an empirical datum from SubjectAuxInversion.lean with the GenHM chain configuration assigned in §1, the probe-content Boolean (lexical V = false, auxiliary = true), and the do-support prediction.

Coverage: A&P's three core contexts (negation, SAI, verum focus) each tested with both lexical V and auxiliary; VPE tested with lexical V only (the auxiliary case is not a do-support trigger and not in A&P's discussion of VPE).

Equations

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

theorem ArregiPietraszko2021.all_bridges_hold (row : Phenomena.WordOrder.SubjectAuxInversion.SAIDatum × Minimalist.GenHMChain × Bool × Bool) : row ∈ doSupportTable → row.1.acceptability = Phenomena.WordOrder.SubjectAuxInversion.Acceptability.grammatical ∧ Minimalist.needsDoSupportGenHM row.2.1 row.2.2.1 = row.2.2.2

Every row in the bridge table holds: the example is grammatical AND GenHM predicts the right do-support outcome. This single theorem replaces the per-example bridge theorems of earlier drafts — A&P's parallelism claim is precisely that the table is uniform.

theorem ArregiPietraszko2021.doSupport_parallel_lexical (chain : Minimalist.GenHMChain) (h : chain.isSplit = true) : Minimalist.needsDoSupportGenHM chain false = true

Parallelism for lexical verbs: any split chain triggers do-support when the probe is contentless. Concrete consequence of the substrate theorem lexical_verb_needs_doSupport_when_split.

theorem ArregiPietraszko2021.doSupport_parallel_aux (chain : Minimalist.GenHMChain) : Minimalist.needsDoSupportGenHM chain true = false

Parallelism for auxiliaries: no chain triggers do-support when the probe carries lexical content. Concrete consequence of auxiliaries_dont_need_doSupport.

theorem ArregiPietraszko2021.doSupport_context_irrelevant (chain₁ chain₂ : Minimalist.GenHMChain) (content : Bool) (h : chain₁.isSplit = chain₂.isSplit) : Minimalist.needsDoSupportGenHM chain₁ content = Minimalist.needsDoSupportGenHM chain₂ content

Context-irrelevance: any two chains with the same split status give the same do-support decision. The reason for the split (intervention vs deletion) is irrelevant.

theorem ArregiPietraszko2021.genHM_derives_raises : Minimalist.genHM_to_vMovementParam declarativeChain = Minimalist.VMovementParam.raises

A clear chain (no split) yields the .raises surface pattern.

theorem ArregiPietraszko2021.genHM_derives_inSitu : Minimalist.genHM_to_vMovementParam negationChain = Minimalist.VMovementParam.inSitu

A split chain yields the .inSitu surface pattern.

TODO: a substantive chainOf : TenseSupportContext → GenHMChain map would let us state needsDoSupport p ctx = needsDoSupportGenHM (chainOf ctx) (contentOf p) — converting Pollock1989's flat parameter into a derived view of GenHM's chain structure. Deferred to a cross-framework wiring follow-up that also touches Pollock1989.lean.