  RUS  ENG ЖУРНАЛЫ   ПЕРСОНАЛИИ   ОРГАНИЗАЦИИ   КОНФЕРЕНЦИИ   СЕМИНАРЫ   ВИДЕОТЕКА   ПАКЕТ AMSBIB  Ближайшие семинары Календарь семинаров Список семинаров Архив по годам Регистрация семинара Поиск RSS Ближайшие семинары

Семинар отдела математической логики «Теория доказательств»
23 марта 2020 г. 18:30, г. Москва, МИАН, ауд. 530 On the logical complexity of cyclic arithmetic

Anupam Das

University of Birmingham
 Видеозаписи: MP4 2,270.4 Mb MP4 1,271.5 Mb

 Количество просмотров: Эта страница: 46 Видеофайлы: 21   Видео не загружается в Ваш браузер: Активируйте JavaScript в Вашем браузере Установите Adobe Flash Player Проверьте с Вашим администратором, что из Вашей сети разрешены исходящие соединения на порт 8080 Сообщите администратору портала о данной ошибке

Аннотация: We study the logical complexity of proofs in cyclic arithmetic ($\mathsf{CA}$), as introduced in Simpson '17, in terms of quantifier alternations of formulae occurring. Writing C\Sigma_n for (the logical consequences of) cyclic proofs containing only $\Sigma_n$ formulae, our main result is that $I\Sigma_{n+1}$ and $C\Sigma_n$ prove the same $\Pi_{n+1}$ theorems, for all $n\geq 0$. Furthermore, due to the 'uniformity' of our method, we also show that $\mathsf{CA}$ and Peano Arithmetic ($\mathsf{PA}$) proofs of the same theorem differ only exponentially in size. The inclusion $I\Sigma_{n+1} \subseteq C\Sigma_n$ is obtained by proof theoretic techniques, relying on normal forms and structural manipulations of $\mathsf{PA}$ proofs. It improves upon the natural result that $I\Sigma_n$ is contained in $C\Sigma_n$. The converse inclusion, $C\Sigma_n \subseteq I\Sigma_{n+1}$, is obtained by calibrating the approach of Simpson '17 with recent results on the reverse mathematics of Büchi's theorem in Kołodziejczyk, Michalewski, Pradic & Skrzypczak '16 (KMPS'16), and specialising to the case of cyclic proofs. These results improve upon the bounds on proof complexity and logical complexity implicit in Simpson '17 and also an alternative approach due to Berardi & Tatsuta '17. The uniformity of our method also allows us to recover a metamathematical account of fragments of $\mathsf{CA}$; in particular we show that, for $n\geq 0$, the consistency of $C\Sigma_n$ is provable in $I\Sigma_{n+2}$ but not $I\Sigma_{n+1}$. As a result, we show that certain versions of McNaughton's theorem (the determinisation of $\omega$-word automata) are not provable in $\mathsf{RCA}_0$, partially resolving an open problem from KMPS '16.

Язык доклада: английский

 ОТПРАВИТЬ:       Обратная связь: math-net2020_04 [at] mi-ras ru Пользовательское соглашение Регистрация Логотипы © Математический институт им. В. А. Стеклова РАН, 2020