Let's say we have systems of modal logic defined as smallest sets

  • containing propositional tautologies,
  • all instances of schema $\square F \to (\square(F \to G) \to \square G)$
  • all instances of schema X, where X contains only propositional connectives, modal operator $\square$ and metavariables ($F$, $G$, ...)
  • is closed under modus ponens and necessitation (for every theorem $F$, $\square F$ is also a theorem)

Given two (such) modal logics $A$ and $B$, is it decidable whether for all $F$, $A \vdash F$ implies $B \vdash F$?

In other words, is there a mechanical way to describe the hierarchy of normal modal logics (containing one modality)?

I've found some theorems regarding systems with finite model property (but not all normal modal logics have fmp), and theorems regarding undecidability of some other systems (but perhaps more complex than those I'm interested in). For some systems of modal logic, and perhaps all of those I'm interested in - hope dies last - there is an adequate semantic tableau method (truth trees). If there was a mechanical way to describe the rules for producing the tableau adequate to an arbitrary system, then that would solve my question.



1 Answer 1


Can we reformulate the question as follows? Is the following problem decidable:

Problem Given two modal formulas $A$ and $B$, determine whether $$ \mathbf{K}\oplus A = \mathbf{K}\oplus B, $$ where $\mathbf{K}$ is the (well-known) minimal normal modal logic and $\oplus$ is the closure under the rules of modus ponens, substitution, and necessitation.

If this is your question, then the answer is definitely `No'. And hence the inclusion between these logics is undecidable, too. Moreover, there are fixed formulas $B$ for which the above problem is undecidable.

See Chapter 17 of Chagrov, Zakharyaschev "Modal Logic" for lots of lots of details. For instance, see Corollary 17.16: there is a finitely axiomatizable extension of $\mathbf{GL}$ (i.e., a fixed (!) modal formula $B$ in the above problem) such that the problem of coincidence with $\mathbf{K}\oplus B$ is indecidable. There is much more in that Chapter, so it will be interesting for you!

  • $\begingroup$ Yes, we can reformulate my question like that. Thanks! $\endgroup$
    – Luka Mikec
    Commented Apr 3, 2014 at 16:46

You must log in to answer this question.

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