Фрагменты арифметики и циклические выводы

Обложка
  • Авторы: Беклемишев Л.Д.1, Шамканов Д.С.1, Смирнов И.Н.1,2,3
  • Учреждения:
    1. Математический институт им. В. А. Стеклова Российской академии наук, г. Москва
    2. Институт системного программирования им. В. П. Иванникова Российской академии наук, г. Москва
    3. Московский физико-технический институт (национальный исследовательский университет), г. Долгопрудный, Московская обл.
  • Выпуск: Том 216, № 10 (2025)
  • Страницы: 3-28
  • Раздел: Статьи
  • URL: https://journal-vniispk.ru/0368-8666/article/view/331243
  • DOI: https://doi.org/10.4213/sm10276
  • ID: 331243

Цитировать

Полный текст

Открытый доступ Открытый доступ
Доступ закрыт Доступ предоставлен
Доступ закрыт Только для подписчиков

Аннотация

Мы определяем новую циклическую систему доказательств для арифметики Пеано, которая проще существующих и может быть адаптирована как для анализа формальных выводов, так и для автоматизации поиска индуктивных доказательств. Мы показываем, как различные известные подсистемы арифметики Пеано, определяемые ограниченными формами индукции, представляются в качестве фрагментов предлагаемой системы.
Библиография: 45 названий.

Об авторах

Лев Дмитриевич Беклемишев

Математический институт им. В. А. Стеклова Российской академии наук, г. Москва

Email: bekl@mi-ras.ru
ORCID iD: 0000-0002-2949-0600
Scopus Author ID: 6602096489
ResearcherId: F-7814-2013
доктор физико-математических наук, без звания

Данияр Салкарбекович Шамканов

Математический институт им. В. А. Стеклова Российской академии наук, г. Москва

Email: daniyar.shamkanov@gmail.com
ORCID iD: 0000-0002-1421-9965
SPIN-код: 2216-1138
Scopus Author ID: 38562114000
ResearcherId: P-5451-2016
кандидат физико-математических наук, без звания

Иван Николаевич Смирнов

Математический институт им. В. А. Стеклова Российской академии наук, г. Москва; Институт системного программирования им. В. П. Иванникова Российской академии наук, г. Москва; Московский физико-технический институт (национальный исследовательский университет), г. Долгопрудный, Московская обл.

Email: smirnov.in@phystech.su
без ученой степени

Список литературы

  1. B. Afshari, G. E. Leigh, “Lyndon interpolation for modal $mu$-calculus”, Language, logic, and computation, Lecture Notes in Comput. Sci., 13206, FoLLI Publ. Log. Lang. Inf., Springer, Cham, 2022, 197–213
  2. B. Afshari, G. E. Leigh, G. Menendez Turata, “Uniform interpolation from cyclic proofs: the case of modal mu-calculus”, Automated reasoning with analytic tableaux and related methods, Lecture Notes in Comput. Sci., 12842, Lecture Notes in Artificial Intelligence, Springer, Cham, 2021, 335–353
  3. D. Baelde, A. Doumane, A. Saurin, “Infinitary proof theory: the multiplicative additive case”, Computer science logic 2016, LIPIcs. Leibniz Int. Proc. Inform., 62, Schloss Dagstuhl. Leibniz-Zentrum für Informatik, Wadern, 2016, 42, 17 pp.
  4. L. D. Beklemishev, “Induction rules, reflection principles, and provably recursive functions”, Ann. Pure Appl. Logic, 85:3 (1997), 193–242
  5. L. D. Beklemishev, “Proof-theoretic analysis by iterated reflection”, Arch. Math. Logic, 42:6 (2003), 515–552
  6. S. Berardi, M. Tatsuta, “Equivalence of inductive definitions and cyclic proofs under arithmetic”, 2017 32nd annual {ACM/IEEE} symposium on logic in computer science (LICS) (Reykjavik, 2017), IEEE Press, Piscataway, NJ, 2017, 54, 12 pp.
  7. S. Berardi, M. Tatsuta, “Classical system of Martin-Lof's inductive definitions is not equivalent to cyclic proofs”, Log. Methods Comput. Sci., 15:3 (2019), 10, 25 pp.
  8. J. Brotherston, “Cyclic proofs for first-order logic with inductive definitions”, Automated reasoning with analytic tableaux and related methods, Lecture Notes in Comput. Sci., 3702, Lecture Notes in Artificial Intelligence, Springer-Verlag, Berlin, 2005, 78–92
  9. J. Brotherston, R. Bornat, C. Calcagno, “Cyclic proofs of program termination in separation logic”, POPL'08: Proceedings of the 35th annual ACM SIGPLAN–SIGACT symposium on principles of programming languages (San Francisco, CA, 2008), ACM, New York, 2008, 101–112
  10. J. Brotherston, N. Gorogiannis, R. L. Petersen, “A generic cyclic theorem prover”, Programming languages and systems, Lecture Notes in Comput. Sci., 7705, Springer, Berlin–Heidelberg, 2012, 350–367
  11. J. Brotherston, A. Simpson, “Sequent calculi for induction and infinite descent”, J. Logic Comput., 21:6 (2011), 1177–1216
  12. G. Curzi, A. Das, “Computational expressivity of (circular) proofs with fixed points”, 2023 38th annual ACM/IEEE symposium on logic in computer science (LICS) (Boston, MA, 2023), IEEE Comput. Soc. Press, Los Alamitos, CA, 2023, 1–13
  13. M. Dam, D. Gurov, “$mu$-calculus with explicit points and approximations”, J. Logic Comput., 12:2 (2002), 255–269
  14. A. Das, “On the logical complexity of cyclic arithmetic”, Log. Methods Comput. Sci., 16:1 (2020), 1, 39 pp.
  15. A. Das, A circular version of Gödel's T and its abstraction complexity
  16. A. Das, D. Pous, “Non-wellfounded proof theory for $(Kleene+action)(algebras+lattices)$”, Computer science logic 2018, LIPIcs. Leibniz Int. Proc. Inform., 119, Schloss Dagstuhl. Leibniz-Zent. Inform., Wadern, 2018, 19, 18 pp.
  17. Ch. Dax, M. Hofmann, M. Lange, “A proof system for the linear time $mu$-calculus”, FSTTCS 2006: Foundations of software technology and theoretical computer science, Lecture Notes in Comput. Sci., 4337, Springer, Berlin, 2006, 273–284
  18. J. Fortier, L. Santocanale, “Cuts for circular proofs: semantics and cut-elimination”, Computer science logic 2013, LIPIcs. Leibniz Int. Proc. Inform., 23, Schloss Dagstuhl. Leibniz-Zent. Inform., Wadern, 2013, 248–262
  19. P. Hajek, P. Pudlak, Metamathematics of first-order arithmetic, Perspect. Math. Logic, Springer-Verlag, Berlin, 1993, xiv+460 pp.
  20. S. Hetzl, J. Vierling, “Unprovability results for clause set cycles”, Theoret. Comput. Sci., 935 (2022), 21–46
  21. E. Jeřabek, “Induction rules in bounded arithmetic”, Arch. Math. Logic, 59:3-4 (2020), 461–501
  22. N. Jungteerapanich, “A tableau system for the modal $mu$-calculus”, Automated reasoning with analytic tableaux and related methods, Lecture Notes in Comput. Sci., 5607, Lecture Notes in Artificial Intelligence, Springer, Berlin, 2009, 220–234
  23. R. Kaye, J. Paris, C. Dimitracopoulos, “On parameter free induction schemas”, J. Symb. Log., 53:4 (1988), 1082–1097
  24. D. Kimura, K. Nakazawa, T. Terauchi, H. Unno, “Failure of cut-elimination in cyclic proofs of separation logic”, Computer Software, 37:1 (2020), 39–52
  25. M. Kori, T. Tsukada, N. Kobayashi, “A cyclic proof system for $operatorname{HFL}_mathbb{N}$”, Computer science logic 2021, LIPIcs. Leibniz Int. Proc. Inform., 183, 2021, 29, 22 pp.
  26. S. Negri, J. von Plato, Structural proof theory, Appendix C by A. Ranta, Cambridge Univ. Press, Cambridge, 2001, xviii+257 pp.
  27. S. Negri, J. von Plato, “Cut elimination in the presence of axioms”, Bull. Symb. Log., 4:4 (1998), 418–435
  28. D. Niwinski, I. Walukiewicz, “Games for the $mu$-calculus”, Theoret. Comput. Sci., 163:1-2 (1996), 99–116
  29. R. Nollet, A. Saurin, C. Tasson, “Local validity for circular proofs in linear logic with fixed points”, Computer science logic 2018, LIPIcs. Leibniz Int. Proc. Inform., 119, Schloss Dagstuhl. Leibniz-Zent. Inform., Wadern, 2018, 35, 23 pp.
  30. Y. Oda, J. Brotherston, M. Tatsuta, “The failure of cut-elimination in cyclic proof for first-order logic with inductive definitions”, J. Logic Comput., 35:2 (2025), exad068, 28 pp.
  31. C. Parsons, “Hierarchies of primitive recursive functions”, Z. Math. Logik Grundlagen Math., 14:21-24 (1968), 357–376
  32. L. Santocanale, “A calculus of circular proofs and its categorical semantics”, Foundations of software science and computation structures, Lecture Notes in Comput. Sci., 2303, Springer-Verlag, Berlin, 2002, 357–371
  33. A. Saurin, “A linear perspective on cut-elimination for non-wellfounded sequent calculi with least and greatest fixed-points”, Automated reasoning with analytic tableaux and related methods, Lecture Notes in Comput. Sci., 14278, Lecture Notes in Artificial Intelligence, Springer, Cham, 2023, 203–222
  34. H. Schwichtenberg, “Proof theory: some applications of cut-elimination”, Handbook of mathematical logic, Stud. Logic Found. Math., 90, North Holland Publishing Co., Amsterdam, 1977, 867–895
  35. D. Shamkanov, “Global neighbourhood completeness of the provability logic GLP”, Advances in modal logic, v. 13, College Publications, London, 2020, 581–596
  36. D. Shamkanov, “On structural proof theory of the modal logic $mathbf K^+$ extended with infinitary derivations”, Log. J. IGPL, 33:3 (2025), jzae121, 46 pp.
  37. D. S. Shamkanov, “A realization theorem for the modal logic of transitive closure $mathsf{K}^+$”, Изв. РАН. Сер. матем., 89:2 (2025), 189–212
  38. B. Sierra-Miranda, Th. Studer, L. Zenger, “Coalgebraic proof translations for non-wellfounded proofs”, Advances in modal logic, v. 15, College Publications, London, 2024, 527–548
  39. A. Simpson, “Cyclic arithmetic is equivalent to {Peano} arithmetic”, Foundations of software science and computation structures, Lecture Notes in Comput. Sci., 10203, Springer-Verlag, Berlin, 2017, 283–300
  40. I. N. Smirnov, Automated derivation in cyclic arithmetic, Thesis, Moscow Institute of Physics and Technology, 2023
  41. C. Stirling, “A tableau proof system with names for modal mu-calculus”, HOWARD-60. A festschrift on the occasion of Howard Barringer's 60th birthday, EPiC Ser. Comput., 42, EasyChair, 2014, 306–318
  42. Th. Studer, “On the proof theory of the modal mu-calculus”, Studia Logica, 89:3 (2008), 343–363
  43. A. J. Wilkie, J. B. Paris, “On the scheme of induction for bounded arithmetic formulas”, Ann. Pure Appl. Logic, 35:3 (1987), 261–302

Дополнительные файлы

Доп. файлы
Действие
1. JATS XML
Скачать

© Беклемишев Л.Д., Шамканов Д.С., Смирнов И.Н., 2025

Согласие на обработку персональных данных с помощью сервиса «Яндекс.Метрика»

1. Я (далее – «Пользователь» или «Субъект персональных данных»), осуществляя использование сайта https://journals.rcsi.science/ (далее – «Сайт»), подтверждая свою полную дееспособность даю согласие на обработку персональных данных с использованием средств автоматизации Оператору - федеральному государственному бюджетному учреждению «Российский центр научной информации» (РЦНИ), далее – «Оператор», расположенному по адресу: 119991, г. Москва, Ленинский просп., д.32А, со следующими условиями.

2. Категории обрабатываемых данных: файлы «cookies» (куки-файлы). Файлы «cookie» – это небольшой текстовый файл, который веб-сервер может хранить в браузере Пользователя. Данные файлы веб-сервер загружает на устройство Пользователя при посещении им Сайта. При каждом следующем посещении Пользователем Сайта «cookie» файлы отправляются на Сайт Оператора. Данные файлы позволяют Сайту распознавать устройство Пользователя. Содержимое такого файла может как относиться, так и не относиться к персональным данным, в зависимости от того, содержит ли такой файл персональные данные или содержит обезличенные технические данные.

3. Цель обработки персональных данных: анализ пользовательской активности с помощью сервиса «Яндекс.Метрика».

4. Категории субъектов персональных данных: все Пользователи Сайта, которые дали согласие на обработку файлов «cookie».

5. Способы обработки: сбор, запись, систематизация, накопление, хранение, уточнение (обновление, изменение), извлечение, использование, передача (доступ, предоставление), блокирование, удаление, уничтожение персональных данных.

6. Срок обработки и хранения: до получения от Субъекта персональных данных требования о прекращении обработки/отзыва согласия.

7. Способ отзыва: заявление об отзыве в письменном виде путём его направления на адрес электронной почты Оператора: info@rcsi.science или путем письменного обращения по юридическому адресу: 119991, г. Москва, Ленинский просп., д.32А

8. Субъект персональных данных вправе запретить своему оборудованию прием этих данных или ограничить прием этих данных. При отказе от получения таких данных или при ограничении приема данных некоторые функции Сайта могут работать некорректно. Субъект персональных данных обязуется сам настроить свое оборудование таким способом, чтобы оно обеспечивало адекватный его желаниям режим работы и уровень защиты данных файлов «cookie», Оператор не предоставляет технологических и правовых консультаций на темы подобного характера.

9. Порядок уничтожения персональных данных при достижении цели их обработки или при наступлении иных законных оснований определяется Оператором в соответствии с законодательством Российской Федерации.

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