Directive Modality: Strong and Weak Necessity

[Kra12] [vFI08]

[vFI08] 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 over the g'-best of the g-best worlds

The secondary ordering g' selects within the primary best set — the lexicographic refinement of [Kra81]'s Conclusion, where later ordering sources undo the ties left by their predecessors. Selecting within a set can only shrink it, so the universal quantification is over a subset, making the claim weaker (easier to satisfy).

Key Result

strong_entails_weak: strong necessity entails weak necessity, since the g'-best of the g-best worlds are g-best (bestAmong_sub).

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 Modality.Directive.combineOrdering {W : Type u_1} (g₁ g₂ : Kratzer.OrderingSource W) : Kratzer.OrderingSource W

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

Equations

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

theorem Modality.Directive.primary_sub_combined {W : Type u_1} (g g' : Kratzer.OrderingSource W) (w : W) (p : W → Prop) : p ∈ g w → p ∈ combineOrdering g g' w

The primary ordering is contained in the combined one.

theorem Modality.Directive.combine_empty_right {W : Type u_1} (g : Kratzer.OrderingSource W) (w : W) : combineOrdering g Kratzer.emptyBackground w = g w

Combining with empty ordering preserves the original.

Strong and weak necessity

def Modality.Directive.strongNecessity {W : Type u_1} (f : Kratzer.ModalBase W) (g : Kratzer.OrderingSource W) (p : W → Prop) (w : W) : Prop

Strong necessity ("must φ"): standard Kratzer necessity.

Equations

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

def Modality.Directive.weakNecessity {W : Type u_1} (f : Kratzer.ModalBase W) (g g' : Kratzer.OrderingSource W) (p : W → Prop) (w : W) : Prop

Weak necessity ("ought φ"): necessity over the g'-best of the g-best worlds — the lexicographic refinement of [Kra81]'s Conclusion.

Equations

• Modality.Directive.weakNecessity f g g' p w = ∀ w' ∈ Modality.Kratzer.bestAmong (Modality.Kratzer.bestWorlds f g w) (g' w), p w'

Main entailment

theorem Modality.Directive.strong_entails_weak {W : Type u_1} (f : Kratzer.ModalBase W) (g g' : Kratzer.OrderingSource W) (p : W → Prop) (w : W) (h : strongNecessity f g p w) : weakNecessity f g g' p w

Strong entails weak: if "must φ" holds, then "ought φ" holds.

The converse fails

theorem Modality.Directive.weak_not_entails_strong : ¬∀ (W : Type) (f : Kratzer.ModalBase W) (g g' : Kratzer.OrderingSource W) (p : W → Prop) (w : W), weakNecessity f g g' p w → strongNecessity f g p w

Weak necessity does NOT entail strong necessity.

Counterexample: W = Bool. g is the trivial ordering (all worlds tied), so both worlds are g-best; g' identifies true, so only true is g'-best among them. With p = (· = true), weakNecessity holds but strongNecessity fails at the g-best world false.

Deontic application

structure Modality.Directive.DeonticStrength (W : Type u_2) : Type u_2

• primary : Kratzer.DeonticFlavor W
• secondaryNorms : Kratzer.OrderingSource W

def Modality.Directive.DeonticStrength.must {W : Type u_1} (d : DeonticStrength W) (p : W → Prop) (w : W) : Prop

Equations

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

def Modality.Directive.DeonticStrength.ought {W : Type u_1} (d : DeonticStrength W) (p : W → Prop) (w : W) : Prop

Equations

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

theorem Modality.Directive.deontic_must_eq_kratzer {W : Type u_1} (d : Kratzer.DeonticFlavor W) (p : W → Prop) (w : W) : Kratzer.necessity d.circumstances d.norms p w ↔ strongNecessity d.circumstances d.norms p w

theorem Modality.Directive.deontic_must_entails_ought {W : Type u_1} (d : DeonticStrength W) (p : W → Prop) (w : W) (h : d.must p w) : d.ought p w

theorem Modality.Directive.weak_eq_strong_no_secondary {W : Type u_1} (f : Kratzer.ModalBase W) (g : Kratzer.OrderingSource W) (p : W → Prop) (w : W) : weakNecessity f g Kratzer.emptyBackground p w ↔ strongNecessity f g p w