Documentation

Linglib.Phenomena.WordOrder.Studies.ArregiPietraszko2021

GenHM and Do-Support #

@cite{arregi-pietraszko-2021}

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

Structure #

§1 English terminal strength assignment §2 English GenHM chain configurations for the five do-support contexts §3 Theorems pairing each empirical datum with GenHM predictions §4 The parallelism theorem: do-support uniformity across all five contexts §5 Deriving VMovementParam from GenHM

Central Result #

The parallelism of do-support across negation, SAI, verum focus, tag questions, and VP ellipsis is a DERIVED consequence of GenHM chain structure, not a stipulation about the V-movement parameter. The five contexts involve three distinct structural reasons for chain-splitting — weak intervention, probe displacement, and goal absence — yet all produce the same do-support outcome because spell-out depends only on WHETHER the chain is split.

source
def Phenomena.WordOrder.Studies.ArregiPietraszko2021.englishStrength :
Minimalism.TerminalStrengthAssignment

English terminal strength: Neg and Foc are weak; all others strong.

Equations
Instances For
    source
    theorem Phenomena.WordOrder.Studies.ArregiPietraszko2021.neg_is_weak :
    englishStrength Minimalism.Cat.Neg = Minimalism.TerminalStrength.weak
    source
    theorem Phenomena.WordOrder.Studies.ArregiPietraszko2021.foc_is_weak :
    englishStrength Minimalism.Cat.Foc = Minimalism.TerminalStrength.weak
    source
    theorem Phenomena.WordOrder.Studies.ArregiPietraszko2021.v_is_strong :
    englishStrength Minimalism.Cat.V = Minimalism.TerminalStrength.strong
    source
    theorem Phenomena.WordOrder.Studies.ArregiPietraszko2021.t_is_strong :
    englishStrength Minimalism.Cat.T = Minimalism.TerminalStrength.strong
    source
    theorem Phenomena.WordOrder.Studies.ArregiPietraszko2021.c_is_strong :
    englishStrength Minimalism.Cat.C = Minimalism.TerminalStrength.strong

    The five do-support contexts, formalized as GenHM chains. Each chain has:

    The five chains involve three distinct split mechanisms:

    source
    def Phenomena.WordOrder.Studies.ArregiPietraszko2021.negationChain :
    Minimalism.GenHMChain

    Negation chain: T ... Neg ... V

    "Sue does not eat fish" — Neg (weak) intervenes between T and V. Split-by-Intervention.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def Phenomena.WordOrder.Studies.ArregiPietraszko2021.verumChain :
      Minimalism.GenHMChain

      Verum focus chain: T ... Foc ... V

      "Sue DOES eat fish" — Foc (weak) intervenes between T and V. Split-by-Intervention.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        def Phenomena.WordOrder.Studies.ArregiPietraszko2021.questionChain :
        Minimalism.GenHMChain

        Question chain (SAI): C ← T ... V

        "Where does Sue eat fish?" — T is displaced to C via GenHM(C,T), breaking the T–V chain. The M-value cannot lower to V because T is no longer structurally adjacent to V. Split-by-Displacement.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          def Phenomena.WordOrder.Studies.ArregiPietraszko2021.tagChain :
          Minimalism.GenHMChain

          Tag question chain: T ... [VP absent]

          "She likes him, doesn't she?" — VP is anaphoric/absent in the tag. The M-value cannot lower because the goal is not available. Split-by-Deletion.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            def Phenomena.WordOrder.Studies.ArregiPietraszko2021.vpEllipsisChain :
            Minimalism.GenHMChain

            VP ellipsis chain: T ... [VP deleted]

            "She runs faster than he does" — VP is elided at PF. The M-value cannot lower because the goal has been deleted. Split-by-Deletion.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              def Phenomena.WordOrder.Studies.ArregiPietraszko2021.declarativeChain :
              Minimalism.GenHMChain

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

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

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                theorem Phenomena.WordOrder.Studies.ArregiPietraszko2021.negation_chain_split :
                negationChain.isSplit = true
                source
                theorem Phenomena.WordOrder.Studies.ArregiPietraszko2021.verum_chain_split :
                verumChain.isSplit = true
                source
                theorem Phenomena.WordOrder.Studies.ArregiPietraszko2021.question_chain_split :
                questionChain.isSplit = true
                source
                theorem Phenomena.WordOrder.Studies.ArregiPietraszko2021.tag_chain_split :
                tagChain.isSplit = true
                source
                theorem Phenomena.WordOrder.Studies.ArregiPietraszko2021.vpEllipsis_chain_split :
                vpEllipsisChain.isSplit = true
                source
                theorem Phenomena.WordOrder.Studies.ArregiPietraszko2021.declarative_chain_clear :
                declarativeChain.isSplit = false
                source
                theorem Phenomena.WordOrder.Studies.ArregiPietraszko2021.negation_chain_wf :
                negationChain.wellFormed = true

                Well-formedness: intervention chains have genuinely weak interveners.

                source
                theorem Phenomena.WordOrder.Studies.ArregiPietraszko2021.verum_chain_wf :
                verumChain.wellFormed = true
                source
                theorem Phenomena.WordOrder.Studies.ArregiPietraszko2021.question_chain_wf :
                questionChain.wellFormed = true
                source
                theorem Phenomena.WordOrder.Studies.ArregiPietraszko2021.tag_chain_wf :
                tagChain.wellFormed = true
                source
                theorem Phenomena.WordOrder.Studies.ArregiPietraszko2021.vpEllipsis_chain_wf :
                vpEllipsisChain.wellFormed = true
                source
                theorem Phenomena.WordOrder.Studies.ArregiPietraszko2021.declarative_chain_wf :
                declarativeChain.wellFormed = true
                source
                theorem Phenomena.WordOrder.Studies.ArregiPietraszko2021.declarative_lowers :
                Minimalism.spellOutTarget declarativeChain = Minimalism.SpellOutTarget.onGoal

                In declaratives, the M-value lowers to V (affix hopping).

                source
                theorem Phenomena.WordOrder.Studies.ArregiPietraszko2021.declarative_no_doSupport :
                Minimalism.needsDoSupportGenHM declarativeChain false = false

                In declaratives with lexical verbs, no do-support is needed.

                source
                theorem Phenomena.WordOrder.Studies.ArregiPietraszko2021.bridge_genHM_ex32 :
                (SubjectAuxInversion.ex32.acceptability == SubjectAuxInversion.Acceptability.grammatical) = true ∧ Minimalism.needsDoSupportGenHM negationChain false = true

                ex32 "Sue does not eat fish" — negation + lexical V → do-support

                source
                theorem Phenomena.WordOrder.Studies.ArregiPietraszko2021.bridge_genHM_ex34 :
                (SubjectAuxInversion.ex34.acceptability == SubjectAuxInversion.Acceptability.grammatical) = true ∧ Minimalism.needsDoSupportGenHM negationChain true = false

                ex34 "Sue is not eating fish" — negation + auxiliary → no do-support

                source
                theorem Phenomena.WordOrder.Studies.ArregiPietraszko2021.bridge_genHM_ex27 :
                (SubjectAuxInversion.ex27.acceptability == SubjectAuxInversion.Acceptability.grammatical) = true ∧ Minimalism.needsDoSupportGenHM questionChain false = true

                ex27 "Where does Sue eat fish?" — question + lexical V → do-support

                source
                theorem Phenomena.WordOrder.Studies.ArregiPietraszko2021.bridge_genHM_ex30 :
                (SubjectAuxInversion.ex30.acceptability == SubjectAuxInversion.Acceptability.grammatical) = true ∧ Minimalism.needsDoSupportGenHM questionChain true = false

                ex30 "Where is Sue eating fish?" — question + auxiliary → no do-support

                source
                theorem Phenomena.WordOrder.Studies.ArregiPietraszko2021.bridge_genHM_ex39 :
                (SubjectAuxInversion.ex39.acceptability == SubjectAuxInversion.Acceptability.grammatical) = true ∧ Minimalism.needsDoSupportGenHM verumChain false = true

                ex39 "Sue DOES eat fish" — verum + lexical V → do-support

                source
                theorem Phenomena.WordOrder.Studies.ArregiPietraszko2021.bridge_genHM_ex40 :
                (SubjectAuxInversion.ex40.acceptability == SubjectAuxInversion.Acceptability.grammatical) = true ∧ Minimalism.needsDoSupportGenHM verumChain true = false

                ex40 "She IS eating fish" — verum + auxiliary → no do-support

                source
                theorem Phenomena.WordOrder.Studies.ArregiPietraszko2021.bridge_genHM_ex36 :
                (SubjectAuxInversion.ex36.acceptability == SubjectAuxInversion.Acceptability.grammatical) = true ∧ Minimalism.needsDoSupportGenHM tagChain false = true

                ex36 "She likes him, doesn't she?" — tag + lexical V → do-support

                source
                theorem Phenomena.WordOrder.Studies.ArregiPietraszko2021.bridge_genHM_ex38 :
                (SubjectAuxInversion.ex38.acceptability == SubjectAuxInversion.Acceptability.grammatical) = true ∧ Minimalism.needsDoSupportGenHM vpEllipsisChain false = true

                ex38 "She runs faster than he does" — VP ellipsis + lexical V → do-support

                source
                theorem Phenomena.WordOrder.Studies.ArregiPietraszko2021.doSupport_parallel_all_contexts_lexical :
                Minimalism.needsDoSupportGenHM negationChain false = true ∧ Minimalism.needsDoSupportGenHM questionChain false = true ∧ Minimalism.needsDoSupportGenHM verumChain false = true ∧ Minimalism.needsDoSupportGenHM tagChain false = true ∧ Minimalism.needsDoSupportGenHM vpEllipsisChain false = true

                The Parallelism Theorem (lexical verbs): Do-support is triggered in ALL five contexts with lexical verbs (contentless T), despite three different structural reasons for chain-splitting.

                source
                theorem Phenomena.WordOrder.Studies.ArregiPietraszko2021.doSupport_parallel_all_contexts_aux :
                Minimalism.needsDoSupportGenHM negationChain true = false ∧ Minimalism.needsDoSupportGenHM questionChain true = false ∧ Minimalism.needsDoSupportGenHM verumChain true = false ∧ Minimalism.needsDoSupportGenHM tagChain true = false ∧ Minimalism.needsDoSupportGenHM vpEllipsisChain true = false

                With auxiliaries, do-support is never needed in ANY context.

                source
                theorem Phenomena.WordOrder.Studies.ArregiPietraszko2021.doSupport_context_irrelevant (chain₁ chain₂ : Minimalism.GenHMChain) (content : Bool) (h : chain₁.isSplit = chain₂.isSplit) :
                Minimalism.needsDoSupportGenHM chain₁ content = Minimalism.needsDoSupportGenHM chain₂ content

                The abstract parallelism: for ANY two chains with the same split status, the do-support decision is identical. The reason for the split (intervention, displacement, deletion) is irrelevant.

                source
                theorem Phenomena.WordOrder.Studies.ArregiPietraszko2021.genHM_derives_raises :
                Minimalism.genHM_to_vMovementParam declarativeChain = Minimalism.VMovementParam.raises

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

                source
                theorem Phenomena.WordOrder.Studies.ArregiPietraszko2021.genHM_derives_inSitu :
                Minimalism.genHM_to_vMovementParam negationChain = Minimalism.VMovementParam.inSitu

                A split chain yields the .inSitu surface pattern.

                source
                theorem Phenomena.WordOrder.Studies.ArregiPietraszko2021.genHM_consistent_with_pollock_lexical (ctx : Minimalism.TenseSupportContext) :
                Minimalism.needsDoSupport Minimalism.englishLexical ctx = true

                The Pollock1989 needsDoSupport function is consistent with GenHM predictions for lexical verbs across all contexts.

                source
                theorem Phenomena.WordOrder.Studies.ArregiPietraszko2021.genHM_consistent_with_pollock_aux (ctx : Minimalism.TenseSupportContext) :
                Minimalism.needsDoSupport Minimalism.englishAux ctx = false

                The Pollock1989 needsDoSupport function is consistent with GenHM predictions for auxiliaries across all contexts.