@[reducible, inline]

abbrev Semantics.Modality.ModalForce : Type

Modal force: necessity (□) or possibility (◇). Reuses Core.Modality.ModalForce.

Equations

• Semantics.Modality.ModalForce = Core.Modality.ModalForce

@[reducible, inline]

abbrev Semantics.Modality.Proposition : Type

A proposition is a function from worlds to truth values.

Equations

• Semantics.Modality.Proposition = BProp Semantics.Attitudes.Intensional.World

def Semantics.Modality.allWorlds' : List Attitudes.Intensional.World

The set of all worlds (from Attitudes.lean).

Equations

• Semantics.Modality.allWorlds' = Semantics.Attitudes.Intensional.allWorlds

theorem Semantics.Modality.proposition_eq_bprop : Proposition = BProp Attitudes.Intensional.World

Modal.Proposition equals Core.Proposition.BProp World.

structure Semantics.Modality.ModalTheory : Type

A semantic theory for modal auxiliaries, with eval : ModalForce -> Proposition -> World -> Bool.

• name : String

  Name of the theory.

• citation : String

  Academic citation.

• eval : ModalForce → Proposition → Attitudes.Intensional.World → Bool

  Core evaluation function: is modal force applied to proposition p true at world w?

def Semantics.Modality.ModalTheory.necessity (T : ModalTheory) (p : Proposition) (w : Attitudes.Intensional.World) : Bool

Necessity operator: □p is true at w.

Equations

• T.necessity p w = T.eval Core.Modality.ModalForce.necessity p w

def Semantics.Modality.ModalTheory.possibility (T : ModalTheory) (p : Proposition) (w : Attitudes.Intensional.World) : Bool

Possibility operator: ◇p is true at w.

Equations

• T.possibility p w = T.eval Core.Modality.ModalForce.possibility p w

def Semantics.Modality.ModalTheory.weakNecessity (T : ModalTheory) (p : Proposition) (w : Attitudes.Intensional.World) : Bool

Weak necessity operator: □wφ is true at w. Note: For Kratzer semantics, weak necessity differs from strong necessity in the ordering source, not the quantifier. Use Directive.weakNecessity (which takes a secondary ordering source) for the proper von Fintel & Iatridou (2008) semantics. Calling T.eval .weakNecessity on a KratzerTheory returns the same result as T.eval .necessity — the distinction lives in which KratzerParams you pass, not in the force enum.

Equations

• T.weakNecessity p w = T.eval Core.Modality.ModalForce.weakNecessity p w

def Semantics.Modality.ModalTheory.necessityEntailsPossibility (T : ModalTheory) (p : Proposition) (w : Attitudes.Intensional.World) : Bool

Consistency check: □p -> ◇p.

Equations

• T.necessityEntailsPossibility p w = (!T.necessity p w || T.possibility p w)

def Semantics.Modality.ModalTheory.dualityHolds (T : ModalTheory) (p : Proposition) (w : Attitudes.Intensional.World) : Bool

Duality check: □p ↔ ¬◇¬p at world w.

Equations

• T.dualityHolds p w = (T.necessity p w == !T.possibility (fun (w' : Semantics.Attitudes.Intensional.World) => !p w') w)

def Semantics.Modality.ModalTheory.checkDuality (T : ModalTheory) (p : Proposition) : Bool

Check duality across all worlds for a proposition.

Equations

• T.checkDuality p = Semantics.Modality.allWorlds'.all fun (w : Semantics.Attitudes.Intensional.World) => T.dualityHolds p w

def Semantics.Modality.ModalTheory.checkConsistency (T : ModalTheory) (p : Proposition) : Bool

Check consistency across all worlds for a proposition.

Equations

• T.checkConsistency p = Semantics.Modality.allWorlds'.all fun (w : Semantics.Attitudes.Intensional.World) => T.necessityEntailsPossibility p w

def Semantics.Modality.ModalTheory.isNormal (T : ModalTheory) : Prop

A theory is normal iff duality holds universally: ∀ p w, □p ↔ ¬◇¬p.

Equations

• T.isNormal = ∀ (p : Semantics.Modality.Proposition) (w : Semantics.Attitudes.Intensional.World), T.dualityHolds p w = true

def Semantics.Modality.ModalTheory.isConsistent (T : ModalTheory) : Prop

A theory is consistent iff □p -> ◇p universally (D axiom / seriality).

Equations

• T.isConsistent = ∀ (p : Semantics.Modality.Proposition) (w : Semantics.Attitudes.Intensional.World), T.necessityEntailsPossibility p w = true