A joint logic of problems and propositions

Cover Page

Cite item

Full Text

Open Access Open Access
Restricted Access Access granted
Restricted Access Subscription Access

Abstract

In a 1985 commentary to his collected works, Kolmogorov informed the reader that his 1932 paper On the interpretation of intuitionistic logic “was written in hope that with time, the logic of solution of problems [i.e., intuitionistic logic] will become a permanent part of a [standard] course of logic. A unified logical apparatus was intended to be created, which would deal with objects of two types – propositions and problems.” We construct such a formal system as well as its predicate version, QHC, which is a conservative extension of both the intuitionistic predicate calculus QH and the classical predicate calculus QC. The axioms of QHC are obtained as a result of a simultaneous formalization of two well-known alternative explanations of intiuitionistic logic: 1) Kolmogorov's problem interpretation (with familiar refinements by Heyting and Kreisel) and 2) the proof interpretation by Orlov and Heyting, as clarified and extended by Gödel.

About the authors

S. A. Melikhov

Steklov Mathematical Institute of Russian Academy of Sciences

Author for correspondence.
Email: melikhov@mi-ras.ru
Russian Federation, Moscow

References

  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.

Supplementary files

Supplementary Files
Action
1. JATS XML
Download

Copyright (c) 2024 Russian Academy of Sciences