Совместная логика задач и высказываний

Обложка

Цитировать

Полный текст

Открытый доступ Открытый доступ
Доступ закрыт Доступ предоставлен
Доступ закрыт Только для подписчиков

Аннотация

В комментарии 1985г. к своему собранию сочинений А. Н. Колмогоров сообщил, что его статья К толкованию интуиционистской логики 1932 г. “писалась в надежде на то, что логика решения задач [т.е. интуиционистская логика] сделается со временем постоянным разделом курса логики. Предполагалось создание единого логического аппарата, имеющего дело с объектами двух типов — высказываниями и задачами”. Ниже построена подобная формальная система, а также её предикатная версия QHC, являющаяся консервативным расширением как интуиционисткого предикатного исчисления QH, так и классического предикатного исчисления QC. Аксиоматика логики QHC является результатом одновременной формализации двух известных альтернативных толкований интуиционистской логики: 1) задачной интерпретации Колмогорова (с известными уточнениями Гейтинга и Крайзеля) и 2) доказательной интерпретации Орлова и Гейтинга, прояснённой и расширенной Гёделем.

Об авторах

С. А. Мелихов

Математический институт им. В.А. Стеклова РАН

Автор, ответственный за переписку.
Email: melikhov@mi-ras.ru
Россия, Москва

Список литературы

  1. Melikhov S.A. A Galois connection between classical and intuitionistic logics. I: Syntax. arXiv:1312.2575v5.
  2. Melikhov S.A. A Galois connection between classical and intuitionistic logics. II: Semantics. arXiv:1504.03379v5.
  3. Paulson L.C. The foundation of a generic theorem prover // J. Automat. Reason. 1989. V. 5 P. 363–397.
  4. Melikhov S.A. Mathematical semantics of intuitionistic logic. arXiv:1504.03380v3.
  5. Колмогоров A.H. К работам no интуиционистской логике. Избранные труды // Математика и механика. М.: Наука, 1985. С. 393; English transl., On the papers on intuitionistic logic. Selected Works of A.N. Kolmogorov // Mathematics and its Applications. 1991. V. 1. P. 451–452. Kluwer, Dordrecht: Soviet Series. V. 25.
  6. Kolmogoroff A. Zur Deutung der intuitionistischen Logik // Math. 1932. Z. 35. S. 58–65. Рус. пер. Колмогоров А.Н. К толкованию интуиционистской логики. Избранные труды // Математика и механика. М.: Наука, 1985. С. 142–148; English transl. Kolmogorov A.N. On the interpretation of intuitionistic logic. Selected works // Mathematics and its Applications. 1991. V. 1. P. 151–158. Kluwer, Dordrecht: Soviet Series. V. 25.
  7. Godcl K. Lecture at ZilseTs. Collected Works. V. Iii. New York: The Clarendon Press, Oxford Univ. Press, 1995. P. 86-113.
  8. Artcmov S.N. Explicit provability and constructive semantics // Bull. Symbolic Logic. 2001. N 7. P. 1–36.
  9. Fairtlough M. and Walton M. Quantified lax logic. Tech, report CS-97-11, Univ, of Sheffield (1997).https://citeseerx.ist.psu.edu/viewdoc/versions? https://doi.org/10.1.1.50.69
  10. Aczcl P. The Russell-Prawitz modality // Math. Structures Comput. Sci. 2001. N 11. P. 541–554.
  11. Artcmov S.N. and Protopopcscu T. Intuitionistic epistemic logic (early preprint version).arXiv: 1406.1582v2 (нс путать c v4 и опубликованной версией).
  12. Curry H.В. A Theory of Formal Deducibility // Notre Dame Math. Lectures. V. 6. Notre Dame, IN: Univ. of Notre Dame, 1950.
  13. Оноприенко А.А. Семантика типа Крипке для пропозициональной логики задач и высказываний // Матем. сб. 2020. Т. 211. № 5. С. 98–125; English transl., Onoprienko A.A. Kripke type semantics for a logic of problems and propositions // Sbornik Math. 2020. V. 211. P. 709–732.
  14. Оноприенко А.А. Предикатный вариант совместной логики задач и высказываний // Матем. сб. 2022. Т. 213. № 7. С. 7, 97–120; English transl., Onoprienko A.A. The predicate version of the joint logic of problems and propositions. Sbornik Math. 2022. V. 213. P. 981–1003.
  15. Оноприенко А.А. Топологические модели пропозициональной логики задач и высказываний // Вестник Москов. унив. 2022. № 5. С. 25–30; English transl., Onoprienko A.A. Topological models of the propositional logic of problems and propositions // Moscow Univ. Math. Bull. 2022. N 77. P. 236–241.
  16. Fitting M. An embedding of classical logic in S4 // J. Symbolic Logic. 1970. N 35. P. 529–534.
  17. Mclikhov S.A. A Galois connection between classical and intuitionistic logics. III: Geometry. Preliminary version: §1A and §§3-4 in arXiv: 1504.03379v2.

Дополнительные файлы

Доп. файлы
Действие
1. JATS XML
Скачать

© Российская академия наук, 2024