Documentation

Linglib.Phenomena.AuxiliaryVerbs.Studies.Anderson2006

Anderson (2006): Auxiliary Verb Constructions #

@cite{anderson-2006}

Cross-linguistic typology of auxiliary verb constructions (AVCs), establishing a five-pattern classification based on how inflection distributes between auxiliary and lexical verb.

Key contributions formalized #

  1. Five-pattern inflectional typology (InflPattern): auxHeaded, lexHeaded, doubled, split, splitDoubled — defined in Typology.lean, verified here
  2. Semantic head invariant: the lexical verb is always the semantic head, regardless of where inflection sits
  3. Typed inflectional distribution: InflDistribution (from Core.Morphology) records which MorphCategory values each element hosts, replacing ad-hoc string lists in Fragment files
  4. Grammaticalization cline: full verb → auxiliary → clitic → affix → zero

Coverage #

Data from 7 languages (8 data points): English (aux-headed), Doyayo (split), Gorum (doubled), Jakaltek (split), Pipil (split + lex-headed), Finnish (split), Hemba (split/doubled). All five patterns attested.

Grammaticalization Cline #

The grammaticalization cline and source constructions are now in Theories.Diachronic.Grammaticalization. GramStage and AVCSource are opened from there.

source
def Phenomena.AuxiliaryVerbs.Studies.Anderson2006.GramStage.toMorphStatus :
Diachronic.Grammaticalization.GramStage → Option Core.Morphology.MorphStatus

The grammaticalization cline maps to MorphStatus categories. Auxiliaries and full verbs are free words; clitics and affixes map to their respective statuses; zero has no overt realization.

Equations
Instances For
    source
    def Phenomena.AuxiliaryVerbs.Studies.Anderson2006.negStrategyStage :
    NegativeAuxiliaries.NegStrategy → Diachronic.Grammaticalization.GramStage

    Negative auxiliary strategies map to stages on the cline: neg verb = auxiliary stage, neg affix = affix stage, neg particle = auxiliary stage (free word).

    Equations
    Instances For
      source
      theorem Phenomena.AuxiliaryVerbs.Studies.Anderson2006.negAffix_more_grammaticalized :
      (negStrategyStage NegativeAuxiliaries.NegStrategy.negAffix).boundedness > (negStrategyStage NegativeAuxiliaries.NegStrategy.negVerb).boundedness

      Negative affixes are further along the cline than negative verbs.

      Pattern Coverage Theorems #

      source
      theorem Phenomena.AuxiliaryVerbs.Studies.Anderson2006.five_patterns_attested :
      (Typology.allData.any fun (x : Typology.AVCDatum) => x.inflPattern == Typology.InflPattern.auxHeaded) = true ∧ (Typology.allData.any fun (x : Typology.AVCDatum) => x.inflPattern == Typology.InflPattern.lexHeaded) = true ∧ (Typology.allData.any fun (x : Typology.AVCDatum) => x.inflPattern == Typology.InflPattern.doubled) = true ∧ (Typology.allData.any fun (x : Typology.AVCDatum) => x.inflPattern == Typology.InflPattern.split) = true ∧ (Typology.allData.any fun (x : Typology.AVCDatum) => x.inflPattern == Typology.InflPattern.splitDoubled) = true

      All five of Anderson's inflectional patterns are attested in current data.

      Structural Theorems on Distribution #

      These theorems verify structural properties of the typed InflDistribution data, connecting Fragment-level category lists to Anderson's pattern classification.

      source
      theorem Phenomena.AuxiliaryVerbs.Studies.Anderson2006.gorum_doubled_same_categories :
      (have dist := Fragments.Gorum.AuxiliaryVerbs.inflDistribution; dist.onAux == dist.onLex) = true

      In Gorum's doubled AVC, aux and lex host exactly the same categories.

      source
      theorem Phenomena.AuxiliaryVerbs.Studies.Anderson2006.doyayo_split_disjoint :
      have dist := Fragments.Doyayo.AuxiliaryVerbs.inflDistribution; (dist.onAux.all fun (c : Core.Morphology.MorphCategory) => !dist.onLex.contains c) = true

      In Doyayo's split AVC, aux and lex host disjoint category types.

      source
      theorem Phenomena.AuxiliaryVerbs.Studies.Anderson2006.pipil_split_disjoint :
      have dist := Fragments.Pipil.AuxiliaryVerbs.inflDistribution; (dist.onAux.all fun (c : Core.Morphology.MorphCategory) => !dist.onLex.contains c) = true

      In Pipil's split AVC, aux and lex host disjoint category types.

      source
      theorem Phenomena.AuxiliaryVerbs.Studies.Anderson2006.finnish_split_disjoint :
      have dist := Fragments.Finnish.Negation.finnishNegDistribution; (dist.onAux.all fun (c : Core.Morphology.MorphCategory) => !dist.onLex.contains c) = true

      In Finnish's split AVC, aux and lex host disjoint category types. (.stem on the lex side is a base, not an inflectional overlap.)

      source
      theorem Phenomena.AuxiliaryVerbs.Studies.Anderson2006.jakaltek_split_within_agreement :
      have dist := Fragments.Jakaltek.AuxiliaryVerbs.inflDistribution; dist.onAux.contains Core.Morphology.MorphCategory.agreement = true ∧ dist.onLex.contains Core.Morphology.MorphCategory.agreement = true

      Jakaltek's split distributes agreement across both elements — absolutive on AUX and ergative on LV. At the MorphCategory level, both are .agreement, so the split is within a single category type rather than between category types. This is the correct representation: Anderson classifies Jakaltek as split despite the shared .agreement label because the specific agreement relations (absolutive vs. ergative) differ.

      source
      theorem Phenomena.AuxiliaryVerbs.Studies.Anderson2006.pipil_lexHeaded_aux_empty :
      Fragments.Pipil.AuxiliaryVerbs.lexHeadedDistribution.onAux = []

      In Pipil's lex-headed AVC, the auxiliary hosts no inflection.

      source
      theorem Phenomena.AuxiliaryVerbs.Studies.Anderson2006.hemba_splitDoubled_agreement_doubled :
      have dist := Fragments.Hemba.AuxiliaryVerbs.inflDistribution; dist.onAux.contains Core.Morphology.MorphCategory.agreement = true ∧ dist.onLex.contains Core.Morphology.MorphCategory.agreement = true ∧ dist.onAux.contains Core.Morphology.MorphCategory.tense = true ∧ dist.onLex.contains Core.Morphology.MorphCategory.tense = false ∧ dist.onAux.contains Core.Morphology.MorphCategory.mood = false ∧ dist.onLex.contains Core.Morphology.MorphCategory.mood = true

      In Hemba's split/doubled AVC, agreement is doubled (on both elements), while tense is AUX-only and mood is LV-only. This is the defining characteristic of the split/doubled pattern: some categories are shared (doubled) while others are exclusive to one element (split).

      Dual Headedness #

      Anderson's central insight: AVCs have two distinct notions of head. The semantic head (content provider) is always the lexical verb. The inflectional host varies by pattern. This mismatch is what makes AVCs typologically distinctive.

      source
      theorem Phenomena.AuxiliaryVerbs.Studies.Anderson2006.heads_coincide_iff_lexHeaded (p : Typology.InflPattern) :
      (p.semanticHead == p.inflHost) = (p == Typology.InflPattern.lexHeaded)

      The semantic head and inflectional host coincide only in lex-headed AVCs. In all other patterns, they diverge: the semantic head is always the lexical verb, but inflection may sit on the auxiliary.

      Negative Auxiliaries as AVCs #

      @cite{anderson-2006} treats negative auxiliaries (Finnish ei, Komi oz) as a special case of aux-headed AVCs: the negative element IS the auxiliary, hosting inflection that the lexical verb would otherwise carry.

      source
      theorem Phenomena.AuxiliaryVerbs.Studies.Anderson2006.negVerb_creates_auxHeaded :
      NegativeAuxiliaries.NegStrategy.negVerb.expectedInflPattern = some Typology.InflPattern.auxHeaded

      Negative verb strategy creates aux-headed AVCs.

      source
      theorem Phenomena.AuxiliaryVerbs.Studies.Anderson2006.negAffix_no_avc :
      NegativeAuxiliaries.NegStrategy.negAffix.expectedInflPattern = none

      Non-verbal negation strategies do not create AVCs.

      source
      theorem Phenomena.AuxiliaryVerbs.Studies.Anderson2006.negParticle_no_avc :
      NegativeAuxiliaries.NegStrategy.negParticle.expectedInflPattern = none

      LV Form Predictions (Anderson's Table 2.3) #

      Anderson predicts the verb form of the lexical verb from the inflectional pattern. Aux-headed AVCs have a nonfinite LV (infinitive/participle); all other patterns have a finite LV (carrying at least some inflection). This is formalized in Typology.lvVerbForm and verified here.

      source
      theorem Phenomena.AuxiliaryVerbs.Studies.Anderson2006.auxHeaded_predicts_nonfinite_lv :
      Typology.InflPattern.auxHeaded.lvVerbForm = UD.VerbForm.Inf

      Aux-headed → nonfinite LV.

      source
      theorem Phenomena.AuxiliaryVerbs.Studies.Anderson2006.lexHeaded_predicts_finite_lv :
      Typology.InflPattern.lexHeaded.lvVerbForm = UD.VerbForm.Fin

      Lex-headed → finite LV.

      source
      theorem Phenomena.AuxiliaryVerbs.Studies.Anderson2006.doubled_predicts_finite_lv :
      Typology.InflPattern.doubled.lvVerbForm = UD.VerbForm.Fin

      Doubled → finite LV.

      source
      theorem Phenomena.AuxiliaryVerbs.Studies.Anderson2006.split_predicts_finite_lv :
      Typology.InflPattern.split.lvVerbForm = UD.VerbForm.Fin

      Split → finite LV.

      source
      theorem Phenomena.AuxiliaryVerbs.Studies.Anderson2006.splitDoubled_predicts_finite_lv :
      Typology.InflPattern.splitDoubled.lvVerbForm = UD.VerbForm.Fin

      Split/doubled → finite LV.

      Bridge to Auxiliary Selection #

      Be/have auxiliary selection (Selection.lean) operates within aux-headed AVCs: the question of which auxiliary appears presupposes the auxiliary hosts inflection. All split-auxiliary languages in Selection.allData are aux-headed (the auxiliary carries tense, the LV is a past participle).

      source
      theorem Phenomena.AuxiliaryVerbs.Studies.Anderson2006.selection_presupposes_auxHeaded :
      Typology.InflPattern.auxHeaded.inflHost = Typology.AVCElement.aux

      Auxiliary selection presupposes aux-headed pattern: the selecting auxiliary hosts tense/agreement (is the inflectional head).

      source
      theorem Phenomena.AuxiliaryVerbs.Studies.Anderson2006.selection_lv_is_nonfinite :
      Typology.InflPattern.auxHeaded.lvVerbForm = UD.VerbForm.Inf

      In aux-headed AVCs with be/have selection, the LV is nonfinite (past participle). This connects Selection's selectedAux to Typology's lvVerbForm.

      source
      theorem Phenomena.AuxiliaryVerbs.Studies.Anderson2006.italian_selection_is_auxHeaded :
      Selection.italianArrivare.selectionRule = Selection.SelectionRule.split ∧ Selection.canonicalSelection Selection.italianArrivare.transitivityClass = Selection.PerfectAux.be

      Italian arrivare (Selection datum) selects be and lives in an aux-headed system where the LV is nonfinite: è arrivat-o (AUX.3SG arrive-PTCP.M.SG).