О циклических доказательствах в классической логике первого порядка с индуктивными определениями

В статье 2011 г. А. Симпсон и Дж. Брозерстон рассмотрели две дедуктивные системы для классической логики первого порядка с индуктивными определениями, а именно исчисление секвенций с индуктивными определениями в стиле Мартин-Лёфа LKID и секвенциальное исчисление CLKIDω, формулировка которого не содержит правил индукции, но допускает циклические доказательства. Указав, что все секвенции, выводимые в LKID, также выводимы в CLKIDω, А. Симпсон и Дж. Брозерстон поставили вопрос: верно ли обратное утверждение? Как показали К. Берарди и М. Тацута, в общем случае обратное утверждение неверно, однако для систем над арифметикой Пеано LKID + PA и CLKIDω + PA обратное включение имеет место. Настоящий доклад будет посвящен разбору статьи К. Берарди и М. Тацуты "Equivalence of Inductive Definitions and Cyclic Proofs under Arithmetic", в которой доказана эквивалентность систем LKID + PA и CLKIDω + PA.