def Semantics.Modality.Simple (R : Attitudes.Intensional.World → Attitudes.Intensional.World → Bool) : ModalTheory

Construct a simple modal theory from accessibility relation R.

Equations

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

def Semantics.Modality.universalR : Attitudes.Intensional.World → Attitudes.Intensional.World → Bool

Universal accessibility: every world is accessible from every world. Matches Core.ModalLogic.universalR.

Equations

• Semantics.Modality.universalR = Core.ModalLogic.universalR

def Semantics.Modality.reflexiveR : Attitudes.Intensional.World → Attitudes.Intensional.World → Bool

Reflexive accessibility: each world is accessible from itself. Matches Core.ModalLogic.identityR.

Equations

• Semantics.Modality.reflexiveR = Core.ModalLogic.identityR

def Semantics.Modality.emptyR : Attitudes.Intensional.World → Attitudes.Intensional.World → Bool

Empty accessibility: no world is accessible from any world. Matches Core.ModalLogic.emptyR.

Equations

• Semantics.Modality.emptyR = Core.ModalLogic.emptyR

def Semantics.Modality.sampleEpistemicR : Attitudes.Intensional.World → Attitudes.Intensional.World → Bool

Sample epistemic accessibility: w0↔w2, w1↔w3.

Equations

• Semantics.Modality.sampleEpistemicR Core.Proposition.World4.w0 Core.Proposition.World4.w0 = true
• Semantics.Modality.sampleEpistemicR Core.Proposition.World4.w0 Core.Proposition.World4.w2 = true
• Semantics.Modality.sampleEpistemicR Core.Proposition.World4.w2 Core.Proposition.World4.w0 = true
• Semantics.Modality.sampleEpistemicR Core.Proposition.World4.w2 Core.Proposition.World4.w2 = true
• Semantics.Modality.sampleEpistemicR Core.Proposition.World4.w1 Core.Proposition.World4.w1 = true
• Semantics.Modality.sampleEpistemicR Core.Proposition.World4.w1 Core.Proposition.World4.w3 = true
• Semantics.Modality.sampleEpistemicR Core.Proposition.World4.w3 Core.Proposition.World4.w1 = true
• Semantics.Modality.sampleEpistemicR Core.Proposition.World4.w3 Core.Proposition.World4.w3 = true
• Semantics.Modality.sampleEpistemicR w w' = false

def Semantics.Modality.sampleDeonticR : Attitudes.Intensional.World → Attitudes.Intensional.World → Bool

Sample deontic accessibility: ideal worlds w0, w2 accessible from anywhere.

Equations

• Semantics.Modality.sampleDeonticR x✝ w' = (w' == Core.Proposition.World4.w0 || w' == Core.Proposition.World4.w2)

def Semantics.Modality.SimpleUniversal : ModalTheory

Simple theory with universal accessibility (S5-like).

Equations

• Semantics.Modality.SimpleUniversal = Semantics.Modality.Simple Semantics.Modality.universalR

def Semantics.Modality.SimpleReflexive : ModalTheory

Simple theory with reflexive-only accessibility (T-like).

Equations

• Semantics.Modality.SimpleReflexive = Semantics.Modality.Simple Semantics.Modality.reflexiveR

def Semantics.Modality.SimpleEpistemic : ModalTheory

Simple epistemic theory.

Equations

• Semantics.Modality.SimpleEpistemic = Semantics.Modality.Simple Semantics.Modality.sampleEpistemicR

def Semantics.Modality.SimpleDeontic : ModalTheory

Simple deontic theory.

Equations

• Semantics.Modality.SimpleDeontic = Semantics.Modality.Simple Semantics.Modality.sampleDeonticR

def Semantics.Modality.raining : Proposition

Proposition: it is raining. True at w0, w1; false at w2, w3.

Equations

• Semantics.Modality.raining Core.Proposition.World4.w0 = true
• Semantics.Modality.raining Core.Proposition.World4.w1 = true
• Semantics.Modality.raining Core.Proposition.World4.w2 = false
• Semantics.Modality.raining Core.Proposition.World4.w3 = false

def Semantics.Modality.johnHome : Proposition

Proposition: John is home. True at w0, w2; false at w1, w3.

Equations

• Semantics.Modality.johnHome Core.Proposition.World4.w0 = true
• Semantics.Modality.johnHome Core.Proposition.World4.w1 = false
• Semantics.Modality.johnHome Core.Proposition.World4.w2 = true
• Semantics.Modality.johnHome Core.Proposition.World4.w3 = false

def Semantics.Modality.triviallyTrue : Proposition

A trivially true proposition (true at all worlds).

Equations

• Semantics.Modality.triviallyTrue x✝ = true

def Semantics.Modality.triviallyFalse : Proposition

A trivially false proposition (false at all worlds).

Equations

• Semantics.Modality.triviallyFalse x✝ = false

theorem Semantics.Modality.simple_universal_necessity (p : Proposition) (w : Attitudes.Intensional.World) : SimpleUniversal.eval Core.Modality.ModalForce.necessity p w = allWorlds'.all p

With universal accessibility, necessity means truth at all worlds.

theorem Semantics.Modality.simple_universal_possibility (p : Proposition) (w : Attitudes.Intensional.World) : SimpleUniversal.eval Core.Modality.ModalForce.possibility p w = allWorlds'.any p

With universal accessibility, possibility means truth at some world.

theorem Semantics.Modality.simple_reflexive_necessity_raining (w : Attitudes.Intensional.World) : SimpleReflexive.eval Core.Modality.ModalForce.necessity raining w = raining w

With reflexive-only accessibility, □p at w = p w (for concrete propositions).

theorem Semantics.Modality.simple_reflexive_necessity_johnHome (w : Attitudes.Intensional.World) : SimpleReflexive.eval Core.Modality.ModalForce.necessity johnHome w = johnHome w

theorem Semantics.Modality.simple_duality (R : Attitudes.Intensional.World → Attitudes.Intensional.World → Bool) (p : Proposition) (w : Attitudes.Intensional.World) : (Simple R).dualityHolds p w = true

Simple theories satisfy modal duality: □p ↔ ¬◇¬p.

theorem Semantics.Modality.simple_universal_consistent_raining (w : Attitudes.Intensional.World) : SimpleUniversal.necessityEntailsPossibility raining w = true

Consistency (□p -> ◇p) holds with universal accessibility.

theorem Semantics.Modality.simple_universal_consistent_johnHome (w : Attitudes.Intensional.World) : SimpleUniversal.necessityEntailsPossibility johnHome w = true

theorem Semantics.Modality.simple_universal_consistent_triviallyTrue (w : Attitudes.Intensional.World) : SimpleUniversal.necessityEntailsPossibility triviallyTrue w = true

theorem Semantics.Modality.simple_isNormal (R : Attitudes.Intensional.World → Attitudes.Intensional.World → Bool) : (Simple R).isNormal

All Simple theories are normal modal logics.

theorem Semantics.Modality.simpleUniversal_isNormal : SimpleUniversal.isNormal

Corollary: SimpleUniversal is normal.

theorem Semantics.Modality.simpleReflexive_isNormal : SimpleReflexive.isNormal

Corollary: SimpleReflexive is normal.

Kripke correspondence: R properties correspond to modal axioms.

@[reducible, inline]

abbrev Semantics.Modality.isReflexive (R : Attitudes.Intensional.World → Attitudes.Intensional.World → Bool) : Prop

Reflexivity of R: every world accesses itself. Alias for Core.ModalLogic.Refl.

Equations

• Semantics.Modality.isReflexive R = Core.ModalLogic.Refl R

theorem Semantics.Modality.T_axiom_from_reflexivity (R : Attitudes.Intensional.World → Attitudes.Intensional.World → Bool) (hRefl : isReflexive R) (p : Proposition) (w : Attitudes.Intensional.World) (hNec : (Simple R).eval Core.Modality.ModalForce.necessity p w = true) : p w = true

T Axiom: reflexive R implies □p -> p. Uses Core.ModalLogic.T_of_refl under the hood.

theorem Semantics.Modality.reflexive_implies_T (R : Attitudes.Intensional.World → Attitudes.Intensional.World → Bool) (hRefl : isReflexive R) (p : Proposition) (w : Attitudes.Intensional.World) : (Simple R).eval Core.Modality.ModalForce.necessity p w = true → p w = true

Reflexive accessibility gives T axiom: □p -> p.

@[reducible, inline]

abbrev Semantics.Modality.isSerial (R : Attitudes.Intensional.World → Attitudes.Intensional.World → Bool) : Prop

Seriality of R: every world accesses at least one world. Alias for Core.ModalLogic.Serial.

Equations

• Semantics.Modality.isSerial R = Core.ModalLogic.Serial R

theorem Semantics.Modality.D_axiom_from_seriality (R : Attitudes.Intensional.World → Attitudes.Intensional.World → Bool) (hSerial : isSerial R) (p : Proposition) (w : Attitudes.Intensional.World) (hNec : (Simple R).eval Core.Modality.ModalForce.necessity p w = true) : (Simple R).eval Core.Modality.ModalForce.possibility p w = true

D Axiom: serial R implies □p -> ◇p. Uses Core.ModalLogic.D_of_serial under the hood.

theorem Semantics.Modality.serial_implies_D (R : Attitudes.Intensional.World → Attitudes.Intensional.World → Bool) (hSerial : isSerial R) (p : Proposition) (w : Attitudes.Intensional.World) : (Simple R).eval Core.Modality.ModalForce.necessity p w = true → (Simple R).eval Core.Modality.ModalForce.possibility p w = true

Serial accessibility gives D axiom: □p -> ◇p.

theorem Semantics.Modality.universalR_isSerial : isSerial universalR

Universal R is serial. Uses Core.ModalLogic.universalR_serial.

theorem Semantics.Modality.reflexiveR_isSerial : isSerial reflexiveR

Reflexive R is serial (reflexivity implies seriality).

theorem Semantics.Modality.simple_universal_isConsistent_from_D (p : Proposition) (w : Attitudes.Intensional.World) : SimpleUniversal.necessityEntailsPossibility p w = true

Universal accessibility gives consistency via D axiom.

def Semantics.Modality.pImpl (p q : Proposition) : Proposition

Material implication as a proposition.

Equations

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

theorem Semantics.Modality.K_axiom (R : Attitudes.Intensional.World → Attitudes.Intensional.World → Bool) (p q : Proposition) (w : Attitudes.Intensional.World) (hImpl : (Simple R).eval Core.Modality.ModalForce.necessity (pImpl p q) w = true) (hP : (Simple R).eval Core.Modality.ModalForce.necessity p w = true) : (Simple R).eval Core.Modality.ModalForce.necessity q w = true

K Axiom: □(p -> q) -> (□p -> □q). Holds for any R.

theorem Semantics.Modality.simple_K_axiom (R : Attitudes.Intensional.World → Attitudes.Intensional.World → Bool) (p q : Proposition) (w : Attitudes.Intensional.World) : (Simple R).eval Core.Modality.ModalForce.necessity (pImpl p q) w = true → (Simple R).eval Core.Modality.ModalForce.necessity p w = true → (Simple R).eval Core.Modality.ModalForce.necessity q w = true

K axiom holds for all Simple theories unconditionally.