def Semantics.Modality.Kratzer.kratzerR {W : Type u_1} (f : ModalBase W) : Core.Logic.Intensional.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.Intensional.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)

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

Simple f-necessity (@cite{kratzer-1981}): p is true at ALL accessible worlds.

⟦must⟧_f(p)(w) = ∀w' ∈ ⋂f(w). p(w')

Defined as boxR with modal-base accessibility.

Equations

• Semantics.Modality.Kratzer.simpleNecessity f p w = Core.Logic.Intensional.boxR (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 (@cite{kratzer-1981}): p is true at SOME accessible world.

⟦can⟧_f(p)(w) = ∃w' ∈ ⋂f(w). p(w')

Defined as diamondR with modal-base accessibility.

Equations

• Semantics.Modality.Kratzer.simplePossibility f p w = Core.Logic.Intensional.diamondR (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 (@cite{kratzer-1981}): p is true at ALL best worlds.

⟦must⟧_{f,g}(p)(w) = ∀w' ∈ Best(f,g,w). p(w')

Defined as boxR with best-world accessibility.

Equations

• Semantics.Modality.Kratzer.necessity f g p w = Core.Logic.Intensional.boxR (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 is true at SOME best world.

⟦can⟧_{f,g}(p)(w) = ∃w' ∈ Best(f,g,w). p(w')

Defined as diamondR with best-world accessibility.

Equations

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

theorem Semantics.Modality.Kratzer.kratzerR_iff_accessible {W : Type u_1} (f : ModalBase W) (w w' : W) : kratzerR f w w' ↔ w' ∈ accessibleWorlds f w

kratzerR f w w' iff w' ∈ accessibleWorlds f w.

theorem Semantics.Modality.Kratzer.kratzerBestR_iff_best {W : Type u_1} (f : ModalBase W) (g : OrderingSource W) (w w' : W) : kratzerBestR f g w w' ↔ w' ∈ bestWorlds f g w

kratzerBestR f g w w' iff w' ∈ bestWorlds f g w (definitional).

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 empty ordering, best-world accessibility reduces to base accessibility.

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'

simpleNecessity f p w iff p holds at all accessible worlds.

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'

simplePossibility f p w iff p holds at some accessible world.

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'

necessity f g p w iff p holds at all best worlds.

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'

possibility f g p w iff p holds at some best world.

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

Necessity with empty ordering = simple necessity.

These theorems derive frame conditions on kratzerR from properties of conversational backgrounds. This is the Kratzer-specific contribution: the frame conditions aren't stipulated, they follow from what kind of conversational background the modal base is.

Frame conditions on kratzerR are stated directly via the polymorphic IsReflexive/IsTransitive/IsSymmetric/IsEuclidean predicates from RestrictedModality.

theorem Semantics.Modality.Kratzer.realistic_refl {W : Type u_1} (f : ModalBase W) (hReal : isRealistic f) : Core.Logic.Intensional.IsReflexive (kratzerR f)

A realistic modal base gives reflexive accessibility.

theorem Semantics.Modality.Kratzer.empty_base_universalR {W : Type u_1} : kratzerR emptyBackground = Core.Logic.Intensional.universalR

An empty modal base gives universal accessibility.

Each modal axiom is a direct application of the corresponding boxR_* theorem from RestrictedModality. The Kratzer-specific work is deriving the frame condition from the conversational background property — the modal logic is inherited for free.

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

Theorem: Modal duality holds.

□p ↔ ¬◇¬p

This is the contradiction diagonal of the Kratzer modal Aristotelian square ({□p, ◇p, □¬p, ◇¬p}). The abstract framework lives in Core.Logic.Opposition.Square.fromBox (a Square (W → Bool) from any box-style modal operator) — the bridge from Kratzer's Prop-valued box to that Bool-valued framework requires DecidablePred glue, deferred. Five sibling theorem dualitys (Inertia, Temporal, BiasedPQ, EventRelativity, EpistemicBlocking) instantiate the same pattern and would unify under one Square.fromBox instance once the Prop↔Bool coercion is settled.

theorem Semantics.Modality.Kratzer.necessity_satisfies_isContradictory_pointwise {W : Type u_1} (f : ModalBase W) (g : OrderingSource W) (p : W → Prop) : Core.Opposition.IsContradictory (necessity f g p) (possibility f g fun (w' : W) => ¬p w')

Bundled (Prop↔Bool gap closure demo, parallel to Quantifier.every_satisfies_isContradictory_pointwise): the modal A↔O contradiction diagonal □p vs ◇¬p packaged as Core.Opposition.IsContradictory over the Pi-instance Boolean algebra on W → Prop. Follows from duality (□p ↔ ¬◇¬p).

Demonstrates that the polymorphic IsContradictory works on Prop-valued modal predicates the same way it does on Bool-valued GQ scope predicates. The other 4 Kratzer-square corners (E ↔ ¬I, A ⊓ E = ⊥, etc.) follow the same template.

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 Axiom (Distribution): □(p → q) → (□p → □q)

Holds for any accessibility relation.

theorem Semantics.Modality.Kratzer.T_axiom {W : Type u_1} (f : ModalBase W) (p : W → Prop) (w : W) (hReal : isRealistic f) (hNec : simpleNecessity f p w) : p w

T Axiom: Realistic base → □p → p.

What is necessary is actual.

theorem Semantics.Modality.Kratzer.D_axiom_simple {W : Type u_1} (f : ModalBase W) (p : W → Prop) (w : W) (hReal : isRealistic f) (hNec : simpleNecessity f p w) : simplePossibility f p w

D Axiom: IsSerial accessibility → □p → ◇p.

What is necessary is possible.

theorem Semantics.Modality.Kratzer.four_axiom {W : Type u_1} (f : ModalBase W) (p : W → Prop) (w : W) (hTrans : Core.Logic.Intensional.IsTransitive (kratzerR f)) (hNec : simpleNecessity f p w) : simpleNecessity f (fun (w' : W) => simpleNecessity f p w') w

4 Axiom: Transitive accessibility → □p → □□p.

Positive introspection.

theorem Semantics.Modality.Kratzer.B_axiom {W : Type u_1} (f : ModalBase W) (p : W → Prop) (w : W) (hSym : Core.Logic.Intensional.IsSymmetric (kratzerR f)) (hP : p w) : simpleNecessity f (fun (w' : W) => simplePossibility f p w') w

B Axiom: Symmetric accessibility → p → □◇p.

What is actual is necessarily possible.

theorem Semantics.Modality.Kratzer.five_axiom {W : Type u_1} (f : ModalBase W) (p : W → Prop) (w : W) (hEuc : Core.Logic.Intensional.IsEuclidean (kratzerR f)) (hPoss : simplePossibility f p w) : simpleNecessity f (fun (w' : W) => simplePossibility f p w') w

5 Axiom: Euclidean accessibility → ◇p → □◇p.

Positive possibility introspection.

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

Totally realistic base implies T axiom for full necessity.

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 gives reflexive accessibility.

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.

Frame condition derivations on kratzerR (IsReflexive/IsTransitive/IsSymmetric/IsEuclidean from the polymorphic foundation) flow through realistic_refl etc. above. S5 collapse is RestrictedModality.S5_equiv applied to kratzerR f.

theorem Semantics.Modality.Kratzer.realistic_is_serial {W : Type u_1} (f : ModalBase W) (hReal : isRealistic f) (w : W) : (accessibleWorlds f w).Nonempty

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

p is at least as good a possibility as q in w with respect to f and g.

For every accessible world satisfying q-but-not-p, there exists an accessible world satisfying p-but-not-q that is at least as good.

Equations

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

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

Equations

• Semantics.Modality.Kratzer.betterPossibility f g p q w = (Semantics.Modality.Kratzer.atLeastAsGoodPossibility f g p q w ∧ ¬Semantics.Modality.Kratzer.atLeastAsGoodPossibility f g q p w)

theorem Semantics.Modality.Kratzer.comparative_poss_reflexive {W : Type u_1} (f : ModalBase W) (g : OrderingSource W) (p : W → Prop) (w : W) : atLeastAsGoodPossibility f g p p w

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

Conditionals as modal base restrictors.

"If α, (must) β" = must_f+α β

Equations

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

def Semantics.Modality.Kratzer.implies {W : Type u_1} (p q : W → Prop) : W → Prop

Pointwise material implication.

Equations

• Semantics.Modality.Kratzer.implies p q w = (p w → q w)

def Semantics.Modality.Kratzer.strictImplication {W : Type u_1} (p q : W → Prop) : Prop

Strict implication: p entails q at every world.

Equations

• Semantics.Modality.Kratzer.strictImplication p q = ∀ (w : W), p w → q w