Abstract
We prove that the positive fragment of first-order intuitionistic logic in the language with two individual variables and a single monadic predicate letter, without functional symbols, constants, and equality, is undecidable. This holds true regardless of whether we consider semantics with expanding or constant domains. We then generalise this result to intervals \([\mathbf{QBL}, \mathbf{QKC}]\) and \([\mathbf{QBL}, \mathbf{QFL}]\), where QKC is the logic of the weak law of the excluded middle and QBL and QFL are first-order counterparts of Visser’s basic and formal logics, respectively. We also show that, for most “natural” first-order modal logics, the two-variable fragment with a single monadic predicate letter, without functional symbols, constants, and equality, is undecidable, regardless of whether we consider semantics with expanding or constant domains. These include all sublogics of QKTB, QGL, and QGrz—among them, QK, QT, QKB, QD, QK4, and QS4.
This is a preview of subscription content, log in via an institution to check access.
Similar content being viewed by others
Change history
23 December 2021
A Correction to this paper has been published: https://doi.org/10.1007/s11225-021-09977-8
References
Behmann, H., Beiträige zür algebra der logik, inbesondere zum entscheidungsproblem, Mathematische Annalen 86:163–229, 1922.
Berger, R., The Undecidability of the Domino Problem, volume 66 of Memoirs of AMS. AMS, 1966.
Börger, E., E. Grädel, and Y. Gurevich, The Classical Decision Problem. Springer, 1997.
Chagrov, A., and M. Rybakov, How many variables does one need to prove PSPACE-hardness of modal logics? in Advances in Modal Logic, vol. 4, 2003, pp. 71–82.
Chagrov, A., and M. Zakharyaschev, Modal Logic. Oxford University Press, 1997.
Church, A., A note on the “Entscheidungsproblem”, The Journal of Symbolic Logic 1:40–41, 1936.
Feys, R., Modal Logics. E. Nauwelaerts, 1965.
Gabbay, D. M., Semantical Investigations in Heyting’s Intuitionistic Logic. D. Reidel, 1981.
Gödel, K., Zum Entsheidungsproblem des logischen Funktionenkalküls, Monatschefte für Mathematische Physika 40:433–443, 1933.
Grädel, E., P. G. Kolaitis, and M. Y. Vardi, On the decision problem for two-variable first-order logic, Bulletin of Symbolic Logic 3(1):53–69, 1997.
Halpern, J. Y., The effect of bounding the number of primitive propositions and the depth of nesting on the complexity of modal logic, Artificial Intelligence 75(2):361–372, 1995.
Kontchakov, R., A. Kurucz, and M. Zakharyaschev, Undecidability of first-order intuitionistic and modal logics with two variables, Bulletin of Symbolic Logic 11(3):428–438, 2005.
Kremer, P., On the complexity of propositional quantification in intuitionistic logic, The Journal of Symbolic Logic 62(2):529–544, 1997.
Kripke, S., The undecidability of monadic modal quantification theory, Zeitschrift für Matematische Logik und Grundlagen der Mathematik 8:113–116, 1962.
Maslov, S., G. Mints, and V. Orevkov, Unsolvability in the constructive predicate calculus of certain classes of formulas containing only monadic predicate variables, Soviet Mathematics Doklady 6:918–920, 1965.
Montagna, F., The predicate modal logic of provability, Notre Dame Journal of Formal Logic 25(2):179–189, 1984.
Mortimer, M., On languages with two variables, Zeitschrift für Mathematische Logik und Grundlagen der Mathematik, 1975, pp. 135–140.
Nerode, A., and R. A. Shore, Second order logic and first order theories of reducibility ordering, in J. Barwise, H. J. Keisler, and K. Kunen, (eds.), The Kleene Symposium, North-Holland, 1980, pp. 181–200.
Nishimura, I., On formulas of one variable in intuitionistic propositional calculus, The Journal of Symbolic Logic 25(4):327–331, 1960.
Rybakov, M., Enumerability of modal predicate logics and the condition of non-existence of infinite ascending chains, Logicheskiye Issledovaniya 8:155–167, 2001.
Rybakov, M., Complexity of intuitionistic propositional logic and its fragments, Journal of Applied Non-Classical Logics 18(2–3):267–292, 2008.
Rybakov, M., and D. Shkatov, Complexity and expressivity of propositional dynamic logics with finitely many variables. Logic Journal of the IGPL, 10.1093/jigpal/jzy014.
Rybakov, M., and D. Shkatov, Complexity of finite-variable fragments of propositional modal logics of symmetric frames. Logic Journal of the IGPL, 10.1093/jigpal/jzy018.
Surányi, J., Zur Reduktion des Entscheidungsproblems des logischen Funktioskalküls, Mathematikai és Fizikai Lapok 50:51–74, 1943.
Visser, A., A propositional logic with explicit fixed points, Studia Logica 40:155–175, 1981.
Wolter, F., and M. Zakharyaschev, Decidable fragments of first-order modal logics, The Journal of Symbolic Logic 66:1415–1438, 2001.
Acknowledgements
We are grateful to the anonymous referees for comments that helped to significantly improve the presentation of the paper.
Funding
This work has been supported by Russian Foundation for Basic Research, Projects 17-03-00818 and 18-011-00869.
Author information
Authors and Affiliations
Corresponding author
Additional information
Presented by Yde Venema
Rights and permissions
About this article
Cite this article
Rybakov, M., Shkatov, D. Undecidability of First-Order Modal and Intuitionistic Logics with Two Variables and One Monadic Predicate Letter. Stud Logica 107, 695–717 (2019). https://doi.org/10.1007/s11225-018-9815-7
Received:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s11225-018-9815-7