# Article

Full entry | PDF   (0.3 MB)
Keywords:
intuitionistic logic; polynomial-space; sequent calculus; Kripke semantics
Summary:
The well-known Dyckoff's 1992 calculus/procedure for intuitionistic propositional logic is considered and analyzed. It is shown that the calculus is Kripke complete and the procedure in fact works in polynomial space. Then a multi-conclusion intuitionistic calculus is introduced, obtained by adding one new rule to known calculi. A simple proof of Kripke completeness and polynomial-space decidability of this calculus is given. An upper bound on the depth of a Kripke counter-model is obtained.
References:
[1] Buss S., Pudlák P.: On the computational content of intuitionistic propositional proofs. Ann. Pure Appl. Logic 109 49-64 (2001). MR 1835237 | Zbl 1009.03027
[2] van Dalen D.: Intuitionistic logic. in: Handbook of Philosophical Logic, D. Gabbay and F. Guenthner, Eds., no. 164-167 in Synthese Library, Chapter III.4, pp.225-340, Kluwer, Dordrecht, 1986. Zbl 1002.03053
[3] Dershowitz N., Manna Z.: Proving termination with multiset orderings. Comm. ACM 22 465-476 (1979). MR 0540043 | Zbl 0431.68016
[4] Dyckhoff R.: Contraction-free sequent calculi for intuitionistic logic. J. Symbolic Logic 57 795-807 (1992). MR 1187448 | Zbl 0761.03004
[5] Hudelmaier J.: An \$O(n\log n)\$-space decision procedure for intuitionistic propositional logic. J. Logic Comput. 3 1 63-75 (1993). MR 1240404 | Zbl 0788.03010
[6] Kleene S.C.: Introduction to Metamathematics. D. van Nostrand, New York, 1952. MR 0051790 | Zbl 0875.03002
[7] Ladner R.: The computational complexity of provability in systems of modal logic. SIAM J. Comput. 6 3 467-480 (1977). MR 0450027