Неразрешимость модальных логик одноместного предиката
Main Article Content
Аннотация
Рассматриваются модальные предикатные логики в языке, содержащем только одноместные предикатные буквы. Показано, что любая логика, содержащаяся в ${\bf QS5}, {\bf QGLLin}$ или ${\bf QGrz.3}$ является алгоритмически неразрешимой в языке с одной одноместной предикатной буквой (как при наличии, так и при отсутствии в логике формулы Баркан). Также показано, что логики конечных шкал Крипке (как с расширяющимися, так и с постоянными областями) для ${\bf QK}, {\bf QT}, {\bf QD}, {\bf QK4}, {\bf QS4}, {\bf QS5}, {\bf QGL}, {\bf QGrz}$ и многих других не являются рекурсивно перечислимыми в языке с одной одноместной предикатной буквой. Тем не менее табличные логики и логики шкал Крипке с ограничением на число миров, достижимых из произвольного мира, разрешимы в языке с бесконечным множеством одноместных предикатных букв.
DOI: 10.21146/2074-1472-2017-23-2-60-75
DOI: 10.21146/2074-1472-2017-23-2-60-75
Скачивания
Данные скачивания пока не доступны.
Article Details
Как цитировать
РыбаковM. Н. Неразрешимость модальных логик одноместного предиката // Логические исследования / Logical Investigations. 2017. Т. 23. № 2. C. 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.
Мендельсон Э. Введение в математическую логику. М.: Наука, 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.