def Semantics.Modality.Kratzer.simpleNecessity (f : ModalBase) (p : BProp Attitudes.Intensional.World) (w : Attitudes.Intensional.World) : Bool

Simple f-necessity (Kratzer p. 32): p is true at ALL accessible worlds.

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

Equations

• Semantics.Modality.Kratzer.simpleNecessity f p w = (Semantics.Modality.Kratzer.accessibleWorlds f w).all p

def Semantics.Modality.Kratzer.simplePossibility (f : ModalBase) (p : BProp Attitudes.Intensional.World) (w : Attitudes.Intensional.World) : Bool

Simple f-possibility (Kratzer p. 32): p is true at SOME accessible world.

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

Equations

• Semantics.Modality.Kratzer.simplePossibility f p w = (Semantics.Modality.Kratzer.accessibleWorlds f w).any p

def Semantics.Modality.Kratzer.necessity (f : ModalBase) (g : OrderingSource) (p : BProp Attitudes.Intensional.World) (w : Attitudes.Intensional.World) : Bool

Necessity with ordering (Kratzer p. 40): p is true at ALL best worlds.

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

Equations

• Semantics.Modality.Kratzer.necessity f g p w = (Semantics.Modality.Kratzer.bestWorlds f g w).all p

def Semantics.Modality.Kratzer.possibility (f : ModalBase) (g : OrderingSource) (p : BProp Attitudes.Intensional.World) (w : Attitudes.Intensional.World) : Bool

Possibility with ordering: p is true 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 = (Semantics.Modality.Kratzer.bestWorlds f g w).any p

theorem Semantics.Modality.Kratzer.duality (f : ModalBase) (g : OrderingSource) (p : BProp Attitudes.Intensional.World) (w : Attitudes.Intensional.World) : (necessity f g p w == !possibility f g (fun (w' : Attitudes.Intensional.World) => !p w') w) = true

Theorem: Modal duality holds.

□p ↔ ¬◇¬p

theorem Semantics.Modality.Kratzer.totally_realistic_gives_T (f : ModalBase) (g : OrderingSource) (hTotal : ∀ (w : Attitudes.Intensional.World), accessibleWorlds f w = [w]) (p : BProp Attitudes.Intensional.World) (w : Attitudes.Intensional.World) (hNec : necessity f g p w = true) : p w = true

Theorem 4: Totally realistic base gives T axiom.

If f is totally realistic (∩f(w) = {w}), then □p → p.

theorem Semantics.Modality.Kratzer.realistic_gives_reflexive_access (f : ModalBase) (hReal : isRealistic f) (w : Attitudes.Intensional.World) : w ∈ accessibleWorlds f w

Theorem 5: Realistic base gives reflexive accessibility.

If f is realistic (w ∈ ∩f(w) for all w), then the evaluation world is always accessible from itself.

theorem Semantics.Modality.Kratzer.empty_base_universal_access (w : Attitudes.Intensional.World) : accessibleWorlds emptyBackground w = Attitudes.Intensional.allWorlds

Theorem 6: Empty modal base gives universal accessibility.

If f(w) = ∅ for all w, then ∩f(w) = W (all worlds accessible).

def Semantics.Modality.Kratzer.isTransitiveAccess (f : ModalBase) : Prop

Equations

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

def Semantics.Modality.Kratzer.isSymmetricAccess (f : ModalBase) : Prop

Equations

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

def Semantics.Modality.Kratzer.isEuclideanAccess (f : ModalBase) : Prop

Equations

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

theorem Semantics.Modality.Kratzer.D_axiom (f : ModalBase) (g : OrderingSource) (p : BProp Attitudes.Intensional.World) (w : Attitudes.Intensional.World) (hSerial : (bestWorlds f g w).length > 0) (hNec : necessity f g p w = true) : possibility f g p w = true

D Axiom (Seriality): □p → ◇p

theorem Semantics.Modality.Kratzer.realistic_is_serial (f : ModalBase) (hReal : isRealistic f) (w : Attitudes.Intensional.World) : (accessibleWorlds f w).length > 0

theorem Semantics.Modality.Kratzer.D_axiom_realistic (f : ModalBase) (hReal : isRealistic f) (p : BProp Attitudes.Intensional.World) (w : Attitudes.Intensional.World) (hNec : necessity f emptyBackground p w = true) : possibility f emptyBackground p w = true

theorem Semantics.Modality.Kratzer.four_axiom (f : ModalBase) (p : BProp Attitudes.Intensional.World) (w : Attitudes.Intensional.World) (hTrans : isTransitiveAccess f) (hNec : necessity f emptyBackground p w = true) : necessity f emptyBackground (necessity f emptyBackground p) w = true

4 Axiom (Transitivity): □p → □□p

theorem Semantics.Modality.Kratzer.B_axiom (f : ModalBase) (p : BProp Attitudes.Intensional.World) (w : Attitudes.Intensional.World) (hSym : isSymmetricAccess f) (hP : p w = true) : necessity f emptyBackground (possibility f emptyBackground p) w = true

B Axiom (Symmetry): p → □◇p

theorem Semantics.Modality.Kratzer.five_axiom (f : ModalBase) (p : BProp Attitudes.Intensional.World) (w : Attitudes.Intensional.World) (hEuc : isEuclideanAccess f) (hPoss : possibility f emptyBackground p w = true) : necessity f emptyBackground (possibility f emptyBackground p) w = true

5 Axiom (Euclidean): ◇p → □◇p

def Semantics.Modality.Kratzer.isS4Base (f : ModalBase) : Prop

Equations

• Semantics.Modality.Kratzer.isS4Base f = (Semantics.Modality.Kratzer.isRealistic f ∧ Semantics.Modality.Kratzer.isTransitiveAccess f)

def Semantics.Modality.Kratzer.isS5Base (f : ModalBase) : Prop

Equations

• Semantics.Modality.Kratzer.isS5Base f = (Semantics.Modality.Kratzer.isRealistic f ∧ Semantics.Modality.Kratzer.isEuclideanAccess f)

theorem Semantics.Modality.Kratzer.euclidean_reflexive_implies_symmetric (f : ModalBase) (hReal : isRealistic f) (hEuc : isEuclideanAccess f) : isSymmetricAccess f

theorem Semantics.Modality.Kratzer.euclidean_reflexive_implies_transitive (f : ModalBase) (hReal : isRealistic f) (hEuc : isEuclideanAccess f) : isTransitiveAccess f

theorem Semantics.Modality.Kratzer.S5_satisfies_all (f : ModalBase) (hS5 : isS5Base f) : isRealistic f ∧ isSymmetricAccess f ∧ isTransitiveAccess f ∧ isEuclideanAccess f

def Semantics.Modality.Kratzer.atLeastAsGoodPossibility (f : ModalBase) (g : OrderingSource) (p q : BProp Attitudes.Intensional.World) (w : Attitudes.Intensional.World) : Bool

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

Equations

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

def Semantics.Modality.Kratzer.betterPossibility (f : ModalBase) (g : OrderingSource) (p q : BProp Attitudes.Intensional.World) (w : Attitudes.Intensional.World) : Bool

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 (f : ModalBase) (g : OrderingSource) (p : BProp Attitudes.Intensional.World) (w : Attitudes.Intensional.World) : atLeastAsGoodPossibility f g p p w = true

def Semantics.Modality.Kratzer.implies (p q : BProp Attitudes.Intensional.World) : BProp Attitudes.Intensional.World

Material conditional as material implication.

Equations

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

theorem Semantics.Modality.Kratzer.K_axiom (f : ModalBase) (g : OrderingSource) (p q : BProp Attitudes.Intensional.World) (w : Attitudes.Intensional.World) (hImpl : necessity f g (implies p q) w = true) (hP : necessity f g p w = true) : necessity f g q w = true

Theorem: K Axiom (Distribution) holds.

□(p → q) → (□p → □q)

def Semantics.Modality.Kratzer.restrictedBase (f : ModalBase) (antecedent : BProp Attitudes.Intensional.World) : ModalBase

Conditionals as modal base restrictors.

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

Equations

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

def Semantics.Modality.Kratzer.materialImplication (p q : BProp Attitudes.Intensional.World) (w : Attitudes.Intensional.World) : Bool

Material implication, pointwise form of implies.

Equations

• Semantics.Modality.Kratzer.materialImplication p q w = Semantics.Modality.Kratzer.implies p q w

def Semantics.Modality.Kratzer.strictImplication (p q : BProp Attitudes.Intensional.World) : Bool

Equations

• Semantics.Modality.Kratzer.strictImplication p q = Semantics.Attitudes.Intensional.allWorlds.all fun (w : Semantics.Attitudes.Intensional.World) => !p w || q w