On sequent calculi for intuitionistic propositional logic

Vítězslav Švejdar

Commentationes Mathematicae Universitatis Carolinae (2006)

  • Volume: 47, Issue: 1, page 159-173
  • ISSN: 0010-2628

Abstract

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

How to cite

top

Švejdar, Vítězslav. "On sequent calculi for intuitionistic propositional logic." Commentationes Mathematicae Universitatis Carolinae 47.1 (2006): 159-173. <http://eudml.org/doc/249855>.

@article{Švejdar2006,
abstract = {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.},
author = {Švejdar, Vítězslav},
journal = {Commentationes Mathematicae Universitatis Carolinae},
keywords = {intuitionistic logic; polynomial-space; sequent calculus; Kripke semantics; Kripke semantics; completeness; polynomial-space complexity},
language = {eng},
number = {1},
pages = {159-173},
publisher = {Charles University in Prague, Faculty of Mathematics and Physics},
title = {On sequent calculi for intuitionistic propositional logic},
url = {http://eudml.org/doc/249855},
volume = {47},
year = {2006},
}

TY - JOUR
AU - Švejdar, Vítězslav
TI - On sequent calculi for intuitionistic propositional logic
JO - Commentationes Mathematicae Universitatis Carolinae
PY - 2006
PB - Charles University in Prague, Faculty of Mathematics and Physics
VL - 47
IS - 1
SP - 159
EP - 173
AB - 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.
LA - eng
KW - intuitionistic logic; polynomial-space; sequent calculus; Kripke semantics; Kripke semantics; completeness; polynomial-space complexity
UR - http://eudml.org/doc/249855
ER -

References

top
  1. Buss S., Pudlák P., On the computational content of intuitionistic propositional proofs, Ann. Pure Appl. Logic 109 49-64 (2001). (2001) Zbl1009.03027MR1835237
  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. Zbl1002.03053
  3. Dershowitz N., Manna Z., Proving termination with multiset orderings, Comm. ACM 22 465-476 (1979). (1979) Zbl0431.68016MR0540043
  4. Dyckhoff R., Contraction-free sequent calculi for intuitionistic logic, J. Symbolic Logic 57 795-807 (1992). (1992) Zbl0761.03004MR1187448
  5. Hudelmaier J., An O ( n log n ) -space decision procedure for intuitionistic propositional logic, J. Logic Comput. 3 1 63-75 (1993). (1993) Zbl0788.03010MR1240404
  6. Kleene S.C., Introduction to Metamathematics, D. van Nostrand, New York, 1952. Zbl0875.03002MR0051790
  7. Ladner R., The computational complexity of provability in systems of modal logic, SIAM J. Comput. 6 3 467-480 (1977). (1977) MR0450027
  8. Papadimitriou C.H., Computational Complexity, Addison-Wesley, Reading, MA, 1994. Zbl0833.68049MR1251285
  9. Statman R., Intuitionistic propositional logic is polynomial-space complete, Theoretical Comput. Sci. 9 67-72 (1979). (1979) Zbl0411.03049MR0535124
  10. Švejdar V., On the polynomial-space completeness of intuitionistic propositional logic, Arch. Math. Logic 42 7 (2003), 711-716; {http://dx.doi.org/10.1007/s00153-003-0179-x}. (2003) Zbl1025.03030MR2015096
  11. Takeuti G., Proof Theory, North-Holland, Amsterdam, 1975. Zbl0681.03039MR0882549
  12. Troelstra A.S., Schwichtenberg H., Basic Proof Theory, Cambridge University Press, Cambridge, 1996. Zbl0957.03053MR1409368

NotesEmbed ?

top

You must be logged in to post comments.

To embed these notes on your page include the following JavaScript code on your page where you want the notes to appear.

Only the controls for the widget will be shown in your chosen language. Notes will be shown in their authored language.

Tells the widget how many notes to show per page. You can cycle through additional notes using the next and previous controls.

    
                

                
Note: Best practice suggests putting the JavaScript code just before the closing </body> tag.