# Is there a decision procedure for intuitionistic propositional logic?

Is institutionistic 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".

-

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.

-
Thanks. I'm sorry to say that what I really wanted to ask was about intuitionistic propositional logic. –  Pteromys Apr 25 '12 at 10:56
Okay, answer edited. –  Henning Makholm Apr 25 '12 at 11:07
You can also get the completeness semantically. If we fix a finite number of variables for propositional logic, there are only a finite number of possible Kripke frames for that set of variables, and therefore we can do an exhaustive search whether a particular formula is satisfied by every one of those frames. –  Carl Mummert Apr 25 '12 at 11:19
Is there any decision procedure that can be carried out by hand? –  Pteromys Apr 25 '12 at 11:20
@Pteromys: unless I am missing something, if there was a polynomial-time decision procedure for intuitionistic propositional logic, the double-negation translation would let us use this to make a polynomial-time decision procedure for classical propositional logic, and no such procedure is known to exist (if it does exist, then $P=NP$). So you can perform these decision procedures by hand, because they are effective, but they will not be very efficient. –  Carl Mummert Apr 25 '12 at 11:23

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.

-
I'll have a look at them after studying about using Heyting algebras as the models of intuitionist logic. Do you know good references? Most of textbooks I know of explain Kripke models, but not Heyting algebras. –  Pteromys Apr 25 '12 at 14:54
Let me add that "intutionistic propositional logic with one variable" is decidable in linear time, while "intutionistic propositional logic with two variables" is Pspace-complete. The first result is the classical one by Rieger-Nishimura, and the second one is a recent result by Mikhail Rybakov. –  boumol Apr 25 '12 at 14:55
@Pteromys I think the Sørensen-Urzyczyn book is a good introduction. Section 2.4 is specifically about Heyting algebras as models of intuitionistic logic. You may be able to find it online, since it was widely distributed before it was published by Springer. A Heyting algebra is more general than a Boolean algebra, but less general than a distributive lattice. –  MJD Apr 25 '12 at 15:00

Gentzen was the first to show decidability. Papers about 1990 by Jörg Hudelmaier (giving an O(n log n)-space decision procedure) and by myself (Roy Dyckhoff) should be studied by anyone interested in using such a procedure. These show (following earlier work of Vorob'ev in 1950) how to avoid loop-checking in a root-first sequent calculus search. Avoiding back-tracking is a harder problem... The appropriate calculus G4ip is covered in the standard text, Basic Proof Theory. The ILTP library at Potsdam (maintained by Jens Otten) links to implementations and classes of problems. Use of large Heyting algebras isn't really the best way to do it...

-
and, yes, the G4ip calculus is simple for the decision procedure to be carried out by hand. –  Roy Dyckhoff Oct 25 '13 at 2:18