Polynomial space hardness without disjunction property (Q1935776)

The present paper is a study of polynomial space hardness (PSPACE-hard) on all varieties in the interval between Heyting algebras with weak excluded middle (i.e., \(\lnot \alpha \vee \lnot \lnot \alpha \)) and divisible commutative integral residuated lattices. (This interval is referred to by H/CIR in this review.) In [\textit{R. Horčík} and \textit{K. Terui}, Theor. Comput. Sci. 412, No. 31, 3992--4006 (2011; Zbl 1231.03021)], it is shown that if a variety of residuated lattices has the \textit{disjunctive property }(DP), then it has a PSPACE-hard equational theory. (The DP reads as follows: If \(\alpha \vee \beta \) is logically provable, then at least one of \(\alpha \) and \(\beta \) is logically provable as well.) Therefore, notice that all varieties with DP in H/CIR have a PSPACE-hard equational theory. In the paper under review, this result is extended by proving that all varieties in H/CIR have a PSPACE-hard equational theory, whence it follows that there are uncountably many varieties of residuated lattices lacking the DP and having a PSPACE-hard equational theory. The authors extend the idea of Statman's reduction [\textit{R. Statman}, Theor. Comput. Sci. 9, 67--72 (1979; Zbl 0411.03049)], which is essentially that ``a decision algorithm for intuitionistic tautologies can simulate effectively a brute force decision algorithm for the quantified Boolean sentences'' (p. 6). In particular, they show that Statman's reduction only requires a special case of DP (i.e., it does not require the full\ DP). Finally, it is to be noted that the authors' reduction only uses lattice and residual operations (multiplications and negations are not used).