Edward Hauesler, PUC - Rio de Janeiro, Brasil

July 17, 2014, Thursday, 16h15m.

Abstract: 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 {γ1,…,γk}⊢Lα there is a proof in which each formula occurrence is either a sub-formula of α or of some of γ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.
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 {γ1,…,γk}⊢Lα there is a proof in which each formula occurrence is either a sub-formula of α or of some of γ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.

Room: 3.10, Mathematics

Support: SQIG/Instituto de Telecomunicações with support from FCT and FEDER namely by the FCT project PEst-OE/EEI/LA0008/2013.