# What is the computational complexity of intuitionistic propositional logic?

Consider the decision problem: given formulas of propositional logic $$\phi_1, \ldots, \phi_n, \psi$$, determine whether $$\phi_1, \ldots, \phi_n \vdash \psi$$ intuitionistically. This problem is well-known to be decidable, for example using an algorithm derived from the LJT* sequent calculus. I was wondering if the computational complexity of this problem is known.

Trivially, the complexity is polynomial-equivalent to the complexity of the intuitionistic tautology problem: $$\phi_1, \ldots, \phi_n \vdash \psi$$ if and only if $$\phi_1 \wedge \ldots \wedge \phi_n \rightarrow \psi$$ is a tautology; and conversely, $$\phi$$ is a tautology if and only if $$\vdash \phi$$. Certainly, the problem is co-NP-hard: as a corollary of the double-negation embedding, a formula $$\phi$$ is classically satisfiable if and only if $$\lnot \phi$$ is not a tautology of intuitionistic logic.

On the other hand, if I'm not mistaken, the problem is in PSPACE: the only rule of LJT* which could possibly increase the total length of a proof context is in the first subgoal of $$(\alpha, \beta \rightarrow \gamma, \Gamma \vdash \beta) \wedge (\gamma, \Gamma \vdash \delta) \implies (\alpha \rightarrow \beta) \rightarrow \gamma, \Gamma \vdash \delta$$. But in that case, the second copy of $$\beta$$ should still be at most equal to the length of a formula in the original context.

(Also, since the Rieger-Nishimura lattice, the free Heyting algebra on one generator, has a simple computable description, the special case of this problem restricted to problems with a single atom would be in P. That would be a severe restriction, though.)

Beyond that, in a quick Google search, I didn't find any results directly on this problem, just a few papers where the abstracts seemed to indicate they were considering fragments of propositional logic. I also can't find any proof on my own which would refine the status. (For example, for all I know, it might be possible that whenever the sequent is not intuitionistically valid, there exists a Kripke model of polynomial size which demonstrates this - in which case the problem would be co-NP-complete. Or more generally, a Heyting algebra with a polynomial-size "description" would suffice. It's harder for me to imagine some way to reduce a problem such as QBF to an instance of this problem to prove it's PSPACE-complete, though I also can't entirely rule out the possibility.)