Is there a decision procedure for intuitionistic propositional logic?

Question

Is intutionistic propositional logic decidable? If so, what is a decision procedure for it, like tableaux for classical propositional logic?

EDIT: In the first revision I mistook "predicate" for "propositional".

Answer 1

No, there cannot be a decision procedure for intuitionistic predicate logic. If there were, then by the double-negation translation we could use it to decide classical predicate logic, which is known to be undecidable.

(Tableaux are not a decision procedure for classical predicate logic, because it is not guaranteed to terminate in the presence of quantifiers).

---

Edit: The question was changed to speak about intuitionistic propositional calculus. That is indeed decidable; one decision procedure is to search for a cut-free proof in the intuitionistic sequent calculus LJ. Since every formula in a cut-free and quantifier-free proof is a subformula of the eventual conclusion, there are only finitely many possible sequents that don't repeat formulas to the left of the turnstile, so even a brute-force proof search will terminate.

Answer 2

Even though you accepted Henning Makholm's answer already, this seemed likely to be of some use, and was too big for a comment, so I am posting it anyway.

I found some material related to your question on pages 33–34 of Lectures on the Curry-Howard Isomorphism by Sørensen and Urzyczyn. In particular (theorem 2.4.8 and surrounding discussion):

A [intuitionistic propositional] formula of length $n$ is valid iff it is valid in all Heyting algebras of cardinality at most $2^{2^n}$.

This might be feasible to check by hand if $n<3$. I think that by "length" here they mean "number of variables". They sketch the proof and refer the reader to Rasiowa and Sikorski The Mathematics of Metamathematics (Warsaw 1963) for details.

The next bit is perhaps more interesting:

From … the above theorem, it follows that intuitionistic propositional logic is decidable. But the upper bound obtained this way (double exponential space) can be improved down to polynomial space, with help of other methods, see ….

This time the reference is R. Statman. "Intuitionistic propositional logic is polynomial-space complete." Theoretical Computer Science, 9:67–72, 1979.

I hope this is of some use.