Directive Modality: Strong and Weak Necessity

@cite{kratzer-2012} @cite{von-fintel-iatridou-2008}

@cite{von-fintel-iatridou-2008} argue that natural languages systematically distinguish strong necessity ("must", "have to") from weak necessity ("ought", "should"). The difference is not in modal force — both are universal quantifiers over best worlds — but in the ordering source.

Core Analysis

Strong and weak necessity share the same modal base (circumstantial) but differ in ordering:

• Strong necessity (must φ): necessity under ordering g
• Weak necessity (ought φ): necessity under refined ordering g ∪ g'

The secondary ordering g' adds criteria beyond the primary norms, creating a more discriminating ranking. More criteria → smaller "best" set → the universal quantification is over a subset, making it a weaker (easier to satisfy) claim.

Key Result

strong_entails_weak: strong necessity entails weak necessity. If all g-best worlds have φ, then all (g∪g')-best worlds have φ, because the refined best set is a subset of the original.

weak_not_entails_strong: the converse fails. A concrete counterexample shows that refining the ordering can eliminate a world where φ fails, making weak necessity hold while strong necessity does not.

Connection to Kratzer Framework

Strong necessity IS Kratzer's standard necessity from Kratzer.lean. Weak necessity adds a secondary ordering source via combineOrdering. The DeonticStrength structure pairs primary and secondary norms, bridging to DeonticFlavor.

Combined ordering sources

def Semantics.Modality.Directive.combineOrdering (g₁ g₂ : Kratzer.OrderingSource) : Kratzer.OrderingSource

Combine two ordering sources by concatenation. The combined source g₁ ∪ g₂ yields the union of ideals from both.

Equations

• Semantics.Modality.Directive.combineOrdering g₁ g₂ w = g₁ w ++ g₂ w

theorem Semantics.Modality.Directive.primary_sub_combined (g g' : Kratzer.OrderingSource) (w : Attitudes.Intensional.World) (p : BProp Attitudes.Intensional.World) : p ∈ g w → p ∈ combineOrdering g g' w

The primary ordering is contained in the combined one: every ideal in g is also in g ∪ g'.

theorem Semantics.Modality.Directive.combine_empty_right (g : Kratzer.OrderingSource) (w : Attitudes.Intensional.World) : combineOrdering g Kratzer.emptyBackground w = g w

Combining with empty ordering preserves the original.

Strong and weak necessity

def Semantics.Modality.Directive.strongNecessity (f : Kratzer.ModalBase) (g : Kratzer.OrderingSource) (p : BProp Attitudes.Intensional.World) (w : Attitudes.Intensional.World) : Bool

Strong necessity ("must φ"): standard Kratzer necessity under modal base f and ordering source g.

Equations

• Semantics.Modality.Directive.strongNecessity f g p w = Semantics.Modality.Kratzer.necessity f g p w

def Semantics.Modality.Directive.weakNecessity (f : Kratzer.ModalBase) (g g' : Kratzer.OrderingSource) (p : BProp Attitudes.Intensional.World) (w : Attitudes.Intensional.World) : Bool

Weak necessity ("ought φ"): Kratzer necessity under modal base f and a refined ordering g ∪ g', where g' is a secondary ordering source (e.g., stereotypical expectations beyond strict norms).

Equations

• Semantics.Modality.Directive.weakNecessity f g g' p w = Semantics.Modality.Kratzer.necessity f (Semantics.Modality.Directive.combineOrdering g g') p w

Ordering extension lemma

Best worlds monotonicity

theorem Semantics.Modality.Directive.best_refines (f : Kratzer.ModalBase) (g g' : Kratzer.OrderingSource) (w w' : Attitudes.Intensional.World) : w' ∈ Kratzer.bestWorlds f (combineOrdering g g') w → w' ∈ Kratzer.bestWorlds f g w

Refining the ordering can only shrink the set of best worlds.

Best(f, g∪g') ⊆ Best(f, g): adding criteria to the ordering eliminates worlds that were previously tied. A world that dominates all others under the more discriminating ordering a fortiori dominates under the coarser one.

Main entailment

theorem Semantics.Modality.Directive.strong_entails_weak (f : Kratzer.ModalBase) (g g' : Kratzer.OrderingSource) (p : BProp Attitudes.Intensional.World) (w : Attitudes.Intensional.World) (h : strongNecessity f g p w = true) : weakNecessity f g g' p w = true

Strong entails weak: if "must φ" holds (under ordering g), then "ought φ" holds (under any refinement g ∪ g').

∀w' ∈ Best(f,g). φ(w') → ∀w' ∈ Best(f, g∪g'). φ(w')

This captures the linguistic intuition: "must φ" is a stronger claim than "ought φ" — the former entails the latter but not vice versa.

The converse fails

theorem Semantics.Modality.Directive.weak_not_entails_strong : ¬∀ (f : Kratzer.ModalBase) (g g' : Kratzer.OrderingSource) (p : BProp Attitudes.Intensional.World) (w : Attitudes.Intensional.World), weakNecessity f g g' p w = true → strongNecessity f g p w = true

Weak necessity does NOT entail strong necessity.

Counterexample: g-best worlds are {w0, w1}. The secondary ordering g' distinguishes them, making w1 strictly better. Under g∪g', only w1 is best. If p holds at w1 but not w0, weak necessity holds but strong necessity fails.

Deontic application

structure Semantics.Modality.Directive.DeonticStrength : Type

A deontic scenario with strong and weak norms.

Contains a DeonticFlavor (circumstantial base + primary norms) and adds a secondary ordering source for weak necessity. This makes the structural relationship to Kratzer's framework explicit: strong necessity IS the primary DeonticFlavor; weak necessity refines it.

• Primary norms g (via DeonticFlavor): legal/institutional obligations
• Secondary norms g': social expectations, stereotypical behavior

"Must" quantifies over worlds satisfying legal obligations; "ought" further refines by social expectations.

• primary : Kratzer.DeonticFlavor

  The primary deontic scenario (circumstantial base + primary norms)

• secondaryNorms : Kratzer.OrderingSource

  Secondary norms (social, stereotypical)

def Semantics.Modality.Directive.DeonticStrength.must (d : DeonticStrength) (p : BProp Attitudes.Intensional.World) (w : Attitudes.Intensional.World) : Bool

Strong deontic necessity: "You must do X" (legal obligation).

Equations

• d.must p w = Semantics.Modality.Directive.strongNecessity d.primary.circumstances d.primary.norms p w

def Semantics.Modality.Directive.DeonticStrength.ought (d : DeonticStrength) (p : BProp Attitudes.Intensional.World) (w : Attitudes.Intensional.World) : Bool

Weak deontic necessity: "You ought to do X" (refined by social norms).

Equations

• d.ought p w = Semantics.Modality.Directive.weakNecessity d.primary.circumstances d.primary.norms d.secondaryNorms p w

theorem Semantics.Modality.Directive.deontic_must_eq_kratzer (d : Kratzer.DeonticFlavor) (p : BProp Attitudes.Intensional.World) (w : Attitudes.Intensional.World) : Kratzer.necessity d.circumstances d.norms p w = strongNecessity d.circumstances d.norms p w

Bridge to Kratzer's DeonticFlavor: strong necessity with DeonticFlavor is exactly standard Kratzer necessity.

theorem Semantics.Modality.Directive.deontic_must_entails_ought (d : DeonticStrength) (p : BProp Attitudes.Intensional.World) (w : Attitudes.Intensional.World) (h : d.must p w = true) : d.ought p w = true

Must entails ought for any deontic scenario.

theorem Semantics.Modality.Directive.weak_eq_strong_no_secondary (f : Kratzer.ModalBase) (g : Kratzer.OrderingSource) (p : BProp Attitudes.Intensional.World) (w : Attitudes.Intensional.World) : weakNecessity f g Kratzer.emptyBackground p w = strongNecessity f g p w

With no secondary norms, weak necessity reduces to strong necessity.

Bridge: Kratzer semantics ↔ typological force

The typological ModalForce.weakNecessity corresponds to Kratzer's necessity evaluated with a refined ordering source (g ∪ g'). Strong necessity is necessity with the primary ordering source alone. The entailment chain □ → □w → ◇ is the semantic content of ModalForce.atLeastAsStrong.

theorem Semantics.Modality.Directive.strongNecessity_is_necessity (f : Kratzer.ModalBase) (g : Kratzer.OrderingSource) (p : BProp Attitudes.Intensional.World) (w : Attitudes.Intensional.World) : strongNecessity f g p w = (Kratzer.KratzerTheory { base := f, ordering := g }).eval Core.Modality.ModalForce.necessity p w

Strong necessity under Kratzer params IS ModalForce.necessity.

theorem Semantics.Modality.Directive.weakNecessity_is_weakForce (f : Kratzer.ModalBase) (g g' : Kratzer.OrderingSource) (p : BProp Attitudes.Intensional.World) (w : Attitudes.Intensional.World) : weakNecessity f g g' p w = (Kratzer.KratzerTheory { base := f, ordering := combineOrdering g g' }).eval Core.Modality.ModalForce.weakNecessity p w

Weak necessity under Kratzer params with refinement IS ModalForce.weakNecessity evaluated under combined ordering.