Degree Collapse — @cite{kratzer-2012} §2.5 #

Modal strength as a degree: the proportion of best worlds where the prejacent holds. This formalizes Kratzer's observation that ordering sources create a spectrum of modal strength between bare possibility and necessity.

Strength 1 = all best worlds satisfy p → necessity
Strength 0 = no best world satisfies p → impossibility
0 < strength < 1 = graded possibility

Reuses the rain/wet-streets scenario from ConditionalModality/Data.lean to maximize interconnection density.

Reference: Kratzer, A. (2012). Modals and Conditionals. OUP. Ch. 2 §2.5.

source

def Phenomena.Modality.DegreeCollapse.modalStrength (f : Semantics.Modality.Kratzer.ModalBase) (g : Semantics.Modality.Kratzer.OrderingSource) (p : BProp Semantics.Attitudes.Intensional.World) (w : Semantics.Attitudes.Intensional.World) :

ℚ

Modal strength: the proportion of best worlds satisfying p.

When the set of best worlds is empty (inconsistent base), strength is 0. Otherwise, strength = |{w ∈ Best : p(w)}| / |Best|.

This captures Kratzer's graded modality: the ordering source modulates modal strength between bare possibility and necessity.

Equations

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

Instances For

Concrete scenario: Rain / Wet Streets #

We reuse ConditionalModality.Data's rain scenario. With the normalcy ordering, best = {w0} (normal rain), so streetWet has strength 1. Without normalcy ordering, best = all rain-worlds {w0, w1}, and streetWet holds only at w0, so strength = 1/2.

source

theorem Phenomena.Modality.DegreeCollapse.strength_with_normalcy (w : Semantics.Attitudes.Intensional.World) :

modalStrength (Semantics.Modality.Kratzer.restrictedBase Semantics.Modality.Kratzer.emptyBackground ConditionalModality.rained) ConditionalModality.normalcySource ConditionalModality.streetWet w = 1

With normalcy ordering: strength = 1. Best = {w0}, streetWet w0 = true.

source

theorem Phenomena.Modality.DegreeCollapse.strength_without_normalcy (w : Semantics.Attitudes.Intensional.World) :

modalStrength (Semantics.Modality.Kratzer.restrictedBase Semantics.Modality.Kratzer.emptyBackground ConditionalModality.rained) Semantics.Modality.Kratzer.emptyBackground ConditionalModality.streetWet w = 1 / 2

Without normalcy ordering: strength = 1/2. Best = {w0, w1}, streetWet w0 = true, streetWet w1 = false.

source