English Auxiliaries

The English auxiliaries as Auxiliary entries: the modals can, could, will, would, shall, should, may, might, must, the periphrastic have to and the semi-modals dare, need, ought, each with its force–flavor meanings and register; and the agreeing forms of do-support, be and have. The contracted negatives (can't, won't, …) are entries in their own right, carrying Polarity=Neg, paired with their bases in contractions; mayn't and amn't are paradigm gaps.

The modal adverbs (certainly, possibly, …) and the infinitival marker to also live here, since they enter the same modal-concord and control constructions.

References

• [Kra81]
• [Pal01]
• [zwicky-pullum-1983], Table 1
• [imel-guo-steinert-threlkeld-2026]

def English.Auxiliaries.can : Auxiliary

Equations

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

def English.Auxiliaries.could : Auxiliary

Equations

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

def English.Auxiliaries.will : Auxiliary

Equations

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

def English.Auxiliaries.would : Auxiliary

Equations

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

def English.Auxiliaries.shall : Auxiliary

Equations

• English.Auxiliaries.shall = { form := "shall", modality := English.Auxiliaries.cp✝ [Modality.ModalForce.necessity] [Modality.ModalFlavor.deontic], register := Features.Register.Level.formal }

def English.Auxiliaries.should : Auxiliary

Equations

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

def English.Auxiliaries.may : Auxiliary

Equations

• English.Auxiliaries.may = { form := "may", modality := English.Auxiliaries.cp✝ [Modality.ModalForce.possibility] [Modality.ModalFlavor.epistemic, Modality.ModalFlavor.deontic] }

def English.Auxiliaries.might : Auxiliary

Equations

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

def English.Auxiliaries.must : Auxiliary

Equations

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

def English.Auxiliaries.haveTo : Auxiliary

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

Equations

• English.Auxiliaries.dare = { form := "dare" }

def English.Auxiliaries.need : Auxiliary

Equations

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

def English.Auxiliaries.ought : Auxiliary

Equations

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

def English.Auxiliaries.do_ : Auxiliary

Equations

• English.Auxiliaries.do_ = { form := "do", features := English.Auxiliaries.agr✝ none (some UD.Number.Plur) }

def English.Auxiliaries.does : Auxiliary

Equations

• English.Auxiliaries.does = { form := "does", features := English.Auxiliaries.agr✝ (some UD.Person.third) (some UD.Number.Sing) }

def English.Auxiliaries.did : Auxiliary

Equations

• English.Auxiliaries.did = { form := "did", features := English.Auxiliaries.agr✝ none none (some UD.Tense.Past) }

def English.Auxiliaries.am : Auxiliary

Equations

• English.Auxiliaries.am = { form := "am", features := English.Auxiliaries.agr✝ (some UD.Person.first) (some UD.Number.Sing) }

def English.Auxiliaries.is_ : Auxiliary

Equations

• English.Auxiliaries.is_ = { form := "is", features := English.Auxiliaries.agr✝ (some UD.Person.third) (some UD.Number.Sing) }

def English.Auxiliaries.are : Auxiliary

Equations

• English.Auxiliaries.are = { form := "are", features := English.Auxiliaries.agr✝ none (some UD.Number.Plur) }

def English.Auxiliaries.was : Auxiliary

Equations

• English.Auxiliaries.was = { form := "was", features := English.Auxiliaries.agr✝ none (some UD.Number.Sing) (some UD.Tense.Past) }

def English.Auxiliaries.were : Auxiliary

Equations

• English.Auxiliaries.were = { form := "were", features := English.Auxiliaries.agr✝ none (some UD.Number.Plur) (some UD.Tense.Past) }

def English.Auxiliaries.have_ : Auxiliary

Equations

• English.Auxiliaries.have_ = { form := "have", features := English.Auxiliaries.agr✝ none (some UD.Number.Plur) }

def English.Auxiliaries.has : Auxiliary

Equations

• English.Auxiliaries.has = { form := "has", features := English.Auxiliaries.agr✝ (some UD.Person.third) (some UD.Number.Sing) }

def English.Auxiliaries.had : Auxiliary

Equations

• English.Auxiliaries.had = { form := "had", features := English.Auxiliaries.agr✝ none none (some UD.Tense.Past) }

def English.Auxiliaries.modals : List Auxiliary

The modal auxiliaries.

Equations

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

def English.Auxiliaries.doForms : List Auxiliary

The forms of do-support.

Equations

• English.Auxiliaries.doForms = [English.Auxiliaries.do_, English.Auxiliaries.does, English.Auxiliaries.did]

def English.Auxiliaries.beForms : List Auxiliary

The finite forms of be.

Equations

• English.Auxiliaries.beForms = [English.Auxiliaries.am, English.Auxiliaries.is_, English.Auxiliaries.are, English.Auxiliaries.was, English.Auxiliaries.were]

def English.Auxiliaries.haveForms : List Auxiliary

The finite forms of have.

Equations

• English.Auxiliaries.haveForms = [English.Auxiliaries.have_, English.Auxiliaries.has, English.Auxiliaries.had]

def English.Auxiliaries.allAuxiliaries : List Auxiliary

Equations

• English.Auxiliaries.allAuxiliaries = English.Auxiliaries.modals ++ English.Auxiliaries.doForms ++ English.Auxiliaries.beForms ++ English.Auxiliaries.haveForms

Contracted negatives

The -n't forms ([zwicky-pullum-1983] Table 1). mayn't and amn't are paradigm gaps and have no entry.

def English.Auxiliaries.cant : Auxiliary

Equations

• English.Auxiliaries.cant = English.Auxiliaries.contract✝ English.Auxiliaries.can "can't"

def English.Auxiliaries.couldnt : Auxiliary

Equations

• English.Auxiliaries.couldnt = English.Auxiliaries.contract✝ English.Auxiliaries.could "couldn't"

def English.Auxiliaries.wont : Auxiliary

Equations

• English.Auxiliaries.wont = English.Auxiliaries.contract✝ English.Auxiliaries.will "won't"

def English.Auxiliaries.wouldnt : Auxiliary

Equations

• English.Auxiliaries.wouldnt = English.Auxiliaries.contract✝ English.Auxiliaries.would "wouldn't"

def English.Auxiliaries.shant : Auxiliary

Equations

• English.Auxiliaries.shant = English.Auxiliaries.contract✝ English.Auxiliaries.shall "shan't"

def English.Auxiliaries.shouldnt : Auxiliary

Equations

• English.Auxiliaries.shouldnt = English.Auxiliaries.contract✝ English.Auxiliaries.should "shouldn't"

def English.Auxiliaries.mightnt : Auxiliary

Equations

• English.Auxiliaries.mightnt = English.Auxiliaries.contract✝ English.Auxiliaries.might "mightn't"

def English.Auxiliaries.mustnt : Auxiliary

Equations

• English.Auxiliaries.mustnt = English.Auxiliaries.contract✝ English.Auxiliaries.must "mustn't"

def English.Auxiliaries.darent : Auxiliary

Equations

• English.Auxiliaries.darent = English.Auxiliaries.contract✝ English.Auxiliaries.dare "daren't"

def English.Auxiliaries.neednt : Auxiliary

Equations

• English.Auxiliaries.neednt = English.Auxiliaries.contract✝ English.Auxiliaries.need "needn't"

def English.Auxiliaries.oughtnt : Auxiliary

Equations

• English.Auxiliaries.oughtnt = English.Auxiliaries.contract✝ English.Auxiliaries.ought "oughtn't"

def English.Auxiliaries.dont : Auxiliary

Equations

• English.Auxiliaries.dont = English.Auxiliaries.contract✝ English.Auxiliaries.do_ "don't"

def English.Auxiliaries.doesnt : Auxiliary

Equations

• English.Auxiliaries.doesnt = English.Auxiliaries.contract✝ English.Auxiliaries.does "doesn't"

def English.Auxiliaries.didnt : Auxiliary

Equations

• English.Auxiliaries.didnt = English.Auxiliaries.contract✝ English.Auxiliaries.did "didn't"

def English.Auxiliaries.isnt : Auxiliary

Equations

• English.Auxiliaries.isnt = English.Auxiliaries.contract✝ English.Auxiliaries.is_ "isn't"

def English.Auxiliaries.arent : Auxiliary

Equations

• English.Auxiliaries.arent = English.Auxiliaries.contract✝ English.Auxiliaries.are "aren't"

def English.Auxiliaries.wasnt : Auxiliary

Equations

• English.Auxiliaries.wasnt = English.Auxiliaries.contract✝ English.Auxiliaries.was "wasn't"

def English.Auxiliaries.werent : Auxiliary

Equations

• English.Auxiliaries.werent = English.Auxiliaries.contract✝ English.Auxiliaries.were "weren't"

def English.Auxiliaries.havent : Auxiliary

Equations

• English.Auxiliaries.havent = English.Auxiliaries.contract✝ English.Auxiliaries.have_ "haven't"

def English.Auxiliaries.hasnt : Auxiliary

Equations

• English.Auxiliaries.hasnt = English.Auxiliaries.contract✝ English.Auxiliaries.has "hasn't"

def English.Auxiliaries.hadnt : Auxiliary

Equations

• English.Auxiliaries.hadnt = English.Auxiliaries.contract✝ English.Auxiliaries.had "hadn't"

def English.Auxiliaries.negatives : List Auxiliary

The contracted negatives.

Equations

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

def English.Auxiliaries.contractions : List (Auxiliary × Auxiliary)

Each auxiliary paired with its contracted negative.

Equations

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

def English.Auxiliaries.negative (a : Auxiliary) : Option Auxiliary

The contracted negative of an auxiliary, if it has one.

Equations

• English.Auxiliaries.negative a = Option.map (fun (x : Auxiliary × Auxiliary) => x.2) (List.find? (fun (x : Auxiliary × Auxiliary) => x.1 == a) English.Auxiliaries.contractions)

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 Modality.ForceFlavor

  Modal meaning in the force-flavor space.

• register : Features.Register.Level

  Register level.

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

Equations

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

@[instance_reducible]

instance English.Auxiliaries.instReprModalAdvEntry : Repr ModalAdvEntry

Equations

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

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

@[instance_reducible]

instance English.Auxiliaries.instBEqModalAdvEntry : BEq ModalAdvEntry

Equations

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

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

Equations

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

def English.Auxiliaries.ModalAdvEntry.toModalItem (a : ModalAdvEntry) : 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✝ [Modality.ModalForce.possibility] [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✝ [Modality.ModalForce.necessity] [Modality.ModalFlavor.epistemic] }

def English.Auxiliaries.potentially : ModalAdvEntry

Equations

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

def English.Auxiliaries.allModalAdverbs : List ModalAdvEntry

Equations

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

def English.Auxiliaries.toInf : Morphology.Word

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

Equations

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