<p>The most immediate way of doing this that occurs to me is to set up a datatype for you modal language <code>datatype fml = ...</code>, and a satisfaction predicate <code>sat :: ('w ⇒ 'w ⇒ bool) ⇒ 'w ⇒ fml ⇒ bool</code>, and embed the logic in Isabelle. This is (essentially) the approach taken by Xu and Norrish (<a href="https://tqft.net/web/research/students/YimingXu/thesis.pdf" rel="nofollow noreferrer">Xu's Honour's Thesis</a>; <a href="https://doi.org/10.1007/978-3-030-51074-9_30" rel="nofollow noreferrer">IJCAR Paper</a>).
The downside to this approach is that it's a deep embedding, which means you would have to deal with variable binding and substitution yourself.</p>
<p>You could also declare that worlds and an accessibility relation exist, using <code>typedecl</code> and <code>consts</code>, and define 'lifted connectives' as functions which take a world, and return a boolean, e.g. <code>TT ≡ λw. True</code> and <code>◊φ ≡ λw. ∃v. (w R v) ∧ φ v</code> (where <code>R</code> is defined by <code>consts</code>). This is the approach taken by Christoph Benzmüller in this <a href="https://export.arxiv.org/abs/2001.04701" rel="nofollow noreferrer">preprint on Gödel's Ontological Argument</a>.</p>
How to model/formalize the change of the variable (change of world) in Isabelle/HOL?
<p>I am trying to formalize business rules in Isabelle/HOL, but business rules involve the change of the values of some variables, like <code>if x=5 =&gt; x=6</code>. <code>=&gt;</code> is not the usual implication there, because x is 5 in one world (interpretation, semantic domain) and after the execution of the rule the x is 6 and it is already a different world (different interpretation, assignment function, semantic domain). So - technically <code>is x=5 =&gt; x=6</code> is not the formula in First Order Logic and it is not also the formula of Higher Order Logic of Isabelle/HOL. More possible is that it is the formula in dynamic/action logic <code>[rule1](x=5)=(x=6)</code> (that defines that upon application of <code>rule1</code> to the formula in some world yields to the truthful formula in some other world (dynamic/action logic is essentially a kind of modal logic and Kripke/possible world semantics can be applied here).</p>
<p>Now, back to Isabelle/HOL or Coq: FOL/HOL theory is set of formulas in all the worlds or in one particular world. If we stay at FOL/HOL then there is no change of the world, no change of the values of the variables. We should go to the modal logics if we would like to model, reasong about such changes. But can it be done in HOL? This change of world?</p>
<p><a href="http://matryoshka.gforge.inria.fr/pubs/fernandez_burgos_bsc_thesis.pdf" rel="nofollow noreferrer">http://matryoshka.gforge.inria.fr/pubs/fernandez_burgos_bsc_thesis.pdf</a> is good work about formalization of sorting algorithms in Isabelle/HOL, functional programming is used there and there is no need of variables and hence - no this change among worlds. But if we try to model Reinforcement Learning, Markov processes, impertative/object oriented programming, business rules in Isabelle/HOL, then we should express this change. How to do that?</p>
<p>How to express business rule <code>if x=5 =&gt; x=6</code> in Isabelle/HOL?</p>
<p>The same approach can be used in Coq, that is why answers from the Coq community are welcome as well.</p>