Accessibility relations

def Semantics.Modality.Kratzer.kratzerR {W : Type u_1} (f : ModalBase W) : Core.Logic.Modal.AccessRel W

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

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

def Semantics.Modality.Kratzer.kratzerBestR {W : Type u_1} (f : ModalBase W) (g : OrderingSource W) : Core.Logic.Modal.AccessRel W

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

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

theorem Semantics.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 Semantics.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

• Semantics.Modality.Kratzer.simpleNecessity f p w = Core.Logic.Modal.box (Semantics.Modality.Kratzer.kratzerR f) p w

def Semantics.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

• Semantics.Modality.Kratzer.simplePossibility f p w = Core.Logic.Modal.diamond (Semantics.Modality.Kratzer.kratzerR f) p w

def Semantics.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

• Semantics.Modality.Kratzer.necessity f g p w = Core.Logic.Modal.box (Semantics.Modality.Kratzer.kratzerBestR f g) p w

def Semantics.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

• Semantics.Modality.Kratzer.possibility f g p w = Core.Logic.Modal.diamond (Semantics.Modality.Kratzer.kratzerBestR f g) p w

Characterization lemmas

@[simp]

theorem Semantics.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 Semantics.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 Semantics.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 Semantics.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 Semantics.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.

Frame conditions on kratzerR

theorem Semantics.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 Semantics.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 Semantics.Modality.Kratzer.realistic_is_serial {W : Type u_1} (f : ModalBase W) (hReal : isRealistic f) : Core.Logic.Modal.IsSerial (kratzerR f)

Realistic ⟹ serial.

theorem Semantics.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 Semantics.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 of the modal square of opposition (Core.Logic.Modal.modalSquare_relations).

theorem Semantics.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 Semantics.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 Semantics.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

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