[go: up one dir, main page]
More Web Proxy on the site http://driver.im/ Skip to main content
Springer Nature Link
Log in

On Different Intuitionistic Calculi and Embeddings from Int to S4

  • Published:
Studia Logica Aims and scope Submit manuscript

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.

Access this article

Log in via an institution

Subscribe and save

Springer+ Basic
£29.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Price includes VAT (United Kingdom)

Instant access to the full article PDF.

Institutional subscriptions

Similar content being viewed by others

References

  1. Dragalin, A.G.: 1988, Mathematical Intuitionism. Introduction to Proof Theory, Vol. 67 of Translations of Mathematical Monographs. American Mathematical Society. Russian original 1979.

  2. Dyckhoff, R.: 1992, 'Contraction-free sequent calculi for intuitionistic logic'. Journal of Symbolic Logic 57(3), 795-807.

    Google Scholar 

  3. Eder, E.: 1992, Relative Complexities of First Order Calculi. Braunschweig: Vieweg.

    Google Scholar 

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

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

  6. Egly, U., and S. Schmitt: 1999, 'On Intuitionistic Proof Transformations, Their Complexity and Application to Constructive Program Synthesis'. Fundamenta Informaticæ 39, 59-83.

    Google Scholar 

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

    Google Scholar 

  8. Fitting, M.: 1983, Proof Methods for Modal and Intuitionistic Logics. Dordrecht: D. Reidel.

    Google Scholar 

  9. Gentzen, G.: 1935, 'Untersuchungen über das logische Schließen'. Mathematische Zeitschrift 39, 176-210, 405-431. English translation in [18].

    Google Scholar 

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

    Google Scholar 

  11. Kleene, S. C.: 1952, Introduction to Metamathematics. Amsterdam: North-Holland Publishing Company.

    Google Scholar 

  12. Letz, R.: 1992, 'Polynomial Simulation of Sequent Systems by Tree Sequent Systems'. Technical report, Institut für Informatik, TU München.

    Google Scholar 

  13. Maehara, S.: 1954, 'Eine Darstellung der intuitionistischen Logik in der klassischen'. Nagoya Mathematical Journal 7, 45-64.

    Google Scholar 

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

    Google Scholar 

  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.

  16. Rasiowa, H. and R. Sikorski: 1953, 'Algebraic Treatment of the Notion of Satisfiability'. Fundamenta Mathematicæ 40, 62-95.

    Google Scholar 

  17. Schütte, K.: 1968, Vollständige Systeme modaler und intuitionistischer Logik, Vol. 42 of Ergebnisse der Mathematik und ihrer Grenzgebiete. Springer Verlag.

  18. Szabo, M. E. (ed.): 1969, The Collected Papers of Gerhard Gentzen, Studies in Logic and the Foundations of Mathematics. North-Holland Publishing Company.

  19. Troelstra, A. S., and H. Schwichtenberg: 1996, Basic Proof Theory, Vol. 43 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press.

  20. Wallen, L.A.: 1990, Automated Deduction in Nonclassical Logics. MIT Press.

Download references

Author information

Authors and Affiliations

  1. Institut f[uuml, TU Wien, Favoritenstr. 9-11, A-1040, Wien, Austria

    Uwe Egly

Authors
  1. Uwe Egly
    View author publications

    You can also search for this author in PubMed Google Scholar

Rights and permissions

Reprints 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

Download citation

  • Issue Date:

  • DOI: https://doi.org/10.1023/A:1013869924088

Search

Navigation