Consider the decision problem: given formulas of propositional logic. $ phi_1, ldots, phi_n, psi $, determine if $ phi_1, ldots, phi_n vdash psi $ intuitionist It is known that this problem is decidable, for example, by using an algorithm derived from the sequential calculation LJT *. I was wondering if you know the computational complexity of this problem.

Trivially, complexity is polynomial-equivalent to the complexity of the problem of intuitionistic tautology: $ phi_1, ldots, phi_n vdash psi $ If and only if $ phi_1 wedge ldots wedge phi_n rightarrow psi $ It is a tautology; and on the contrary, $ phi $ it's a tautology if and only if $ vdash phi $.

Certainly, the problem is co-NP-hard: as a corollary of the inclusion of double negation, a formula $ phi $ is classically satisfactory if and only if $ lnot phi $ It is not a tautology of intuitionist logic.

On the other hand, if I'm not mistaken, the problem is in PSPACE: the only LJT rule * that could possibly increase the total length of a test context is in the first sub-goal 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 $ It should still be at most equal to the length of a formula in the original context.

(Also, since the Rieger-Nishimura network, the Heyting free algebra in a 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 constraint, although .)

Beyond that, in a quick Google search, I did not find any results directly on this problem, just some articles where the summaries seemed to indicate that they were considering fragments of propositional logic. Nor can I find any proof on my own that refines the state. (For example, as far as I know, it could be possible that as long as the sequence is not a valid intuitionist, there is a polynomial-sized Kripke model that demonstrates this, in which case the problem would be co-NP-complete. Heyting's algebra with a polynomial-sized "description" would suffice.I find it more difficult to imagine a way to reduce a problem like QBF to an instance of this problem to show that it is full PSPACE, although I can not do it at all either. .)