the analysis of monadic second-order logic (contra full second-order logic) and the decomposition of $\mathcal$. It's worth noting that the idea of looking at "tame" fragments of "wild" logics appears all over the place, e.g. The last section of Chagrov and Zakharyaschev's book is also relevant, and in general I strongly recommend that book: it's quite dense, but has a huge wealth of material. At this point we move beyond the focus of this specific question the point I want to make is that modal logic is not a strengthening of first-order logic, but rather quite the opposite, and that for many applications this is actually a good thing. Vardi goes on to talk about types of tameness, specifically focusing on two ways of generating tame fragments of first-order logic - bounding the quantifiers and limiting the number of variables - and then argues that modal logic really represents a third, and extremely robust, kind of tameness. Only very restricted fragments of first-order logic are decidable. Furthermore, the undecidability of first-order logic is very robust. This is rather surprising when one considers the fact that modal logic, in spite of its apparent propositional syntax, is essentially a first-order logic, since the necessity and possibility modalities quantify over the set of possible worlds, and model checking and validity for first-order logic are computationally hard problems. The model-checking problem can be solved in linear time, while the validity problem is PSPACE-complete. This problem is known as the validity problem. The second problem is checking if a given formula is true in all states of all Kripke structures. This problem is known as the model-checking problem. The first problem is checking if a given formula is true in a given state of a given Kripke structure. "There are two main computational problems associated with modal logic.In particular, the following passage from page $2$ is quite relevant:
This paper by Vardi is a useful source in this regard.
After first-order logic burst on the scene, we came to understand modal logic as an intermediate logic, and that's the perspective I'm describing here since I think it matches more the perspective you're adopting. Note that this is reflected in the history of modal logic: it long predated first-order logic, and was an expansion of propositional logic by adding modal operators. Modal logic should be thought of as a particularly well-behaved fragment of first-order logic: we're often interested in decidable (or similarly nice) fragments of first-order logic in applications, and modal logic and its variants provide a wide swath of examples of such logics. Your impression is right, but missing the point in some sense: modal logic is strictly less powerful than first-order logic, and this is one of the reasons it is so important in various contexts (especially applications of logic in computer science)! The reason is that there is a fundamental "power-versus-tameness" tradeoff implicit in any choice of logic, and we often prefer the latter to the former. The remainder variously make use of reflexive, symmetry and transitive properties on R. Theorems 1-5, make no use of any restrictions on the accessibility relation R. See Standard Translation (from modal to FOL) at įOLLOW-UP: Using these Standard Translations, I was able to formally derive a number of "axioms" of modal logic (some said to be controversial at wiki). What can we do in this basic modal logic that we cannot do in predicate logic or vice versa?ĮDIT: No need to reinvent the wheel. It also seems that the other logical connectors are the same as those in propositional logic. Instead of $\forall x: P(x)$, we write $\square P$ (quantifying over a domain of discourse corresponding the set of all "possible worlds.") Instead of $\exists x: P(x)$, we write $\diamond P$. My first impression - I'm sure it can't be right - is that it is just different symbols for the same concepts in ordinary predicate logic. I am just beginning to study basic modal logic as described here (up to page 5 so far).
0 kommentar(er)
