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

Для каждой рекурсивно аксиоматизируемой первопорядковой теории $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}$. Доклад основан на совместной статье с Антоном Фройндом.