On the Undecidability of Some Sub-classical First-Order Logics | SpringerLink
Skip to main content
Springer Nature Link
Log in

On the Undecidability of Some Sub-classical First-Order Logics

  • Conference paper
  • First Online:
Foundations of Software Technology and Theoretical Computer Science (FSTTCS 1999)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 1738))

Abstract

A general criterion for the undecidabily of sub-classical firstorder logics and important fragments thereof is established. It is applied, among others, to Urquart’s (original version of) C and the closely related logic C*.In addition, hypersequent systems for (first-order) C and C* are introduced and shown to enjoy cut-elimination.

Partly supported by COST-Action No.15, FWF grant P-12652-MAT and WTZ Austria-Italy 1999-2000, Project No.4

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
¥17,985 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
JPY 3498
Price includes VAT (Japan)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
JPY 5719
Price includes VAT (Japan)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
JPY 7149
Price includes VAT (Japan)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Similar content being viewed by others

References

  1. A. Avron. Hypersequents, logical consequence and intermediate logics for concurrency. Annals for Mathematics and Artificial Intelligence, 4(199):225–248, 1991. 263, 264, 265, 265

    Article  MATH  MathSciNet  Google Scholar 

  2. A. Avron. The method of hypersequents in the proof theory of propositional nonclassical logics.In Logic: from Foundations to Applications, European Logic Colloquium, pages 1–32. Oxford Science Publications. Clarendon Press. Oxford, 1996. 264

    Google Scholar 

  3. M. Baaz, A. Ciabattoni, C. F ermüller, and H. Veith. Proof theory of fuzzy logics: Urquhart’s C and related logics. In Mathematical Foundations of Computer Science 1998, 23rd International Symposium, MFCS’98, Brno, Czech Republic, August 24-28, 1998, Proceedings, volume 1450 of LNCS, pages 203–212. Springer-Verlag, 1998. 258, 259, 263, 263, 263, 263, 264, 265, 265, 266

    Google Scholar 

  4. A. Ciabattoni. Bounded contraction in systems with linearity. In N. Murray, editor, Automated Reasoning with Analytic Tableaux and Related Methods, International Conference, TABLEAUX’99, Saratoga Springs, volume 1617 of LNAI, pages 113–128. Springer-Verlag, 1999. To appear. 266

    Google Scholar 

  5. M. Dummett. A propositional calculus with a denumerable matrix. Journal of Symbolic Logic, 24:96–107, 1959. 263

    MathSciNet  Google Scholar 

  6. J. Y. Girard. Linear logic. Theoretical Computer Science, 50:1–101, 1987. 263

    Article  MATH  MathSciNet  Google Scholar 

  7. K. Gödel. Zum intuitionistischen Aussagenkalkül. Anzeiger der Akademie der Wissenschaften in Wien, 69:65–66, 1932. 263

    Google Scholar 

  8. P. Hájek. Metamathematics of Fuzzy Logic. Kluwer, 1998. 258, 259, 263, 263

    Google Scholar 

  9. P. Hájek, L. Godo, and F. Esteva. A complete many-valued logic with productconjunction. Archive for Math. Logic, 35:191–208, 1996. 263

    MATH  Google Scholar 

  10. E. Kiriyama and H. Ono. The contraction rule in decision problems for logics without structural rules. Studia Logica, 50/2:299–319, 1991. 258

    Article  MathSciNet  Google Scholar 

  11. Y. Komori. Predicate logics without structural rules. Studia Logica, 45:393–404, 1985. 258

    Article  MathSciNet  Google Scholar 

  12. J. Lukasiewicz. Philosophische Bemerkungen zu mehrwertigen Systemen des Aussagenkalk üls. Comptes rendus des séances de la Société des Sciences et des Lettres de Varsovie Cl. III, 23:51–77, 1930. 263

    Google Scholar 

  13. J.M. M endez and F. Salto. Urquhart’s C with intuitionistic negation: Dummett’s LC without the contraction axiom. Notre Dame Journal of Formal Logic, 36/3:407–413, 1995. 258, 258, 263

    Article  MathSciNet  Google Scholar 

  14. H. Ono and Y. Komori. Logics without the contraction rule. Journal of Symbolic Logic, 50/1:169–201, 1985. 258, 265

    MathSciNet  Google Scholar 

  15. G. Takeuti. Proof Theory. North-Holland, Amsterdam, 2nd edition, 1987.

    Google Scholar 

  16. A. Urquhart. Many-valued logic. In D. Gabbay and F. Guenthner, editors, Handbook of Philosophical Logic, volume III. Reidel, Dordrecht, 1984. 258, 258, 263

    Google Scholar 

  17. A. Urquhart. Basic Many-valued logic. Manuscript, private communication, 1999. 258

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Technische Universität Wien, Austria

    Matthias Baaz, Christian Fermüller & Helmut Veith

  2. Università di Milano, Italy

    Agata Ciabattoni

Authors
  1. Matthias Baaz
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Agata Ciabattoni
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Christian Fermüller
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Helmut Veith
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computer Science and Engineering, Indian Institute of Technology, Chennai, 600036, India

    C. Pandu Rangan

  2. Institute of Mathematical Sciences C.I.T. Campus, Chennai, 600113, India

    V. Raman  & R. Ramanujam  & 

Rights and permissions

Reprints and permissions

Copyright information

© 1999 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Baaz, M., Ciabattoni, A., Fermüller, C., Veith, H. (1999). On the Undecidability of Some Sub-classical First-Order Logics. In: Rangan, C.P., Raman, V., Ramanujam, R. (eds) Foundations of Software Technology and Theoretical Computer Science. FSTTCS 1999. Lecture Notes in Computer Science, vol 1738. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-46691-6_20

Download citation

  • DOI: https://doi.org/10.1007/3-540-46691-6_20

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-66836-7

  • Online ISBN: 978-3-540-46691-8

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation