German Modal Verb Fragment

Lexical entries for German modal verbs; like English AuxEntry, they instance the Auxiliary word-class category.

German has six core modals, each with fixed force and contextually variable flavor. All modal meanings are Cartesian products (force × flavors), so they all satisfy IFF.

Modal	3sg	Force	Flavors
können	kann	possibility	epistemic, circumstantial
dürfen	darf	possibility	deontic
müssen	muss	necessity	epistemic, deontic
sollen	soll	necessity	deontic
mögen	mag	possibility	epistemic
wollen	will	necessity	bouletic

Reference: Kratzer, A. (1981). The Notional Category of Modality.

structure German.Predicates.Modal.GermanModalEntry : Type

German modal verb entry.

• form : String

  Infinitive form

• form3sg : String

  3sg present form

• modalMeaning : List Modality.ForceFlavor

  Modal meaning as force-flavor pairs

@[instance_reducible]

instance German.Predicates.Modal.instReprGermanModalEntry : Repr GermanModalEntry

Equations

• German.Predicates.Modal.instReprGermanModalEntry = { reprPrec := German.Predicates.Modal.instReprGermanModalEntry.repr }

def German.Predicates.Modal.instReprGermanModalEntry.repr : GermanModalEntry → ℕ → Std.Format

Equations

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

def German.Predicates.Modal.instBEqGermanModalEntry.beq : GermanModalEntry → GermanModalEntry → Bool

Equations

• One or more equations did not get rendered due to their size.
• German.Predicates.Modal.instBEqGermanModalEntry.beq x✝¹ x✝ = false

@[instance_reducible]

instance German.Predicates.Modal.instBEqGermanModalEntry : BEq GermanModalEntry

Equations

• German.Predicates.Modal.instBEqGermanModalEntry = { beq := German.Predicates.Modal.instBEqGermanModalEntry.beq }

@[instance_reducible]

instance German.Predicates.Modal.instAuxiliaryGermanModalEntry : Auxiliary GermanModalEntry

Every German modal projects to a UD AUX word (cited by its infinitive).

Equations

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

def German.Predicates.Modal.koennen : GermanModalEntry

können — "can/may": epistemic + circumstantial possibility.

Equations

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

def German.Predicates.Modal.duerfen : GermanModalEntry

dürfen — "may/be allowed to": deontic possibility.

Equations

• German.Predicates.Modal.duerfen = { form := "dürfen", form3sg := "darf", modalMeaning := German.Predicates.Modal.cp✝ [Modality.ModalForce.possibility] [Modality.ModalFlavor.deontic] }

def German.Predicates.Modal.muessen : GermanModalEntry

müssen — "must/have to": epistemic + deontic necessity.

Equations

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

def German.Predicates.Modal.sollen : GermanModalEntry

sollen — "should/be supposed to": deontic necessity.

Equations

• German.Predicates.Modal.sollen = { form := "sollen", form3sg := "soll", modalMeaning := German.Predicates.Modal.cp✝ [Modality.ModalForce.necessity] [Modality.ModalFlavor.deontic] }

def German.Predicates.Modal.moegen : GermanModalEntry

mögen — "may" (epistemic): epistemic possibility.

Equations

• German.Predicates.Modal.moegen = { form := "mögen", form3sg := "mag", modalMeaning := German.Predicates.Modal.cp✝ [Modality.ModalForce.possibility] [Modality.ModalFlavor.epistemic] }

def German.Predicates.Modal.wollen : GermanModalEntry

wollen — "want to": bouletic necessity.

Equations

• German.Predicates.Modal.wollen = { form := "wollen", form3sg := "will", modalMeaning := German.Predicates.Modal.cp✝ [Modality.ModalForce.necessity] [Modality.ModalFlavor.bouletic] }

def German.Predicates.Modal.sollte : GermanModalEntry

sollte — Konjunktiv II of sollen: weak necessity across multiple flavors. Treated as a separate modal from sollen because it has complex morphology (root + Konj. II), following the morphological individuation criterion of [STIG23] §4.3. Both soll and sollte individually satisfy IFF.

Equations

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

def German.Predicates.Modal.allModals : List GermanModalEntry

Equations

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

theorem German.Predicates.Modal.koennen_is_possibility : koennen.modalMeaning = German.Predicates.Modal.cp✝ [Modality.ModalForce.possibility] [Modality.ModalFlavor.epistemic, Modality.ModalFlavor.circumstantial]

können is possibility.

theorem German.Predicates.Modal.muessen_is_necessity : muessen.modalMeaning = German.Predicates.Modal.cp✝ [Modality.ModalForce.necessity] [Modality.ModalFlavor.epistemic, Modality.ModalFlavor.deontic]

müssen is necessity.

theorem German.Predicates.Modal.duerfen_is_deontic : duerfen.modalMeaning = German.Predicates.Modal.cp✝ [Modality.ModalForce.possibility] [Modality.ModalFlavor.deontic]

dürfen is deontic possibility only.

theorem German.Predicates.Modal.sollen_deontic : sollen.modalMeaning = German.Predicates.Modal.cp✝ [Modality.ModalForce.necessity] [Modality.ModalFlavor.deontic]

sollen is deontic necessity; wollen is bouletic necessity.

theorem German.Predicates.Modal.wollen_bouletic : wollen.modalMeaning = German.Predicates.Modal.cp✝ [Modality.ModalForce.necessity] [Modality.ModalFlavor.bouletic]

theorem German.Predicates.Modal.sollte_wider_than_sollen : sollte.modalMeaning.length > sollen.modalMeaning.length

sollte has wider flavor range than sollen (morphological flavor change).

theorem German.Predicates.Modal.allModals_size : allModals.length = 7

Seven modals total (including sollte as distinct from sollen).