16
$\begingroup$

I am currently taking a graduate logic course on Modal Logic and I can't help notice that there are a certain class of graphs characterized by the modal axioms such as (4) $\Box p \rightarrow \Box \Box p$, (5) $\Diamond p \rightarrow \Box \Diamond p$, or (B) $p \rightarrow \Box \Diamond p$ which can characterize frames as being transitive, Euclidean, and symmetric, respectively. In general, I notice many similarities between the models used in Modal Logic and the graphs in Graph Theory and I'm wondering if anyone knows if there are applications of Modal Logic to Graph Theory, or if one subject might be a special case of the other?

In any case, if anyone has studied this before or knows of any references on the interplay between Modal Logic and Graph Theory I would be very interested to read about it, and if it has not been studied before then I would be interested of any ideas regarding what open research problems could be stated to tackle the correspondence between these two topics. (A category theory perspective on this interplay would also be very interesting)

$\endgroup$
4
  • 3
    $\begingroup$ One category-theoretic approach to this is that Kripke models of modal logic can be seen as sheaf/presheaf models, with the modalities often coming from sheafification for some Grothendieck coverage (equivalently, some Lawvere-Tierney closure operator). I can’t off the top of my head remember where is a good source for reading up on this, but hopefully those keywords should at least be useful for searching with. $\endgroup$ Commented Feb 3, 2013 at 19:28
  • 1
    $\begingroup$ The answers below have mentioned that not every first order definable class of graphs is definable by a formula of propositional modal logic. It might be worth mentioning that first order logic is the smallest extension of modal logic endowed with nominals (variables whose semantics is a singleton) and the universal modality (allowing one to assert truth at every state) that has interpolation. Also, modal logic with nominals and the universal modality is decidable. See Balder Ten Cate's thesis hylo.loria.fr/content/papers/files/phd-thesis.pdf. $\endgroup$
    – Rob Myers
    Commented Feb 4, 2013 at 18:59
  • $\begingroup$ @Peter LeFanu Lumsdaine: Your comment is very interesting to me and I can't find many references on the topic you alluded to. Have you thought of anything I could look up regarding this? Possibly a survey article, or at least a journal article which defines the words you are using in the context of modal logic? Thanks $\endgroup$ Commented Feb 6, 2013 at 17:16
  • 1
    $\begingroup$ I believe the book "Toposes and local set theories" treats this to some extent, in chapter 6; I think Maclane/Moerdijk also goes into this, albeit at a much higher level of abstraction. $\endgroup$ Commented Feb 22, 2013 at 2:35

4 Answers 4

16
$\begingroup$

The relationship between modal logic and graph theory has, indeed, been studied before. Peter mentioned sheaf models in the comments; I want to mention a more classical-logic-y perspective.

(First, let me note that when we say that $\phi$ characterizes a class of frames $V$, we mean that for every frame in $V$, and every valuation on that frame, $\phi$ is true, i.e., $\phi$ is a validity on every frame in $V$. There are frames together with valuations which satisfy, e.g., $\square p\implies \square \square p$ without the frame being transitive.)

It's a natural question to ask which properties of frames can be defined by propositional modal formulas. For example, as you mentioned in the question, we can characterize transitivity by a single modal formula. It turns out that the class of properties of frames which can be captured by modal formulas is substantially larger than the class of first-order-definable properties. Blackburn, de Rijke, and Venema's book ("Modal logic") gives the example of the Lob formula: $$ \square (\square p\implies p)\implies \square p$$ They show that this formula is a validity in precisely those frames in which the relation $R$ is transitive and well-founded (although they use the term "converse well-founded"). By a compactness argument, this class of frames is not first-order axiomatizable. A result of Goldblatt and Thomason in 1974 showed that "a first-order frame property is modally definable iff it is preserved under taking generated subframes, p-morphic frame images, disjoint unions, and inverse ultrafilter extensions." I don't really understand what all that means, but at the very least we can take away that not every first-order property of frames is characterized by a (propositional) modal formula.

In the other direction, since the definition of "valid modal formula" is second-order, it's clear that any class of frames which can be captured by a modal formula is definable in second-order logic. I recall a paper on the strength of modal logic that showed that a sort of converse to this held, despite the converse itself failing (since, as mentioned above, not even every first-order property of frames is modally definable) but I can't track it down at the moment. EDIT: Emil found it - it's "Reduction of second-order logic to modal logic" by S. K. Thomason, and a (very poor) copy can be found here: http://onlinelibrary.wiley.com/doi/10.1002/malq.19750210114/abstract.

In general, the book "Modal logics" by Chagrov and Zakharyaschev is probably the book to look at. I don't know how up-to-date it is anymore, but it seems to include every perspective on modal logics that I've heard of, short of the category-theoretic aspects.

EDIT: Another aspect, which I didn't think of at first, is given by alternate interpretations of modalities. For example, suppose we interpret $\square p$ as meaning "more than half of visible nodes satisfy $p$," instead of "all visible nodes satisfy $p$;" or some other interpretation. Under each interpretation, the classes of graphs we can charaterize by modal formulas changes; and while any specific alternate interpretation is probably not too interesting, general tools for studying that would probably be very deep and valuable. I don't know of any work on this, but I suspect it's been done before; the closest related source I can find at present is the extended abstract of "The Modal Logic of Probability" (Heifetz, Mongin) which seems vaguely along these lines.

$\endgroup$
4
  • $\begingroup$ Well, $R\subseteq X^2$ is well-founded if every nonempty subset of $X$ has an $R$-minimal element, and converse well-founded if every such set has an $R$-maximal element. These are distinct properties, and GL corresponds to transitive frames with the latter property. As for the connection to second-order logic: modally definable second-order properties are indeed rather special (e.g., they are monadic $\Pi^1_1$, and they are preserved by the four operations listed), but the “sort of converse” you mention might be the result (due to Thomason, IIRC) that validity in full second-order logic ... $\endgroup$ Commented Feb 4, 2013 at 13:01
  • $\begingroup$ ... is recursively reducible to the relation “$\psi$ is valid in every Kripke frame in which $\phi$ is valid”. $\endgroup$ Commented Feb 4, 2013 at 13:02
  • $\begingroup$ It’s S. K. Thomason, Reduction of second-order logic to modal logic, Zeitschrift für mathematische Logik und Grundlagen der Mathematik 21 (1975), no. 1, 107–114. One can in fact fix $\phi$, so the reduction is to Kripke validity in a particular finitely axiomatized modal logic. (Thomason only states it for monadic second-order logic, but as far as I can see, this makes no difference, as one can encode a pairing function in the binary relation.) $\endgroup$ Commented Feb 4, 2013 at 13:56
  • $\begingroup$ @Emil: thanks for the citation! I spent a while looking for that paper with no luck. Re: your first point on terminology, I recall learning the opposite convention, that $R$ being well-founded meant that every $R$-increasing sequence terminates, but looking through my notes/books I can't see where I got that convention; so maybe I'm just conflating the picture with that of descriptive set theory (where, if your trees grow upwards, a tree is well-founded if every increasing chain terminates). $\endgroup$ Commented Feb 4, 2013 at 20:00
11
$\begingroup$

The ability of modal assertions to define natural and interesting classes of frames (or digraphs) is indeed intensely studied and constitutes one of the principal perpsectives of the subject, pervasive in all the literature and textbooks. Indeed, I heard Blackburn assert at a conference talk last fall that one should think about modal assertions mainly as a way of describing certain classes of graphs.

Any of the standard reference texts on modal logic will tell you that:

  • the modal theory S5 characterizes the equivalence relations;
  • the modal theory S4.3 characterizes the linear pre-orders;
  • the modal theory S4.2 characterizes the directed partial pre-orders;
  • the modal theory S4 characterizes the partial pre-orders;
  • And so on.

There are numerous instances of this phenomenon for various logics, and modal logicians are particularly interested in logics with the finite frame property, which are those definable as arising from a class of finite frames.

In some of my recent work, Structural connections between a forcing class and its modal logic, for example, we have been looking at all those logics and also what we call S4.tBA, topless-Boolean-algebra logic, which is characterized as the assertions true in every finite topless pre-Boolean algebra (a finite pre-Boolean algebra whose maximal cluster has been removed). We keep being pushed toward the idea that this may be the modal logic of class forcing, and also of c.c.c. forcing. The connection between the modal assertions and the nature of the frames is exploited throughout the work.

$\endgroup$
2
  • $\begingroup$ +1 for the unexpected appearance of Medvedev’s logic. (A minor quibble: since ML is not known to [and seems not to] coincide with the logic of arbitrary topless Boolean algebras, this applies to S4.tBA as well. That is, you shouldn’t drop “finite” from the definition.) $\endgroup$ Commented Feb 4, 2013 at 15:52
  • $\begingroup$ Thanks, Emil, I have inserted "finite", and this is indeed how we define it in the paper. This logic seems to be related to the modal logic of class forcing, and also curiously of c.c.c. forcing, but we can't yet settle either case exactly. $\endgroup$ Commented Feb 4, 2013 at 18:19
6
$\begingroup$

Maybe look at arrow logic?

$\endgroup$
1
  • $\begingroup$ Welcome to MO, Richard! $\endgroup$ Commented Mar 14, 2013 at 1:39
5
$\begingroup$

On page 724 the book "Handbook of Modal Logic" contains the phrase "modal logics are merely sublogics of appropriate monadic second-order logic" therefore you might be interested in the book "Graph Structure and Monadic Second-Order Logic" by Bruno Courcelle and Joost Engelfriet.

$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .