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):

• Modality: Studies/{Ferreira2023, Rubinstein2014, CarianiSantorio2018, AghaJeretic2022, AghaJeretic2026, CiardelliGuerrini2026, ImelGuoST2026, LiuRotter2025, RotterLiu2025, YingEtAl2025}
• Auxiliary diagnostics: Studies/ZwickyPullum1983
• Argument structure / control: Studies/ Osborne2019, Studies/Osborne2019Control
• Reference: Studies/Percus2000 (via modal-adverb side, indirectly)

To find every claim made about a particular entry, grep for English.Auxiliaries.<entry> across the library.

inductive English.Auxiliaries.AuxType : Type

Auxiliary type

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

@[implicit_reducible]

instance English.Auxiliaries.instDecidableEqAuxType : DecidableEq AuxType

Equations

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

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

Equations

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

@[implicit_reducible]

instance English.Auxiliaries.instReprAuxType : Repr AuxType

Equations

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

structure English.Auxiliaries.AuxEntry : Type

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

  Person/number agreement

• number : Option UD.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 Semantics.Modality.ForceFlavor

  Modal meaning in the force-flavor space (Imel, Guo, & [IGST26]). 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 Semantics.Modality.ModalInterpretability

  Modal feature interpretability ([Zei07]). 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).

  [CG26] 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 English.Auxiliaries.instReprAuxEntry : Repr AuxEntry

Equations

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

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

Equations

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

@[implicit_reducible]

instance English.Auxiliaries.instBEqAuxEntry : BEq AuxEntry

Equations

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

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

Equations

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

@[implicit_reducible]

instance English.Auxiliaries.instHasNumberAuxEntry : HasNumber AuxEntry

An auxiliary bears its agreement number (HasNumber).

Equations

• English.Auxiliaries.instHasNumberAuxEntry = { numberOf := fun (a : English.Auxiliaries.AuxEntry) => a.number.bind Number.fromUD }

@[implicit_reducible]

instance English.Auxiliaries.instHasPersonAuxEntry : HasPerson AuxEntry

Equations

• English.Auxiliaries.instHasPersonAuxEntry = { personOf := fun (a : English.Auxiliaries.AuxEntry) => Option.map Person.fromUD a.person }

def English.Auxiliaries.can : AuxEntry

Equations

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

def English.Auxiliaries.could : AuxEntry

Equations

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

def English.Auxiliaries.will : AuxEntry

Equations

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

def English.Auxiliaries.would : AuxEntry

Equations

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

def English.Auxiliaries.shall : AuxEntry

Equations

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

def English.Auxiliaries.should : AuxEntry

Equations

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

def English.Auxiliaries.may : AuxEntry

Equations

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

def English.Auxiliaries.might : AuxEntry

Equations

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

def English.Auxiliaries.must : AuxEntry

Equations

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

def 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 English.Auxiliaries.dare : AuxEntry

Equations

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

def English.Auxiliaries.need : AuxEntry

Equations

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

def English.Auxiliaries.ought : AuxEntry

Equations

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

def English.Auxiliaries.do_ : AuxEntry

Equations

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

def English.Auxiliaries.does : AuxEntry

Equations

• English.Auxiliaries.does = { form := "does", auxType := English.Auxiliaries.AuxType.doSupport, person := some UD.Person.third, number := some UD.Number.Sing, negForm := some "doesn't" }

def English.Auxiliaries.did : AuxEntry

Equations

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

def English.Auxiliaries.am : AuxEntry

Equations

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

def English.Auxiliaries.is_ : AuxEntry

Equations

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

def English.Auxiliaries.are : AuxEntry

Equations

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

def English.Auxiliaries.was : AuxEntry

Equations

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

def English.Auxiliaries.were : AuxEntry

Equations

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

def English.Auxiliaries.have_ : AuxEntry

Equations

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

def English.Auxiliaries.has : AuxEntry

Equations

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

def English.Auxiliaries.had : AuxEntry

Equations

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

def English.Auxiliaries.allAuxiliaries : List AuxEntry

Equations

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

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

Equations

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

def English.Auxiliaries.AuxEntry.toModalItem (a : AuxEntry) : Semantics.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 English.Auxiliaries.AuxEntry.toModalFeature (a : AuxEntry) : Option Semantics.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 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 Semantics.Modality.ForceFlavor

  Modal meaning in the force-flavor space.

• register : Features.Register.Level

  Register level.

@[implicit_reducible]

instance English.Auxiliaries.instReprModalAdvEntry : Repr ModalAdvEntry

Equations

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

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

Equations

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

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

Equations

• English.Auxiliaries.instBEqModalAdvEntry.beq { form := a, modalMeaning := a_1, register := a_2 } { form := b, modalMeaning := b_1, register := b_2 } = (a == b && (a_1 == b_1 && a_2 == b_2))
• English.Auxiliaries.instBEqModalAdvEntry.beq x✝¹ x✝ = false

@[implicit_reducible]

instance English.Auxiliaries.instBEqModalAdvEntry : BEq ModalAdvEntry

Equations

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

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

Equations

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

def English.Auxiliaries.ModalAdvEntry.toModalItem (a : ModalAdvEntry) : Semantics.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 English.Auxiliaries.certainly : ModalAdvEntry

Equations

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

def English.Auxiliaries.definitely : ModalAdvEntry

Equations

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

def English.Auxiliaries.necessarily : ModalAdvEntry

Equations

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

def English.Auxiliaries.possibly : ModalAdvEntry

Equations

• English.Auxiliaries.possibly = { form := "possibly", modalMeaning := English.Auxiliaries.mcp✝ [Semantics.Modality.ModalForce.possibility] [Semantics.Modality.ModalFlavor.epistemic] }

def English.Auxiliaries.perhaps : ModalAdvEntry

Equations

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

def English.Auxiliaries.maybe : ModalAdvEntry

Equations

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

def English.Auxiliaries.probably : ModalAdvEntry

Equations

• English.Auxiliaries.probably = { form := "probably", modalMeaning := English.Auxiliaries.mcp✝ [Semantics.Modality.ModalForce.necessity] [Semantics.Modality.ModalFlavor.epistemic] }

def English.Auxiliaries.potentially : ModalAdvEntry

Equations

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

def English.Auxiliaries.allModalAdverbs : List ModalAdvEntry

Equations

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

def English.Auxiliaries.toInf : Word

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

Equations

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