1
$\begingroup$

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

$\endgroup$
1
$\begingroup$

A quick google search shows that the problem is PSPACE complete, a result apparently first proven by R. Statman.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.