Fragments of arithmetic and cyclic proofs

Мұқаба

Дәйексөз келтіру

Толық мәтін

Ашық рұқсат Ашық рұқсат
Рұқсат жабық Рұқсат берілді
Рұқсат жабық Тек жазылушылар үшін

Аннотация

We define a new cyclic proof system for Peano arithmetic that that is simpler than existing one and can be adapted for an analysis of formal inference and for automatizing inductive proof search. We show how various traditional subsystems of Peano arithmetic defined by restricted forms of induction can be represented as fragments of the system proposed.

Негізгі сөздер

Авторлар туралы

Lev Beklemishev

Steklov Mathematical Institute of Russian Academy of Sciences, Moscow, Russia

Email: bekl@mi-ras.ru
ORCID iD: 0000-0002-2949-0600
Scopus Author ID: 6602096489
ResearcherId: F-7814-2013
Doctor of physico-mathematical sciences, no status

Daniyar Shamkanov

Steklov Mathematical Institute of Russian Academy of Sciences, Moscow, Russia

Email: daniyar.shamkanov@gmail.com
ORCID iD: 0000-0002-1421-9965
SPIN-код: 2216-1138
Scopus Author ID: 38562114000
ResearcherId: P-5451-2016
Candidate of physico-mathematical sciences, no status

Ivan Smirnov

Steklov Mathematical Institute of Russian Academy of Sciences, Moscow, Russia; Ivannikov Institute for System Programming of the Russian Academy of Science, Moscow, Russia; Moscow Institute of Physics and Technology, Dolgoprudny, Moscow Region, Russia

Email: smirnov.in@phystech.su
without scientific degree

Әдебиет тізімі

  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
Жүктеу

© Beklemishev L.D., Shamkanov D.S., Smirnov I.N., 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») на элемент с текстом «Принять и продолжить».