# Modal logics axiomatised with nesting depth one which are unlikely to be in PSPACE?

I am looking for modal logics, which are axiomatised by a finite set of axioms of modal nesting depth one, and whose satisfiability / derivability problem is unlikely to be in PSPACE. Without the restriction on the modal nesting depth this is not a problem, see for example PDL. But it seems that in proving for example EXPTIME-hardness by reduction to some kind of tiling problem or acceptance problem for Turing machines, one would need some kind of transitivity, which is axiomatised in depth two. There are also undecidable logics with a binary modality (Kurucz et al.: Decidable and undecidable logics with a binary modality, 1995), but these typically require associativity, which is depth two as well. In Conditional Logic, again it seems that we need depth two for EXPTIME-hardness (Friedman, Halpern: On the Complexity of Conditional Logics, 1994).

Can we get EXPTIME-hardness with axioms of nesting depth one?

Background: We are trying to find generic decision procedures of a good complexity for logics axiomatised with nesting depth one.

I just realized that there is a nice solution to your problem, if you are willing to consider linear logic as your ambient logic instead of intuitionistic or classical logic. As is well-known, linear logic with the exponential modality $!A$ is not decidable. Furthermore, the exponential is a comonad featuring the duplication axiom $!A \multimap !!A$, which is evidently an axiom of nesting depth 2.

(I got this far right away, and then I got stuck -- which is why this answer is so late.)

However, I just realized that in implicit complexity, people modify the exponential $!A$ of linear logic to more precisely control the space and time usage of cut-elimination. Critically, all systems for doing so eliminate the duplication axiom! As a result, you can choose a system for which normalization likely goes past PSPACE (e.g., Elementary Affine Logic is as strong as elementary bounded Turing machines), and then the axiomatization of that will be unlikely to be in PSPACE, since that would imply that you could find cut-free proofs quickly.

Link: Ugo dal Lago and Simone Martini, Phase Semantics and Decidability of Elementary Affine Logic

I would suggest reading Blackburn, de Rijke and Venema's book Modal Logic.

• Based on the way the question is phrased, it seems quite clear that Bjoern is quite familiar with the book. – András Salamon Jun 4 '11 at 16:19
• While reading this book is always a good idea, I could not find much information on my question in it. The examples for EXPTIME-hardness (or undecidability) all make use of a depth 2 (or more) axiomatisation, mostly for a transitive accessibility relation. Did you have a specific section / example in mind? – Bjoern Lellmann Jun 6 '11 at 10:39
• I think you have registered a new account with the same name, which is why you can't comment. The moderators should be able to merge these accounts..? – Neel Krishnaswami Jun 6 '11 at 10:42
• @Bjoern, done as requested. (The problem: it seems that as Neel said you created a new account while you used another unregistered user account for posting the question. I merged your accounts so you shouldn't have no problem commenting anymore (it might take a few hours for the system's database to update). Let me know if the problem persists.) – Kaveh Jun 7 '11 at 1:57