The formal axiomatic feature of an example of the Kripke model in terms of ∀, ∃

Question

I am looking for a formal axiomatic definition of an example of the Kripke model in terms of ∀, ∃ , implying knowledge of a simple predicate logic, logical logic, ...

All descriptions of Kripke models i encounter simply introduce new notations through paraphrasing to english linguistic concepts (ie ☐ = "necessity"). While certainly both helpfull and motivating, it does not assure that I will have the same interpretation of what a Kripke model is as someone else.

(This question is the result of a good answer to the question of Kripke semantics: is training software available? )

Answer 1

You can easily replace the forall box, and the diamond with it (or just rewrite it to double). But the point of interpretation in Kripke's models is that the formulas are evaluated on a purely local level. If you represent the Kripke model as a directed graph with labels on tops (labels correspond to sentences), then the formula is always * evaluated in state . It is often called the world according to Cripkes' possible world philosophy.

Now, how do you rate it? Well, just saying that box phi evaluates to true (in the world / state / vertex) if and only if for all reachable worlds (the outgoing neighborhood of the current vertex) phi is true. Compare this to first-order logic, where forall phi is true if and only if phi is true for all objects (globally!).

Now, the diamond follows, replacing it with a double box not, but if you want, diamond phi is evaluated as true (in the world / state / vertex) if and only if there are reachable worlds (the vertex has an outgoing neighbor) in which phi is true. Again, compare this to first-order logic, where phi is true if there is an object (globally), where phi is true.

Ps. The vertices at which we evaluate the formulas have many different names: states, worlds and nodes, among others. It depends on what area of ​​logic you work in, for example. in computer science (CTL, CTL *, ATL, LTL, etc.) we call vertices states , because they can represent some internal state of the system, where, like in epistemic logic, deontic logic, doxal logic, or whatever you have , we could call them (possible) worlds.

Edit, trying to make it clearer:

In FOL, a formula is evaluated globally in a structure / model. forall phi means phi is executed for each member of the domain. In Kripke semantics, the formula is evaluated in a member of the domain w, and the field phi means that for each neighbor w, phi takes place. diamond phi is true in w if there is a neighbor w in which phi is running.