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

Циклический вывод отличается от классического возможностью наличия циклов в "графе вывода", который для классического вывода является деревом. А. Симпсон [1] (и независимо С. Берарди и М. Татсута) доказал эквивалентность некоторой формальной системы арифметики 1-го порядка, основанной на циклических выводах, и арифметики Пеано.
В докладе мы расскажем о новой системе циклических выводов для арифметики 1-го порядка, предложенной в работе [2]. Глобальные ограничения корректности на выводы в этой системе выглядят проще, чем в предшествующих: задача проверки корректности вывода в ней лежит в классе P, а не только в PSPACE. Мы также определим некоторые фрагменты этой системы, основанные на ограничении сложности формул, входящих в вывод, эквивалентные известным фрагментам арифметики Пеано: $I \Sigma_n$ и $I \Sigma_n^R$.
Список литературы: [1] A. Simpson. “Cyclic arithmetic is equivalent to Peano arithmetic”. In: FOSSACS 2017, Proceedings. pp. 283–300. [2] L. Beklemishev, D. Shamkanov and I. Smirnov. "Fragments of arithmetic and cyclic proofs". arxiv.org/abs/2502.06639