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

(по совместной работе с Данияром Шамкановым и Иваном Смирновым)
Мы формулируем альтернативную циклическую систему доказательств для арифметики Пеано, которая, возможно, проще существующих и адаптирована как для анализа формальных доказательств, так и для автоматизации поиска индуктивных доказательств. Мы показываем, как различные традиционные подсистемы арифметики Пеано, определяемые ограниченными формами индукции, могут быть представлены в качестве фрагментов предлагаемой системы.