<p>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. </p>

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

<p>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. </p>

<p>Link: Ugo dal Lago and Simone Martini, <a href="http://www.cs.unibo.it/~martini/papers-to-ftp/phasem.pdf.gz" rel="nofollow">Phase Semantics and Decidability of Elementary Affine Logic</a></p>

CC BY-SA 3.0
2011-08-08T07:44:09.690Z
2011-08-08T07:44:09.690Z
Neel Krishnaswami
<p>I would suggest reading Blackburn, de Rijke and Venema's book <a href="http://www.mlbook.org/" rel="nofollow">Modal Logic</a>.</p>

CC BY-SA 3.0
2011-06-04T16:19:06.810Z
Based on the way the question is phrased, it seems quite clear that Bjoern is quite familiar with the book.
András Salamon
CC BY-SA 3.0
2011-06-06T10:39:00.977Z
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
CC BY-SA 3.0
2011-06-06T10:42:41.930Z
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
CC BY-SA 3.0
2011-06-07T01:57:13.247Z
@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
CC BY-SA 3.0
2011-06-04T13:49:44.890Z
2011-06-04T13:49:44.890Z
Rob
<p>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.: <em>Decidable and undecidable logics with a binary modality</em>, 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: <em>On the Complexity of Conditional Logics</em>, 1994). </p>

<blockquote>
  <p>Can we get EXPTIME-hardness with
  axioms of nesting depth one?</p>
</blockquote>

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

<cc.complexity-theory><lo.logic><modal-logic>
Modal logics axiomatised with nesting depth one which are unlikely to be in PSPACE?
Bjoern Lellmann
# Modal logics axiomatised with nesting depth one which are unlikely to be in PSPACE?

(Asked by: username_0 on 2011-06-02)

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.

**Tags:** cc.complexity-theory, lo.logic, modal-logic


---

## 2 answers

### Answer by username_1 on 2011-08-08. Score: 4

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](http://www.cs.unibo.it/~martini/papers-to-ftp/phasem.pdf.gz)


---

### Answer by username_2 on 2011-06-04. Score: 0

I would suggest reading Blackburn, de Rijke and Venema's book [Modal Logic](http://www.mlbook.org/).

> **Comments:**
> **username_3**: Based on the way the question is phrased, it seems quite clear that Bjoern is quite familiar with the book.  
> **username_0**: 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?  
> **username_1**: 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..?  
> **username_4**: @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.)  

---

