The Closed Fragment of IL is PSPACE Hard

In this paper we consider IL0, the closed fragment of the basic interpretability logic IL. We show that we can translate GL1, the one variable fragment of Gödel-Löbʼs provabilty logic GL, into IL0. Invoking result on the PSPACE completeness of GL1 we obtain the PSPACE hardness of IL0.