О некоторых нестандартных предикатах доказуемости для формальной арифметики Пеано

В докладе будет рассмотрен альтернативный предикат доказуемости для формальной арифметики PA, а именно предикат $\square_s$, который может использовать аксиомы теории $I\Sigma_n$ только если определено значение $F_{\varepsilon_0}(n)$. Этот предикат был введен в статье С. Фридмана, М. Ратьена и А. Вайермана «Медленная непротиворечивость». Отметим, что $F_{\varepsilon_0}(x)$ это общерекурсивная функция для которой в PA недоказуема ее определенность на всех натуральных числах . В стандартной модели арифметики доказуемость $\square_s$ эквивалентна обычной $\square$. В указанной выше статье было показано, что для любого натурального n в PA доказуемо, что для всякого арифметического предложения $\phi$ имеется эквивалентность $\square\square_s^n \phi \leftrightarrow \square\phi$. Там был поставлен вопрос о трансфинитных итерациях $\square_s$. В докладе дается ответ на этот вопрос — будет рассказано о результате состоящем в том, что в PA доказуемо, что для каждого арифметического предложения $\phi$ имеет место эквивалентность $\square \phi\leftrightarrow \square_s^{\varepsilon_0}\phi$. Кроме того, будут рассмотрены похожие предикаты доказуемости, получаемые путем замены функции $F_{\varepsilon_0}(x)$ на некоторые другие общерекурсивные функции в определении $\square_s$. Будут приведены общерекурсивные функции $f$ и $g$ такие, что для соответствующих предикатов доказуемости $\square_f$ и $\square_g$ в PA доказуемо, что для всех формул $\phi$ имеют место эквивалентности $\square\phi\leftrightarrow \square_f^\omega\phi$ и $\square\phi\leftrightarrow\square_g^2\phi$.