Цепи из утверждений о медленной непротиворечивости

Пусть $\mathtt{f}(x)$ - всюду определенная быстро-растущая рекурсивная функция. Тогда с n можно связать альтернативный, "замедленный", вариант аксиоматизации арифметики Пеано $\mathsf{PA}$, мы обозначаем его $\mathsf{PA}\upharpoonright\mathtt{f}$; в $\mathsf{PA}\upharpoonright \mathtt{f}$ аксиома $\mathsf{I\Sigma_n}$ появляется лишь на шаге $\mathtt{f}(n)$. С этой функцией также естественным образом связывается утверждение о медленной непротиворечивости $\mathsf{Con}(\mathsf{PA}\upharpoonright\mathtt{f})$. Несложно показать, что если в $\mathsf{PA}$ доказуемо, что $\mathtt{f}(x)$ тотальна, то $\mathsf{PA}$ доказывает эквивалентность обычной непротиворечивости $\mathsf{Con}(\mathsf{PA})$ и медленной непротиворечивости $\mathsf{Con}(\mathsf{PA}\upharpoonright \mathtt{f})$. Как оказывается, если $\mathtt{f}(x)$ не является $\mathsf{PA}$-доказуемо тотальной и для нее выполнены некоторые естественные условия, то
$$\mathsf{PA}\subsetneq \mathsf{PA}+\mathsf{Con}(\mathsf{PA}\upharpoonright \mathtt{f})\subsetneq \mathsf{PA}+\mathsf{Con}(\mathsf{PA}).$$

Недавно М. Ратьен построил цепочку рекурсивных функций $\mathsf{f}_{\alpha}(x)$, для ординалов $\alpha$ меньших ординала Бахмана-Говарда (большой счетный рекурсивный ординал существенно превосходящий $\varepsilon_0$; и являющийся теоретико-доказательственным ординалом теории множеств Крипке-Платека с аксиомой бесконечности $\mathsf{KP+Infinity}$). Для этой цепочки Ратьен показал, что соответствующие утверждения о медленной непротиворечивости $\mathsf{PA}$ образуют убывающую цепь:
$$\mathsf{PA}+\mathsf{Con}(\mathsf{PA}\upharpoonright \mathtt{f}_\beta)\nvdash \mathsf{Con}(\mathsf{PA}\upharpoonright f_\alpha),\;для\;\alpha<\beta.$$

В докладе будет рассказано об обобщение этого результата. Мы формулируем условия на пару рекурсивных функций $\mathtt{f}(x)$ и $\mathtt{g}(x)$, которые гарантируют, что $\mathsf{PA}+\mathsf{Con}(\mathsf{PA}\upharpoonright\mathtt{f})\nvdash\mathsf{Con}(\mathsf{PA}\upharpoonright \mathtt{g})$. Мы используем эти условия для построения естественного примера цепочки рекурсивных функций с порядковым типом $\mathbb{Q}$, дающей цепочку утверждений о медленной непротиворечивости с порядковым типом $\mathbb{Q}$. Мы приводим конструкцию цепочки функций $\mathtt{f}_\alpha(x)$ для произвольных рекурсивных ординалов $\alpha$, соответствующей убывающей цепочке утверждений о медленной непротиворечивости. Кроме того, в докладе будет рассказано об обощении конструкции медленной непротиворечивости на случай произвольных $\Sigma_1$-корректных рефлексивных теорий.