Abstract
In this paper, we compare several cut-free sequent systems for propositional intuitionistic logic Intwith respect to polynomial simulations. Such calculi can be divided into two classes, namely single-succedent calculi (like Gentzen's LJ) and multi-succedent calculi. We show that the latter allow for more compact proofs than the former. Moreover, for some classes of formulae, the same is true if proofs in single-succedent calculi are directed acyclic graphs (dags) instead of trees. Additionally, we investigate the effect of weakening rules on the structure and length of dag proofs.
The second topic of this paper is the effect of different embeddings from Int to S4. We select two different embeddings from the literature and show that translated (propositional) intuitionistic formulae have sometimes exponentially shorter minimal proofs in a cut-free Gentzen system for S4than the original formula in a cut-free single-succedent Gentzen system for Int. Moreover, the length and the structure of proofs of translated formulae crucially depend on the chosen embedding.
This is a preview of subscription content, log in via an institution to check access.
Similar content being viewed by others
References
Dragalin, A.G.: 1988, Mathematical Intuitionism. Introduction to Proof Theory, Vol. 67 of Translations of Mathematical Monographs. American Mathematical Society. Russian original 1979.
Dyckhoff, R.: 1992, 'Contraction-free sequent calculi for intuitionistic logic'. Journal of Symbolic Logic 57(3), 795-807.
Eder, E.: 1992, Relative Complexities of First Order Calculi. Braunschweig: Vieweg.
Egly, U.: 2000, 'Properties of Embeddings from Int to S4'. In: Proceedings of the International Conference on Automated Reasoning with Analytic Tableaux and Related Methods.
Egly, U., and S. Schmitt: 1998, 'Intuitionistic Proof Transformations and their Application to Constructive Program Synthesis'. In: J. Calmet and J. Plaza (eds.): Proceedings of the International Conference on Artifical Intelligence and Symbolic Computation (AISC'98), Vol. 1476 of Lecture Notes in Artificial Intelligence. pp. 132-144.
Egly, U., and S. Schmitt: 1999, 'On Intuitionistic Proof Transformations, Their Complexity and Application to Constructive Program Synthesis'. Fundamenta Informaticæ 39, 59-83.
Feferman, S., J.H. Dawson, Jr., S. C. Kleene, G.H. Moore, R. M. Solovay, and J. van Heijenoort (eds.): 1986, 'Kurt Gödel Collected Works', Vol. 1. New York:, Oxford University Press.
Fitting, M.: 1983, Proof Methods for Modal and Intuitionistic Logics. Dordrecht: D. Reidel.
Gentzen, G.: 1935, 'Untersuchungen über das logische Schließen'. Mathematische Zeitschrift 39, 176-210, 405-431. English translation in [18].
Gödel, K.: 1933, 'Eine Interpretation des intuitionistischen Aussagenkalkls'. In: Ergebnisse eines Mathematischen Kolloquiums, Vol. 4. pp. 39-40. English translation in [7], pp. 300-303.
Kleene, S. C.: 1952, Introduction to Metamathematics. Amsterdam: North-Holland Publishing Company.
Letz, R.: 1992, 'Polynomial Simulation of Sequent Systems by Tree Sequent Systems'. Technical report, Institut für Informatik, TU München.
Maehara, S.: 1954, 'Eine Darstellung der intuitionistischen Logik in der klassischen'. Nagoya Mathematical Journal 7, 45-64.
McKinsey, J.C. and A. Tarski: 1948, 'Some Theorems About the Sentential Calculus of Lewis and Heyting'. Journal of Symbolic Logic 13(1), 1-15.
Otten, J. and C. Kreitz: 1996, 'A Uniform Proof Procedure for Classical and Nonclassical Logics'. In: Proceedings of the 20 th German Annual Conference on AI. pp. 307-319.
Rasiowa, H. and R. Sikorski: 1953, 'Algebraic Treatment of the Notion of Satisfiability'. Fundamenta Mathematicæ 40, 62-95.
Schütte, K.: 1968, Vollständige Systeme modaler und intuitionistischer Logik, Vol. 42 of Ergebnisse der Mathematik und ihrer Grenzgebiete. Springer Verlag.
Szabo, M. E. (ed.): 1969, The Collected Papers of Gerhard Gentzen, Studies in Logic and the Foundations of Mathematics. North-Holland Publishing Company.
Troelstra, A. S., and H. Schwichtenberg: 1996, Basic Proof Theory, Vol. 43 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press.
Wallen, L.A.: 1990, Automated Deduction in Nonclassical Logics. MIT Press.
Author information
Authors and Affiliations
Rights and permissions
About this article
Cite this article
Egly, U. On Different Intuitionistic Calculi and Embeddings from Int to S4 . Studia Logica 69, 249–277 (2001). https://doi.org/10.1023/A:1013869924088
Issue Date:
DOI: https://doi.org/10.1023/A:1013869924088