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.