The predicate version of the joint logic of problems and propositions

A. A. Onoprienko

Sbornik. Mathematics, Tome 213 (2022) no. 7, pp. 981-1003

Résumé

We consider the joint logic of problems and propositions $\mathrm{QHC}$ introduced by Melikhov. We construct Kripke models with audit worlds for this logic and prove the soundness and completeness of $\mathrm{QHC}$ with respect to this type of model. The conservativity of the logic $\mathrm{QHC}$ over the intuitionistic modal logic $\mathrm{QH4}$, which coincides with the ‘lax logic’ $\mathrm{QLL}^+$, is established. We construct Kripke models with audit worlds for the logic $\mathrm{QH4}$ and prove the corresponding soundness and completeness theorems. We also prove that the logics $\mathrm{QHC}$ and $\mathrm{QH4}$ have the disjunction and existence properties. Bibliography: 33 titles.

Détail

Keywords: nonclassical 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. A. Onoprienko, “Kripke semantics for the logic of problems and propositions”, Mat. Sb., 211:5 (2020), 98–125 ; English transl. in Sb. Math., 211:5 (2020), 709–732 | DOI | MR | Zbl | DOI

[4] S. Artemov and T. Protopopescu, “Intuitionistic epistemic logic”, Rev. Symb. Log., 9:2 (2016), 266–298 ; (2014), arXiv: 1406.1582v2 | DOI | MR | Zbl

[5] A. N. Kolmogorov, Selected works, Nauka, Moscow, 1985, 470 pp. ; English transl., v. I, Math. Appl. (Soviet Ser.), 25, Mathematics and mechanics, Kluwer Acad. Publ., Dordrecht, 1991, xix+551 pp. | MR | Zbl | MR | Zbl

[6] A. N. Kolmogorov, “On the tertium non datur principle”, Mat. Sb., 32:4 (1925), 646–667 (Russian) | Zbl

[7] A. Heyting, Intuitionism. An introduction, Stud. Logic Found. Math., North-Holland Publishing Co., Amsterdam, 1956, viii+133 pp. | MR | Zbl

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

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

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

[11] 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

[12] 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

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

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

[15] S. N. Artemov, “Kolmogorov and Gödel's approach to intuitionistic logic: current developments”, Uspekhi Mat. Nauk, 59:2(356) (2004), 9–36 ; English transl. in Russian Math. Surveys, 59:2 (2004), 203–229 | DOI | MR | Zbl | DOI

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

[17] K. Gödel, “Vortrag bei Zilsel (*1938a)”, Collected works, v. III, ed. S. Feferman, Oxford Univ. Press, New York–Oxford, 1995, 86–113 | MR | Zbl

[18] S. C. Kleene, “On the interpretation of intuitionistic number theory”, J. Symbolic Logic, 10:4 (1945), 109–124 | DOI | MR | Zbl

[19] Ju. T. Medvedev, “Finite problems”, Dokl. Akad. Nauk SSSR, 142:5 (1962), 1015–1018 ; English transl. in Soviet Math. Dokl., 3 (1962), 227–230 | MR | Zbl

[20] A. S. Troelstra and D. van Dalen, Constructivism in mathematics, v. I, II, Stud. Logic Found. Math., 121, 123, North-Holland Publishing Co., Amsterdam, 1988, xx+342 and XIV pp., xviii and 345–880 and LII pp. | MR | MR | Zbl

[21] Junhua Yu, “Self-referentiality of Brouwer-Heyting-Kolmogorov semantics”, Ann. Pure Appl. Logic, 165:1 (2014), 371–388 | DOI | MR | Zbl

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

[23] R. I. Goldblatt, “Grothendieck topology as geometric modality”, Z. Math. Logik Grundlagen Math., 27:31–35 (1981), 495–529 | DOI | MR | Zbl

[24] A. G. Dragalin, Mathematical intuitionism. Introduction to proof theory, Nauka, Moscow, 1979, 256 pp. ; English transl., Transl. Math. Monogr., 67, Amer. Math. Soc., Providence, RI, 1988, x+228 pp. | MR | Zbl | DOI | MR | Zbl

[25] M. Fairtlough and M. Mendler, “Propositional lax logic”, Inform. and Comput., 137:1 (1997), 1–33 | DOI | MR | Zbl

[26] M. V. H. Fairtlough and M. Walton, Quantified lax logic, Tech. rep. CS-97-11, Univ. of Sheffield, 1997, 79 pp.

[27] P. Aczel, “The Russell-Prawitz modality”, Math. Structures Comput. Sci., 11:4 (2001), 541–554 | DOI | MR | Zbl

[28] R. Goldblatt, “Cover semantics for quantified lax logic”, J. Logic Comput., 21:6 (2011), 1035–1063 | DOI | MR | Zbl

[29] D. Rogozin, “Categorical and algebraic aspects of the intuitionistic modal logic $\mathrm{IEL}^-$ and its predicate extensions”, J. Logic Comput., 31:1 (2021), 347–374 | DOI | MR | Zbl

[30] A. Tarski, “What is elementary geometry?”, The axiomatic method (Univ. of Calif., Berkeley 1957/1958), Stud. Logic Found. Math., 27, North-Holland Publishing Co., Amsterdam, 1959, 16–29 | DOI | MR | Zbl

[31] M. Beeson, “A constructive version of Tarski's geometry”, Ann. Pure Appl. Logic, 166:11 (2015), 1199–1273 | DOI | MR | Zbl

[32] V. E. Plisko and V. Kh. Khakhanyan, Intutionistic logic, Publishing house of the Faculty of Mechanics and Mathematics at Moscow State University, Moscow, 2009, 159 pp. (Russian)

[33] Youan Su and K. Sano, “First-order intuitionistic epistemic logic”, Logic, rationality, and interaction, Lecture Notes in Comput. Sci., 11813, Springer, Berlin, 2019, 326–339 | DOI | MR | Zbl