The closed fragment of IL is PSPACE hard

Abstract

In this paper from 2011 we consider ${\text{IL}}_0$, the closed fragment of the basic interpretability logic $\text{IL}$. We show that we can translate ${\text{GL}}_1$, the one variable fragment of Gödel-Löb's provabilty logic $\text{GL}$, into ${\text{IL}}_0$. Invoking a result on the PSPACE completeness of ${\text{GL}}_1$ we obtain the PSPACE hardness of ${\text{IL}}_0$.