Kripke Frames
This blueprint, and more generally the kripke-frames Lean project, is part of the assignment for the course Formalized mathematics and proof assistants. The project follows chapters \(1\) and \(2\) of the textbook Boxes and Diamonds.
1 Basic definitions
A Kripke frame or modal frame is a pair \(F = \langle W, R \rangle \) where \(W\) is a nonempty set of worlds and \(R\) is a binary relation on \(W\). Elements of \(W\) are called nodes or worlds, and \(R\) is known as the accessibility relation. When \(Rww'\) holds, we say that \(w'\) is accessible from \(w\).
A Kripke model for the basic modal language is a triple \(M = \langle W, R, V \rangle \), where:
\(W\) is a nonempty set of worlds,
\(R\) is a binary accessibility relation on \(W\), and
\(V\) is a function assigning to each propositional variable \(p\) a set \(V(p)\) of possible worlds.
When \(w \in V(p)\), we say that \(p\) is true at \(w\).
A model \(M\) is based on a frame \(F = \langle W, R \rangle \) iff \(M = \langle W, R, V \rangle \) for some valuation \(V\).
Every modal model determines which modal formulas count as true at which worlds in it. The relation “model \(M\) makes formula \(A\) true at world \(w\)” is the basic notion of relational semantics. The relation is defined inductively and coincides with the usual characterization using truth tables for the non-modal operators.
Truth of a formula \(A\) at world \(w\) in a model \(M\), in symbols \(M, w \Vdash A\), is defined, for the modal operators \(\Box \) and \(\Diamond \), inductively as follows:
\(A \equiv \Box B\): \(M, w \Vdash \Box B\) iff for all \(w' \in W\) such that \(Rww'\), we have \(M, w' \Vdash B\).
\(A \equiv \Diamond B\): \(M, w \Vdash \Diamond B\) iff there exists \(w' \in W\) such that \(Rww'\) and \(M, w' \Vdash B\).
Note that by the first clause, a formula \(\Box B\) is true at \(w\) whenever there are no \(w'\) with \(Rww'\). In such a case, \(\Box B\) is vacuously true at \(w\). Also, \(\Box B\) may be satisfied at \(w\) even if \(B\) is not. The truth of \(B\) at \(w\) does not guarantee the truth of \(\Diamond B\) at \(w\). This holds, however, if \(Rww\) holds (e.g., if \(R\) is reflexive). If there is no \(w'\) such that \(Rww'\), then \(M, w \not\Vdash \Diamond A\), for any \(A\).
1.1 Truth in a model
We will be interested in which formulas are true at every world in a given model. Let’s introduce a notation for this.
A formula \(A\) is true in a model \(M = \langle W, R, V \rangle \), written \(M \Vdash A\), iff \(M, w \Vdash A\) for every \(w \in W\).
1.2 Validity
Formulas that are true in all models, i.e., true at every world in every model, are particularly interesting. They represent those modal propositions which are true regardless of how \(\Box \) and \(\Diamond \) are interpreted, as long as the interpretation is generated by some accessibility relation on possible worlds. We call such formulas valid.
Part of the interest of relational models is that different interpretations of \(\Box \) and \(\Diamond \) can be captured by different kinds of accessibility relations. This suggests that we should define validity not just relative to all models, but relative to all models of a certain kind.
It will turn out, e.g., that \(\Box p \to p\) is true in all models where every world is accessible from itself, i.e., \(R\) is reflexive. Defining validity relative to classes of models enables us to formulate this succinctly: \(\Box p \to p\) is valid in the class of reflexive models.
A formula \(A\) is KripkeModel,valid in a class \(\mathcal{C}\) of models if it is true in every model in \(\mathcal{C}\) (i.e., true at every world in every model in \(\mathcal{C}\)). If \(A\) is valid in \(\mathcal{C}\), we write \(\mathcal{C} \vDash A\), and we write \(\vDash A\) if \(A\) is valid in the class of all models.
A schema, i.e., a set of formulas comprising all and only the substitution instances of some modal characteristic formula \(C\), is true in a model iff all of its instances are (where a formula \(A\) is an instance of a schema if it is a member of the set); and a schema is valid if and only if it is true in every model.
The following schema, called the duality schema, is valid:
By straightforward unfolding of definitions and classical equivalences between \(\diamond \) and \(\Box \).
If \(A\) and \(A \rightarrow B\) are true at a world in a model, then so is \(B\). Hence, the valid formulas are closed under modus ponens.
A formula \(A\) is valid iff all its substitution instances are. In other words, a schema is valid iff its characteristic formula is.
1.3 Entailment
With the definition of truth at a world, we can define an entailment relation between formulas. A formula \(B\) entails \(A\) if and only if, whenever \(B\) is true, \(A\) is true as well.
If \(\Gamma \) is a set of formulas and \(A\) a formula, then \(\Gamma \vDash A\) iif for every model \(M = \langle W, R, V \rangle \) and world \(w \in W\), if \(M, w \vDash B\) for every \(B \in \Gamma \), then \(M, w \vDash A\).
If \(\Gamma \) contains a single formula \(B\), then we write \(B \vDash A\).
2 Properties of accessibility relations
Many modal formulas turn out to be characteristic of simple, and even familiar, properties of the accessibility relation. In one direction, that means that any model that has a given property makes a corresponding formula (and all its substitution instances) true.
The five classical examples of kinds of accessibility relations and the formulas the truth of which they guarantee are listed in Table 1.
Let \(M = \langle W, R, V \rangle \) be a model. If \(R\) has the property on the left side of Table 1, then every instance of the formula on the right side is true in \(M\).
We prove the validity of the modal axioms as follows:
modal axiom K valid:
By unfolding the definition of \(\Box \) and applying function application at accessible worlds.modal axiom T valid:
By reflexivity of the accessibility relation and unfolding of \(\Box \).modal dense valid:
By using density of the accessibility relation and applying the nested \(\Box \) accordingly.modal axiom 4 valid:
By transitivity of the accessibility relation and unfolding the definition of nested \(\Box .\)modal axiom D valid:
By seriality, we find an accessible world witnessing the \(\Diamond \) modality.modal axiom B valid:
By symmetry of the accessibility relation and constructing a witness for \(\Diamond \).modal axiom 5 valid:
By Euclidean property of the relation and unfolding \(\Diamond \) and \(\Box \).
3 Frame definability
One question that interests modal logicians is the relationship between the accessibility relation and the truth of certain formulas in models with that accessibility relation.
It turns out, however, that truth in models is not appropriate for bringing out such correspondences between formulas and properties of the accessibility relation, as special valuations may validate axioms even though the underlying frame has no nice behavior at all. The solution is to remove the variable assignment \(V\) from the equation beuse the correspondence between schemas and properties of the accessibility relation \(R\) turs out to be at the level of frames.
We can define \(F \vDash A\), the notion of a formula being valid in a frame, as: \(M \vDash A\) for all models \(M\) based on \(F\). With this notation, we can establish correspondence relations between formulas and classes of frames. For example: \(F \vDash \Box p \rightarrow p \quad \text{if and only if} \quad F \text{ is reflexive.}\)
If \(F\) is a frame, we say that a formula \(A\) is valid in \(F\), written \(F \Vdash A\), iff \(M \Vdash A\) for every model \(M\) based on \(F\).
If \(\mathcal{F}\) is a class of frames, we say \(A\) is valid in \(\mathcal{F}\), written \(\mathcal{F} \Vdash A\), iff \(F \Vdash A\) for every frame \(F \in \mathcal{F}\).
Even though the converse implications of Theorem 2.1 fail, they hold if we replace “model” by “frame”: for the properties considered in Theorem 2.1, it is true that if a formula is valid in a frame then the accessibility relation of that frame has the corresponding property. So, the formulas considered define the classes of frames that have the corresponding property.
If \(\mathcal{F}\) is a class of frames, we say that a formula \(A\) defines \(\mathcal{F}\) iff \(F \vDash A\) for all and only frames \(F \in \mathcal{F}\).
We now proceed to establish the full definability results for frames.
If the formula on the right side of Table 1 is valid in a frame \(F\), then \(F\) has the property on the left side.
We prove the implications of validity on frame properties as follows:
valid T implies reflexive:
By defining a valuation reflecting the accessibility relation and applying the T axiom.valid 4 implies transitive:
By contraposition: assume failure of transitivity and build a valuation violating the 4 axiom.valid D implies serial:
By contraposition: assume no successor exists and construct a counterexample model violating \(\Diamond \)A.valid B implies symmetric:
By contraposition: assume asymmetry and derive a contradiction from the validity of \(\Box \Diamond A\).valid 5 implies euclidean:
By contraposition: assume failure of Euclidean property and construct a counterexample valuation to contradict \(\Box \Diamond A\).
We notice, that in the proof for D no mention was made of the valuation V. Hence, it proves p that if \( M \Vdash \textbf{D} \) then \( M \) is serial. So D defines the class of serial models, not just frames.
Examples
A small example of a kripke frame is provided.