Intuitionistic propositional logic is polynomial-space complete

Abstract

It is the purpose of this note to show that the question of whether a given propositional formula is intuitionistically valid (in Brouwer's sense, in Kripke's sense, or just provable by Heyting's rules, see Kreisel [7]) is p-space complete (see Stockmeyer [14]). 1. (a) There is a simple (i.e. polynomial time) translation of intuitionistic propositional logic into classical propositional logic if and only if NP = p-space.2. (b) The problem of determining if a type of the typed [lambda]-calculus is the type of a closed [lambda]-term is p-space complete (this will be discussed below).3. (c) There is a polynomial bounded intuitionistic proof system if and only if NP = p-space (see Cook and Reckhow [2]).