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