Undecidability of Modal Logics of Unary Predicate


M. N. Rybakov


We consider first-order modal logics with unary predicate letters only. We show that any sublogic of ${\bf QS5}, {\bf QGLLin}$ or ${\bf QGrz.3}$ is undecidable in the language with just one unary predicate letter (with or without Barcan formula). We also show that logics of finite Kripke models (with expanding or constant domains) for ${\bf QK}, {\bf QT}, {\bf QD}, {\bf QK4}, {\bf QS4}, {\bf QS5}, {\bf QGL}, {\bf QGrz}$ , and some others are not recursively enumerable in the language with one unary letter. Nevertheless tabular logics and mlogics of Kripke frames with restrictions on the number of worlds accessible from any world are decidable in the language with infinitely many unary predicate letters.
DOI: 10.21146/2074-1472-2017-23-2-60-75






Булос Дж., Джеффри Р. Вычислимость и логика. М.: Мир, 1994.
Мендельсон Э. Введение в математическую логику. М.: Наука, 1984.
Маслов С.Ю., Минц Г.Е., Оревков В.П. Неразрешимость в конструктивном исчислении предикатов некоторых классов формул, содержащих только одноместные предикатные переменные // Докл. АН СССР. Т. 163. № 2. 1965. С. 295–297.
Рыбаков М.Н. Об алгоритмической выразительности модального языка с одной лишь одноместной предикатной буквой // Логические исследования. Вып. 9. М.: Наука. 2002. С.179–201.
Трахтенброт Б.А. Невозможность алгорифма для проблемы разрешимости на конечных классах // Докл. АН СССР. Т. 70. № 4. 1950. С. 569–572.
Фейс Р. Модальная логика. М.: Наука. 1974.
Chagrov A.V., Zakharyaschev M.V. Modal Logic. Oxford University Press, 1997.
Church A. An Unsolvable Problem of Elementary Number Theory // American Journal of Mathematics. 1936. Vol. 58. P. 345–363.
Church A. A note on the Entscheidungsproblem // Journal of Symbolic Logic. 1936. Vol. 1. P. 40–41.
Gabbay D.M. Semantical investigations in Heyting’s intuitionistic logic // Synthese Library. Vol. 148. Reidel; Dordrecht: 1989.
Gabbay D.M., Shehtman V.B. Undecidability of Modal and Intermediate First-Order Logics with Two Individual Variables // The Journal of Symbolic Logic. Sept. 1993. Vol. 58. № 3. P. 800–823.
Kremer P. On the Complexity of Propositional Quantification in Intuitionistic Logic // The Journal of Symbolic Logic. 1997. Vol. 62. № 2. P. 529–544.
Kripke S. The Undecidability of Monadic Modal Quantificational Theory // Zeitschrift f_ur Mathematische Logik und Grundlagen der Mathematik. 1962. Vol. 8. P. 113–116.
Motohashi N. A Decision Method for a Set of First Order Classical Formulas and its Applications to Decision Problem for Non-Classical Propositional Logics // J. Math. Soc. Japan. 1990. Vol. 42. № 1. P. 127–132.
Nerode A., Shore R. Second Order Logic and First Order Theories of Reducibility Orderings // The Kleene Symposium, J. Barwise, H. J. Keisler, K. Kuner, eds., North-Holland, Amsterdam. 1980. P. 181–200.
Turing A.M. On Computable Numbers with an Application to the Entscheidungsproblem // Proc. London Maths. Soc. 1936. ser. 2. Vol. 42. P. 230–265.
Turing A.M. On Computable Numbers, with an Application to the Entscheidungsproblem. A Correction // Proc. London Maths. Soc. 1937. ser. 2. Vol. 43. P. 544–546.