- Код статьи
- 10.31857/S2686954324020077-1
- DOI
- 10.31857/S2686954324020077
- Тип публикации
- Статья
- Статус публикации
- Опубликовано
- Авторы
- Том/ Выпуск
- Том 516 / Номер выпуска 1
- Страницы
- 38-50
- Аннотация
- В комментарии 1985г. к своему собранию сочинений А. Н. Колмогоров сообщил, что его статья К толкованию интуиционистской логики 1932 г. “писалась в надежде на то, что логика решения задач [т.е. интуиционистская логика] сделается со временем постоянным разделом курса логики. Предполагалось создание единого логического аппарата, имеющего дело с объектами двух типов — высказываниями и задачами”. Ниже построена подобная формальная система, а также её предикатная версия QHC, являющаяся консервативным расширением как интуиционисткого предикатного исчисления QH, так и классического предикатного исчисления QC. Аксиоматика логики QHC является результатом одновременной формализации двух известных альтернативных толкований интуиционистской логики: 1) задачной интерпретации Колмогорова (с известными уточнениями Гейтинга и Крайзеля) и 2) доказательной интерпретации Орлова и Гейтинга, прояснённой и расширенной Гёделем.
- Ключевые слова
- интуиционистская логика BHK-интерпретация формальная металогика
- Дата публикации
- 15.10.2024
- Год выхода
- 2024
- Всего подписок
- 0
- Всего просмотров
- 45
Библиография
- 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.
