Incomplete and Utter Introduction to Modal Logic, Pt. 1

Modal Logic: Introduction

Foreword

Modal logic is one of the most popular branches of mathematical logic. Modal logic covers such areas of human knowledge as mathematics (especially, topology and graph theory), computer science, linguistics, artificial intelligence, and philosophy. Moreover, modal logic in itself still attracts by its mathematical beauty. We would like to introduce the reader to modal logic, fundamental technical tools, and connections with other disciplines. Our introduction is not so comprehensive indeed, the title is an allusion to the wonderful book by Stephen Fry.

History and background

The grandfather of modal logic is the 17th-century German mathematician and philosopher Gottfried Leibniz, one of the founders of calculus and mechanics.

Leibniz

From his point of view, there are two kinds of truth. The statement is called necessarily true if it’s true for any state of affair. Note that, one also has possibly true statements. That is, such statements that could be false, other things being equal. For instance, the proposition “sir Winston Churchill was a prime minister of Great Britain in 1940” is possibly true. As we know, Edward Wood, 1st Earl of Halifax, also could be a prime minister at the same time. Of course, one may provide any other example from the history of the United Kingdom and all of them would be valid to the same degree. In other words, any factual statement might be possibly true since “the trueness” of any factual statement depends strongly on circumstances and external factors. The example of a statement which is necessarily true is 1+1=21 + 1 = 2, where signs 11, 22, ++ and == are understood in the usual sense.

Modal logic became a part of contemporary logic at the beginning of the 20th century. In the 1910s, Clarence Lewis, American philosopher, was the first who proposed to extend the language of classical logic with two modal connectives \Box and \Diamond.

Lewis

Informally, one may read φ\Box \varphi as φ\varphi is necessary. φ\Diamond \varphi has a dual interpretation as φ\varphi is possible. Lewis sought to analyse the notion of necessity from a logical point of view. Thus, modalities in mathematical logic arose initially as a tool for philosophical issue analysis. Lewis understood those modalities intuitively rather than formally. In other words, modal operators had no mathematically valid semantical interpretation.

In the year 1944, Alfred Tarski and John McKinsey wrote a paper called The Algebra of Topology. In this work, the strong connection between modal logic S4{\bf S}4 and topological and metric spaces was established. Historically, topological semantics is the very first mathematical semantics of modal logic. Those results marked the beginning of a separate branch of modal logic that studies the topological aspects of modalities.

Tarski

In the 1950s and 1960s, Saul Kripke formulated relational semantics for modal logic. Note that we will mostly consider Kripke semantics in this post.

Kripke

Later, in the 1970s, such mathematicians as Dov Gabbay, Krister Segerberg, Robert Goldblatt, S. K. Thomason, Henrik Sahlqvist, Johan van Benthem provided the set of technical tools to investigate systems of modal logic much more deeply and precisely. So, modal logic continues its development in the direction that was established by these researchers.

Let us briefly overview some areas of modal logic use.

Topology and graphs

Modal logic provides a compact and laconic language to characterise some properties of directed graphs and topological spaces. In this blog post, we study Kripke frames as the underlying structures. Without loss of generality, one may think of Kripke frames as directed graphs. It means that formal definitions of a Kripke frame and a directed graph are precisely the same. Here, modal language is a powerful tool in representing first-order adjacency properties. We realise the fact that not every reader has a background in first-order logic. In order to keep the post self-contained, we remind the required notions from first-order logic to describe this connection quite clearly.

As we will see, modal logic is strongly connected with binary relations through Kripke frames. The properties of binary relation in a Kripke frame are mostly first-order. We consider examples of first-order relation properties expressed in modal language. Moreover, we formulate and discuss the famous Salqvist’s theorem that connects modal formulas of the special kind with binary relation properties that are first-order definable. Anyway, in such a perspective, one may consider modal logic as a logic of directed graphs since there is no formal difference between a binary relation and edges in a graph. That is, one may use modal logic in directed graph characterisation in a limited way.

You may draw any directed graph you prefer on a plane. A graph is a combinatorial object rather than a geometrical one. A topological space is closer to geometry. Although, there’s a topological way of graph consideration, however. We also discuss how exactly modal logic has a topological interpretation. In the author’s opinion, topological and geometrical aspects of modal logic are one of the most astonishing and beautiful.

It is a well-known result proved by Alfred Tarski and John McKinsey that the modal logic S4{\bf S}4 is the logic of all topological spaces. Similarly to directed graphs, modal logic might be used in classifying topological spaces and other spatial constructions in a restricted way. We will discuss the topological and spatial aspects of modal logic in the second part.

The foundations of mathematics

The foundation of mathematics is the branch of mathematical logic that studies miscellaneous metamathematical issues. In mathematics, we often consider some abstract structure and formulate a theory based on some list axioms that describe primitive properties of considered constructions. The examples are group theory, elementary geometry, graph theory, arithmetics, etc.

In metamathematics, we are interested in what a mathematical theory is in itself. That is, metamathematics arose at the beginning of the previous century to answer philosophical questions mathematically. The main interest was to prove the consistency of formal arithmetics with purely formal methods. As it’s well known, Gödel’s famous incompleteness theorems place limits the formal proof of arithmetics consistency within arithmetics itself.

However, modal logic also allows one to study the properties of provability in formal arithmetical theories. Moreover, the second Gödel’s incompleteness theorem has a purely modal formulation! We discuss that topic in more detail in the follow-up of the series.

Basic definitions and constructions

Let us define the modal language. That’s the starting point for every logic which we take into consideration. In our case, a modal language is a grammar according to rules of which we write logical formulas enriched with modalities. Let PV={p0,p1,}\operatorname{PV} = \{ p_0, p_1, \dots \} be a countably infinite set of propositional variables, or atomic propositions, or propositional letters. Informally, a propositional variable ranges over such atomic statements as “it is raining” or something like that.

A modal language as the set of modal formulas Fm\operatorname{Fm} is defined as follows:

  1. Any piPVp_i \in \operatorname{PV} is a formula.
  2. If φ\varphi is a formula, then ¬φ\neg \varphi is a formula.
  3. If φ\varphi and ψ\psi are formulas, then (φψ)(\varphi \circ \psi) is formula, where {,,}\circ \in \{ \to, \land, \lor\}.
  4. If φ\varphi is a formula, then φ\Box \varphi is a formula.

Note that the possibility operator \Diamond is expressed as \Diamond = ¬¬\neg \Box \neg. In our approach, the statement φ\varphi is possibly true if it’s false that necessiation of ¬φ\neg \varphi is true. Also, one may introduce \Diamond as the primitive one, that is =¬¬\Box = \neg \Diamond \neg.

Also, it is useful to have constants \top and \bot that we define as ¬p0p0\neg p_0 \lor p_0 and ¬\neg \top correspondingly.

As we said, a modal language extends the classical one. One may ask how we can read \Box. Here are several ways to understand this modal connective:

  1. φ\Box \varphi as φ\varphi is necessary. This is historically the very first way of the modal connective reading. Dually, one may read φ\Diamond \varphi as φ\varphi is possible. Modalities of this kind are alethic modalities.
  2. φ\Box \varphi as it is known that φ\varphi. In this case, we call \Box an epistemic modality.
  3. φ\Box \varphi as φ\varphi is a statement provable in formal arithmetics.
  4. \Box as an interior in a topological space. Here, we call such modality a topological one.
  5. φ\Box \varphi as there will be φ\varphi always in the future, a temporal modality, in other words.

We will discuss items 3-5 in the next part of the series as promised.

We defined the syntax of modal logic above. But syntax doesn’t provide logic, only grammar. In logic, one has inference rules and the definition of proof. We also want to know what kind of modal statements we need to prove basically. Firstly, let us describe a more basic notion like normal modal logic.

By normal modal logic, we mean a set of modal formulas L\mathcal{L} that contains all Boolean tautologies; AK{\bf AK}-axiom (named after Kripke) (pq)(pq)\Box (p \to q) \to (\Box p \to \Box q) and closed under the following three inference rules:

  1. If φL\varphi \in \mathcal{L} and φψL\varphi \to \psi \in \mathcal{L}, then ψL\psi \in \mathcal{L} (Modus ponens). That is the basic logical rule that allows you to get a consequence from an implication if you have a premise.
  2. If φL\varphi \in \mathcal{L}, then φL\Box \varphi \in \mathcal{L} (Necessiation rule). If φ\varphi belongs to a logic, then φ\Box \varphi belongs to L\mathcal{L} too. Informally, if φ\varphi is provable, then φ\varphi is necessary.
  3. If φ(p)L\varphi ( p ) \in \mathcal{L}, then φ(p:=ψ)L\varphi (p := \psi) \in \mathcal{L}. If formula φ\varphi with variable pp belongs to a logic, then its instances belong to the same logic. Here, the instance of the formula is the result of a substitution of another formula instead of a variable. In other words, any normal modal logic is closed under substitution.

The fact that any normal modal logic contains all Boolean tautologies tell us that modal logic extends the classical one. Literally, the Kripke axiom AK{\bf AK}-axiom denotes that \Box distributes over implication. Such an explanation doesn’t help us so much, indeed. It’s quite convenient to read this axiom in terms of necessity. Then, if the implication φψ\varphi \to \psi is necessary and the premise is necessary, then the consequence is also necessary. For instance, it is necessary that if the number is divided by four then this number is divided by two. Then, if it is necessary that the number is divided by four, then it is necessary that it’s divided by two.

Of course, within the natural language that we use in everyday speech the last two sentences sound quite monotonous, but we merely illustrated how this logical form works by example. In such a situation, it’s crucially important to follow the formal structure even if this structure looks wordy and counterintuitive. Of course, this sometimes runs counter to our preferences in linguistic aesthetics, although structure following allows analysing modal sentences much more precisely.

If we take into consideration some logical system represented by axioms and inference rules, then one needs to determine what derivation is in an arbitrary normal modal logic. A derivation of formula φ\varphi in normal modal logic L\mathcal{L} is a sequence of formulas, each element of which is either axiom or some formula obtained from the previous ones via inference rules. The last element of such a sequence is a formula φ\varphi itself.

Here is an example of derivation in normal modal logic:

  1. φ(ψ(φψ))\varphi \to (\psi \to (\varphi \land \psi)) Boolean tautology
  2. (φ(ψ(φψ)))\Box (\varphi \to (\psi \to (\varphi \land \psi))) Necessiation rule
  3. (φ(ψ(φψ)))(φ(ψ(φψ)))\Box (\varphi \to (\psi \to (\varphi \land \psi))) \to (\Box \varphi \to \Box (\psi \to (\varphi \land \psi))) AK{\bf AK}-axiom.
  4. φ(ψ(φψ))\Box \varphi \to \Box (\psi \to (\varphi \land \psi)) Modus ponens, (2), (3)
  5. (ψ(φψ))(ψ(φψ))\Box (\psi \to (\varphi \land \psi)) \to (\Box \psi \to \Box (\varphi \land \psi)) K{\bf K}-axiom
  6. φ(ψ(φψ))\Box \varphi \to (\Box \psi \to \Box (\varphi \land \psi)) Transitivity of implication, (4), (5)
  7. (φ(ψ(φψ)))(φψ(φψ))(\Box \varphi \to (\Box \psi \to \Box (\varphi \land \psi))) \to (\Box \varphi \land \Box \psi \to \Box (\varphi \land \psi)) The instance of a Boolean tautology
  8. (φψ)(φψ)(\Box \varphi \land \Box \psi) \to \Box (\varphi \land \psi) Modus ponens, (6), (7)

We leave the converse implication as an exercise to the reader.

The minimal normal modal logic K{\bf K} is defined via the following list of axioms and inference rules:

  1. (p(qr))((pq)(pr))(p \to (q \to r)) \to ((p \to q) \to (p \to r))
  2. p(qp)p \to (q \to p)
  3. p(q(pq))p \to (q \to (p \land q))
  4. (p1p2)pi(p_1 \land p_2) \to p_i, i=1,2i = 1,2
  5. pi(p1p2)p_i \to (p_1 \lor p_2), i=1,2i = 1,2
  6. (qp)((rp)(qr)p)(q \to p) \to ((r \to p) \to (q \lor r) \to p)
  7. (pq)((p¬q)¬p)(p \to q) \to ((p \to \neg q) \to \neg p)
  8. ¬¬pp\neg \neg p \to p
  9. (pq)(pq)\Box (p \to q) \to (\Box p \to \Box q)
  10. Inference rules: Modus Ponens, Necessiation, Substitution.

The axioms (1)-(8) are exactly axioms of the usual classical propositional logic that axiomatise the set of Boolean tautologies together with Modus Ponens and Substitution rule. The axiom (9) is a Kripke axiom AK{\bf AK}. One may also claim that K{\bf K} is the smallest normal modal logic. In the definition of normal modal logic, we just require that the set of formulas should contain Boolean tautologies, etc. By the way, there might be something different from the required list of formulas. For instance, the set of all formulas is also a normal modal logic, the trivial one. The minimal normal modal logic is a normal modal logic that contains only Boolean tautologies, AK{\bf AK}-axiom and closed under the inference rules, no less no more. The logic K{\bf K} is the underlying logic for us. Other modal logics are solely extensions of K{\bf K}. Note that modal logic is not needed to be a normal one. Weaker modal logics are studied via so-called neighbourhood semantics that we drop in our introductory post.

Kripke semantics

We have defined the syntax of the modal logic above introducing the grammar of a modal language. Let us define Kripke frames and models to have the truth definition in modal logic.

Definition A Kripke frame is a pair F=W,R\mathbb{F} = \langle W, R \rangle, where WW is a non-empty set, a set of so-called possible worlds, informally. Note that we will call an element of WW a world or a point. World and point are synonyms for us. RW×WR \subseteq W \times W is a binary relation on WW. For example, the set {0,1,...,n}\{0, 1, ..., n\} with strict order relation << is a Kripke frame. Moreover, any directed graph might be considered as a Kripke frame, where the set of vertices is a set of possible worlds and the set of edges is a binary relation.

Definition A Kripke model is a pair M=F,ϑ\mathcal{M} = \langle \mathcal{F}, \vartheta \rangle, where F=W,R\mathbb{F} = \langle W, R \rangle is a Kripke frame and ϑ:PV2W\vartheta : \operatorname{PV} \to 2^W is a valuation function that maps any proposition variable to some subset of possible words. Informally, we should match any atomic statement with corresponding states of affairs in which this atomic statement is true. For complex formulas, we introduce the truth definition inductively. We denote this relation as M,wφ\mathcal{M}, w \models \varphi that should be readen as “in model M\mathcal{M}, in world ww the statement φ\varphi is true”.

  1. M,wp\mathcal{M}, w \models p iff wv(p)w \in v ( p )
  2. M,w⊭\mathcal{M}, w \not\models \bot, that is, there is no point in which false could be true.
  3. M,wφψ\mathcal{M}, w \models \varphi \to \psi iff M,wφ\mathcal{M}, w \models \varphi implies M,wψ\mathcal{M}, w \models \psi
  4. M,wφ\mathcal{M}, w \models \Box \varphi iff for all vv such that wRvw R v, M,vφ\mathcal{M}, v \models \varphi

It is not so difficult to obtain the truth conditions for other connectives. One needs to keep in mind that the other Boolean connectives are introduced via implication and bottom as

  1. ¬φφ\neg \varphi \leftrightharpoons \varphi \to \bot
  2. φψ¬(φ¬ψ)\varphi \lor \psi \leftrightharpoons \neg (\varphi \to \neg \psi)
  3. φψ¬(¬φ¬ψ)\varphi \land \psi \leftrightharpoons \neg (\neg \varphi \lor \neg \psi)

We also know that =¬¬\Diamond = \neg \Box \neg, so the truth definition for φ\Diamond \varphi is the following one:

M,wφ\mathcal{M}, w \models \Diamond \varphi iff there exists vv such that wRvw R v and M,vφ\mathcal{M}, v \models \varphi.

There are a lot of examples of Kripke models, indeed. Here, we refer the reader to the book Modal Logic of Open Minds by Johan van Benthem to study miscellaneous cases in depth. Let us consider briefly the following graph as a Kripke frame with the valuation map ϑ\vartheta:

Example Frame Example Model
As an exercise, the reader might determine which formulas are true in every point of the model above.

Also, we will use the following notions:

  1. Mφ\mathcal{M} \models \varphi iff M,wφ\mathcal{M}, w \models \varphi for each ww. That is, a formula φ\varphi is true in a Kripke model M\mathcal{M} if and only if it’s true in each possible world ww
  2. Fφ\mathcal{F} \models \varphi iff for each valuation vv and for all ww, F,wφ\langle \mathcal{F}, w \rangle \models \varphi. One should read Fφ\mathcal{F} \models \varphi as φ\varphi is valid in a frame F\mathcal{F} In other words, a formula φ\varphi is true in a Kripke frame F\mathcal{F} if and only if it’s true in every Kripke model on this frame as an underlying one.
  3. Log(F)={φFmFφ}\operatorname{Log}(\mathcal{F}) = \{ \varphi \in Fm \: | \: \mathcal{F} \models \varphi \}, where F\mathcal{F} is a Kripke frame. We will call the set Log(F)\operatorname{Log} (\mathcal{F}) the logic of frame F\mathcal{F}
  4. Let F\mathbb{F} be a class of Kripke frames, then Log(F)=FFLog(F)\operatorname{Log}(\mathbb{F}) = \bigcap \limits_{\mathcal{F} \in \mathbb{F}} \operatorname{Log}(\mathcal{F}). More simply, the logic of class is a set of formulas each of which is true in every Kripke frame that belongs to this class.

In logic, we often require that any true formula should be provable. If some logic satisfies this requirement, then we call that the logic is complete. Here, a modal logic L\mathcal{L} is a Kripke complete if and only if there exists some class of Kripke frames F\mathbb{F} such that L=Log(F)\mathcal{L} = \operatorname{Log}(\mathbb{F}). That is, any valid formula in this class of frames is provable in L\mathcal{L}.

So, we’re going to solve the following issue. What’s the most general logic which is valid in an arbitrary Kripke frame? In other words, we are going to characterise the logic of all possible Kripke frames. We defined above what minimal normal modal logic is. One may show that this logic is the logic of all Kripke frames:

Theorem

K=Log(F){\bf K} = \operatorname{Log} (\mathbb{F}), where F\mathbb{F} is the class of all Kripke frames.

The left inclusion KLog(F){\bf K} \subseteq \operatorname{Log} (\mathcal{F}) called soundness is more or less obvious. The soundness theorem claims that the logic of all Kripke frames is the normal modal one. We will prove only that any formula provable in K{\bf K} is valid in any Kripke frame and show that Log(F)\operatorname{Log}(\mathcal{F}) is closed under substitution, where FF\mathcal{F} \in \mathbb{F} is an arbitrary Kripke frame.

Let us show that the normality axiom is valid in an arbitrary Kripke frame.

Let F=W,R\mathbb{F} = \langle W, R \rangle be a Kripke frame and ϑ:PVP(W)\vartheta : \operatorname{PV} \to \mathcal{P}(W) a valuation map. So, we have a Kripke model M=F,ϑ\mathcal{M} = \langle \mathbb{F}, \vartheta \rangle. Let M,a(φψ)\mathcal{M}, a \models \Box (\varphi \to \psi) and M,aφ\mathcal{M}, a \models \Box \varphi. Let aRba R b, then M,bφψ\mathcal{M}, b \models \varphi \to \psi and M,bφ\mathcal{M}, b \models \varphi by the truth definition for \Box. So M,bφ\mathcal{M}, b \models \varphi, so far as Modus Ponens holds in every Kripke model. Thus, M,aφ\mathcal{M}, a \models \Box \varphi.

Now we show that Log(F)\operatorname{Log}(\mathbb{F}) is closed under substitution. We provide only a sketch since the full proof is quite technical.

Let ϑ:PVP(W)\vartheta : \operatorname{PV} \to \mathcal{P}(W) be a valuation and M=F,ϑ\mathcal{M} = \langle \mathcal{F}, \vartheta \rangle a Kripke model. Let us put φ={wWM,wφ}||\varphi|| = \{ w \in W \: | \: \mathcal{M}, w \models \varphi \}, the set of all points in a Kripke model, where the formula φ\varphi is true. Let Fφ(p)\mathcal{F} \models \varphi ( p ) and let ψ\psi be an arbitrary formula. We build a Kripke model M=F,ϑ\mathcal{M} = \langle \mathcal{F}, \vartheta' \rangle such that ϑ(p)=ψ\vartheta' ( p ) = ||\psi||. Then, one may show by induction that M,xφ(p:=ψ)M,xφ(p)\mathcal{M}, x \models \varphi ( p := \psi ) \Leftrightarrow \mathcal{M}', x \models \varphi ( p ).

The right inclusion (KLog(F){\bf K} \supseteq \operatorname{Log}(\mathbb{F})) called completeness is quite non-trivial, one needs to build the so-called canonical model. We haven’t defined what a canonical frame and model are. The idea of a canonical frame is that an observed logic itself forms a Kripke frame (and Kripke model too). Canonical frames and models often allow us to prove the fact that some normal modal logic is complete with respect to some class of Kripke frames. We provide only the main proof sketch. The following construction is very and very abstract, but sometimes one has to be patient to produce fruits.

Let Γ\Gamma be a set of formulas and L\mathcal{L} a normal modal logic. Γ\Gamma is L\mathcal{L}-inconsistent, if there exist some formulas φ1,,φn\varphi_1, \dots, \varphi_n such that ¬(φ1φn)L\neg (\varphi_1 \land \dots \land \varphi_n) \in \mathcal{L}. That is, the set of formulas Γ\Gamma is L\mathcal{L}-inconsistent, if there exists a finite subset such that negation of its conjuction is provable in an observed logic. Γ\Gamma is L\mathcal{L}-consistent, if Γ\Gamma is not inconsistent.

A L\mathcal{L}-consistent set Γ\Gamma is maximal if it doesn’t have any non-trivial extensions. In other words, if Γ\Gamma is a subset of Γ\Gamma', where Γ\Gamma' is a L\mathcal{L}-consistent, then Γ=Γ\Gamma = \Gamma'.

Now we are ready to define a canonical frame. Let L\mathcal{L} be a normal modal logic, then a canonical frame is a pair FL=WL,RL\mathcal{F}^{\mathcal{L}} = \langle W^{\mathcal{L}}, R^{\mathcal{L}} \rangle, where WLW^{\mathcal{L}} is the set of all maximal L\mathcal{L}-consistent set. RR is a canonical relation such that:

ΓRLΔφΓφΔ\Gamma R^{\mathcal{L}} \Delta \Leftrightarrow \Box \varphi \in \Gamma \Rightarrow \varphi \in \Delta. That is, any boxed formula from Γ\Gamma can be unboxed in Δ\Delta.

A canonical model is a canonical frame equipped with the canonical valuation ϑL(p)={ΓWLpΓ}\vartheta^{\mathcal{L}} ( p ) = \{ \Gamma \in W^{\mathcal{L}} \: | \: p \in \Gamma \}. This valuation maps each variable to set of all maximal L\mathcal{L}-consistent sets that contain a given variable.

Here comes the theorem:

Theorem

  1. ML,ΓφφΓ\mathcal{M}^{\mathcal{L}}, \Gamma \models \varphi \Leftrightarrow \varphi \in \Gamma, i.e., the truth definition is generated by membership to some maximal consistent set.
  2. φ\varphi is provable in L\mathcal{L} iff MLφ\mathcal{M}^{\mathcal{L}} \models \varphi, i.e. any formula is provable iff it is true at every point of a canonical model.
  3. If φLog(FL)\varphi \in \operatorname{Log}(\mathcal{F}^{\mathcal{L}}), then φ\varphi is provable in L\mathcal{L}, i.e. any formula that valid in a canonical frame is provable.

The completeness theorem for K{\bf K} is a simple corollary from the theorem above. Any formula that provable in K{\bf K} is valid in every frame. If it is valid in every frame, then it is also valid in the canonical frame. Thus, a formula provable in K{\bf K}. That’s it. The construction above allow us to claim that any formula that valid in all possible Kripke frames is provable in K{\bf K}. The reader might read the complete proof here.

As we told above, modal logic is strictly connected with first-order logic. First-order logic extends classical logic with quantifiers as follows. Classical propositional logic deals with statements and the ways of their combinations with such connectives as a conjunction, disjunction, negation, and implication. For example, if Neil Robertson will make a maximum 147 break, then he will win the current frame (a snooker frame, not Kripke frame). This statement has the form pqp \to q. pp denotes Neil Robertson will make a maximum 147 break. qq denotes he will win the current frame. In first-order logic, one may analyse formally universal and existential statements which tell about properties of objects.

More strictly, we add to the list of logical connectives quantifiers \forall (for all …) and \exists (there exists …). We extended the set of connectives, so one needs to redefine the notion of formula. Suppose also we have a countably infinite set of relation symbols (or letters) of arbitrary finite arity. We well denote them as PP. Also one has a countably infinite set of individual variables x,y,z,x, y, z, \dots.

The notion of formula with such set of predicate symbols:

  1. If x1,,xnx_1, \dots, x_n are variables and PP is a relation symbol of an arity nn, then P(x1,,xn)P(x_1, \dots, x_n) is a formula
  2. \bot is a formula
  3. If A,BA, B are formulas, then (AB)(A \to B) is a formula
  4. If xx is a variable and xA\forall x \: A is a formula

The other connectives and quantifiers are expressed as follows:

  1. ¬A:=A\neg A := A \to \bot
  2. (AB):=¬(A¬B)(A \land B) := \neg (A \to \neg B)
  3. (AB):=¬(¬A¬B)(A \lor B) := \neg (\neg A \land \neg B)
  4. (xA):=¬x¬A(\exists x \: A) := \neg \forall x \: \neg A

Note that there is a need to distinguish free and bound variables in a first-order formula. A variable is bounded if it’s captured by a quantifier. Otherwise, a variable is called free. For instance, the variable xx is bounded in the formula xR(x,y,z)\exists x \: R(x, y, z). One may read this formula, for instance, as there is exists a point xx such that xx lies between points yy and zz. Variables yy and zz are free in this formula since there are no quantifiers that bound them.

Now we would like to realise what truth for a first-order formula is. Unfortunately, we don’t have truth tables with 0 and 1 as in classical propositional logic. The definition of truth for the first-order case is much more sophisticated. An interpretation of the first-order language (as the infinite set of relation symbols) is a pair A,I\langle A, I \rangle, where AA is a non-empty set (a domain) and II is an interpretation function. II maps every relation letter PP of an arity nn to the function of type An{0,1}A^{n} \to \{ 0, 1 \}, i.e., some nn-ary predicate on a domain AA. To define truth conditions for first-order formulas, we suppose that we have an arbitrary variable assignment function vv such that vv maps every variable to some element of our domain MM. An interpretation and variable assignment give us a first-order model, the definition of truth is the following one:

  1. MFOP(x1,,xn)I(P)(v(x1),,v(xn))=1\mathcal{M} \models_{\operatorname{FO}} P(x_1, \dots, x_n) \Leftrightarrow I ( P ) (v(x_1), \dots, v(x_n)) = 1
  2. MFOABMFOAMFOB\mathcal{M} \models_{\operatorname{FO}} A \to B \Leftrightarrow \mathcal{M} \models_{\operatorname{FO}} A \Rightarrow \mathcal{M} \models_{\operatorname{FO}} B
  3. MFO\mathcal{M} \nvDash_{\operatorname{FO}} \bot
  4. MFOxA(x)MFOA(a)\mathcal{M} \models_{\operatorname{FO}} \forall x \: A(x) \Leftrightarrow \mathcal{M} \models_{\operatorname{FO}} A(a) for each aAa \in A

Note that the truth definition for existential formulas might be expressed as follows: MxA(x)MFOA(a)\mathcal{M} \models \exists x \: A(x) \Leftrightarrow \mathcal{M} \models_{\operatorname{FO}} A(a) for some aAa \in A.

A first-order formula is satisfiable if it’s true in some model and it’s valid if it’s true in every interpretation.

We use FO\models_{\operatorname{FO}} in the same sense as in Kripke models, but with the index FO\operatorname{FO} to distinguish both relations that denoted equally.

Let us comment on the conditions briefly. The first condition is the underlying one. As we said above any nn-ary relation symbol maps to nn-ary relation on observed domain, that is, nn-ary truth function An{0,1}A^n \to \{ 0,1 \}. On the other hand, any variable (which should be free, indeed) maps to some element of a domain. After that, we apply the obtained truth function to the result of the variable assignment. We obviously require that an elementary formula P(x1,,xn)P(x_1, \dots, x_n) is true in the model M\mathcal{M} if the result of that application equals 11. The last fact mean that a predicate is true on elements v(x1),,v(xn)v(x_1), \dots, v(x_n).

For example, suppose we have a ternary relation symbol RR such that we have interpret R(x,y,z)R(x,y,z) as yy lies between points xx and zz. Suppose also that our domain is the real line R\mathbb{R}. We map our ternary symbol to the truth function π\pi such that π(a,b,c)=1\pi(a,b,c) = 1 if and only if aba \leq b and bcb \leq c. We also define the variable assignment as v(x)=2v(x) = \sqrt{2}, v(y)=3v(y) = \sqrt{3}, and v(z)=5v(z) = \sqrt{5}.

It is clear that in the model on real numbers M\mathcal{M} the formula R(x,y,z)R(x,y,z) is true since I(R)(v(x),v(y),v(z))=π(2,3,5)=1I ( R ) (v(x), v(y), v(z)) = \pi(\sqrt{2}, \sqrt{3}, \sqrt{5}) = 1. The last equation follows from the obvious fact that 235\sqrt{2} \leq \sqrt{3} \leq \sqrt{5}.

The items 2 and 3 are agreed with our understanding of what false and implication are. The last condition is the truth condition for quantified formulas. This condition describes our intuition about the circumstance when a universal statement is true. Let us consider an example. Let us assume that we want to read the formula A(x)A(x) as xx has a father. Our domain MM is the set of all people who have ever lived on the planet. Then the statement xA(x)\forall x \: A(x) is true since every human has a father, as the reader already knows even regardless of this post.

Now let us return to modal logic and Kripke models. Let us take a look at truth defitions for \Box and \Diamond one more time:

  1. M,wφuwRu&M,uφ\mathcal{M}, w \vdash \Diamond \varphi \Leftrightarrow \exists u \:\: w R u \: \& \: \mathcal{M}, u \models \varphi, i.e., a formula φ\Diamond \varphi is true at the point ww, if there exists RR-successor of ww, namely, uu such that a formula φ\varphi is true.
  2. M,wφuwRuM,uφ\mathcal{M}, w \vdash \Box \varphi \Leftrightarrow \forall u \:\: w R u \Rightarrow \mathcal{M}, u \models \varphi, i.e., a formula φ\Box \varphi is true at the point ww, if at every RR-successor of ww a formula φ\varphi is true.

In those explanations, we used first-order quantifiers over points in Kripke models informally. But we may build the bridge between Kripke models and first-order one more precisely. Let us assume that we have the following list of predicate and relation symbols:

  1. A binary relation symbols RR
  2. A countable infinite set of unary predicate letters PiP_i, where i=0,1,2i = 0, 1, 2 \dots

The translation tt from modal formulas to first-order ones is defined inductively

  1. t(pi)(w)=Pi(a)t(p_i)(w) = P_i (a), where xx is a variable
  2. t(φψ)(w)=t(φ)(w)t(ψ)(w)t(\varphi \to \psi)(w) = t(\varphi)(w) \to t(\psi)(w)
  3. t()(w)=t(\bot)(w) = \bot
  4. t(φ)(w)=v(R(w,v)t(φ)(v))t(\Box \varphi)(w) = \forall v \: (R(w, v) \to t(\varphi)(v))

The translation for diamonds is the following one:

t(ϕ)(w)=v(R(w,v)t(ϕ)(v))t(\Diamond \phi)(w) = \exists v \: (R(w, v) \land t(\phi)(v))

In other words, every modal formula has its first-order counterpart, a formula with one free variable ww.

The reader can see that we just mapped modalised formulas the first-order one with respect to their truth definition. But there’s the question: is the truth of formula really preserved with such a translation? Here is the lemma:

Lemma

Let M=W,R,ϑ\mathcal{M} = \langle W, R, \vartheta \rangle be a Kripke model and aWa \in W, then M,aφ\mathcal{M}, a \models \varphi if and only if MFOt(φ)(a)\mathcal{M}' \models_{\operatorname{FO}} t(\varphi)(a).

Here M\mathcal{M}' is the first-order model such that its domain is WW, and interpretation for the predicate letter is agreed with the relation on an observed Kripke frame. An interpretation of unary predicate letters is agreed with the evaluation in a Kripke model as follows. MPi(w)\mathcal{M}' \models P_i(w) if and only if wϑ(pi)w \in \vartheta(p_i). Here pip_i is a propositional variable with the same index ii. In other words, those unary predicate letters allow us to encode an evaluation via the first-order language.

The lemma claims that a modal formula is true at some point ww if only if its translation (in which a point ww is a parameter) in the first-order language is true in the corresponding model and, hence, satisfiable. That is, one has a bridge between truth in a Kripke modal and first-order satisfiability. If a formula is true in some model at some point, it doesn’t imply its provability in the minimal normal modal logic. We would like to connect provability in K{\bf K} and in first-order predicate calculus. Here is the theorem proved by Johan van Benthem in the 1970s:

Theorem

A formula ϕ\phi is provable in K{\bf K} iff and only the universal closure of its standard translation wt(ϕ)(w)\forall w \: t(\phi)(w) is provable in the first-order predicate calculus.

That is, there’s an embedding of K{\bf K} to first-order logic. The lemma and the theorem above gives more precise meaning of the analogy between modalities and quantifiers which looks informal prima facie.

Modal formulas are closely connected with the special properties of relations on Kripke frames. We mean a modal formula is able to express the condition on a relation in a Kripke frame. Let us consider a simple example.

Suppose we have a set WW with transitive relation RR. It means that for all a,b,cWa, b, c \in W, if aRba R b and bRcb R c, then aRca R c. Let us show that formula pp\Box p \to \Box \Box p is valid on frame W,R\langle W, R \rangle if and only if this frame is transitive. For simplicity, we will use the equivalent form written in diamonds: pp\Diamond \Diamond p \to \Diamond p. It is very easy to show that these formulas are equivalent to each other:

Transitivity Inference

Lemma

Let F=W,R\mathcal{F} = \langle W, R \rangle, then Fpp\mathcal{F} \models \Diamond \Diamond p \to \Diamond p iff RR is transitive.

Let W,R\langle W, R \rangle be a transitive frame, ϑ\vartheta be a valutation and wWw \in W. So, we have a Kripke model M=W,R,ϑ\mathcal{M} = \langle W, R, \vartheta \rangle. Suppose M,wp\mathcal{M}, w \models \Diamond \Diamond p. We need to show that M,wp\mathcal{M}, w \models \Diamond p. If M,wp\mathcal{M}, w \models \Diamond \Diamond p, then there exists vWv \in W such that wRvw R v and M,vp\mathcal{M}, v \models \Diamond p. But, there exists uWu \in W such that vRuv R u and M,up\mathcal{M}, u \models p. Well, we have wRvw R v and vRuv R u, so we also have wRuw R u by transitivity. Hence, M,wp\mathcal{M}, w \models \Diamond p. Consequently, M,wpp\mathcal{M}, w \models \Diamond \Diamond p \to \Diamond p.

The converse implication is harder a little bit. Let F=W,R\mathbb{F} = \langle W, R \rangle be a Kripke frame such that Fpp\mathcal{F} \models \Diamond \Diamond p \to \Diamond p, that is, this formula is true for each valuation map. Let w,v,uWw, v, u \in W such that wRvw R v and vRuv R u. Let us show that wRuw R u.

Suppose, we have the valuation such that ϑ(p)={w}\vartheta ( p ) = \{ w \}. So, F,ϑ,wp\langle \mathcal{F}, \vartheta \rangle, w \models \Diamond \Diamond p. On the other hand, F,ϑ,wpp\langle \mathcal{F}, \vartheta \rangle, w \models \Diamond \Diamond p \to \Diamond p, so F,ϑ,wp\langle \mathcal{F}, \vartheta \rangle, w \models \Diamond p. But we have only one point, where pp is true, uu. So, wRuw R u.

Also we may make this table that describes the correspondence between modal formulas:

Name Modal formula Relation
AT{\bf AT} pp\Box p \to p for all xWx \in W, xRxx R x
A4{\bf A4} pp\Box p \to \Box \Box p for all x,y,zWx, y, z \in W, xRyx R y and yRzy R z implies xRzx R z
AD{\bf AD} pp\Box p \to \Diamond p Seriality: for all xWx \in W there exists yWy \in W such that xRyx R y
ACR{\bf ACR} pp\Diamond \Box p \to \Box \Diamond p Church-Rosser property (confluence): if xRyx R y and xRzx R z, then there exists x1x_1 such that yRx1y R x_1 and zRx1z R x_1
AB{\bf AB} ppp \to \Box \Diamond p Symmetry: for all x,yWx, y \in W, xRyx R y implies yRxy R x

Let us take a look at the corresponding frame properties on a picture:

Reflexivity Transitivity Seriality Confluence Symmetry

More formally and generally, a modal formula φ\varphi defines (or characterises) the class of frames F\mathbb{F}, if for each frame F\mathcal{F},FφFF\mathcal{F} \models \varphi \Leftrightarrow F \in \mathcal{F}. That is, a formula pp\Box p \to p characterises the class of all reflexive frames, etc.

It is clear that our list is incomplete as this blog post itself, but we have described the most popular formulas and the corresponding relation properties. By the way, one may obtain new modal logics adding one of these formulae as axioms and get a botanic garden of modal logics. There are three columns in the following table. The first column is the name of the concrete logic, a sort of identification mark. The second column describes how the given logic is axiomatised. Generally, KΓ{\bf K} \oplus \Gamma denotes that we extend minimal normal modal logic with formulas from Γ\Gamma as the additional axioms. The third column is the completeness theorem that claims that a given logic is the set of formulas that are valid in some class of Kripke frames.

Name Logic Frames
T{\bf T} KAT{\bf K} \oplus {\bf AT} The logic of all reflexive frames
K4{\bf K}4 KA4{\bf K} \oplus {\bf A}4 The logic of all transitive frames
D{\bf D} KAD=K{\bf K} \oplus {\bf AD} = {\bf K} \oplus \Diamond \top The logic of all serial frames
S4{\bf S}4 TA4{\bf T} \oplus {\bf A}4 = K4AT{\bf K}4 \oplus {\bf AT} The logic of all preorders (reflexive and transitive relations)
S4.2{\bf S}4.2 S4ACR{\bf S}4 \oplus {\bf ACR} The logic of all confluent preorders (preorders that satisfy the Church-Rosser property)
S5{\bf S}5 S4AB{\bf S}4 \oplus {\bf AB} The logic of all equivalence relations

The fact that a given logic is the logic of some class of frames tells us that this logic is complete with respect to this class. For instance, when we tell that T{\bf T} is the logic of all reflexive frames, it means that any formula which is valid in an arbitrary reflexive frame is provable in T{\bf T}. One may prove the corresponding completeness theorem ensuring that the formulas from the table are canonical ones.

A modal formula φ\varphi is called canonical, if the logic L=Kφ\mathcal{L} = {\bf K} \oplus \varphi is the logic of its canonical frame. It’s not difficult to ensure that if logic has an axiomatisation with canonical formulas, then this logic is Kripke complete. For example, if we want to prove that S4{\bf S}4 is the logic of all preorders, it’s enough to check that the relation on the S4{\bf S}4-canonical frame is a preorder.

Let us remember first-order logic once more. The first is to rewrite the first table above changing the properties for the third column with the relevant first-order formulas as follows:

Name Modal formula Property of a frame written in the first-order language
AT{\bf AT} pp\Box p \to p x(xRx)\forall x \: (x R x)
A4{\bf A4} pp\Box p \to \Box \Box p xyz(xRyyRzxRz)\forall x \: \forall y \: \forall z \: (x R y \land y R z \to x R z)
AD{\bf AD} pp\Box p \to \Diamond p xy(xRy)\forall x \: \exists y \:\: (x R y)
ACR{\bf ACR} pp\Diamond \Box p \to \Box \Diamond p xyz(xRyxRzz1(yRz1zRz1))\forall x \: \forall y \: \forall z \:\: (x R y \land x R z \to \exists z_1 \:\: (y R z_1 \land z R z_1))
AB{\bf AB} ppp \to \Box \Diamond p xy(xRyyRx)\forall x \: \forall y \:\: (x R y \to y R x)

The current question we would like to ask is there some bridge between modal formulas and first-order properties of relation in a Kripke frame. Before that, we introduce a fistful of definitions.

A modal formula φ\varphi is called elementary if the class of frames which this formula characterises is defined by some first-order formula. For example, the formulas from the table above are elementary since the corresponding frame properties might be arranged as well-formed first-order formulas.

Let us define the special kind of formulas that we call Sahlqvist formulas:

A box-atom is a formula of the form p\nabla p or ¬p\nabla \neg p, where \nabla is a finite (possibly, empty) sequence of boxes. A Sahlqvist formula is a modal formula of the form (φψ)\Box \dots \Box (\varphi \to \psi). \Box \dots \Box is a nn-sequence of boxes, n0n \geq 0. φ\varphi is formula that contains \land, \lor, \Box, \Diamond, perhaps, 00 times. ϕ\phi is constructed from box-atoms, \land and \Diamond.

For instance, any formula from our table is a Sahlqvist formula. The example of a non-Sahlqvist formula is the McKinsey formula pp\Box \Diamond p \to \Diamond \Box p, which is also non-elementary. This formula should be a separate topic for an extensive discussion. The reader may continue such a discussion herself with the classical paper by Robert Goldblatt called The McKinsey Axiom is not Canonical.

Theorem (Sahlqvist’s theorem)

Let φ\varphi be a Sahlqvist formula, then φ\varphi is canonical and elementary.

Sahlqvist’s theorem is extremely non-trivial to be proved accurately in detail. However, this theorem gives us crucially significant consequences. If some normal modal logic is defined with Sahlqvist formulas as axioms, then it’s automatically Kripke complete since every axiom is canonical and elementary.

Moreover, any Sahlqvist formula defines some property of a Kripke frame which is definable in the first-order language. The modal definability of first-order properties in itself has certain advantages. Let us observed them concisely and slightly philosophically. As we said at the beginning, a modal language extends the propositional one with unary operators \Box and \Diamond. As the reader could have seen, necessity and possibility have connections with universality and existence. We established this connection defining the standard translation and embedding the minimal normal modal logic into the first-order predicate logic.

On the one hand, it is a well-known result that first-order logic is undecidable. Thus, we don’t have a general procedure that defines whether a given first-order formula is true or not (alternatively, provable or not). On the other hand, we have already observed the analogy between quantifiers and modalities. On the third hand (yes, I have three hands, it’s practically useful sometimes), modal logics are mostly decidable as we will see a little bit later.

That is, one has a method to check the validity of some binary relation properties by encoding them in modal logic. Such a way doesn’t work for an arbitrary property, indeed. But a large class of such characteristics might be covered via modal language. In the second part, we also take a look at the example of a formula whose class of Kripke frames is not first-order definable.

In order to remain intellectually honest, we should note quite frankly and openly that there also exist first-order properties of Kripke frames which are undefinable in a modal language. A relation is called irreflexive, if it is false that aRaa R a for each aa. The example of an irreflexive relation is the set of natural numbers with <<, just because there is no natural number that could be less than itself, indeed.

Let us define the notion of pp-morphism, a natural homomorphism between Kripke frames. By natural homomorphism, we mean a map that preserves a structure of Kripke frame and validness at the same time. Let us explain the idea with the precise definition and related lemma.

Definition

Let F1=W1,R1\mathcal{F}_1 = \langle W_1, R_1 \rangle, F2=W2,R2\mathcal{F}_2 = \langle W_2, R_2 \rangle be Kripke frames, then pp-morphism is a map f:F1F2f : \mathcal{F}_1 \to \mathcal{F}_2 such that:

  1. ff is monotone, i. e., aR1ba R_1 b implies f(a)R2f(b)f(a) R_2 f(b):
Monotone
  1. ff has a lifting property, i. e., f(a)R2cf(a) R_2 c implies that there exists bW1b \in W_1 aRba R b and f(b)=cf(b) = c
Lift

A pp-mophism between Kripke models M1=F1,v1\mathcal{M}_1 = \langle \mathcal{F}_1, v_1 \rangle, M2=F2,v2\mathcal{M}_2 = \langle \mathcal{F}_2, v_2 \rangle is a pp-morphism f:F1F2f : \mathcal{F}_1 \to \mathcal{F}_2 such that:

M1,wpM2,f(w)p\mathcal{M}_1, w \models p \Leftrightarrow \mathcal{M}_2, f(w) \models p for every variable pp.

PMorphism

If f:F1F2f : \mathcal{F}_1 \to \mathcal{F}_2 is a surjective pp-morphism, then we will write f:F1F2f : \mathcal{F}_1 \twoheadrightarrow \mathcal{F}_2. By surjection, we mean a map f:F1F2f : \mathcal{F}_1 \to \mathcal{F}_2 such that for each yF2y \in \mathcal{F}_2 there exists xF1x \in \mathcal{F}_1 such that f(x)=yf(x) = y.

The following lemma describes a pp-morphism behaviour with formulas that are true in models and valid in frames.

Lemma

  1. If f:M1M2f : \mathcal{M}_1 \to \mathcal{M}_2, then M1,wφ\mathcal{M}_1, w \models \varphi iff M2,f(w)φ\mathcal{M}_2, f(w) \models \varphi
  2. If f:F1F2f : \mathcal{F}_1 \twoheadrightarrow \mathcal{F}_2, then Log(F1)Log(F2)\operatorname{Log}(\mathcal{F}_1) \subseteq \operatorname{Log}(\mathcal{F}_2)

Proof

We prove only the first part of the lemma. Let us suppose that \Diamond is a primitive modality for a technical simplicity. The base case with variables is already proved since the condition of the lemma for variables is the part of model pp-morphism definition.

Let us assume that φψ\varphi \eqcirc \Diamond \psi. We prove that M1,wψ\mathcal{M}_1, w \models \Diamond \psi iff M2,f(w)ψ\mathcal{M}_2, f(w) \models \Diamond \psi. In other words, one needs to prove two implications:

  1. If M1,wψ\mathcal{M}_1, w \models \Diamond \psi, then M2,f(w)ψ\mathcal{M}_2, f(w) \models \Diamond \psi.

Let M1,wψ\mathcal{M}_1, w \models \Diamond \psi, then there exists vR1(w)v \in R_1(w) such that M1,vψ\mathcal{M}_1, v \models \psi. By induction hypothesis, M2,f(v)ψ\mathcal{M}_2, f(v) \models \psi. ff is a pp-morphism, hence ff is monotone and wR1vw R_1 v implies f(w)R2f(v)f(w) R_2 f(v). Thus, M2,f(w)ψ\mathcal{M}_2, f(w) \models \Diamond \psi. We visualise the reasoning above as follows:

PMorphism Lemma 1
  1. If M2,f(w)ψ\mathcal{M}_2, f(w) \models \Diamond \psi, then M1,wψ\mathcal{M}_1, w \models \Diamond \psi

Let M2,f(w)ψ\mathcal{M}_2, f(w) \models \Diamond \psi. Then there exists xR2(f(w))x \in R_2 (f(w)) such that f(w)R2xf(w) R_2 x. ff is a pp-morphism and f(w)R2xf(w) R_2 x, then there exists vW1v \in W_1 such that wR1vw R_1 v and f(v)=xf(v) = x. By induction hypothesis, M1,vψ\mathcal{M}_1, v \models \psi. But wR1vw R_1 v, so M1,wψ\mathcal{M}_1, w \models \Diamond \psi. Take a look at the picture.

PMorphism Lemma 2

Now we show that there doesn’t exist a modal formula that expresses irreflexivity of a relation.

Lemma The class of all irreflexive frame is not modal definable.

Proof Let F1=N,<\mathcal{F}_1 = \langle \mathbb{N}, < \rangle be a Kripke frame, a natural numbers with less-than relation, which is obviously irreflexive. Let F2={},R={(,)}\mathcal{F}_2 = \langle \{ * \}, R = \{ (*, *) \} \rangle. Let us put f:N{}f : \mathbb{N} \to \{ * \} as f(x)=f(x) = * for all xNx \in \mathbb{N}.

Nat To Point

It is easy to see that this map is monotone and surjective. Let us check the lifting property. Let f(x)Rf(x) R *. Let y:=x+1y := x + 1, then x<yx < y and f(y)=f(y) = *. Then ff is a pp-morphism, but F1\mathcal{F}_1 is an irreflexive frame and F2\mathcal{F}_2 is merely reflexive point.

If the reader is interested in modal definability in more detail, then she might take into consideration the Goldblatt-Thomason theorem that connects modal definability, first-order definability with pp-morphisms and some other operations on Kripke frames for further study.

Decidability in modal logic

The decidability of a formal system allows one to establish whether a formula is provable or not algorithmically. In modal logic, the famous Harrop’s theorem provides the most widespread method of decidability proving. Let us introduce some definitions to formulate this theorem.

Definition

A normal modal logic L\mathcal{L} is finitely axiomatisable if L=KΓ\mathcal{L} = {\bf K} \oplus \Gamma for some Γ\Gamma, where Γ\Gamma is a finite set of formulae.

In other words, L\mathcal{L} is finitely axiomatisable if this logic extends minimal normal modal logic with some finite set of axioms.

Definition

A normal modal logic L\mathcal{L} has a finite model property (or finitely approximable), if L=Log(F)\mathcal{L} = \operatorname{Log}(\mathbb{F}), where F\mathbb{F} is some class of finite frames.

That is, a finite model property is a Kripke completeness with respect to the class of finite Kripke frames. Now we formulate the famous Harrop’s theorem:

Theorem (Harrop)

Let L\mathcal{L} be a normal modal logic such that L\mathcal{L} is finitely axiomatisable and has a finite model property. Then L\mathcal{L} is decidable.

Proof

We provide only a quite brief proof sketch. It is clear that the set of formulas provable in L\mathcal{L} is enumerable since this logic merely extends K{\bf K} with the finite set of axioms. On the other hand, let φL\varphi \notin \mathcal{L}. Then the set Bad={φFmφL}\operatorname{Bad} = \{ \varphi \in Fm \: | \: \varphi \notin \mathcal{L} \} is also enumerable, so far as one may enumerate finite frames such that FL\mathcal{F} \models \mathcal{L} and Fφ\mathcal{F} \nvDash \varphi, where φBad\varphi \in \operatorname{Bad}.

So, if we have some finitely axiomatisable logic, then one needs to can show that this logic is complete with respect to some class of finite frames. Here, we will assume that \Diamond is a primitive modality for simplicity.

Definition

Let M=W,R,ϑ\mathcal{M} = \langle W, R, \vartheta \rangle be a Kripke model and Γ\Gamma a set of formulas closed under subformulas (that is, if φΓ\varphi \in \Gamma and ψ\psi is a subformula of φ\varphi, then ψΓ\psi \in \Gamma). We put the following equivalence relation:

xΓyM,xφM,yφx \sim_{\Gamma} y \Leftrightarrow \mathcal{M}, x \models \varphi \Rightarrow \mathcal{M}, y \models \varphi, where φΓ\varphi \in \Gamma

Then, a filtration of a model M\mathcal{M} through a set Γ\Gamma is a model M=W,R,ϑ\overline{M} = \langle \overline{W}, \overline{R}, \overline{\vartheta} \rangle, where

  1. W=W/Γ\overline{W} = W / \sim_{\Gamma}. In other words, W\overline{W} is a quotient by relation Γ\sim_{\Gamma}, the set of equivalence classes.
  2. Let xˉ,yˉW\bar{x}, \bar{y} \in \overline{W}, then xˉRyˉwxˉvyˉwRy\bar{x} \overline{R} \bar{y} \Leftrightarrow \exists w \in \bar{x} \: \exists v \in \bar{y} \:\: w R y
  3. ϑ(p)={xˉWˉwxˉM,wp}\overline{\vartheta} ( p ) = \{ \bar{x} \in \bar{W} \: | \: \exists w \in \bar{x} \: \mathcal{M}, w \models p \}

Here is a quite obvious observation. Suppose, one have a model M=W,R,ϑ\mathcal{M} = \langle W, R, \vartheta \rangle and its filtration M=W,R,ϑ\overline{M} = \langle \overline{W}, \overline{R}, \overline{\vartheta} \rangle through the set of subformulas Sub(φ)\operatorname{Sub}(\varphi), where φ\varphi is a arbitrary formula. Then W2Sub(φ)|\overline{W}| \leq 2^{|\operatorname{Sub}(\varphi)|}.

Harrop’s theorem provides the uniform method to prove that some normal modal logic is decidable if this logic is finitely axiomatisable and has finite model property. We need filtration to prove that a given logic is finitely approximable.

Here comes the first lemma about minimal filtration.

Lemma

Let M\mathcal{M} be a Kripke model and Γ\Gamma a set of formulas closed under subformulas, then M,xφM,xˉφ\mathcal{M}, x \models \varphi \Leftrightarrow \overline{\mathcal{M}}, \bar{x} \models \varphi, where φΓ\varphi \in \Gamma.

Proof

Quite simple induction on φ\varphi. Let us check this statement for φψ\varphi \eqcirc \Diamond \psi.

At first, let us check the only if part. Let M,xψ\mathcal{M}, x \models \Diamond \psi. Then there exists yR(x)y \in R(x) such that M,yψ\mathcal{M}, y \models \psi. By induction hypothesis, M,yˉψ\overline{\mathcal{M}}, \bar{y} \models \psi. But xˉRyˉ\bar{x} \overline{R} \bar{y} by the definition of R\overline{R}. This, M,xˉψ\overline{\mathcal{M}}, \bar{x} \models \Diamond \psi.

The converse implication has the same level of completexity. Let M,xˉψ\overline{\mathcal{M}}, \bar{x} \models \Diamond \psi. Then there exists cR(xˉ)c \in \overline{R}(\bar{x}) such that M,cψ\overline{\mathcal{M}}, c \models \psi. Consequently, there exist wxˉw \in \bar{x} and vcv \in c such that wRvw R v. By assumption, M,vψ\mathcal{M}, v \models \psi. Thus, M,wψ\mathcal{M}, w \models \Diamond \psi.

Now we may formulate the theorem which claims that the minimal normal modal logic is the logic of all finite Kripke frames.

Theorem

  1. K=Log(F){\bf K} = \operatorname{Log}(\mathbb{F}), where F\mathbb{F} is the class of all finite Kripke frames.
  2. T=Log(F){\bf T} = \operatorname{Log}(\mathbb{F}), where F\mathbb{F} is the class of all finite reflexive frames.
  3. D=Log(F){\bf D} = \operatorname{Log}(\mathbb{F}), where F\mathbb{F} is the class of all finite serial frames.
  4. B=Kpp=Log(F){\bf B} = {\bf K} \oplus p \to \Box \Diamond p = \operatorname{Log}(\mathbb{F}), where F\mathbb{F} is the class of all finite symmetric frames.

Proof

Let K⊬φ{\bf K} \not\vdash \varphi. It means that there exists a model M\mathcal{M} and xMx \in \mathcal{M} such that M,x⊭ψ\mathcal{M}, x \not\models \psi according to the completeness theorem. Let M\overline{\mathcal{M}} be a minimal filtration of a model M\mathcal{M} through Sub(ψ)\operatorname{Sub}(\psi), the set of subformulas of ψ\psi. By the previous lemma, M,xˉ⊭ψ\overline{\mathcal{M}}, \bar{x} \not\models \psi. It is clear that this model is finite, since W2Sub(φ)|\overline{W}| \leq 2^{|\operatorname{Sub}(\varphi)|}, as we observed above.

(2), (3), (4) are proved similarly, but one needs to check that a minimal filtration preserves reflexivity, seriality, and symmetry.

However, we are in trouble. We haven’t already discussed a finite model property of logics that contain transitivity as an axiom. Unfortunately, a minimal filtration doesn’t have to preserve the transitivity. Let M=W,R,ϑ\mathcal{M} = \langle W, R, \vartheta \rangle be a transitive model and M=W,R,ϑ\overline{M} = \langle \overline{W}, \overline{R}, \overline{\vartheta} \rangle a minimal filtration of M\mathcal{M} through Γ\Gamma. Let wˉ,vˉ,uˉW\bar{w}, \bar{v}, \bar{u} \in \overline{W} such that wˉRvˉ\bar{w} \overline{R} \bar{v} and vˉRuˉ\bar{v} \overline{R} \bar{u}. If wˉRvˉ\bar{w} \overline{R} \bar{v}, then there exists xwˉx \in \bar{w} and yvˉy \in \bar{v} such that xRyx R y. From the other hand, if vˉRuˉ\bar{v} \overline{R} \bar{u}, then there exists yvˉy' \in \bar{v} and zuˉz \in \bar{u} such that yRzy' R z.

Filter 1

It is clear that yy doesn’t have to see yy' within the equivalence class uˉ\bar{u}. Thus, a relation in minimally filtrated model isn’t necessarily transitive, even if the original relation is transitive.

A solution to that problem is the transitive closure of a relation in a minimal filtration. Let us discuss what a transitive closure is. Suppose we have some set WW with a binary relation RR. Generally, this relation is not transitive, but we’d like to extend it to the transitive one. What should we make? Suppose we have x,y,zWx, y, z \in W such that xRyx R y and yRzy R z. We add xRzx R z to the extended relation which we denote as R+R^{+}. We perform this action for each situation. That gives us a transitive version of a relation.

Here we going to extend a relation in a minimal filtration. This solution was proposed initially by Dov Gabbay. We will denote this closure (R)+(\overline{R})^{+}.

Filter 2

A transitive closure of a relation in a minimal filtration allows us to prove that K4{\bf K}4 is the logic of finite transitive frames. Firstly, we formulate the lemma that explains why a transitive closure is a good idea:

Lemma

Let M=W,R,ϑ\mathcal{M} = \langle W, R, \vartheta \rangle be a transitive model and M=W,R,ϑ\overline{M} = \langle \overline{W}, \overline{R}, \overline{\vartheta} \rangle a minimal filtration through Γ\Gamma, then the following conditions hold:

  1. If aRba \overline{R} b, then a(R)+ba (\overline{R})^{+} b, where a,bWa, b \in \overline{W}. This statement claims that a relation in a minimal filtration is a subrelation if its transitive closure.
  2. If wRvw R v, then wˉRvˉ\bar{w} \overline{R} \bar{v}. If two relation are connected with the underlying relation, then a transitive closure preserve this connection.
  3. Let wˉ(R)+vˉ\bar{w} (\overline{R})^{+} \bar{v} and M,wφ\mathcal{M}, w \models \Box \varphi, then M,vφ\mathcal{M}, v \models \varphi. Here we claim that a transitive closure should respect the truth condition for \Box.

Using the lemma above, it is not so hard to obtain the following theorem:

Theorem

  1. K4=Log(F){\bf K}4 = \operatorname{Log}(\mathbb{F}), where F\mathbb{F} is the class of all finite transitive frames
  2. S4=Log(F){\bf S}4 = \operatorname{Log}(\mathbb{F}), where F\mathbb{F} is the class of all finite preorders.
  3. S5=Log(F){\bf S}5 = \operatorname{Log}(\mathbb{F}), where F\mathbb{F} is the class of all finite equivalence relations.

The theorem above allows us to claim that the logics K4{\bf K}4, S4{\bf S}4, and S5{\bf S}5 have a finite model property. All these logics are finitely axiomatisable. Then, by Harrop’s theorem, K4{\bf K}4, S4{\bf S}4, and S5{\bf S}5 are decidable. That is, one has a uniform method to provide a countermodel in which every unprovable formula fails.

Summary

We discussed a brief history of modal logic and its mathematical and philosophical roots. After that, we introduced the grammar of modal logic to define what modal formula is. As we have already told, the definition of a modal language is not enough to deal with modal logic. From a syntactical perspective, we have formal proofs as derivation with axioms and inference rules. We defined normal modal logic as a set of formulas with specific limitations. As an underlying logic, we fixed minimal normal logic K{\bf K}. Here, the other modal logics merely extend the minimal normal modal one with the additional axioms. Note that syntax doesn’t answer the question about the truth of a formula. The distinction between proof and truth is a foundation of the logical culture in itself. Truth is a semantical concept.

To define the truth condition for modal formulas, we defined Kripke frames and Kripke models. After that, we formulated the completeness theorems for the list of modal logics. As usual, completeness tells us that, very roughly speaking, any valid formula is provable. The underlying modal logic K{\bf K} is a logic of all possible Kripke frames. Other modal logics are complete with respect to a narrower class of frames with the relation in which is restricted somehow. Alright, we have the completeness theorem for some logic, but we also would like to define whether a given formula is provable or not algorithmically. For this purpose, we took a look at methods of proving the fact that a given normal modal logic has finite model property. Finite model property with finite axiomatisation gives us decidability according to the Harrop’s theorem.

We studied the background of modal logic so that we could continue our journey in more concrete case studies. In the second part, we will overview concrete branches of modal logic, such as topological semantics, provability logic, and temporal logic. We will discuss how exactly modal logic is connected with geometry, the foundations of mathematics, and computer science.

I sincerely hope the reader managed to survive in this landscape of such an abstract and theoretically saturated material.

Follow Serokell on Twitter and Facebook to keep in touch!

Banner that links to Serokell Shop. You can buy hip FP T-shirts there!
More from Serokell
Rapid introduction to modal logic, part 2Rapid introduction to modal logic, part 2
formal verification thumbnailformal verification thumbnail
Beginner's guide to Elixir programming languageBeginner's guide to Elixir programming language