Kripke models

This file defines KripkeModel, the finite Kripke carrier — successor Finsets and a Bool valuation — that the team-semantic modal logics (BSML, QBSML, modal dependence and inclusion logic, InqML) evaluate on. It is the decidable specialization of the relational primitives of Logic/Modal/Defs.lean.

References

• [Vaa08] — modal dependence logic and team semantics

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.

• access : W → Finset W

  Accessibility: access w is the set of worlds accessible from w.

• val : Atom → W → Bool

  Valuation: val p w is the truth value of atom p at world w.