Incomplete and Utter Introduction to Modal Logic, Pt. 2

In the first part, we introduced the reader to basic modal logic. We discussed Kripke semantics, some of the popular systems of modal logic. We also observed how to prove the decidability of modal logics using such tools as minimal filtration and its transitive closure. Here we observe use cases and take a look at connections of modal logic with topology, foundations of mathematics, and computer science. Finally, we recommend the literature for further reading and study.

Brief introduction to topology and metric spaces

Topology is the branch of mathematics that studies geometric objects such as planes, surfaces, and their continuous deformations. The notion of a continuous deformation might be illustrated with an example. Suppose you have a cube-shaped piece of plasticine. You deform that piece into the sphere continuously, i. e., keeping your hands on that piece all the time:

A continuous deformation

Topology study geometric structures up to homeomorphism. A homeomorphism is a one-to-one continuous transformation as in the example above.

The abstract definition of a topological space is set-theoretical. A topological space is defined as a family of subsets. More formally, a topological space is a pair X=X,τ\mathcal{X} = \langle X, \tau \rangle, where XX is a non-empty set and τ\tau is a family of subsets of XX with the following data:

  1. ,Xτ\emptyset, X \in \tau
  2. If A,BτA, B \in \tau, then ABτA \cap B \in \tau
  3. Let II be an indexing set and for each iIi \in I AiτA_i \in \tau, then iIAi\bigcup \limits_{i \in I} A_i. Here, an indexing set is an arbitrary set that might have any cardinality. If AXA \subseteq X and AτA \in \tau, then we call AA an open set. A subset AXA \subseteq X is called closed, if AA is a complement of some open set.

The most common practice is defining a topological structure via a base of topology. A base of topology is a family of opens such that every open set in this space has the form of union of some elements from the base. We consider instances of a base within examples of topological spaces.

Examples of topological spaces are:

  1. Let XX be a set and P(X)\mathcal{P}(X) a set of all subsets of XX, then X,P(X)\langle X, \mathcal{P}(X) \rangle is a topological space, in which every subset is open. We call such a space discrete since its base is the set of all singletons {x}\{x\}, xXx \in X.
  2. Let XX be a set and τ={,X}\tau = \{ \emptyset, X \}, then X,τ\langle X, \tau \rangle is also space, where only the underlying set and the empty one are open. X,τ\langle X, \tau \rangle is called anti-discrete space.

The topologies above are trivial ones. Let us consider a slightly more curious example.

Let X,ρ\langle X, \rho \rangle be a metric space. By metric space, we mean a set equipped with a distance function ρ:X×XR0\rho : X \times X \to \mathbb{R}_{\geq 0} that every pair of points maps to some non-negative real number, a distance between them. A distance function has the following conditions:

  1. ρ(x,x)=0\rho(x, x) = 0. The distance between the point with itself equals to zero.
  2. ρ(x,y)=ρ(y,x)\rho(x, y) = \rho(y, x). The distance between points doesn’t depens on the arguments order.
  3. ρ(x,z)ρ(x,y)+ρ(y,z)\rho(x, z) \leq \rho(x, y) + \rho(y, z). The triangle inequation.

One may topologise any metric space uniformly. Let ε\varepsilon be a positive real number and xXx \in X. An open ball of radius ε\varepsilon and centre xx is the set Uεx={yXρ(x,y)<ε}U_{\varepsilon}^x = \{ y \in X \: | \: \rho(x, y) < \varepsilon \}.

To visualise the notion of an open ball, just imagine you take a cricket ball. An open ball derived from a given cricket ball is just the content, if we assume that its content is restricted by its leather cover. The centre of a cricket ball is a centre in the usual Euclidean sense. The radius of such an open ball approximately equals to 3.5 centimetres according to International Cricket Council data.

The set of all open balls in this metric space forms the base of topology. Thus, any metric space is a topological one. Moreover, topological spaces historically arose as the generalisation of metric spaces at the beginning of the previous century.

The example of a metric space is real numbers with the distance function defined with the absolute value of subtraction. The second example is a normed vector space, a vector space equipped with a norm function, a generalisation of a vector length. One may produce a metric space from a normed vector one by defining the distance between two vectors as the norm of their subtraction. Such a metric is often called the Minkowski distance. We don’t consider the examples above in detail since those topics are closer to functional analysis and point-set topology rather than modal logic.

Closure and interior operators

Let us motivate interior and closure as follows. Suppose we have a snake on the Euclidian plane R2\mathbb{R}^2. Unfortunately, this snake ate an elephant and lost its full-contour line after that:

The snake

A closure operator on the Euclidean plane helps it to restore the lost part of a boundary:

The closure of the snake

We would like to identify the other regions of this snake. An interior of the snake is its container. The last sentence is not meant to be taken literally in the anatomical sense:

The interior of the snake

The boundary of a snake is its full contour-line without the interior. Here we are not interested in the rich inner world of our snake, only in its external borders. Just imagine that you chalked the snake:

The boundary of the snake

The exterior of a snake is the whole plane without this snake itself. An exterior operator allows the snake to define strictly what an external world is:

The exterior of the snake

Here, the snake is the subset of plane R2\mathbb{R}^2, namely, SS. Let us denote its closure as ClS\operatorname{Cl}S. IS\operatorname{I}S is its interior. The boundary of a snake is the closure of the snake minus its interior, ClSIS\operatorname{Cl} S \cap - \operatorname{I} S. The exterior of this snake is an interior of its complement. Here the basic notions are interior and closure. Let us move on to stricter definitions:

Let X=X,τ\mathcal{X} = \langle X, \tau \rangle be a topological space and AXA \subseteq X a subset of X\mathcal{X}. A closure of XX is the smallest closed set that contains XX. More precisely:

Cl(X)={AClosed(X)XA}\operatorname{Cl}(X) = \bigcap \{ A \in \operatorname{Closed}(\mathcal{X}) \: | \: X \subseteq A \}

A closure operator satisfies the following properties that also knows as Kuratowski’s axioms:

Cl()=\operatorname{Cl}(\emptyset) = \emptyset, empty set is closed. AClAA \subseteq \operatorname{Cl}A, any set is a subset of its closure. ClA=ClClA\operatorname{Cl}A = \operatorname{Cl}\operatorname{Cl}A, you don’t need to apply closure operator twice, it’s idempotent. Cl(AB)=ClAClB\operatorname{Cl}(A \cup B) = \operatorname{Cl}A \cup \operatorname{Cl}B, a closure operator distributres over finite union.

Very and very roughly speaking, a closure operator transforms any subset to a closed one. A dual operator is an interior. An interior of a subset XX is the biggest open subset of XX: I(X)={AτAX}\operatorname{I}(X) = \bigcup \{ A \in \tau \: | \: A \subseteq X \}.

It is not so hard to show that I(X)=(Cl(X))\operatorname{I}(X) = - (\operatorname{Cl}(- X)) since an open set is a complement of a closed one and vice versa. An interior operator satisfies the following conditions: IX=X\operatorname{I}X = X IAA\operatorname{I}A \subseteq A IA=IIA\operatorname{I}A = \operatorname{I}\operatorname{I}A I(AB)=IAIB\operatorname{I}(A \cap B) = \operatorname{I}A \cap \operatorname{I}B

To observe the analogy between Kuratowski’s closure axioms and the logic S4{\bf S}4, let us take a look at the equivalent formulation of S4{\bf S}4. We recall that S4{\bf S}4 is a normal modal logic that extends K{\bf K} with reflexivity and transitivity axioms:

  1. Boolean tautologies
  2. The Kripke axiom (pq)(pq)\Box (p \to q) \to (\Box p \to \Box q)
  3. pp\Box p \to p
  4. pp\Box p \to \Box \Box p Inference rules: Modus Ponens, Substitution, Necessitation.

First of all, we define a normal modal logic as the set of formulas that consists of all Boolean tautologies, the following two formulas:

  1. pq(pq)\Diamond p \lor \Diamond q \leftrightarrow \Diamond (p \lor q)
  2. \Diamond \bot \leftrightarrow \bot and closed under Modus Ponens, Substitution, and monotonicity rule: from φψ\varphi \to \psi infer φψ\Diamond \varphi \to \Diamond \psi.

The reader might check that this definition of normal modal logic is equivalent to the definition we introduced in the first part as an exercise.

The minimal normal modal logic is the least set of formulas that satisfy the previous conditions. Such a logic is deductively equivalent to K{\bf K} defined in the previous post. Then S4{\bf S4} is an extension of the minimal normal modal logic with reflexivity and transitivity axioms, more explicitly:

  1. pq(pq)\Diamond p \lor \Diamond q \leftrightarrow \Diamond (p \lor q)
  2. \Diamond \bot \leftrightarrow \bot
  3. ppp \to \Diamond p
  4. pp\Diamond \Diamond p \to \Diamond p

As the reader could see, the S4{\bf S4} axioms are the same as the Kuratowski’s closure axioms if we read Cl\operatorname{Cl} as \Diamond. Dually, we represent S4{\bf S}4 logic with boxes and observe the analogy with the Kuratowski’s interior axioms, if we read I\operatorname{I} as \Box:

  1. pq(pq)\Box p \land \Box q \leftrightarrow \Box (p \land q)
  2. \Box \top \leftrightarrow \top
  3. pp\Box p \to p
  4. pp\Box p \to \Box \Box p

We may study such an analogy considering topological models (or topo-models) in which we define the truth condition for modalities via open and closed sets in a given topological space.

Topological models

We discussed Kripke-style semantics based on binary relations before. The idea of topological models is the same, but we replace Kripke frames with topological spaces and modal formulas are understood in terms of closed and open sets.

Let X=X,τ\mathcal{X} = \langle X, \tau \rangle be a topological space and ϑ:PV2X\vartheta : \operatorname{PV} \to 2^{X} be a valuation. A topological model is a triple M=X,ϑ\mathcal{M} = \langle \mathcal{X}, \vartheta \rangle with the following thurh conditions. Here we assume that ¬\neg, \lor, and \Box are primitive connectives:

  1. M,xpxϑ(p)\mathcal{M}, x \models p \Leftrightarrow x \in \vartheta ( p )
  2. M,x¬φM,xφ\mathcal{M}, x \models \neg \varphi \Leftrightarrow \mathcal{M}, x \nvDash \varphi
  3. M,xφψM,xφ or X,xψ\mathcal{M}, x \models \varphi \lor \psi \Leftrightarrow \mathcal{M}, x \models \varphi \text{ or } \mathcal{X}, x \models \psi
  4. M,xφ\mathcal{M}, x \models \Box \varphi \Leftrightarrow there exists an open neighbourhood UU such that xUx \in U and for each yUy \in U M,yφ\mathcal{M}, y \models \varphi

Let us define that valuation of an abritrary formula that follows from the semantics above:

  1. p=ϑ(p)||p|| = \vartheta(p)
  2. ¬φ=φ||\neg \varphi|| = - ||\varphi||
  3. φψ=φψ||\varphi \lor \psi|| = ||\varphi|| \lor ||\psi||
  4. φ=I(φ)||\Box \varphi|| = \operatorname{I}(||\varphi||), that is, \Box is exaclty an interior in terms of topological semantics.

As in Kripke models, a valuation function maps each variable to some subset of an underlying set. From a naive geometric intuition, a valuation function determines some region on a space. If we return to our example with the snake on a plane, then we may, for example, require that ϑ(p)=S\vartheta ( p ) = S. The items 2-3 are the same as in Kripke models. The truth condition for \Box is completely different. Logically, this condition declares that φ\Box \varphi is true at the point xx if φ\varphi is locally true. It means that the proposition φ\varphi is true at each point in some region of an observed space.

The truth condition for Box

As we remember, =¬¬\Diamond = \neg \Box \neg. Thus, the possibility modality has the following truth condition in a topological model:

M,xφ\mathcal{M}, x \models \Diamond \varphi \Leftrightarrow for each open neighbourhood UU such that xUx \in U there exists yUy \in U such that M,yφ\mathcal{M}, y \models \varphi. In other words, there exists a point in every open neighbourhood UU of xx at which φ\varphi is true. This definition induces the closure of φ||\varphi||, the set of all points at which φ\varphi is true: φ=¬¬(I(φ))=Cl(φ)||\Diamond \varphi|| = ||\neg \Box \neg || - (\operatorname{I} (- ||\varphi||)) = \operatorname{Cl}(||\varphi||)

The truth condition for Diamond

Also, we will use the same notation as in Kripke semantics: Mφ\mathcal{M} \models \varphi iff φ\varphi is true at every point. φ\varphi is valid in a topological space iff it’s true in every model on this space. The logic of a topological space X\mathcal{X} is the set of valid formulas in this space. The logic of class of topological space is an intersection of logics.

In Kripke semantics, the logic K{\bf K} was the underlying one, K{\bf K} is the logic of all Kripke frames. The same question for topological spaces is quite natural. McKinsey-Tarski theorem claims that S4{\bf S}4, the logic of all preorders from a Kripkean perspective, is the logic of all topological spaces. Let us discuss the soundness theorem first. Moreover, any extension of S4{\bf S}4 is complete with respect to some class of topological spaces.

Theorem Let X\mathbb{X} be a class of all topological spaces, then S4=Log(X){\bf S}4 = \operatorname{Log}(\mathbb{X})

Proof Let us prove that A4=pp{\bf A}4 = \Box p \to \Box \Box p is valid. Let X\mathcal{X} be a topological space and ϑ\vartheta a valuation. Let M,xp\mathcal{M}, x \models \Box p. Then there exists an open neighbourhood UxU_x such that for each yUxy \in U_x M,yp\mathcal{M}, y \models p. yUxy \in U_x, then UxU_x is also open neighbourhood of yy. Thus, M,yp\mathcal{M}, y \models \Box p and M,xp\mathcal{M}, x \models \Box \Box p.

To prove the converse inclusion, one needs to perform the same thing as in the case of Kripke semantics. The set of all maximal S4{\bf S}4-consistent sets forms a topological space. So, one can build a canonical topological model, a topo-model on the set of all maximal S4{\bf S}4-consistent sets with canonical valuation. We refer the reader to the paper called Reasoning About Space: The Modal Way written by Marco Aiello, Johan van Benthem, and Guram Bezhanishvili, where the topological completeness of S4{\bf S}4 is shown quite accurately. Thus, S4{\bf S}4 is the logic of all topological spaces.

Some might say that this is result is too abstract. We would like to take a look at a more precise classification of topological spaces with modal logic. Modal logic is able to provide an invariant for topological spaces, but, frankly speaking, it’s quite weak. Let us observe, however, what had already been done in topological semantics of modal logic. In other words, we discuss how we can particularise the class of topological spaces preserving McKinsey-Tarski theorem.

Let X\mathcal{X} be a discrete space, then Log(X)=Kpp\operatorname{Log}(\mathcal{X}) = {\bf K} \oplus \Box p \leftrightarrow p. This axiom claims that we may box and unbox everywhere. From a topological point of view, it denotes that the interior operator is the trivial one. That is, any subset is open. All modalities fade away since the interior operator is merely the identity function on subsets.

Let X=X,τ\mathcal{X} = \langle X, \tau \rangle be an infinite anti-discrete space, that is, only XX and \emptyset are open, then S5=Log(X){\bf S}5 = \operatorname{Log}(\mathcal{X}). As we told in the first part, S5=S4pp{\bf S}5 = {\bf S}4 \oplus p \to \Diamond \Box p. The last axiom expresses symmetry of a relation. The symmetry formula also has the equivalent form pp\Diamond \Box p \to p.

The truth condition for \Box in models on anti-discrete spaces transforms as follows. φ\Box \varphi is true at the point xx, if there exists an open neighbourhood UxU_x such that M,yφ\mathcal{M}, y \models \varphi. In an anti-discrete space, there is only the one open neighbourhood for every point, the space itself. That is, in an anti-discrete space, M,xφ\mathcal{M}, x \models \Box \varphi iff M,yφ\mathcal{M}, y \models \varphi for each yXy \in X. It’s not hard to check that AB{\bf AB}-axiom is valid on every infinite anti-discrete space. Let xXx \in X and M,xφ\mathcal{M}, x \models \Diamond \Box \varphi. Then for every open neighbourhood UxU_x there exists the point yy such that M,yφ\mathcal{M}, y \models \Box \varphi. But there is only one open neighbourhood of xx, the space itself. Thus, M,xφ\mathcal{M}, x \models \varphi.

Let F=W,R\mathcal{F} = \langle W, R \rangle be a preorder, that is, S4{\bf S}4-frame. One may induce a topological structure on a preorder if we take also upper sets as opens. A set AWA \subseteq W is called upper if xAx \in A and xRyx R y implies yAy \in A. In this topology, any intersection of opens is open, or equivalently, the interior operator distributes over an arbitrary intersection of subsets. Such a space is the instance of Alexandrov space. This connection claims that topological semantics for modal logic generalises Kripkean semantics for S4{\bf S}4 and its extensions.

S4{\bf S}4 is also the logic of the class of all metric spaces as it was proved by McKinsey and Tarski. Rasiowa and Sikorski showed that S4{\bf S}4 is the logic of all dense-in-itself metric spaces, that is, metric spaces that contain no isolated points. Here we may claim that modal logic provides invariants for topological and metric spaces, but such invariants are too rough if we have closure and interior modalities. The roughness of these invariants follows from the fact that all topological spaces, all metric spaces and all dense-in-itself metric spaces have exactly the same logic and those spaces are indistinguishable from a logical point of view.

We refer the reader to the paper by Guram Bezhanishvili, David Gabelaia, and Joel Lucero-Bryan to become familiar with more precise classification of modal logics of metric spaces.

Note that interior and closure are not the only topological modalities. There are also a so-called graduated, tangled, difference, and other modal operators that are of interest from a topological perspective. Such extensions of modal language allow one to study topological and metric spaces from a logical perspective much more faithfully. You may read the recent paper by Ian Hodkinson and Robert Goldblatt called Strong completeness of modal logics over 00-dimensional metric spaces, where those alternative modalities are overviewed quite clearly. Also, you may read the paper Some Results on Modal Axiomatisation and Definability for Topological Spaces by Guram Bezhanishvili, Leo Esakia, and David Gabelaia to understand the expressive power of so-called derivation modality that generalises closure in some sense. Let us observe briefly a universal modality as an example of such an additional modality.

The universal modality is denoted as [][\forall] and has the following semantics: M,x[]φ\mathcal{M}, x \models [\forall] \varphi \Leftrightarrow M,yφ\mathcal{M}, y \models \varphi for each yXy \in \mathcal{X}, where X\mathcal{X} is an underlying topological space.

The modal logic that we seek is the system S4U{\bf S}4{\bf U} which is defined in the bimodal language. We have \Box (an interior modality) that satisfies S4{\bf S}4 axioms and we have [][\forall] with S5{\bf S}5 axioms. We also add the additional postulate that has the form []pp[\forall] p \to \Box p. That is, if the statement is true everywhere, then it’s true in every open neighbourhood. The very first example of a universal modality is an interior operator in an infinite anti-discrete space, as we observed above. In other words, universal modality is stronger than the interior. Logically, []φ[\forall] \varphi denotes that φ\varphi is true at every point. A formula φ\Box \varphi tells us that φ\varphi is locally true, i. e. at some open neighbourhood that shouldn’t cover the whole space. Moreover, there is the result according to which S4U{\bf S}4{\bf U} is the logic of arbitrary zero-dimensional spaces, such as Cantor space, or rational numbers as a metric space with the usual distance.

Also we observe the following postulate:

[](p¬p)[]p[]¬p[\forall](\Box p \land \Box \neg p) \to [\forall] p \vee [\forall] \neg p

This formula denotes the fact that an observed space is connected one, i.e. we cannot split it into two disjoint open subsets. Informally, formula claims that if one can split whole space into two disjoint subsets, then one of them is empty. More formally. Let X\mathcal{X} be a topological space, then X[](p¬p)[]p[]¬p\mathcal{X} \models [\forall](\Box p \land \Box \neg p) \to [\forall] p \vee [\forall] \neg p if and only is X\mathcal{X} is connected. Moreover, S4U[](p¬p)[]p[]¬p{\bf S}4{\bf U} \oplus [\forall](\Box p \land \Box \neg p) \to [\forall] p \vee [\forall] \neg p is the logic of all connected separable dense-in-itself metric spaces.

As we noticed previously, one may study provability and consistency in arithmetic via modal logic. The problem of provability and consistency in Peano arithmetic (briefly, PA{\bf PA}) is connected with famous Gödel’s incompleteness theorems. To understand the connection between modal logic and these aspects of PA{\bf PA}, we show how to prove the incompleteness theorems. Before that, let us explain the historical context of the Gödel’s theorems’ appearance.

At the beginning of the 20th century, one of the commonly discussed topics was the question about the foundations of mathematics and its consistency. Such mathematicians as Richard Dedekind and Georg Cantor were interested in axiomatisation of real analysis in order to describe the principles of real numbers as the set of primitive properties of the real line in terms of order and arithmetical operations.

The notion of a number was defined intuitively before, but one may define a number formally with the set theory proposed by Cantor. Unfortunately, the initial version of the set theory was inconsistent. Inconsistency of Cantor’s set theory was shown by Bertrand Russell who invited the famous paradox which is named after him. The paradox-free version of the set theory is so-called Zermelo-Fraenkel theory which is assumed sometimes as the “default” foundations of mathematics.

Later, in the 1920-s, David Hilbert, a German mathematician who famous for his works in the foundations of geometry, algebra, and mathematical physics announced the programme of establishing mathematics consistency.

David Hilbert, German mathematician

According to Hilbert’s programme, any mathematical theory such as differential equations should be embedded in some formal axiomatic theory. Moreover, any usual mathematical proof must correspond to some formal proof. By formal proof, we mean a finite text written according to a set of strictly defined rules such as inference rules in first-order logic. The finite methods themselves should be formalised in Peano arithmetic, a formal axiomatic theory of natural numbers. Although, there was the open question: how can we prove that formal arithmetic is consistent within itself? In other words, we would like to formalise formal methods in Peano arithmetics and we want to have a finite proof of Peano arithmetic at the same time. Since this hypothetical proof should be finite, then it also should be formalised in Peano arithmetic.

Kurt Gödel solved this problem negatively in 1931.

Kurt Gödel, Austrian logician, mathematician

More precisely, he showed that there is a sentence in Peano arithmetic that is unprovable and true at the same time. In other words, such a statement has no formal proof but it is true as a fact about natural numbers. Let us describe the idea informally. Moreover, the finite proof of PA{\bf PA} consistency is impossible since the formula that expresses desired consistency isn’t provable.

I believe, everybody heard about the Liar paradox. Let me remind it. Suppose we have a character that always lies, for instance, Tartuffe from the same-titled comedy by Molière. Let us assume that Tartuffe claims with courage, clarity, and frankness that he’s lying.

Tartuffe

Here we are in an embarrassing situation. If Tartuffe tells that he’s lying, hence, he lies that he’s lying. Thus, he’s telling the truth. On the other hand, he always lies by definition. Such confusion is often called the Liar paradox.

Gödel used approximately the same idea and we describe how exactly in the further proof sketch. Before that, we define Peano arithmetic as a formal theory.

Peano arithmetic

Peano arithmetic is an axiomatic theory of natural numbers with addition and multiplication. Philosophically, Peano arithmetic describe the basic properties of natural numbers with primitive operations. Formally, we put the arithmetical language, the set of primitive symbols:

  1. 00 is a constant that denotes the number which is also famous as zero.
  2. S\operatorname{S} is a unary function symbol, an increment. C++ engineer may read S(x)\operatorname{S}( x ) as x++
  3. ++, \cdot are binary function symbols which we read as plus and product.
  4. == is a binary relation symbol that denotes equality.

It is not so difficult to see that all those signs are read in accordance with our everyday intuition. To define the grammar of arithmetical formulas, we should restrict the definition of the first-order formula to the observed arithmetical language.

As in first-order logic, we have a countably infinite set of individual variables. Let us define a term first:

  1. Any individual variable is a term
  2. 00 is a term
  3. If tt is a term, then S(t)\operatorname{S}( t ) is a term
  4. If t1,t2t_1, t_2 are terms, then t1+t2t_1 + t_2 and t1t2t_1 \cdot t_2 are terms

Informally, terms are finite strings that we read as arithmetical objects. The definition of a formula is the same as in the first-order case with the additional condition: if t1,t2t_1, t_2 are terms, then t1=t2t_1 = t_2 is a formula.

Now we are able to define Peano arithmetic. Here we introduce two group of axioms. Let us overview the equality axioms which completely agree with our intution:

  1. x(x=x)\forall x \: (x = x). Reflexiity of equality: every object equals to itself.
  2. xy(x=yy=x)\forall x \: \forall y \: (x = y \rightarrow y = x). Symmetry of equality.
  3. xy((x=yy=z)x=z)\forall x \: \forall y \: ((x = y \land y = z) \rightarrow x = z). Transitivity of equality.

Equality respects unary and binary operations: 5. x1x2y1y2((x1=y1x2=y2)x1+y1=x2+y2)\forall x_1 \: \forall x_2 \: \forall y_1 \: \forall y_2 \: ((x_1 = y_1 \land x_2 = y_2) \rightarrow x_1 + y_1 = x_2 + y_2) 6. x1x2y1y2((x1=y1x2=y2)x1y1=x2y2)\forall x_1 \: \forall x_2 \: \forall y_1 \: \forall y_2 \: ((x_1 = y_1 \land x_2 = y_2) \rightarrow x_1 \cdot y_1 = x_2 \cdot y_2) 7. xy(x=yS(x)=S(y))\forall x \: \forall y \: (x = y \Rightarrow \operatorname{S} ( x ) = \operatorname{S} ( y )). Informally, if xx and yy are equal, then x+1x + 1 and y+1y + 1 are also equal.

Equality also respects other predicates: 8. xy((x=yP(x))P(y))\forall x \: \forall y \: ((x = y \land P ( x )) \rightarrow P ( y )) This axiom claims that if objects xx and yy are equal and the property PP holds for xx, then it also holds for yy.

We also split the arithmetical group of axioms into the following subgroups. The first group form the definition of successor function S\operatorname{S}:

  1. ¬x(0=S(x))\neg \exists x (0 = \operatorname{S} ( x ))
  2. xy(S(x)=S(y)x=y)\forall x \: \forall y \: (\operatorname{S} ( x ) = \operatorname{S}( y ) \rightarrow x = y)
  3. x(x0y(S(y)=x))\forall x \: (x \neq 0 \rightarrow \exists y \: (\operatorname{S}( y ) = x))

Recursive definitions of addition and multiplication:

  1. x+0=xx + 0 = x
  2. x+S(y)=S(x+y)x + \operatorname{S}( y ) = \operatorname{S}(x + y)
  3. x0=0x \cdot 0 = 0
  4. xS(y)=(xy)+xx \cdot \operatorname{S}( y ) = (x \cdot y) + x

Induction schema:

  1. A(0)x(A(x)A(S(x)))xA(x)A ( 0 ) \land \forall x \: (A ( x ) \to A(\operatorname{S}( x ))) \to \forall x \: A( x ) The induction schema is an axiom schema that allows you to prove arithmetical theorems inductively. Note that the induction principle is exactly the schema, here AA is a metavariable on arithmetical formulas. The induction schema allows us to prove theorems that depend on parameter nn as follows. In the formula above, a metavariable AA denotes a statement that contains this parameter. Suppose we have the statement A(n)A ( n ) that depends on the parameter nn. To prove that this statement holds for every natural number, we first prove that this fact of 00. This part is often called induction base. After that we assume that A(m)A( m ) holds for an arbitrary mm and we prove A(m+1)A(m + 1), or A(S(m))A(\operatorname{S} ( m )) in our notation. Afterwards, we conclude that A(n)A ( n ) is provable for each nNn \in \mathbb{N}.

As usual, a proof of a formula AA in Peano arithmetic is a sequence of formulas, each of which is either:

  1. First-order or equality axiom
  2. Or arithmetical axiom
  3. Or it’s derived via inference rules (Modus Ponens and so-called Bernays’ rules) from the previous formulas.

The last element of such a sequence is the formula AA itself.

Here’s an example. Let us show that the associativity of addition is provable in PA{\bf PA}. That is, we show that PAxyz((x+y)+z=x+(y+z)){\bf PA} \vdash \forall x \: \forall y \: \forall z \: ((x + y) + z = x + (y + z)). We provide semiformal proof for humanistic reasons.

Induction base: Let z=0z = 0. (x+y)+0=x+y(x + y) + 0 = x + y by the first addition axiom. On the other hand, x+(y+0)=x+yx + (y + 0) = x + y, since y+0=yy + 0 = y be the same addition axiom.

Induction step Let z=S(z1)z = \operatorname{S}(z_1). Suppose we have already proved (x+y)+z1=x+(y+z1)(x + y) + z_1 = x + (y + z_1). Let us show that (x+y)+S(z1)=x+(y+S(z1))(x + y) + \operatorname{S}(z_1) = x + (y + \operatorname{S}(z_1)). Then:

(x+y)+S(z1)=The second addition axiomS((x+y)+z1)=Induction hypothesisS(x+(y+z1))=The second addition axiom (twice)x+S(y+z1)=x+(y+S(z1))\begin{array}{lll} & (x + y) + \operatorname{S}(z_1) = & \\ & \:\:\:\: \text{The second addition axiom} & \\ & \operatorname{S}((x + y) + z_1) = & \\ & \:\:\:\: \text{Induction hypothesis} & \\ & \operatorname{S}(x + (y + z_1)) = & \\ & \:\:\:\: \text{The second addition axiom (twice)} & \\ & x + \operatorname{S}(y + z_1) = x + (y + \operatorname{S}(z_1)) & \end{array}

We also note this way of inductive reasoning is implemented in such proof-assistants as Agda, Coq, Isabelle, etc. To get started with formal inductive reasoning in Agda, read the second part of my blog post on non-constructive proofs.

Gödel numbering

A Gödel numbering is an instrument that encodes the syntax of Peano arithmetic within itself. Informally, we have a function γ\gamma that maps each symbol of our signature maps to some natural number. More precisely, let Term\operatorname{Term} be a set of all arithmetical terms and Form\operatorname{Form} a set of all arithmetical formulas. A Gödel numbering is a function γ:TermFormN\gamma : \operatorname{Term} \cup \operatorname{Form} \to \mathbb{N}, i.e., γ\gamma maps every arithmetical term or formula to some natural number. We denote γ(t)\gamma(t) and γ(A)\gamma(A) as t\lceil t \rceil and A\lceil A \rceil correspondingly.

The next goal is to have a method of proof formalisation within Peano arithmetic. As we told, proof of an arithmetical formula AA is a sequence of formulas with several conditions that we described above. The keyword here is a sequence. First of all, we note that one needs to have an ordered pair since any sequence of an arbitrary length has a representation as a tuple. First of all, we note that one needs to have an ordered pair since any sequence of an arbitrary length has a representation as a tuple. In other words, one has a sequence a1,,an1,an\langle a_1, \dots, a_{n-1}, a_n \rangle that might be represented as a tuple a1,,an1,an\langle \langle a_1, \dots, a_{n-1} \rangle, a_n \rangle. Here, we have Cantor’s encoding c:N×NNc : \mathbb{N} \times \mathbb{N} \to \mathbb{N} that establish bijection between natural numbers and N×N\mathbb{N} \times \mathbb{N}. In order to avoid a technical oversaturation, just believe me that there is a way to encode predicates that define whether a A\lceil A \rceil either is logical axiom or arithmetical one, or it’s obtained from previous formulas via inference rules.

Ultimately, we have a proof predicate that has the form Prf(x,y)\operatorname{Prf}(x, y). This formula should be read as xx is a Gödel number of a sequence that proves yy in Peano arithemtic. Moreover, if A1,,An,AA1, \dots, An, A is a proof of AA, then PA{\bf PA} knows about this fact. In other words, PAPrf(A1,,An,A,A){\bf PA} \vdash \operatorname{Prf} (\lceil A1, \dots, An, A \rceil, \lceil A \rceil). Otherwise, PA⊬Prf(A1,,An,A,A){\bf PA} \not\vdash \operatorname{Prf} (\lceil A1, \dots, An, A \rceil, \lceil A \rceil).

We need the proof predicate to express provability formalised in Peano arithmetic. A provability predicate is a formula Pr(y)\operatorname{Pr} ( y ) which claims that there exists a sequence of formulas that proves yy (in terms of Gödel encoding, indeed) in PA{\bf PA}. It is not so difficult to realise that a provability predicate has the form xPrf(x,y)\exists x \:\: \operatorname{Prf} (x, y). It is also clear that if PAPrf(x,y){\bf PA} \vdash \operatorname{Prf} (x, y), then PAPr(y){\bf PA} \vdash \operatorname{Pr} ( y ).

Provability predicate in Peano arithmetic has crucially important conditions that were established by Hilbert, Bernays, and Löb.

Hilbert-Bernays-Löb conditions

  1. PAAPAPr(A){\bf PA} \vdash A \Rightarrow {\bf PA} \vdash \operatorname{Pr} (\lceil A \rceil). *This condition claims that if the statement AA is provable in PA{\bf PA}, then the provability of AA itself is provable in PA{\bf PA}.
  2. PAPr(AB)(Pr(A)Pr(B)){\bf PA} \vdash \operatorname{Pr} (\lceil A \to B \rceil) \to (\operatorname{Pr} (\lceil A\rceil) \to \operatorname{Pr} (\lceil B \rceil)). This condition claims that provability predicate respect implication.
  3. PAPr(A)Pr(Pr(A)){\bf PA} \vdash \operatorname{Pr}(\lceil A\rceil) \to \operatorname{Pr} (\lceil \operatorname{Pr} (\lceil A\rceil) \rceil). This principle is a formalisation of the first one in PA{\bf PA}.

The reader may observe that these conditions remind the logic K4{\bf K}4, the logic of all transitive frames. Here, the first condition corresponds to the necessitation rule, the second one to Kripke axiom, and the third one to the transitivity axiom pp\Box p \to \Box \Box p. It’s no coincidence as we’ll see further.

Now we are ready to observe the first incompleteness theorem.

The first incompleteness theorem

The fixed-point lemma allows one to build uniformly self-referential statements, i. e. such statements that tell something about themselves. For instance, the root of the Liar paradox is a self-reference, where Tartuffe tell us that he’s lying at the moment being a chronic liar.

Fixed-point lemma Let B(x)B ( x ) be an arithmetical formula with one free variable, then there exists a closed formula AA such that PAAB(A){\bf PA} \vdash A \leftrightarrow B(\lceil A \rceil)

The first Gödel’s incompleteness theorem is a consequence of the fixed-point lemma and the Hilbert-Bernays-Löb conditions.

The first Gödel’s incompleteness theorem Let φ\varphi be an arithmetical formula such that PAφ¬Pr(φ){\bf PA} \vdash \varphi \leftrightarrow \neg \operatorname{Pr} (\lceil \varphi \rceil). Then PA⊬φ{\bf PA} \not\vdash \varphi

Suppose PAφ{\bf PA} \vdash \varphi. Then PAPr(φ){\bf PA} \vdash \operatorname{Pr} (\lceil \varphi \rceil) by the first Hilbert-Bernays-Löb condition. On the other hand, PA¬Pr(φ){\bf PA} \vdash \neg \operatorname{Pr} (\lceil \varphi \rceil) by the given fixed-point. Contradiction.

The fixed-point from the formulation above claims its own unprovability but it’s true in the standard model of Peano arithmetics (the model of arithmetic on usual natural numbers) at the same time! Thus, the elementary theory of natural numbers with addition, multiplication and equality, the set of all true arithmetical statements, contains the proposition that doesn’t belong to the set of all consequences of Peano arithmetic. This fact tells us that Peano arithmetic is not complete with respect to its standard model. That is, there exists a statement that is true and unprovable in PA{\bf PA} at the same time.

The second incompleteness theorem and Löb theorem

The second incompleteness theorem argues that it is impossible to prove the consistency of PA{\bf PA} within PA{\bf PA}. First of all, we define a formula that expresses consistency. Let us put $\operatorname{Con} $ as ¬Pr()\neg \operatorname{Pr} (\lceil \bot \rceil). Here \lceil \bot \rceil is a Gödel number of the false statement, e.g. 0=10 = 1. Here we formulate only the theorem without proof. Note that this theorem might be proved via the same fixed-point as in the first Gödel’s theorem:

The second incompleteness theorem

PA⊬Con{\bf PA} \not\vdash \operatorname{Con}

Löb’s theorem arose as a response to the question about statements in Peano arithmetic that are equivalent to its provability. Martin Löb showed that such statements are exactly all provable in PA{\bf PA} formulas. Note that Löb’s theorem itself has a formalisation in Peano arithmetics as follows. Here we formulate Löb’s theorem in two items, where the second one is a formalised version.

Löb’s theorem

  1. PAA{\bf PA} \vdash A if and only iff PAPr(A)A{\bf PA} \vdash \operatorname{Pr} (\lceil A \rceil) \to A.
  2. PAPr(A)APAPr(A){\bf PA} \vdash \operatorname{Pr}(\lceil A \rceil) \to A \Leftrightarrow {\bf PA} \vdash \operatorname{Pr} (\lceil A \rceil)

Note that the second incompleteness theorem follows from Löb’s theorem as follows: PAPAPr()PAPA¬Pr()PAPACon\begin{array}{lll} & {\bf PA} \vdash \bot \Leftrightarrow {\bf PA} \vdash \operatorname{Pr} (\lceil \bot \rceil) \rightarrow \bot \Leftrightarrow & \\ & {\bf PA} \vdash \bot \Leftrightarrow {\bf PA} \vdash \neg \operatorname{Pr} (\lceil \bot \rceil) \Leftrightarrow & \\ & {\bf PA} \vdash \bot \Leftrightarrow {\bf PA} \vdash \operatorname{Con} & \end{array}

We discussed the incompleteness of formal arithmetic and its influence on the foundations of mathematics. Let us discuss now how we can study provability and consistency using modal logic.

Gödel-Löb logic and Solovay’s theorem

Gödel-Löb logic (GL{\bf GL}) is an extension of the logic K{\bf K} with Löb formula (pp)p\Box (\Box p \to p) \to \Box p. One may rewrite this formula with diamonds as p(p¬p)\Diamond p \to \Diamond (p \land \neg \Diamond p). In terms of possibility, Löb formula has an explanation à la if something is possible then it’s possible for the last time. In other words, every possibility appears only ones, dies after that, and never repeats. It sounds quite pessimistic and very realistic at the same time, isn’t it?

From a Kripkean perspective, GL{\bf GL} is the logic of transitive and Noetherian frames. We have already discussed what transitivity is. Let us discuss Noetherianness. A Noetherian relation (or well-founded) is a binary relation RR such that there are no increasing chains x0Rx1Rx_0 R x_1 R \dots. Equivalently (modulo axiom of choice), any non-empty subset has a RR-maximal element. An element xx is called RR-maximal in some non-empty subset WW', if for each yWy \in W' one has yRxy R x and there is no zz such that xRzx R z. Here we claim that GL=Log(F){\bf GL} = \operatorname{Log}(\mathbb{F}), where F\mathbb{F} is the class of all transitive and Noetherian frames. This relation is named after Emmy Noether, a famous German mathematician, whose results have influence in commutative algebra and ring theory.

Amalie Emmy Noether, German mathematician

Note that the Gödel-Löb formula is not the Salqvist one and it is not canonical. Moreover, well-foundedness is not a first-order definable property of Kripke frames since we need quantifiers over subsets, not only over elements. Thus, we cannot prove that GL{\bf GL} is Kripke complete via its canonical model. One may show the Kripke completeness using more sophisticated tool called selective filtration provided by Dov Gabbay in the 1970-s. We drop the selective filtration in our post, the reader might study this tool herself. Here we recommend the same-titled paper by Gabbay.

By the way, Löb’s formula also has a computational interpretation and connections with functional programming. Read this blog post by Neel Krishnaswami to become acquainted with this aspect of Gödel-Löb logic. A Haskell engineer might have met something similar to Löb’s formula. Here we mean the function called cfix from the module Control.Comonad, a comonadic fixed-point operator.

We need Gödel-Löb logic to charaterise provability and consistency in Peano arithmetic. Let us define an arithmetic realisation. Let ClΩ\operatorname{Cl}{\Omega} be the set of all closed arithmetical formulas. Suppose also one has a valuation of propositional variables r:PVClΩr : \operatorname{PV} \to \operatorname{Cl}{\Omega} such that each variables maps to some arithmetic sentence. An arithmetic realisation is a map ρ\rho such that:

  1. ρ(p)=r(p)\rho ( p ) = r ( p )
  2. ρ()=\rho(\bot) = \bot
  3. ρ(φψ)=ρ(ϕ)ρ(ψ)\rho(\varphi \to \psi) = \rho(\phi) \to \rho(\psi)
  4. ρ(φ)=Pr(ρ(φ))\rho(\Box \varphi) = \operatorname{Pr} (\lceil \rho(\varphi) \rceil)

In other words, an arithmetic realisation is an extension of a given valuation to all modal formulas. An arithmetic realisation is an interpretion of modal formulas in terms of arithmetic sentences and their provability. As you could see, we read φ\Box \varphi as φ\varphi is provable in Peano arithmetic. Solovay’s theorem claims the following fascinating fact:

Theorem A modal formula φ\varphi is provable in GL{\bf GL} if and only if it’s interpretation in PA{\bf PA} is provable for every arithmetic realisation.

The “only if part” is proved quite simply. This part claims that an interpretation of provable in GL{\bf GL} formula is provable in PA{\bf PA} is provable for every arithmetic realisation. The fact that such an interpretation respects the necessitation rule follows from the first Hilbert-Bernays-Löb condition. Kripke axiom also preserves because of the second HBL condition. The provability of Löb axiom interpretation follows from the formalisation of Löb’s theorem in Peano arithmetic. The converse implication is much harder than the previous one and we drop it. The reader might familiarise with the arithmetical completeness proof in the book The Logic of Provability by George Boolos.

This theorem is often called the arithmetical completeness of GL{\bf GL} that gives us a purely modal characterisation of provability in Peano arithmetic. In other words, all statements we can formally prove about provability and consistency are covered in the system of modal logic.

For instance, as we told earlier, PA{\bf PA} doesn’t prove its consistency, a formula of the form ¬PrPA()\neg {\bf Pr}{\bf PA}(\lceil \bot \rceil). The modal counterpart of ConPA\operatorname{Con}{\bf PA} is the formula \Diamond \top which claims that relation in a Kripke frame is serial, i.e., every point has a successor. It is not so hard to check that \Diamond \top isn’t provable in GL{\bf GL} since a frame cannot be Noetherian and serial at the same time: if any increasing chain has a maximal element, then there exists a deadlock that has no successors. Thus, Noetherianess contradicts to seriality. In other words, GL{\bf GL} \oplus \Diamond \top is inconsistent:

(1)(¬)The instance of Lo¨b formula(2)Seriality(3)(¬)(1), (2), Modus Ponens(4)¬Top is a neutral for conjunction(5)¬¬¬Unfolding diamond with negation and box(6)¬Double negation elimination(7)(2), Necessitation(8)¬(6), (7), Conjuction introduction(9)(8), Boolean tautology\begin{array}{lll} (1) & \Diamond \top \to \Diamond (\top \land \neg \Diamond \top)& \\ & \:\:\:\: \text{The instance of Löb formula}& \\ (2) & \Diamond \top& \\ & \:\:\:\: \text{Seriality}& \\ (3) & \Diamond (\top \land \neg \Diamond \top)& \\ & \:\:\:\: \text{(1), (2), Modus Ponens}& \\ (4) & \Diamond \neg \Diamond \top& \\ & \:\:\:\: \text{Top is a neutral for conjunction}& \\ (5) & \neg \Box \neg \neg \Diamond \top& \\ & \:\:\:\: \text{Unfolding diamond with negation and box}& \\ (6) & \neg \Box \Diamond \top& \\ & \:\:\:\: \text{Double negation elimination}& \\ (7) & \Box \Diamond \top& \\ & \:\:\:\: \text{(2), Necessitation}& \\ (8) & \neg \Box \Diamond \top \land \Box \Diamond \top& \\ & \:\:\:\: \text{(6), (7), Conjuction introduction}& \\ (9) & \bot& \\ & \:\:\:\: \text{(8), Boolean tautology}& \\ \end{array}

Under the similar circumstances, GLpp{\bf GL} \oplus \Box p \to p is inconsistent. That is, a Noetherian frame cannot be a reflexive one:

(1)ppReflexivity axiom(2)(pp)(1), Necessitation(3)(pp)pLo¨b formula(4)p(2), (3), Modus Ponens(5)p(1), (4), Modus Ponens(6)(5), Substitution\begin{array}{lll} (1) & \Box p \to p & \\ & \:\:\:\: \text{Reflexivity axiom}& \\ (2) & \Box (\Box p \to p )& \\ & \:\:\:\: \text{(1), Necessitation}& \\ (3) & \Box (\Box p \to p) \to \Box p& \\ & \:\:\:\: \text{Löb formula}& \\ (4) & \Box p & \\ & \:\:\:\: \text{(2), (3), Modus Ponens}& \\ (5) & p & \\ & \:\:\:\: \text{(1), (4), Modus Ponens}& \\ (6) & \bot & \\ & \:\:\:\: \text{(5), Substitution}& \end{array}

Gödel incompleteness theorems admit a variety of generalisations. Here we refer the reader to the book Aspects of Incompleteness by Per Lindström.

We discussed before how modal logic is connected with such fundamental disciplines as metamathematics and topology. Now we overview briefly more applied aspects of modal logic. As we told, modalities in logic have a philosophical interpretation in terms of necessity and possibility. We saw above modal operators also have more mathematical reading such as operators on subsets of topological space and provability in formal arithmetic. First of all, we overview temporal logic.

Temporal logic

Historically, temporal logic arose as a branch of philosophical logic like modal logic itself. Arthur Prior, a New Zealander philosopher and logician, was the first who described logical systems with temporal modalities in the 1950-1960-s. Prior extended modal language with operators \Box^{-} and \Diamond^{-}. Here, φ\Box \varphi and φ\Diamond \varphi denotes φ\varphi will always be true in the future and φ\varphi will occur at some moment correspondingly. Modalities \Box^{-} and \Diamond^{-} have the same interpretation, but in terms of future. If we will consider Kripke models, then the semantics for \Box and \Diamond are the same as we used to consider. \Box^{-} and \Diamond^{-} have similar truth conditions in terms of converse relation:

  1. M,xφyR1(x)M,yφ\mathcal{M}, x \models \Box^{-} \varphi \Leftrightarrow \forall y \in R^{-1}(x) \:\: \mathcal{M}, y \models \varphi
  2. M,xφyR1(x)M,yφ\mathcal{M}, x \models \Diamond^{-} \varphi \Leftrightarrow \exists y \in R^{-1}(x) \:\: \mathcal{M}, y \models \varphi where R1R^{-1} denotes the converse relation.

We are not going to consider such systems of temporal logic more closely. We only note that such modalities allow one to characterise such structures as the real line much more precisely. Instead of unary temporal modalities, we consider binary ones. We reformulate our modal language to stay accurate:

As usual, we have a countably infinite set of propositional variables PV={p0,p1,p2,}\operatorname{PV} = \{ p_0, p_1, p_2, \dots \}. Temporal language with binary modalities is defined as follows:

  1. Any propositional variable is a formula
  2. \bot is a formula
  3. If φ\varphi, ψ\psi are formulas, then (φψ)(\varphi \to \psi) is a formula.

The items above define usual language of classical logic. The following item is completely different: 4. If φ\varphi, ψ\psi are formulas, then (φUψ)(\varphi \mathcal{U} \psi) and (φSψ)(\varphi \mathcal{S} \psi) are formulas.

The question we need to ask is how should we read φUψ\varphi \mathcal{U} \psi and φSψ\varphi \mathcal{S} \psi?

φUψ\varphi \mathcal{U} \psi and φSψ\varphi \mathcal{S} \psi are read as “φ\varphi until ψ\psi” and “φ\varphi since ψ\psi”. More strictly, these modalities have the semantics:

  1. M,sφUψ\mathcal{M}, s \models \varphi \mathcal{U} \psi if and only if there exists tt such that tR(s)t \in R(s) and M,tψ\mathcal{M}, t \models \psi and for all uu such that sRusRu and uRtuRt M,uφ\mathcal{M}, u \models \varphi.
  2. M,sφSψ\mathcal{M}, s \models \varphi \mathcal{S} \psi if and only if there exists tt such that tR1(s)t \in R^{-1}(s) and M,tψ\mathcal{M}, t \models \psi and for all uu such that tRut R u and uRsu R s M,uφ\mathcal{M}, u \models \varphi.

Here we note that unary modalities φ\Diamond \varphi and φ\Diamond^{-} \varphi are expressed as Uφ\top \mathcal{U} \varphi and Sφ\top \mathcal{S} \varphi. Thus, such binary modalities generalise unary modalities proposed by Prior. Initially, such modalities were introduced by Kamp for continuous ordering description on the real line. We will take a look at the system of temporal logic that represents the behaviour of concurrent programs axiomatically.

Here we observe the temporal logic of concurrency briefly. Read the book by Goldblatt called Logics of Time and Computation, Chapter 9 for more details. The core idea is we describe a program behaviour on the set of states with reachability relation as on a Kripke frame. Here, modalities describe alternatives in further actions depending on the execution at the current state, e.g., for process deadlocks and showing correctness.

We will use only U\mathcal{U} modality with unary modality denoted as \bigcirc. Here we work with a state sequence, a pair S,σ\langle S, \sigma \rangle, where SS is a non-empty set and σ\sigma is a surjective enumeration function that map every state to some natural number. We require surjectivity to restore a state by its number. The desired Kripke structure is a state sequence with relation RR such that iRji R j iff j=i+1j = i + 1. A Kripke model is a state sequence equipped with a valuation function, as usual. We extended the language with \bigcirc that has the following semantics:

M,iφ\mathcal{M}, i \models \bigcirc \varphi if and only iff M,i+1φ\mathcal{M}, i+1 \models \varphi.

The logic we are interested in is an extension of classical logic with following modal axioms:

  1. (pq)(pq)\Box (p \to q) \to (\Box p \to \Box q)
  2. (pq)(pq)\bigcirc (p \to q) \to (\bigcirc p \to \bigcirc q)
  3. ¬p¬p\bigcirc \neg p \leftrightarrow \neg \bigcirc p
  4. ppp\Box p \to p \land \bigcirc \Box p
  5. (pp)(pp)\Box (p \to \bigcirc p) \to (p \to \Box p)
  6. pUqqp \mathcal{U} q \to \Diamond q
  7. pUqq(p(pUq))p \mathcal{U} q \leftrightarrow q \lor (p \land \bigcirc (p \mathcal{U} q)) Inference rules: Modus Ponens, Substitution, Necessitation for \Box and \bigcirc.

The first two principles just tell us that both unary modalities are normal ones. The third axiom claims that \bigcirc is a functional relation, that is, if i=ji = j implies i+1=j+1i + 1 = j + 1. The fourth postulate describes the connection between unary modalities: if pp is always true in the future, then it’s true at the current moment and it’s always true at the next moment. The fifth axiom is a sort of induction principle: if it is always true that pp implies itself at the next state, then it’s true for every state. The formal logic that we described above is exactly the logic of all state systems considered as Kripke frames

Temporal logic of concurrency is just an example of modal logic use in computation and program verification. For instance, the reader may take a look at the project called Verified smart contracts based on reachability logic. Reachability logic is a formal system that combines core ideas of Hoare’s logic, separation and temporal logics. This project provides a framework that produces a formal specification for a given smart contract passed as an input. Such a specification is formulated in terms of reachability logic language. After that, one needs to show that a low-level code (EVM bytecode, for instance) behaviour satisfies the infered specification. The fact of this satisfiability should be provable in reachability logic and such proofs are formalised in this formal system via K-framework. The examples of verified smart contracts are OpenZeppelin ERC 20, Ethereum Casper FFG, and Uniswap.

Intuitionistic modal logic and monads

Intuitionistic modal logic is modal logic where the underlying logic is intuitionistic one. That is, we reject the law of excluded middle. Such a rejection is needed to consider formally constructive reasoning in which proof is a method that solves a given task. One may consider intuitionistic modal logic from two perspectives. The first perspective is the philosophical one: we try to answer the question about necessity and possibility from a constructive point of view. The second perspective is closer to constructive mathematics and functional programming. As it is well-known that one may map any constructive proof to typed lambda calculus, where proofs correspond to lambda-terms and formulas to types. In such an approach, modality is a computational environment.

Here we discuss monadic computation within intuitionistic modal logic to consider logical foundations of basic constructions used in such languages as Haskell. One of the most discussed topics in functional programming in Haskell is monad, a type class that represents an abstract data type of computation:

class Functor m => Monad m where
  return :: a -> m a
  (>>=) :: m a -> (a -> m b) -> m b

Here, the definition of the Monad type class is quite old fashioned, but we accept this definition just for simplicity. Monad instances are Maybe, [], Either a, and IO. As the reader might know, Monad represents how to perform a sequence of linearly connected actions within some computational environment such as input-output, for instance. In such a sequence, the result of the current computation depends on the previous ones. Such a computation was considered type-theoretically by Eugenio Moggi who introduced the so-called monadic metalanguage. Without loss of generality, we can claim that monadic metalanguage is an extension of typed lambda-calculus with the additional typing rules that informally correspond to return and (>>=) methods. In fact, monadic metalanguage is a type-theoretic representation of Haskell-style monadic computation.

It is quite convenient to consider such a kind of computation in terms of monads, a categorical construction that arose as a generalisation of a composition of adjoint functors. In fact, Monad in Haskell is closer to Kleisli triple, an equivalent formulation of monad. Here are the typing rules of monadic metalanguage:

Monadic Meta Language

Monadic metalanguage is also studied logically, see the paper Computational Types from a Logical Perspective by P. N. Benton, G. M. Bierman, and V. de Paiva.

It is quite curious, one may consider monadic metalanguage in terms of Curry-Howard correspondence. From this perspective, this modal lambda-calculus is isomorphic to lax logic that was introduced by Robert Goldblatt in the paper called Grothendieck Topology as Geometric Modality, p.p. 131-172, where he studies modal aspects of a Grothendieck Topology, a categorical generalisation of a topological space. This logic is defined as follows:

  1. Axioms of intuitionistic logic. We recall that one needs to take axioms of classical logic and replace ¬¬pp\neg \neg p \to p with p¬pqp \land \neg p \to q
  2. (pq)(pq)\nabla (p \to q) \to (\nabla p \to \nabla q)
  3. ppp \to \nabla p
  4. pp\nabla \nabla p \to \nabla p Rules: Modus Ponens, Necessitation, and Substitution

Note that one may equivalently replace the fourth axiom with (pq)(pq)(p \to \nabla q) \to (\nabla p \to \nabla q), a type of monadic bind in eyes of Haskeller.

This logic also describes syntactically so-called nucleus operator that plays a huge role in pointfree topology, a version of general topology developed within constructive mathematics. If you apparently want to get more familiar with the related concepts, you may read the book Stone Spaces by Peter Johnstone or the third volume of Handbook of Categorical Algebra (the subtitle is Sheaf Theory) by Francis Borceux. Additionally, here we also recommend the brief lecture on Topos Theory course by André Joyal, here’s the link on YouTube where the same notions are covered.

Literature overview

Let us overview some of the monographs, textbooks, and papers that we recommend to you for further study if you are interested in it.

  • Basic Modal Logic by Patrick Blackburn, Maarten de Rijke and Yde Venema is one of the best introductory texts books in modal logic. This book covers such topics as relational semantics, algebraic semantics, first-order frame definability, general frames, computational aspects of modal logic and its complexity. Also, there are a lot of miscellaneous exercises that allow you to improve your mastery of the material.

  • Modal Logic by Alexander Chagrov and Michael Zakharyaschev can serve the reader as a handbook in basic concepts of modal logic. This book might be considered as a more detailed version of the previous book.

  • Modal Logic for Open Minds by Johan van Benthem is another introduction to modal logic. In contrast to the previous two books, Modal Logic for Open Minds is more concentrated on the variety of modal logic applications. In this book, the reader may study and build an understanding of basic spatial logic, epistemic logic, logic of time, logic in information dynamics, provability in formal arithmetic, etc. We also note that Modal Logic for Open Minds is written in accessible language and the textbook is full of humour.

  • An Essay in Classical Modal Logic is a PhD thesis by written Krister Segerberg at the beginning of the 1970-s. As we told in the first part, Segerberg is one of the founders of the contemporary modal logic. One may use this thesis as a laconic introduction to modal logic, especially to such topics as Kripke semantics, neighbourhood semantics, filtrations, and completeness theorems for basic logics.

  • Logics of Time and Computation by Robert Goldblatt is an introduction to modal logic but specified to tense logic and related systems that describes several dynamics and computation. The first part of the textbook is the standard introduction to basic modal logic. Further, Goldblatt studies discrete, dense, and continuous time; describes concurrent and regular computation via temporal logic with binary modalities and propositional dynamic logic. The third part covers model-theoretic aspects of predicate extensions of propositional dynamic logic.

  • Mathematics of Modality is the collection of papers by Robert Goldblatt, the author of the previous book. As an alternative introduction to modal logic, I would recommend the paper called Metamathematics of Modal Logic, the very first paper from this collection. In this paper, Kripke semantics is more discussed from a model-theoretic perspective. In addition to Kripke semantics, the reader may use the paper as an introduction to categorical and algebraic aspects of modal logic. By the way, Goldblatt is one of the pioneers in Categorical Logic and he is also famous as the author of Topoi: The Categorical Analysis of Logic textbook.

  • Handbook of Modal Logic, edition by Patrick Blackburn, Johan van Benthem and Frank Wolter. The title is self-explanatory. This handbook is a collection of introductory papers on diverse branches of modal logic written by well-known experts in corresponding areas. The handbook covers quite comprehensively more advanced topics and applications of modal logic in philosophy, game theory, linguistics, and program verification.

  • Handbook of Spatial Logics. The title is self-explanatory to the same extent as the previous one. This handbook is a collection of papers on applications of logic in spatial structures. Here we recommend especially the paper called Modal Logics of Space written by Johan van Benthem and Guram Bezhanishvili.

  • Provability Logic by Sergei Artemov and Lev Beklemishev is a comprehensive overview on the current state of affairs in provability logic, the area of modal logic that study provability of formal axiomatic theories as arithmetic and set theory. This paper has two parts. The first part is an observation of provability in arithmetical theory and its algebraic and proof-theoretical aspects. The second part is an introduction to logic of proofs that was proposed by Sergei Artemov as an extension of classical logic with proof-terms.

  • Quantification in Nonclassical Logics by Dov Gabbay, Valentin Shehtman and Dmitry Skvortsov is the fundamental monograph on the semantical problems of modal first-order logic. The problem is the variety of modal predicate logics are Kripke incomplete and one has to generalise Kripke semantics of first-order modal logic to make the class of incomplete logic more narrow. Here we recommend bringing to the attention of simplicial semantics, the most general version of predicate Kripke frame based on simplicial sets.

  • As we discussed, one may study weaker logics than normal ones. For that, we need to have a more general semantical framework. Such a framework is called neighbourhood semantics. Read the textbook called Neighbourhood semantics for Modal Logic by Eric Paquit to familiarise yourself with this generalisation of Kripke semantics.

  • If you’re interested in temporal logic, we may recommend the textbook Temporal Logic. Mathematical Foundations and Computational Aspects by Dov M. Gabbay, Ian Hodkinson, and Mark Reynolds.

Summary

I believe the reader did a great job trying to become engaged with all this abstract material. Let us overview what we observe. We started from a philosophical motivation of modal logic and its historical roots. We got acquainted with Kripke frames, the canonical frame and model, and filtrations in the first part. In the second part, we studied some use cases. Pure modal logic is quite abstract and therefore admits miscellaneous interpretations in a variety of subject matters. Our use case observation isn’t comprehensive, it’s merely an invitation. We provided the list above for further reading if the reader considers to study modal logic herself more deeply.

I thank Gints Dreimanis and Jonn Mostovoy for editing and remarkable comments. I want to say thank you to my mate and colleague Rajab Agamov from the Department of Mathematics at Higher School of Economics for helpful conversations and the fact that he is a good lad. I’m grateful to Alexandra Voicehovska for the idea of a snake in topological illustrations. This blog post series is mostly based on the lecture course that I gave at the Computer Science Club based in the Saint-Petersburg Department of Steklov Mathematical Institute last autumn. I’m also grateful to Ilya B. Shapirovsky and Valentin B. Shehtman of the Institute for Information Transmission Problems of the Russian Academy of Sciences for discussions on the course programme.

Banner that links to Serokell Shop. You can buy stylish FP T-shirts there!
More from Serokell
Incomplete and Utter Introduction to Modal Logic, Part 1Incomplete and Utter Introduction to Modal Logic, Part 1
serokell chatserokell chat
Beginner's guide to Elixir programming languageBeginner's guide to Elixir programming language