I am looking for a formal axiomatic definition of an example Kripke model in terms of ∀, ∃ assuming knowledge of simple predicate logic, boolean logic,...
All descriptions of Kripke models I encounter simply introduce new notations through paraphrasing to english linguistic concepts (i.e. ☐ = "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 from good answer at question Kripke semantics: learning software available?)
You can easily replace the box with the forall, and the diamond with exists (or just rewrite it to the dual). But the point of the interpretation in Kripke models, is that the formulae are evaluated at a purely local level. If you imagine a Kripke model as just a directed graph with labels on the vertices (the labels corresponds to the propositions), then a formula is always* evaluated at a state. This is often called a world, as per Kripkes possible world philosophy.
Now, how do you evaluate it? Well, simply by saying that box phi is evaluated to true (in a world/state/vertex) if and only if for all reachable worlds (the outgoing neighbourhood of the current vertex) phi is true. Compare this to in first order logic, where forall phi is true if and only if phi is true for all objects (globally!).
Now, the diamond follows by replacing it with the dual not box not, but if you want, diamond phi is evaluated to true (in a world/state/vertex) if and only if exists reachable worlds (the vertex has an outgoing neighbour) in which phi is true. Again, compare this to first order logic, where exists phi is true if there is an object (globally) where phi is true.
Ps. The vertices in which we evaluate formulae have many different names: states, worlds and nodes, amongst others. It depends on which field of logic you are working in, e.g. in computer science (CTL, CTL*, ATL, LTL, etc), we call the vertices states as they might represent some internal state of a system, where as in epistemic logic, deontic logic, doxastic logics or what have you, we might call them (possible) worlds.
Edit, trying to make it clearer:
In FOL, a formula is evaluated globally in the structure/model. forall phi means that phi holds for every member of the domain. In Kripke semantics, a formula is evaluated in a member of the domain w and box phi means that for every neighbours of w, phi is the case. diamond phi is true in w iff there is a neighbour of w in which phi holds.