Room P3.10, Mathematics Building

Edward Hauesler, PUC - Rio de Janeiro, Brasil

The subformula principle and computational complexity of propositional logics

In 1979 Richard Statman proved, using proof-theory, that the purely implicational fragment of Intuitionistic Logic is PSPACE-complete. He showed a polynomially bounded translation from full Intuitionistic Propositional Logic into its implicational fragment. By the PSPACE-completeness of S4, proved by Ladner, and the Godel translation from S4 into Intuitionistic Logic, the PSPACE-completeness of purely implicational fragment of Intuitionistic Logic is drawn. The sub-formula principle for a deductive system for a logic $L$ states that whenever $\{\gamma_1,\ldots,\gamma_k\} \vdash_{L} \alpha$ there is a proof in which each formula occurrence is either a sub-formula of $\alpha$ or of some of $\gamma_i$. In this work we extend Statman's result and show that any propositional (possibly modal) structural logic satisfying a particular statement of the sub-formula principle is PSPACE-complete. As a consequence, EXPTIME-complete propositional logics, such as PDL and the common-knowledge epistemic logic with at least 2 agents satisfy this particular sub-formula principle, if and only if, PSPACE=EXPTIME.