Математический семинар ФКН «Циклические доказательства»
Беклемишев Лев Дмитриевич
Базовая кафедра Математического института им. В.А. Стеклова РАН: Профессор
21 февраля 2025 в 18:10
Докладчик: Лев Беклемишев, Факультет математики НИУ ВШЭ
Тема: Циклические доказательства
Аннотация:
В последние годы в математической логике получили распространение формальные системы, основанные на циклических и нефундированных доказательствах. Они оказались удобными для аксиоматизации логических языков с разнообразными формами индукции, рекурсии или неподвижных точек. Они применяются как для анализа свойств таких языков, так и для задач автоматизации поиска доказательств.
В циклическом доказательстве логические правила вывода существенно не отличаются от обычных, однако помимо аксиом имеются дополнительные гипотезы, которые обосновываются ссылками на идентичные утверждения, получаемые в выводе *позже* этих гипотез. Для того, чтобы такие доказательства не приводили к порочному кругу, на ссылки накладываются дополнительные условия, и правильная формулировка таких условий представляет собой в каждом конкретном случае нетривиальную задачу.
Мы расскажем о совместной работе с Д.С. Шамкановым и И.Н. Смирновым, в которой разработаны новые циклические системы для классической арифметики Пеано и ее основных фрагментов.
Место проведения: Покровский бульвар 11, аудитория R205.