Видеотека
RUS  ENG    ЖУРНАЛЫ   ПЕРСОНАЛИИ   ОРГАНИЗАЦИИ   КОНФЕРЕНЦИИ   СЕМИНАРЫ   ВИДЕОТЕКА   ПАКЕТ AMSBIB  
Видеотека
Архив
Популярное видео

Поиск
RSS
Новые поступления






Традиционная зимняя сессия МИАН–ПОМИ, посвященная теме «Математическая логика»
24 декабря 2018 г. 15:25–16:00, г. Москва, МИАН, ул. Губкина, д. 8, конференц-зал, 9 этаж
 


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

Ф. Н. Пахомов

Математический институт им. В.А. Стеклова Российской академии наук, г. Москва
Видеозаписи:
MP4 835.0 Mb
MP4 379.2 Mb

Количество просмотров:
Эта страница:135
Видеофайлы:21

Ф. Н. Пахомов
Фотогалерея


Видео не загружается в Ваш браузер:
  1. Проверьте с Вашим администратором, что из Вашей сети разрешены исходящие соединения на порт 8080
  2. Сообщите администратору портала о данной ошибке

Аннотация: Для каждой рекурсивно аксиоматизируемой первопорядковой теории $T$ рассмотрим формулу $Con(T)\upharpoonright x$, являющуюся формализацией в языке арифметики первого порядка $\mathsf{PA}$ утверждения "нет доказательств противоречия из аксиом $T$, состоящего менее чем из $x$ символов". В силу второй теореме Гёделя о неполноте, ни одна непротиворечивая теория $T$ не может доказать $\forall x\; Con(T)\upharpoonright x$. Как было установлено П. Пудлаком, для большого класса теорий $T$ длина кратчайшего доказательства $Con(T)\upharpoonright n$ в самой теории $T$ ограничена полиномом от $n$. Пудлак высказал гипотезу о том, что ни для какой теории $T$ нет полиномиальной серии доказательств утверждений $Con(T+Con(T))\upharpoonright n$. Тем не менее, мы доказываем, что для $\mathsf{PA}$ имеется полиномиальная серия доказательств утверждений $Con(\mathsf{PA}+Con^{\star}(\mathsf{PA}))\upharpoonright n$. Здесь $Con^{\star}(\mathsf{PA})$ - это так называемое утверждение о "медленной" непротиворечивости $\mathsf{PA}$, введенное C.-Д. Фридманом, М. Ратьеном и А. Вайерманом. Отметим, что $Con^{\star}(\mathsf{PA})$ может пониматься как обычная формализация непротиворечивости $\mathsf{PA}$, возникающая из нестандартного выбора машины Тьюринга перечисляющей аксиомы $\mathsf{PA}$. Доклад основан на совместной статье с Антоном Фройндом.

ОТПРАВИТЬ: VKontakte.ru FaceBook Twitter Mail.ru Livejournal Memori.ru
 
Обратная связь:
 Пользовательское соглашение  Регистрация посетителей портала  Логотипы © Математический институт им. В. А. Стеклова РАН, 2021