Циклические доказательства (Лев Беклемишев)

Математический семинар ФКН В последние годы в математической логике получили распространение формальные системы, основанные на циклических и нефундированных доказательствах. Они оказались удобными для аксиоматизации логических языков с разнообразными формами индукции, рекурсии или неподвижных точек. Они применяются как для анализа свойств таких языков, так и для задач автоматизации поиска доказательств. В циклическом доказательстве логические правила вывода существенно не отличаются от обычных, однако помимо аксиом имеются дополнительные гипотезы, которые обосновываются ссылками на идентичные утверждения, получаемые в выводе *позже* этих гипотез. Для того, чтобы такие доказательства не приводили к порочному кругу, на ссылки накладываются дополнительные условия, и правильная формулировка таких условий представляет собой в каждом конкретном случае нетривиальную задачу. Мы расскажем о совместной работе с Д. С. Шамкановым и И. Н. Смирновым, в которой разработаны новые циклические системы для классической арифметики Пеано и ее основных фрагментов. Выступает профессор Лев Беклемишев, ВШЭ, Математический институт им. В. А. Стеклова РАН. https://youtu.be/z6sSnW-aMa8 https://www.youtube.com/playlist?list=PLEqoHzpnmTfBJfTzg4_63Ckra7_kVOCuz Математический семинар ФКН: https://cs.hse.ru/seminatfkn/ ФКН: https://cs.hse.ru Подписывайтесь на нас: 📍 https://vk.com/cshse 📍 https://t.me/fcs_hse