On the polynomial-space completeness of intuitionistic propositional logic. (English) Zbl 1025.03030

Švejdar, Vítězslav

Arch. Math. Logic 42, No. 7, 711-716 (2003).

Summary: We present an alternative, purely semantical and relatively simple, proof of the Statman’s result that both intuitionistic propositional logic and its implicational fragment are PSPACE-complete.

MSC:

03D15	Complexity of computation (including implicit computational complexity)
68Q17	Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.)
03B20	Subsystems of classical logic (including intuitionistic logic)

Keywords:

intuitionistic logic; nonclassical logics; decision problem; polynomial space; Kripke models; logical connectives

References:

[1]	De\(\sim\)Jongh, D.H.J., Veltman, F.: Intensional Logic. Lecture notes. Philosophy Department, University of Amsterdam, Amsterdam, 1988
[2]	Ladner, R.: The computational complexity of provability in systems of modal logic. SIAM Journal of Computing 6(3), 467–480 (1977) · Zbl 0373.02025 · doi:10.1137/0206033
[3]	Papadimitriou, C.H.: Computational Complexity. Addison-Wesley, 1994 · Zbl 0833.68049
[4]	Spaan, E.: Complexity of modal logics. Dissertation, Faculty of mathematics and informatics, University of Amsterdam, Amsterdam, 1993 · Zbl 0831.03005
[5]	Statman, R.: Intuitionistic propositional logic is polynomial-space complete. Theoretical Comput. Sci. 9, 67–72 (1979) · Zbl 0411.03049 · doi:10.1016/0304-3975(79)90006-9
[6]	Takeuti, G.: Proof Theory. North-Holland, Amsterdam, 1975 · Zbl 0354.02027
[7]	Van Dalen, D.: Intuitionistic logic. In: D. Gabbay, F. Guenthner eds, Handbook of Philosophical Logic, number\(\sim\)164–167 in Synthese Library, Chapter III.4, pp. 225–340. Kluwer, Dordrecht, 1986