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.)
