Kripke semantics for the logic of problems and propositions

A. A. Onoprienko

Sbornik. Mathematics, Tome 211 (2020) no. 5, pp. 709-732

Résumé

In this paper we study the propositional fragment $\mathrm{HC}$ of the joint logic of problems and propositions introduced by Melikhov. We provide Kripke semantics for this logic and show that $\mathrm{HC}$ is complete with respect to those models and has the finite model property. We consider examples of the use of $\mathrm{HC}$-models usage. In particular, we prove that $\mathrm{HC}$ is a conservative extension of the logic $\mathrm{H4}$. We also show that the logic $\mathrm{HC}$ is complete with respect to Kripke frames with sets of audit worlds introduced by Artemov and Protopopescu (who called them audit set models). Bibliography: 31 titles.

Détail

Keywords: non-classical logics, Kripke semantics.

Bibliographie

[1] S. A. Melikhov, A Galois connection between classical and intuitionistic logics. I: Syntax, 2013–2017, arXiv: 1312.2575

[2] S. A. Melikhov, A Galois connection between classical and intuitionistic logics. II: Semantics, 2015–2018, arXiv: 1504.03379

[3] A. N. Kolmogorov, Selected works of A. N. Kolmogorov, v. I, Math. Appl. (Soviet Ser.), 25, Mathematics and mechanics, Kluwer Acad. Publ, Dordrecht, 1991, xix+551 pp. | MR | MR | Zbl | Zbl

[4] A. N. Kolmogorov, “O printsipe tertium non datur”, Matem. sb., 32 (1925), 646–667 | Zbl

[5] A. Heyting, Intuitionism. An introduction, North-Holland Publishing Co., Amsterdam, 1956, viii+133 pp. | MR | Zbl | Zbl

[6] S. A. Melikhov, Mathematical semantics of intuitionistic logic, 2015–2017, arXiv: 1504.03380

[7] A. S. Troelstra, “Aspects of constructive mathematics”, Handbook of mathematical logic, Stud. Logic Found. Math., 90, North-Holland, Amsterdam, 1977, 973–1052 | DOI | MR

[8] A. S. Troelstra, H. Schwichtenberg, Basic proof theory, Cambridge Tracts Theoret. Comput. Sci., 43, Cambridge Univ. Press, Cambridge, 1996, xii+343 pp. | MR | Zbl

[9] G. Kreisel, “Perspectives in the philosophy of pure mathematics”, Logic, methodology and philosophy of science (Bucharest, 1971), v. IV, Stud. Logic Found. Math., 74, North-Holland, Amsterdam, 1973, 255–277 | DOI | MR | Zbl

[10] P. Martin-Löf, Intuitionistic type theory, Notes by G. Sambin, Stud. Proof Theory Lecture Notes, 1, Bibliopolis, Naples, 1984, iv+91 pp. | MR | Zbl

[11] S. C. Kleene, Introduction to metamathematics, D. Van Nostrand Co., Inc., New York, NY, 1952, x+550 pp. | MR | MR | Zbl

[12] S. N. Artemov, “Explicit provability and constructive semantics”, Bull. Symbolic Logic, 7:1 (2001), 1–36 | DOI | MR | Zbl

[13] S. N. Artemov, “Kolmogorov and Gödel's approach to intuitionistic logic: current developments”, Russian Math. Surveys, 59:2 (2004), 203–229 | DOI | DOI | MR | Zbl

[14] K. Gödel, “Eine Interpretation des intuitionistischen Aussagenkalküls”, Ergebnisse math. Kolloquium Wien, 4 (1933), 39–40 | Zbl

[15] J.-Y. Girard, “Linear logic”, Theoret. Comput. Sci., 50:1 (1987), 1–101 | DOI | MR | Zbl

[16] J.-Y. Girard, “On the unity of logic”, Ann. Pure Appl. Logic, 59:3 (1993), 201–217 | DOI | MR | Zbl

[17] G. Japaridze, On resources and tasks, 2013, arXiv: 1312.3372

[18] G. Japaridze, “The logic of tasks”, Ann. Pure Appl. Logic, 117:1-3 (2002), 261–293 | DOI | MR | Zbl

[19] G. Japaridze, “Intuitionistic computability logic”, Acta Cybernet., 18:1 (2007), 77–113 | MR | Zbl

[20] G. Japaridze, “The intuitionistic fragment of computability logic at the propositional level”, Ann. Pure Appl. Logic, 147:3 (2007), 187–227 | DOI | MR | Zbl

[21] Chuck Liang, D. Miller, “Kripke semantics and proof systems for combining intuitionistic logic and classical logic”, Ann. Pure Appl. Logic, 164:2 (2013), 86–111 | DOI | MR | Zbl

[22] Chuck Liang, D. Miller, “Unifying classical and intuitionistic logics for computational control”, 2013 28th annual ACM/IEEE symposium on logic in computer science (LICS 2013), IEEE Computer Soc., Los Alamitos, CA, 2013, 283–292 | DOI | MR | Zbl

[23] M. Bílková, G. Greco, A. Palmigiano, A. Tzimoulis, N. Wijnberg, “The logic of resources and capabilities”, Rev. Symb. Log., 11:2 (2018), 371–410 | DOI | MR | Zbl

[24] S. Artemov, T. Protopopescu, Intuitionistic epistemic logic, 2014, arXiv: 1406.1582v2

[25] K. Gödel, “Lecture at Zilsel's”, Collected works, v. III, Clarendon Press, Oxford Univ. Press, New York, 1995, 86–113 | MR | Zbl

[26] H. Rasiowa, R. Sikorski, The mathematics of metamathematics, Monogr. Mat., 41, Państwowe Wydawnictwo Naukowe, Warsaw, 1963, 522 pp. | MR | MR | Zbl | Zbl

[27] V. E. Plisko, V. Kh. Khakhanyan, Intuitsionistskaya logika, MGU, mekh.-matem. f-t, M., 2009, 159 pp. http://lpcs.math.msu.su/~plisko/intlog.pdf

[28] N. K. Vereschagin, A. Shen, Lektsii po matematicheskoi logike i teorii algoritmov, Chast 2. Yazyki i ischisleniya, 4-e izd., ispr., MTsNMO, M., 2012, 240 pp. https://mccme.ru/free-books/shen/shen-logic-part2-2.pdf

[29] T. Protopopescu, “Intuitionistic epistemology and modal logics of verification”, Logics, rationality and interaction (LORI 2015), Lecture Notes in Comput. Sci., 9394, Springer, Heidelberg, 2015, 295–307 | DOI | MR | Zbl

[30] S. Artemov, T. Protopopescu, “Intuitionistic epistemic logic”, Rev. Symb. Log., 9:2 (2016), 266–298 | MR | Zbl

[31] A. Chagrov, M. Zakharyaschev, Modal logic, Oxford Logic Guides, 35, Oxford Univ. Press, New York, 1997, xvi+605 pp. | MR | Zbl