English Auxiliaries Lexicon Fragment

Lexical entries for English auxiliary verbs — the modal hub of the English Fragment. Three integrated sub-inventories:

• Modals: can, could, will, would, shall, should, may, might, must; periphrastic haveTo; semi-modals dare, need, ought. Morphology + force-flavor classification + register
  • contracted-negative form + Zeijlstra-style modal feature interpretability.
• Do-support / Be / Have: do_/does/did, am/is_/are/ was/were, have_/has/had. Carry person/number/tense agreement.
• Modal adverbs: certainly, definitely, necessarily, possibly, perhaps, maybe, probably, potentially. Adverbial expressions of modal force/flavor (used with auxiliaries in modal concord constructions).

Also includes the infinitival marker toInf (PART) — distinct from the preposition to (ADP).

Studies that bind to these entries

This file is a hub: studies analysing English auxiliaries import specific entries from here and contribute precondition theorems that break if the morphological classification changes. Consumers (as of the last audit):

• Word-order / inversion: Phenomena/WordOrder/Studies/{SagWasowBender2003, Adger2003}, Theories/Syntax/Minimalism/Inversion.lean, Theories/Syntax/HPSG/Inversion.lean
• Modality: Phenomena/Modality/Studies/{Ferreira2023, Rubinstein2014, CarianiSantorio2018, AghaJeretic2022, AghaJeretic2026, CiardelliGuerrini2026, ImelGuoST2026, LiuRotter2025, RotterLiu2025Concord, YingEtAl2025}
• Auxiliary diagnostics: Phenomena/AuxiliaryVerbs/{Diagnostics, Typology}, Phenomena/Morphology/Studies/ZwickyPullum1983
• Argument structure / control: Phenomena/ArgumentStructure/Studies/ Osborne2019, Phenomena/Complementation/Studies/Osborne2019Control
• Reference: Phenomena/Reference/Studies/Percus2000 (via modal-adverb side, indirectly)

To find every claim made about a particular entry, grep for Fragments.English.Auxiliaries.<entry> across Phenomena/ and Theories/.

inductive Fragments.English.Auxiliaries.AuxType : Type

Auxiliary type

• modal : AuxType
• doSupport : AuxType
• be : AuxType
• have : AuxType

@[implicit_reducible]

instance Fragments.English.Auxiliaries.instDecidableEqAuxType : DecidableEq AuxType

Equations

• Fragments.English.Auxiliaries.instDecidableEqAuxType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Fragments.English.Auxiliaries.instReprAuxType.repr : AuxType → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Fragments.English.Auxiliaries.instReprAuxType : Repr AuxType

Equations

• Fragments.English.Auxiliaries.instReprAuxType = { reprPrec := Fragments.English.Auxiliaries.instReprAuxType.repr }

structure Fragments.English.Auxiliaries.AuxEntry : Type

• form : String
• auxType : AuxType
• person : Option Person

  Person/number agreement

• number : Option Number
• tense : Option UD.Tense

  Morphological tense. none for base forms (modals like can, will). Note: "past" modals (could, would) carry Past as a morphological feature even when semantically non-past (counterfactual, polite).

• modalMeaning : List Core.Modality.ForceFlavor

  Modal meaning in the force-flavor space (Imel, Guo, & @cite{imel-guo-steinert-threlkeld-2026}). Empty for non-modal auxiliaries.

• register : Features.Register.Level

  Register level. Formal items (must, shall) vs informal items (have to) vs unmarked (can, will).

• negForm : Option String

  Contracted negative form with -n't, if it exists. none for paradigm gaps (mayn't, amn't).

• negIrregular : Bool

  Phonological irregularity in the negative form (Z&P criterion C). true when the contracted form cannot be derived by regular -n't suffixation (e.g., won't ← will, can't ← can, don't ← do).

• interpretability : Option Core.Modality.ModalInterpretability

  Modal feature interpretability (@cite{zeijlstra-2007}). Modal auxiliaries carry uninterpretable features [u∃/∀-MOD]: they are semantically vacuous and checked by a c-commanding interpretable operator. Non-modal auxiliaries (do, be, have) carry no modal feature (none).

  @cite{ciardelli-guerrini-2026} use this to derive narrow-scope LFs for "may A or may B" via modal concord: both "may"s carry [u∃-MOD], checked by a single silent [i∃-MOD] operator.

@[implicit_reducible]

instance Fragments.English.Auxiliaries.instReprAuxEntry : Repr AuxEntry

Equations

• Fragments.English.Auxiliaries.instReprAuxEntry = { reprPrec := Fragments.English.Auxiliaries.instReprAuxEntry.repr }

def Fragments.English.Auxiliaries.instReprAuxEntry.repr : AuxEntry → ℕ → Std.Format

Equations

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

def Fragments.English.Auxiliaries.instBEqAuxEntry.beq : AuxEntry → AuxEntry → Bool

Equations

• One or more equations did not get rendered due to their size.
• Fragments.English.Auxiliaries.instBEqAuxEntry.beq x✝¹ x✝ = false

@[implicit_reducible]

instance Fragments.English.Auxiliaries.instBEqAuxEntry : BEq AuxEntry

Equations

• Fragments.English.Auxiliaries.instBEqAuxEntry = { beq := Fragments.English.Auxiliaries.instBEqAuxEntry.beq }

def Fragments.English.Auxiliaries.can : AuxEntry

Equations

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

def Fragments.English.Auxiliaries.could : AuxEntry

Equations

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

def Fragments.English.Auxiliaries.will : AuxEntry

Equations

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

def Fragments.English.Auxiliaries.would : AuxEntry

Equations

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

def Fragments.English.Auxiliaries.shall : AuxEntry

Equations

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

def Fragments.English.Auxiliaries.should : AuxEntry

Equations

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

def Fragments.English.Auxiliaries.may : AuxEntry

Equations

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

def Fragments.English.Auxiliaries.might : AuxEntry

Equations

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

def Fragments.English.Auxiliaries.must : AuxEntry

Equations

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

def Fragments.English.Auxiliaries.haveTo : AuxEntry

Have to: periphrastic deontic/circumstantial necessity. Informal register variant of must. Inflects unlike true modals: has to, had to, having to.

Equations

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

def Fragments.English.Auxiliaries.dare : AuxEntry

Equations

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

def Fragments.English.Auxiliaries.need : AuxEntry

Equations

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

def Fragments.English.Auxiliaries.ought : AuxEntry

Equations

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

def Fragments.English.Auxiliaries.do_ : AuxEntry

Equations

• Fragments.English.Auxiliaries.do_ = { form := "do", auxType := Fragments.English.Auxiliaries.AuxType.doSupport, number := some Number.pl, negForm := some "don't", negIrregular := true }

def Fragments.English.Auxiliaries.does : AuxEntry

Equations

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

def Fragments.English.Auxiliaries.did : AuxEntry

Equations

• Fragments.English.Auxiliaries.did = { form := "did", auxType := Fragments.English.Auxiliaries.AuxType.doSupport, tense := some UD.Tense.Past, negForm := some "didn't" }

def Fragments.English.Auxiliaries.am : AuxEntry

Equations

• Fragments.English.Auxiliaries.am = { form := "am", auxType := Fragments.English.Auxiliaries.AuxType.be, person := some UD.Person.first, number := some Number.sg }

def Fragments.English.Auxiliaries.is_ : AuxEntry

Equations

• Fragments.English.Auxiliaries.is_ = { form := "is", auxType := Fragments.English.Auxiliaries.AuxType.be, person := some UD.Person.third, number := some Number.sg, negForm := some "isn't" }

def Fragments.English.Auxiliaries.are : AuxEntry

Equations

• Fragments.English.Auxiliaries.are = { form := "are", auxType := Fragments.English.Auxiliaries.AuxType.be, number := some Number.pl, negForm := some "aren't" }

def Fragments.English.Auxiliaries.was : AuxEntry

Equations

• Fragments.English.Auxiliaries.was = { form := "was", auxType := Fragments.English.Auxiliaries.AuxType.be, number := some Number.sg, tense := some UD.Tense.Past, negForm := some "wasn't" }

def Fragments.English.Auxiliaries.were : AuxEntry

Equations

• Fragments.English.Auxiliaries.were = { form := "were", auxType := Fragments.English.Auxiliaries.AuxType.be, number := some Number.pl, tense := some UD.Tense.Past, negForm := some "weren't" }

def Fragments.English.Auxiliaries.have_ : AuxEntry

Equations

• Fragments.English.Auxiliaries.have_ = { form := "have", auxType := Fragments.English.Auxiliaries.AuxType.have, number := some Number.pl, negForm := some "haven't" }

def Fragments.English.Auxiliaries.has : AuxEntry

Equations

• Fragments.English.Auxiliaries.has = { form := "has", auxType := Fragments.English.Auxiliaries.AuxType.have, person := some UD.Person.third, number := some Number.sg, negForm := some "hasn't" }

def Fragments.English.Auxiliaries.had : AuxEntry

Equations

• Fragments.English.Auxiliaries.had = { form := "had", auxType := Fragments.English.Auxiliaries.AuxType.have, tense := some UD.Tense.Past, negForm := some "hadn't" }

def Fragments.English.Auxiliaries.allAuxiliaries : List AuxEntry

Equations

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

def Fragments.English.Auxiliaries.AuxEntry.toWord (a : AuxEntry) : Word

Equations

• a.toWord = { form := a.form, cat := UD.UPOS.AUX, features := { number := a.number, person := a.person } }

def Fragments.English.Auxiliaries.AuxEntry.toModalItem (a : AuxEntry) : Core.Modality.ModalItem

Project to the shared modal item core (form + meaning + register).

Equations

• a.toModalItem = { form := a.form, meaning := a.modalMeaning, register := a.register }

def Fragments.English.Auxiliaries.AuxEntry.toModalFeature (a : AuxEntry) : Option Core.Modality.ModalFeature

Project to the modal feature (force × interpretability) for the primary force value. Returns none for non-modal auxiliaries or entries without modal meaning.

Equations

• a.toModalFeature = match a.interpretability, a.modalMeaning with | some interp, ff :: tail => some { force := ff.force, interp := interp } | x, x_1 => none

structure Fragments.English.Auxiliaries.ModalAdvEntry : Type

Modal adverb entry: an adverb expressing modal force and flavor without auxiliary morphology.

Modal adverbs participate in concord constructions where two modal expressions yield a single-modality reading.

• form : String
• modalMeaning : List Core.Modality.ForceFlavor

  Modal meaning in the force-flavor space.

• register : Features.Register.Level

  Register level.

@[implicit_reducible]

instance Fragments.English.Auxiliaries.instReprModalAdvEntry : Repr ModalAdvEntry

Equations

• Fragments.English.Auxiliaries.instReprModalAdvEntry = { reprPrec := Fragments.English.Auxiliaries.instReprModalAdvEntry.repr }

def Fragments.English.Auxiliaries.instReprModalAdvEntry.repr : ModalAdvEntry → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Fragments.English.Auxiliaries.instBEqModalAdvEntry : BEq ModalAdvEntry

Equations

• Fragments.English.Auxiliaries.instBEqModalAdvEntry = { beq := Fragments.English.Auxiliaries.instBEqModalAdvEntry.beq }

def Fragments.English.Auxiliaries.instBEqModalAdvEntry.beq : ModalAdvEntry → ModalAdvEntry → Bool

Equations

• One or more equations did not get rendered due to their size.
• Fragments.English.Auxiliaries.instBEqModalAdvEntry.beq x✝¹ x✝ = false

def Fragments.English.Auxiliaries.ModalAdvEntry.toWord (a : ModalAdvEntry) : Word

Equations

• a.toWord = { form := a.form, cat := UD.UPOS.ADV }

def Fragments.English.Auxiliaries.ModalAdvEntry.toModalItem (a : ModalAdvEntry) : Core.Modality.ModalItem

Project to the shared modal item core (form + meaning + register).

Equations

• a.toModalItem = { form := a.form, meaning := a.modalMeaning, register := a.register }

def Fragments.English.Auxiliaries.certainly : ModalAdvEntry

Equations

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

def Fragments.English.Auxiliaries.definitely : ModalAdvEntry

Equations

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

def Fragments.English.Auxiliaries.necessarily : ModalAdvEntry

Equations

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

def Fragments.English.Auxiliaries.possibly : ModalAdvEntry

Equations

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

def Fragments.English.Auxiliaries.perhaps : ModalAdvEntry

Equations

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

def Fragments.English.Auxiliaries.maybe : ModalAdvEntry

Equations

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

def Fragments.English.Auxiliaries.probably : ModalAdvEntry

Equations

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

def Fragments.English.Auxiliaries.potentially : ModalAdvEntry

Equations

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

def Fragments.English.Auxiliaries.allModalAdverbs : List ModalAdvEntry

Equations

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

def Fragments.English.Auxiliaries.toInf : Word

Infinitival marker "to" (UD: PART). Distinct from the preposition "to" (ADP). Used in infinitival complements: "John managed to sleep".

Equations

• Fragments.English.Auxiliaries.toInf = Word.mk' "to" UD.UPOS.PART