In the paper we consider complexity of intuitionistic propositional logic and its natural fragments such as implicative fragment, finite-variable fragments, and some others. Most facts we mention here are known and obtained by logicians from different countries and in different time since 1920s; we present these results together to see the whole picture.

The main result of the present paper is that the variable-free fragment of logic K*, the logic with a single K-style modality and its “reflexive and transitive closure,” is EXPTIMEcomplete. It is then shown that this immediately gives EXPTIME-completeness of variable-free fragments of a number of known EXPTIME-complete logics. Our proof contains a general idea of how to construct a polynomial-time reduction of a propositional logic to its n-variable—and even, in the cases of K*, PDL, CTL, ATL, and some others, (...) variable-free—fragments. Complexity of countermodels for such fragments is considered. (shrink)