Kripke models

A Kripke model gives each world the finite set of worlds it accesses and each atom the worlds at which it is true. The team-semantic modal logics (BSML, QBSML, modal dependence and inclusion logic, InqML) evaluate formulas on these models. KripkeModel.accessible reads the successor sets as the relation that □ and ◇ of Logic/Modal/Defs.lean take.

The file also states Aloni's two conditions on the accessibility relation relative to a team, which distinguish epistemic from deontic modals: indisputability, that every world of the team sees the same worlds, and state-basedness, that every world of the team sees exactly the team.

Main definitions

• ModalLogic.KripkeModel, with the accessibility relation KripkeModel.accessible.
• Team.IsIndisputable, Team.IsStateBased: the conditions of [Alo22] Definition 5.

Implementation notes

The sources take any relation R ⊆ W × W and a valuation V : X → ℘(W) ([AAY24] Definition 2.2). Successor sets here are Finsets, since the team clauses evaluate subformulas on R[w] as a team; frames are therefore image-finite. The valuation is Prop-valued, and decision procedures for support take [DecidableRel M.val]. Aloni's conditions are not closed under bisimulation ([Alo22] fn. 21); [Ant21] Definition 3.3.1 (p. 46) restates them up to bisimilarity of the successor sets.

References

• [Alo22] Aloni, Logic and Conversation: The Case of Free Choice
• [AAY24] Aloni, Anttila and Yang, State-based Modal Logics for Free Choice
• [Ant21] Anttila, The Logic of Free Choice: Axiomatizations of State-based Modal Logics
• [Vaa08] Väänänen, Modal Dependence Logic

structure ModalLogic.KripkeModel (W : Type u_1) (Atom : Type u_2) : Type (max u_1 u_2)

A Kripke model over worlds W and atoms Atom has successor sets and a valuation.

• access : W → Finset W

  access w is the set of worlds accessible from w.

• val : Atom → W → Prop

  val p w says that the atom p is true at the world w.

def ModalLogic.KripkeModel.accessible {W : Type u_1} {Atom : Type u_2} (M : KripkeModel W Atom) : SetRel W W

In the accessibility relation of M, v is accessible from w when v ∈ M.access w. This is the relation that □ and ◇ of Logic/Modal/Defs.lean take.

Equations

• M.accessible = SetRel.ofSuccessors fun (w : W) => ↑(M.access w)

@[simp]

theorem ModalLogic.KripkeModel.mem_accessible {W : Type u_1} {Atom : Type u_2} {M : KripkeModel W Atom} {w v : W} : (w, v) ∈ M.accessible ↔ v ∈ M.access w

@[instance_reducible]

instance ModalLogic.instDecidableMemProdSetRelAccessibleMkOfDecidableEq {W : Type u_1} {Atom : Type u_2} [DecidableEq W] (M : KripkeModel W Atom) (w v : W) : Decidable ((w, v) ∈ M.accessible)

Equations

• ModalLogic.instDecidableMemProdSetRelAccessibleMkOfDecidableEq M w v = ModalLogic.instDecidableMemProdSetRelAccessibleMkOfDecidableEq._aux_1 M w v

Conditions on accessibility relative to a team

def Team.IsIndisputable {W : Type u_1} (R : W → Finset W) (t : Finset W) : Prop

R is indisputable on the team t when all worlds of t see the same worlds ([Alo22] Definition 5).

Equations

• Team.IsIndisputable R t = ∀ w₁ ∈ t, ∀ w₂ ∈ t, R w₁ = R w₂

def Team.IsStateBased {W : Type u_1} (R : W → Finset W) (t : Finset W) : Prop

R is state-based on the team t when every world of t sees exactly t ([Alo22] Definition 5).

Equations

• Team.IsStateBased R t = ∀ w ∈ t, R w = t

theorem Team.IsStateBased.isIndisputable {W : Type u_1} {R : W → Finset W} {t : Finset W} (h : IsStateBased R t) : IsIndisputable R t

@[instance_reducible]

instance Team.instDecidableIsIndisputableOfDecidableEq {W : Type u_1} [DecidableEq W] (R : W → Finset W) (t : Finset W) : Decidable (IsIndisputable R t)

Equations

• Team.instDecidableIsIndisputableOfDecidableEq R t = { decide := decide (∀ a ∈ t.val.attach, (fun (w₁ : W) (a : w₁ ∈ t) => ∀ w₂ ∈ t, R w₁ = R w₂) ↑a ⋯), reflects_decide := ⋯ }

@[instance_reducible]

instance Team.instDecidableIsStateBasedOfDecidableEq {W : Type u_1} [DecidableEq W] (R : W → Finset W) (t : Finset W) : Decidable (IsStateBased R t)

Equations

• Team.instDecidableIsStateBasedOfDecidableEq R t = { decide := decide (∀ a ∈ t.val.attach, (fun (w : W) (a : w ∈ t) => R w = t) ↑a ⋯), reflects_decide := ⋯ }