Алгоритмическая проблема финитарного семантического следования пропозициональных формул I: контекст и постановка задачи

##plugins.themes.bootstrap3.article.main##

A.V. Chagrov

Abstract

Different (nonequivalent) notions of the semantic consequence of propositional formulas, among which the notion of finitary semanic consequence is selected, are described. Some statements which are based on certain folklore proofs have been given. The example is Kuznetsov’s observation which allows to prove the following unexpected statement: there is not an algorithm which, given a recursive (that is, decidable) set of propositional formulas, recognizes the presence at least of one invalid formula. But the aim of discussion in this paper is the setting of an algorithmic problem of finitary semantic consequence for various nonclassical propositional logics, such as modal, intuitionistic ones, Visser’s logics. Solutions of these problems will be given in the following papers of series.

##plugins.generic.usageStats.downloads##

##plugins.generic.usageStats.noStats##

##plugins.themes.bootstrap3.article.details##

Section
Papers

References

Kuznetsov A.V. On superintuitionistic logics // Proc. Internat. Congr. of Mathematicians. Vancouver, 1974. Montreal, 1975. P. 243-249. (Русский перевод: Кузнецов А.В. О суперинтуиционистских логиках // Математические исследования (Кишинёв). 1975. Т. 10. N 2. С. 150-158.)
Кузнецов А.В., Герчиу В.Я. О суперинтуиционистских логиках и финитной аппроксимируемости // Доклады АН СССР. 1970. Т. 195. N 5. С. 1029-1032. (Исправление опечаток: там же. 1971. Т. 199. N 6. С. 1222.)
Мальцев А.И. Алгоритмы и рекурсивные функции. М.: Наука, 1986.
Расёва Е. и Сикорский Р. Математика метаматематики. М.: Наука, 1972.
Рыбаков В.В. Некомпактные расширения логики S4 // Алгебра и логика. 1977. Т. 16. N 4. С. 472-490.
Соболев С. К. О конечномерных суперинтуиционистских логиках // Известия АН СССР, Сер. матем. 1977. Т. 41. N 5. С. 963-986.
Трахтенброт Б.А. Невозможность алгорифма для проблемы разрешимости на конечных классах // Доклады АН СССР. 1950. Т. 70. С. 569-572.
Фейс Р. Модальная логика. М.: Наука, 1974.
Чагров А.В. Простые примеры неразрешимых рекурсивно аксиоматизируемых финитно аппроксимируемых эквациональных логик // Восьмая Всесоюзная конференция по математической логике. М., 1986. С. 206.
Чагров А.В. Многообразия логических матриц // Алгебра и логика. 1985. Т. 24. N 4. С. 426-489. (Англ, перев.: Algebra and Logic, Т. 24. С. 278-325.)
Чагров А.В. Нижняя оценка мощности аппроксимирующих шкал Крипке // Логические методы построения эффективных алгоритмов. Калинин: КГУ, 1986. С. 96-125.
Чагров А.В. Неразрешимые свойства суперинтуиционистских логик // Математические вопросы кибернетики. Вып. 5: Сб. статей под ред. С.В. Яблонского. М.: Физматлит, 1994. С. 62-108.
Шехтман В.Б. О неполных логиках высказываний // Доклады АН СССР. 1977. Т. 235. N 3. С. 542-545.
Шехтман В.Б. Неразрешимое суперинтуиционистское исчисление // Доклады АН СССР. 1978. Т. 240. N 3. С. 549-553.
Шехтман В.Б. О счётной аппроксимируемости суперинтуиционистских и модальных логик // Исследования по неклассическим логикам и формальным системам. М.: ВИНИТИ, 1983. С. 287-299.
Шехтман В.Б. Неразрешимые исчисления высказываний // Неклассические логики и их применение. Вопросы кибернетики. М.: Наука, 1982. С. 74-115.
Янков В.А. Построение последовательности сильно независимых суперинтуиционистских исчислений // Доклады АН СССР. 1968. Т. 181. N 1. С. 33-34.
Chagrov A.V., Chagrova L.A. Algorithmic problems concerning first-order definability of modal formulas on the class of all finite frames // Studia Logica. 1995. V. 55. No. 3. P. 421-448.
Chagrov A., Zakharyaschev M. Modal Logic. Oxford University Press, 1997.
Craig W. On axiomatizability within a system // The Journal of Symbolic Logic. V. 18. P. 30-32.
Fine K. Logics containing К4, Part I. // The Journal of Symbolic Logic. 1974. V. 39. No 1. P. 31-42.
Hosoi T. and Ono H. Intermediate propositional logics (A survey) // J. Tsuda College. 1973. V. 5. P. 67-82.
Isard S. A finitely axiomatizable undecidable extension of К // Theoria. 1977. V. 43. P. 195-202.
Kracht M. Modal Logics that Need Very Large Frames // Notre Dame Journal of Formal Logic. 1999. V. 40. No. 2. P. 141-173.
Kripke S. Semantical analysis of modal logic, Part I // Zeitschrift fur Mathematische Logik und Grundlagen der Mathematik. 1963. Bd. 9. S. 67-96.
Makinson D. Some embedding theorems for modal logic // Notre Dame Journal of Formal Logic. 1971. V. 12. P. 252-254.
Thomason S.K. Noncompactness in propositional modal logic // The Journal of Symbolic Logic. 1972. V. 37. P. 716-720.
Thomason S.K. The logical consequence relation of propositional tense logic // Zeitschrift fur Mathematische Logik und Grundlagen der Mathematik. 1975. Bd. 21. S. 29-40.
Thomason S.K. Reduction of tense logic to modal logic, I // The Journal of Symbolic Logic. 1974. V. 39. P. 549-551.
Thomason S.K. Reduction of tense logic to modal logic II // Theoria. 1975. V. 41. P. 154-169.
Thomason S.K. Reduction of second-order logic to modal logic // Zeitschrift fur Mathematische Logik und Grundlagen der Mathematik. 1975. Bd. 21. S. 107-114.
Urquhart A. Decidability and the finite model property // J. Phil. Log. 1981. V. 10. No. 3. P. 367-370.
J.A.F.K. van Benthem. Notes on modal definability // Notre Dame Journal of Formal Logic. 1989. V. 39. P. 20-39.
Visser A. A propositional logic with explicit fixed points // Studia Logica. 1981. V. 40. P. 155-175.