Accessibility relations

def Modality.Kratzer.kratzerR {W : Type u_1} (f : ModalBase W) : W → W → Prop

Accessibility relation derived from a modal base.

kratzerR f w w' iff w' satisfies all propositions in f(w), i.e., w' ∈ ⋂f(w) in Kratzer's notation.

Equations

• Modality.Kratzer.kratzerR f w w' = ∀ p ∈ f w, p w'

def Modality.Kratzer.kratzerBestR {W : Type u_1} (f : ModalBase W) (g : OrderingSource W) : W → W → Prop

Accessibility restricted to best worlds (modal base + ordering source).

kratzerBestR f g w w' iff w' is among the best accessible worlds from w — accessible via f and maximal under the g(w)-ordering.

Equations

• Modality.Kratzer.kratzerBestR f g w w' = (w' ∈ Modality.Kratzer.bestWorlds f g w)

theorem Modality.Kratzer.kratzerBestR_empty {W : Type u_1} (f : ModalBase W) (w w' : W) : kratzerBestR f emptyBackground w w' ↔ kratzerR f w w'

With the empty ordering source, best-world accessibility reduces to base accessibility.

Operators

def Modality.Kratzer.simpleNecessity {W : Type u_1} (f : ModalBase W) (p : W → Prop) (w : W) : Prop

Simple f-necessity: p holds at every accessible world. ⟦must⟧_f(p)(w) = ∀w' ∈ ⋂f(w). p(w').

Equations

• Modality.Kratzer.simpleNecessity f p w = ModalLogic.box (Modality.Kratzer.kratzerR f) p w

def Modality.Kratzer.simplePossibility {W : Type u_1} (f : ModalBase W) (p : W → Prop) (w : W) : Prop

Simple f-possibility: p holds at some accessible world. ⟦can⟧_f(p)(w) = ∃w' ∈ ⋂f(w). p(w').

Equations

• Modality.Kratzer.simplePossibility f p w = ModalLogic.diamond (Modality.Kratzer.kratzerR f) p w

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

Necessity with ordering: p holds at every best world. ⟦must⟧_{f,g}(p)(w) = ∀w' ∈ Best(f,g,w). p(w').

Adopts the Limit-Assumption-collapsed form.

Equations

• Modality.Kratzer.necessity f g p w = ModalLogic.box (Modality.Kratzer.kratzerBestR f g) p w

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

Possibility with ordering: p holds at some best world. ⟦can⟧_{f,g}(p)(w) = ∃w' ∈ Best(f,g,w). p(w').

Equations

• Modality.Kratzer.possibility f g p w = ModalLogic.diamond (Modality.Kratzer.kratzerBestR f g) p w

Human necessity

[Kra81]'s official definition needs no Limit Assumption: it asks each accessible world to see, at least as good, a witness below which only p-worlds occur. necessity (universal quantification over bestWorlds) is its Limit-Assumption collapse.

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

Human necessity ([Kra81]; restated verbatim as "Necessity" in [Kra12]): every accessible world has an accessible world at least as good, below which p holds throughout. Neutral with respect to the Limit Assumption, after Lewis's counterfactual semantics.

Equations

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

theorem Modality.Kratzer.necessity_of_humanNecessity {W : Type u_1} {f : ModalBase W} {g : OrderingSource W} {p : W → Prop} {w : W} (h : humanNecessity f g p w) : necessity f g p w

Human necessity implies best-worlds necessity, unconditionally.

def Modality.Kratzer.LimitAssumption {W : Type u_1} (f : ModalBase W) (g : OrderingSource W) (w : W) : Prop

The Limit Assumption at w: every accessible world sees a best world at least as good.

Equations

• Modality.Kratzer.LimitAssumption f g w = ∀ u ∈ Modality.Kratzer.accessibleWorlds f w, ∃ v ∈ Modality.Kratzer.bestWorlds f g w, v ≤[g w] u

theorem Modality.Kratzer.humanNecessity_of_necessity {W : Type u_1} {f : ModalBase W} {g : OrderingSource W} {p : W → Prop} {w : W} (hlim : LimitAssumption f g w) (h : necessity f g p w) : humanNecessity f g p w

Under the Limit Assumption, best-worlds necessity implies human necessity.

theorem Modality.Kratzer.humanNecessity_iff_necessity {W : Type u_1} {f : ModalBase W} {g : OrderingSource W} {p : W → Prop} {w : W} (hlim : LimitAssumption f g w) : humanNecessity f g p w ↔ necessity f g p w

Under the Limit Assumption, [Kra81]'s human necessity is exactly universal quantification over the best worlds.

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

Human possibility ([Kra12]: "a possibility ... iff its negation ... is not a necessity"): the dual of humanNecessity.

Equations

• Modality.Kratzer.humanPossibility f g p w = ¬Modality.Kratzer.humanNecessity f g (fun (v : W) => ¬p v) w

theorem Modality.Kratzer.humanNecessity_emptyBackground_iff {W : Type u_1} (f : ModalBase W) (p : W → Prop) (w : W) : humanNecessity f emptyBackground p w ↔ simpleNecessity f p w

With the empty ordering source, human necessity is simple necessity ([Kra81], her equivalence for arbitrary f and empty g).

Characterization lemmas

@[simp]

theorem Modality.Kratzer.simpleNecessity_iff_all {W : Type u_1} (f : ModalBase W) (p : W → Prop) (w : W) : simpleNecessity f p w ↔ ∀ w' ∈ accessibleWorlds f w, p w'

@[simp]

theorem Modality.Kratzer.simplePossibility_iff_any {W : Type u_1} (f : ModalBase W) (p : W → Prop) (w : W) : simplePossibility f p w ↔ ∃ w' ∈ accessibleWorlds f w, p w'

@[simp]

theorem Modality.Kratzer.necessity_iff_all {W : Type u_1} (f : ModalBase W) (g : OrderingSource W) (p : W → Prop) (w : W) : necessity f g p w ↔ ∀ w' ∈ bestWorlds f g w, p w'

@[simp]

theorem Modality.Kratzer.possibility_iff_any {W : Type u_1} (f : ModalBase W) (g : OrderingSource W) (p : W → Prop) (w : W) : possibility f g p w ↔ ∃ w' ∈ bestWorlds f g w, p w'

theorem Modality.Kratzer.necessity_empty_iff_simple {W : Type u_1} (f : ModalBase W) (p : W → Prop) (w : W) : necessity f emptyBackground p w ↔ simpleNecessity f p w

Necessity with an empty ordering source collapses to simple necessity.

Monotonicity in the modal base

theorem Modality.Kratzer.simpleNecessity_mono {W : Type u_1} {f f' : ModalBase W} {p : W → Prop} {w : W} (h : f w ⊆ f' w) (hNec : simpleNecessity f p w) : simpleNecessity f' p w

Premise growth preserves simple necessity: more evidence, fewer accessible worlds, at least as many necessities. This is [Kra12]'s point about epistemic change over time (Ch. 4's approaching-man dialogue): one conversational background can represent evidence that grows as time goes by, and what must hold on the earlier evidence still must on the later.

Frame conditions on kratzerR

theorem Modality.Kratzer.realistic_refl {W : Type u_1} (f : ModalBase W) (hReal : isRealistic f) : Std.Refl (kratzerR f)

A realistic modal base gives reflexive accessibility.

theorem Modality.Kratzer.realistic_gives_reflexive_access {W : Type u_1} (f : ModalBase W) (hReal : isRealistic f) (w : W) : w ∈ accessibleWorlds f w

Realistic base: the evaluation world is itself accessible.

theorem Modality.Kratzer.realistic_is_serial {W : Type u_1} (f : ModalBase W) (hReal : isRealistic f) : ModalLogic.IsSerial (kratzerR f)

Realistic ⟹ serial.

theorem Modality.Kratzer.kratzerR_emptyBackground {W : Type u_1} (w w' : W) : kratzerR emptyBackground w w'

Under the empty modal base, every world is accessible.

theorem Modality.Kratzer.kratzerR_singleton {W : Type u_1} (p : W → Prop) (w w' : W) : kratzerR (fun (x : W) => [p]) w w' ↔ p w'

Under a singleton modal base, accessibility is the sole premise.

theorem Modality.Kratzer.empty_base_universal_access {W : Type u_1} (w : W) : accessibleWorlds emptyBackground w = Set.univ

Empty modal base gives universal accessibility.

Modal axioms (from RestrictedModality)

theorem Modality.Kratzer.duality {W : Type u_1} (f : ModalBase W) (g : OrderingSource W) (p : W → Prop) (w : W) : necessity f g p w ↔ ¬possibility f g (fun (w' : W) => ¬p w') w

Modal duality: □p ↔ ¬◇¬p. Since necessity = box (kratzerBestR f g), this is the box–diamond duality (ModalLogic.not_diamond).

theorem Modality.Kratzer.K_axiom {W : Type u_1} (f : ModalBase W) (g : OrderingSource W) (p q : W → Prop) (w : W) (hImpl : necessity f g (fun (w' : W) => p w' → q w') w) (hP : necessity f g p w) : necessity f g q w

K (Distribution): □(p → q) → □p → □q.

theorem Modality.Kratzer.totally_realistic_gives_T {W : Type u_1} (f : ModalBase W) (g : OrderingSource W) (hTotal : isTotallyRealistic f) (p : W → Prop) (w : W) (hNec : necessity f g p w) : p w

Totally realistic base: simple T holds for full necessity.

Conditionals as modal-base restriction

def Modality.Kratzer.restrictedBase {W : Type u_1} (f : ModalBase W) (antecedent : W → Prop) : ModalBase W

"If α, must β" is must_{f + α} β: prepend the antecedent to the modal base.

Equations

• Modality.Kratzer.restrictedBase f antecedent w = antecedent :: f w