The predicate version of the 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

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.

About the authors

Anastasiya Aleksandrovna Onoprienko

Steklov Mathematical Institute of Russian Academy of Sciences

Email: ansidiana@yandex.ru
without scientific degree, no status

References

  1. S. A. Melikhov, A Galois connection between classical and intuitionistic logics. I: Syntax, 2013–2017
  2. S. A. Melikhov, A Galois connection between classical and intuitionistic logics. II: Semantics, 2015–2018
  3. А. А. Оноприенко, “Семантика типа Крипке для пропозициональной логики задач и высказываний”, Матем. сб., 211:5 (2020), 98–125
  4. S. Artemov, T. Protopopescu, “Intuitionistic epistemic logic”, Rev. Symb. Log., 9:2 (2016), 266–298
  5. А. Н. Колмогоров, Избранные труды. Математика и механика, Наука, М., 1985, 470 с.
  6. А. Н. Колмогоров, “О принципе tertium non datur”, Матем. сб., 32:4 (1925), 646–667
  7. А. Гейтинг, Интуиционизм. Введение, Мир, М., 1965, 200 с.
  8. S. A. Melikhov, Mathematical semantics of intuitionistic logic, 2015–2017
  9. A. S. Troelstra, “Aspects of constructive mathematics”, Handbook of mathematical logic, Stud. Logic Found. Math., 90, North-Holland, Amsterdam, 1977, 973–1052
  10. A. S. Troelstra, H. Schwichtenberg, Basic proof theory, Cambridge Tracts Theoret. Comput. Sci., 43, Cambridge Univ. Press, Cambridge, 1996, xii+343 pp.
  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
  12. P. Martin-Löf, Intuitionistic type theory, Notes by G. Sambin, Stud. Proof Theory Lecture Notes, 1, Bibliopolis, Naples, 1984, iv+91 pp.
  13. С. К. Клини, Введение в метаматематику, ИЛ, М., 1957, 526 с.
  14. S. N. Artemov, “Explicit provability and constructive semantics”, Bull. Symbolic Logic, 7:1 (2001), 1–36
  15. С. Н. Артeмов, “Подход Колмогорова и Гeделя к интуиционистской логике и работы последнего десятилетия в этом направлении”, УМН, 59:2(356) (2004), 9–36
  16. K. Gödel, “Eine Interpretation des intuitionistischen Aussagenkalküls”, Ergebnisse math. Kolloquium Wien, 4 (1933), 39–40
  17. K. Gödel, “Vortrag bei Zilsel (*1938a)”, Collected works, v. III, ed. S. Feferman, Oxford Univ. Press, New York–Oxford, 1995, 86–113
  18. S. C. Kleene, “On the interpretation of intuitionistic number theory”, J. Symbolic Logic, 10:4 (1945), 109–124
  19. Ю. Т. Медведев, “Финитные задачи”, Докл. АН СССР, 142:5 (1962), 1015–1018
  20. A. S. Troelstra, 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.
  21. Junhua Yu, “Self-referentiality of Brouwer–Heyting–Kolmogorov semantics”, Ann. Pure Appl. Logic, 165:1 (2014), 371–388
  22. S. Artemov, T. Protopopescu, “Intuitionistic epistemic logic”, Rev. Symb. Log., 9:2 (2016), 266–298
  23. R. I. Goldblatt, “Grothendieck topology as geometric modality”, Z. Math. Logik Grundlagen Math., 27:31-35 (1981), 495–529
  24. А. Г. Драгалин, Математический интуиционизм. Введение в теорию доказательств, Наука, М., 1979, 256 с.
  25. M. Fairtlough, M. Mendler, “Propositional lax logic”, Inform. and Comput., 137:1 (1997), 1–33
  26. M. V. H. Fairtlough, 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
  28. R. Goldblatt, “Cover semantics for quantified lax logic”, J. Logic Comput., 21:6 (2011), 1035–1063
  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
  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
  31. M. Beeson, “A constructive version of Tarski's geometry”, Ann. Pure Appl. Logic, 166:11 (2015), 1199–1273
  32. В. Е. Плиско, В. Х. Хаханян, Интуиционистская логика, Изд-во при мех.-матем. ф-те МГУ, М., 2009, 159 с.
  33. Youan Su, K. Sano, “First-order intuitionistic epistemic logic”, Logic, rationality, and interaction, Lecture Notes in Comput. Sci., 11813, Springer, Berlin, 2019, 326–339

Supplementary files

Supplementary Files
Action
1. JATS XML
Download

Copyright (c) 2022 Onoprienko A.A.

Согласие на обработку персональных данных

 

Используя сайт https://journals.rcsi.science, я (далее – «Пользователь» или «Субъект персональных данных») даю согласие на обработку персональных данных на этом сайте (текст Согласия) и на обработку персональных данных с помощью сервиса «Яндекс.Метрика» (текст Согласия).