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 {W : Type u_1} (g₁ g₂ : Core.Logic.Intensional.OrderingSource W) : Core.Logic.Intensional.OrderingSource W

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 {W : Type u_1} (g g' : Core.Logic.Intensional.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 Semantics.Modality.Directive.combine_empty_right {W : Type u_1} (g : Core.Logic.Intensional.OrderingSource W) (w : W) : combineOrdering g Core.Logic.Intensional.emptyBackground w = g w

Combining with empty ordering preserves the original.

Strong and weak necessity

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

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

Equations

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

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

Weak necessity ("ought φ"): Kratzer necessity under refined ordering g ∪ g'.

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 {W : Type u_1} (f : Core.Logic.Intensional.ModalBase W) (g g' : Core.Logic.Intensional.OrderingSource W) (w w' : W) : 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.

Main entailment

theorem Semantics.Modality.Directive.strong_entails_weak {W : Type u_1} (f : Core.Logic.Intensional.ModalBase W) (g g' : Core.Logic.Intensional.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 Semantics.Modality.Directive.weak_not_entails_strong : ¬∀ (W : Type) (f : Core.Logic.Intensional.ModalBase W) (g g' : Core.Logic.Intensional.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); g' identifies true. Under g, both true and false are best; under g∪g', only true is best. With p = (· = true), weakNecessity holds (only true ∈ best), but strongNecessity fails (false ∈ best, p false).

Deontic application

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

• primary : Kratzer.DeonticFlavor W
• secondaryNorms : Core.Logic.Intensional.OrderingSource W

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

Equations

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

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

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 {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 Semantics.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 Semantics.Modality.Directive.weak_eq_strong_no_secondary {W : Type u_1} (f : Core.Logic.Intensional.ModalBase W) (g : Core.Logic.Intensional.OrderingSource W) (p : W → Prop) (w : W) : weakNecessity f g Core.Logic.Intensional.emptyBackground p w ↔ strongNecessity f g p w