Consider two sets: the set of validities of propositional logic and the set of validities of monadic predicate logic. Call the first set $VP$ and the second set $VQM$. Both of these sets are decidable, so there are Turing machines that recognize both them and their complements.
I'm interested in how the decidability of these two sets translates into grammars for them, along the lines of the Chomsky hierarchy. I have three questions:
(1) Are there context-sensitive grammars that generate $VP$ and $VQM$? The answer would be yes if the Turing machines that recognized these sets were linearly bounded, but I don't think they are.
(2) If these languages aren't context-sensitive, can anything be said about a grammar that generates them?
I would have a better grasp of the second question if I understood something about grammars between the top two levels of the Chomsky hierarchy, context-sensitive and unrestricted.
(3) There is a natural class of automata between linear-bounded Turing machines and unrestricted Turing machines: polynomially bounded TMs, exponentially bounded TMs, etc. Do these classes of TM track anything on the grammar side of the Chomsky hierarchy? If not, is there any structure to the gap between context-sensitive grammars and full-on unrestricted grammars?
(Just to be clear: I'm not talking about a grammar for propositional logic, but a grammar for its validities.)
EDIT: I thought I'd add a comment about why I'm interested in these questions. I know there is an unrestricted grammar that generates the (recursively enumerable but not recursive) set of validities of (full-on, polyadic) predicate logic. But since $VP$ and $VQM$ are not just recursively enumerable but recursive, I was wondering if the grammars that generate them might have more structure, in the Chomsky-hierarchy sense, than the grammar that generates the validities of all of predicate logic. In other words, I'm wondering if there is a grammatical way of detecting the difference between sets of validities that are recursive (as in the case of propositional and monadic predicate logic) and sets of validities that are merely recursively enumerable. What can be said about grammars of recursive but not recursively enumerable languages? Most references on the Chomsky hierarchy say nothing about this gap, but I don't know if that means there's nothing to be said.