Hostname: page-component-cd9895bd7-fscjk Total loading time: 0 Render date: 2024-12-22T14:03:17.579Z Has data issue: false hasContentIssue false
  • English
  • Français

Undecidability of First-Order Intuitionistic and Modal Logics with Two variables

Published online by Cambridge University Press:  15 January 2014

Roman Kontchakov ,
Agi Kurucz  and
Michael Zakharyaschev
Roman Kontchakov
Affiliation:
Department of Computer Science, King's College London, Strand, London WC2R 2LS, UK. E-mail: [email protected]
Agi Kurucz
Affiliation:
Department of Computer Science, King's College London, Strand, London WC2R 2LS, UK. E-mail: [email protected]
Michael Zakharyaschev
Affiliation:
Department of Computer Science, King's College London, Strand, London WC2R 2LS, UK. E-mail: [email protected]
Get access Rights & Permissions [Opens in a new window]

Abstract

We prove that the two-variable fragment of first-order intuitionistic logic is undecidable, even without constants and equality. We also show that the two-variable fragment of a quantified modal logic L with expanding first-order domains is undecidable whenever there is a Kripke frame for L with a point having infinitely many successors (such are, in particular, the first-order extensions of practically all standard modal logics like K, K4, GL, S4, S5, K4.1, S4.2, GL.3, etc.). For many quantified modal logics, including those in the standard nomenclature above, even the monadic two-variable fragments turn out to be undecidable.

Type
Research Article
Information
Bulletin of Symbolic Logic , Volume 11 , Issue 3 , September 2005 , pp. 428 - 438
Copyright
Copyright © Association for Symbolic Logic 2005

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

REFERENCES

[1] Berger, R., The undecidability of the domino problem, Memoirs of the American Mathematical Society, vol. 66 (1966).Google Scholar
[2] Börger, E., Grädel, E., and Gurevich, Yu., The classical decision problem, Perspectives in Mathematical Logic, Springer-Verlag, 1997.CrossRefGoogle Scholar
[3] Bull, R. A., MIPC as the formalization of an intuitionistic concept of modality, The Journal of Symbolic Logic, vol. 31 (1966), pp. 609–616.Google Scholar
[4] Chagrov, A. and Zakharyaschev, M., Modal logic, Oxford Logic Guides, vol. 35, Clarendon Press, Oxford, 1997.CrossRefGoogle Scholar
[5] Church, A., A note on the “Entscheidungsproblem”, The Journal of Symbolic Logic, vol. 1 (1936), pp. 40–41.Google Scholar
[6] Dummett, M., Elements of intuitionism, 2nd ed., Clarendon Press, Oxford, 1977.Google Scholar
[7] Gabbay, D., Semantical investigations in Heyting's intuitionistic logic, D. Reidel, 1981.CrossRefGoogle Scholar
[8] Gabbay, D., Kurucz, A., Wolter, F., and Zakharyaschev, M., Many-dimensional modal logics: Theory and applications, Studies in Logic, vol. 148, Elsevier, 2003.Google Scholar
[9] Gabbay, D. and Shehtman, V., Undecidability of modal and intermediate first-order logics with two individual variables, The Journal of Symbolic Logic, vol. 58 (1993), pp. 800–823.Google Scholar
[10] Grädel, E. and Otto, M., On logics with two variables, Theoretical Computer Science, vol. 224 (1999), pp. 73–113.CrossRefGoogle Scholar
[11] Halmos, P., Algebraic logic, IV, Transactions of the American Mathematical Society, vol. 86 (1957), pp. 1–27.Google Scholar
[12] Henkin, H., Monk, J. D., and Tarski, A., Cylindric algebras, Part II, Studies in Logic, vol. 115, North-Holland, 1985.Google Scholar
[13] Hirsch, R. and Hodkinson, I., Representability is not decidable for finite relation algebras, Transactions of the American Mathematical Society, vol. 353 (2001), pp. 1403–1425.Google Scholar
[14] Hirsch, R., Hodkinson, I., and Kurucz, A., On modal logics between K × K × K and S5 × S5 × S5 , The Journal of Symbolic Logic, vol. 67 (2002), pp. 221–234.Google Scholar
[15] Hodkinson, I., Wolter, F., and Zakharyaschev, M., Decidable fragments of first-order temporal logics, Annals of Pure and Applied Logic, vol. 106 (2000), pp. 85–134.Google Scholar
[16] Hodkinson, I., Wolter, F., and Zakharyaschev, M., Decidable and undecidable fragments of first-order branching temporal logics, Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science (LICS'02), IEEE, 2002, pp. 393–402.Google Scholar
[17] Hughes, G. and Cresswell, M., A new introduction to modal logic, Routledge, 1996.Google Scholar
[18] Kripke, S., The undecidability of monadic modal quantification theory, Zeitschrift für Matematische Logik und Grundlagen der Mathematik, vol. 8 (1962), pp. 113–116.CrossRefGoogle Scholar
[19] Kripke, S., Semantical analysis of intuitionistic logic I, Formal systems and recursive functions (Crossley, J. and Dummett, M., editors), North-Holland, 1965, pp. 92–130.CrossRefGoogle Scholar
[20] Kripke, S., Semantical analysis of intuitionistic logic II, Unpublished, 1968.Google Scholar
[21] Maslov, S., Mints, G., and Orevkov, V., Unsolvability in the constructive predicate calculus of certain classes of formulas containing only monadic predicate variables, Soviet Mathematics Doklady, vol. 6 (1965), pp. 918–920.Google Scholar
[22] Mints, G., Some calculi of modal logic, Trudy Matematicheskogo Instituta imeni V.A. Steklova, vol. 98 (1968), pp. 88–111.Google Scholar
[23] Mortimer, M., On languages with two variables, Zeitschrift für Mathematische Logik und Grundlagen der Mathematik, vol. 21 (1975), pp. 135–140.Google Scholar
[24] Ono, H., On some intuitionistic modal logics, Publications of the Research Institute for Mathematical Science, Kyoto University, vol. 13 (1977), pp. 55–67.Google Scholar
[25] Rasiowa, H. and Sikorski, R., The mathematics of metamathematics, Polish Scientific Publishers, 1963.Google Scholar
[26] Surányi, J., Zur Reduktion des Entscheidungsproblems des logischen Funktionenkalküls, Mathematikai és Fizikai Lapok, vol. 50 (1943), pp. 51–74.Google Scholar
[27] Troelstra, A., Principles of intuitionism, Lecture Notes in Mathematics, vol. 95, Springer-Verlag, 1969.Google Scholar
[28] van Dalen, D., Intuitionistic logic, Handbook of philosophical logic (Gabbay, D. and Guenthner, F., editors), vol. 5, Kluwer, second ed., 2002, pp. 1–114.Google Scholar
[29] Wolter, F. and Zakharyaschev, M., Decidable fragments of first-order modal logics, The Journal of Symbolic Logic, vol. 66 (2001), pp. 1415–1438.CrossRefGoogle Scholar