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.
This is a preview of subscription content, log in via an institution to check access.
Similar content being viewed by others
Notes
These play the role axiom schemata, but technically they are neither schemata nor individual axioms.
A closely related, but more complex logic was studied by Artё-mov [8].
REFERENCES
S. A. Melikhov, “A Galois connection between classical and intuitionistic logics: I. Syntax,” arXiv:1312.2575v5 (2022).
S. A. Melikhov, “A Galois connection between classical and intuitionistic logics: II. Semantics,” arXiv:1504.03379v5 (2022).
L. C. Paulson, “The foundation of a generic theorem prover,” J. Autom. Reason. 5, 363–397 (1989).
S. A. Melikhov, “Mathematical semantics of intuitionistic logic,” arXiv:1504.03380v3 (2017).
A. N. Kolmogorov, “On the papers on intuitionistic logic,” in Selected Works of A. N. Kolmogorov, Vol. 1: Mathematics and Its Applications (Soviet Series) (Kluwer, Dordrecht, 1991), Vol. 25, pp. 451–452.
A. N. Kolmogorov, “On the interpretation of intuitionistic logic,” in Selected Works of A. N. Kolmogorov, Vol. 1: Mathematics and Its Applications (Soviet Series) (Kluwer, Dordrecht, 1991), Vol. 25, pp. 151–158.
K. Gödel, Lecture at Zilsel’s: Collected Works (Clarendon, New York, 1995), Vol. 3, pp. 86–113.
S. N. Artёmov, “Explicit provability and constructive semantics,” Bull. Symb. Logic 7, 1–36 (2001).
M. Fairtlough and M. Walton, “Quantified lax logic,” Tech. Report CS-97-11 (Univ. of Sheffield, Sheffield, 1997). https://citeseerx.ist.psu.edu/viewdoc/versions?doi=10.1.1.50.69
P. Aczel, “The Russell–Prawitz modality,” Math. Struct. Comput. Sci. 11, 541–554 (2001).
S. N. Artёmov and T. Protopopescu, “Intuitio-nistic epistemic logic (early preprint version),” arXiv:1406.1582v2 (2014) (not to be confused with v4 or the published version).
H. B. Curry, A Theory of Formal Deducibility, Notre Dame Math. Lectures (Univ. of Notre Dame, Notre Dame, IN, 1950), Vol. 6.
A. A. Onoprienko, “Kripke type semantics for a logic of problems and propositions,” Sb. Math. 211, 709–732 (2020).
A. A. Onoprienko, “The predicate version of the joint logic of problems and propositions,” Sb. Math. 213 (7), 981–1003 (2022).
A. A. Onoprienko, “Topological models of propositional logic of problems and propositions,” Moscow Univ. Math. Bull. 77, 236–241 (2022).
M. Fitting, “An embedding of classical logic in S4,” J. Symb. Logic 35, 529–534 (1970).
S. A. Melikhov, “A Galois connection between classical and intuitionistic logics: III. Geometry,” Preliminary version: Sects. 1A, 3, 4, arXiv:1504.03379v2.
ACKNOWLEDGMENTS
I would like to thank A. Bauer, L. Beklemishev, M. Bezem, G. Dowek, M. Jibladze, A. Onoprienko, A. L. Semenov, D. Shamkanov, V. Shehtman and A. Shen’ for valuable discussions and useful comments and the two referees of Doklady for reasonable remarks. The present note owes its appearance to the requests from A.L. Semenov and reminders from L. Beklemishev and S. Kuznetsov.
Funding
This work was supported by ongoing institutional funding. No additional grants to carry out or direct this particular research were obtained.
Author information
Authors and Affiliations
Corresponding author
Ethics declarations
The author of this work declares that he has no conflicts of interest.
Additional information
Publisher’s Note.
Pleiades Publishing remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.
Rights and permissions
About this article
Cite this article
Melikhov, S.A. A Joint Logic of Problems and Propositions. Dokl. Math. 109, 130–139 (2024). https://doi.org/10.1134/S1064562424701916
Received:
Revised:
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1134/S1064562424701916