On sequent calculi for intuitionistic propositional logic. (English) Zbl 1138.03008

Švejdar, Vítězslav

Commentat. Math. Univ. Carol. 47, No. 1, 159-173 (2006).

The author analyzes R. Dyckhoff’s [J. Symb. Log. 57, No. 3, 795–807 (1992; Zbl 0761.03004)] calculus for intuitionistic propositional logic. Dyckhoff found a terminating procedure but did not mention Kripke semantics, nor the computational complexity of the procedure obtained. One of the results of the paper consists in making the Kripke completeness theorem explicit for the calculus. Moreover, the author proves that the decision procedure can work in polynomial space. This is an interesting result together with the already known fact that the calculus is polynomial-space hard (the fact was proved by R. Statman). In addition to the single-conclusion version of the calculus, a multi-conclusion version is considered as well, i.e., the calculus allowing sequents with any number of formulas in succedent. The author again proves, this time even in a much simpler way, that the calculus in question is complete with respect to Kripke semantics and yields a polynomial-space decision procedure. The multi-conclusion calculus proposed by the author differs from S. C. Kleene’s and G. Takeuti’s calculi only in one simple implication rule. The paper pays more attention to the question whether decision procedures can be derived from known, more or less traditional, calculi rather than to the question of how to construct the most efficient procedure. However, the question whether the implication rule introduced by the author is necessary in order that the calculus is decidable in polynomial space is left open. The rule is redundant, because it can be simulated by cuts, but it is not known whether the direct polynomial simulation is possible.

Reviewer: Marie Duží (Ostrava)

MSC:

03B20	Subsystems of classical logic (including intuitionistic logic)
03B35	Mechanization of proofs and logical operations
03F05	Cut-elimination and normal-form theorems
03F20	Complexity of proofs

Keywords:

Kripke semantics; completeness; polynomial-space complexity

Citations:

Zbl 0761.03004