Strong and weak necessity

Von Fintel and Iatridou distinguish two necessity forces over Kratzer's conversational backgrounds. Strong necessity (must, have to) is necessity over the best accessible worlds (strongNecessity); weak necessity (ought, should) is necessity over the best of those under a secondary ordering source (weakNecessity), the lexicographic refinement in which a later ordering source undoes the ties left by an earlier one. Selecting within the best worlds can only shrink the domain, so strong necessity entails weak necessity (strong_entails_weak) and not conversely (weak_not_entails_strong); with an empty secondary ordering source the two coincide (weak_eq_strong_no_secondary).

References

• [vFI08]
• [Kra81b]
• [Kra12b]

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

Strong necessity, must φ, is Kratzer's necessity over the best accessible worlds.

Equations

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

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

Weak necessity, ought φ, is necessity over the g'-best of the g-best accessible worlds.

Equations

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

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

Strong necessity entails weak necessity: the g'-best of the g-best worlds are g-best.

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

Weak necessity does not entail strong necessity: with two tied accessible worlds and a secondary ordering source singling out the one where p holds, ought p is true and must p false.

theorem Modality.Directive.weak_eq_strong_no_secondary {W : Type u_1} (f g : Background W) (p : W → Prop) (w : W) : weakNecessity f g ⊥ p w ↔ strongNecessity f g p w

With an empty secondary ordering source, weak necessity is strong necessity.