О формулах, $n$-доказуемость которых выводима в арифметике Пеано

Формула называется $n$-доказуемой в формальной арифметической теории $S$, если она доказуема в теории $S$, расширенной множеством всех истинных $\Pi_n$-предложений в качестве дополнительных аксиом. Множество всех $n$-доказуемых формул, вообще говоря, не является перечислимым. В то же время множество всех формул, $n$-доказуемость которых в $S$ доказуема в некоторой перечислимой теории $Т$, представляет собой рекурсивно аксиоматизируемую теорию, расширяющую $S$. В докладе будут приведены явные аксиоматизации этих теорий в терминах прогрессий Тьюринга итерированных схем локальной рефлексии. В частности, будет доказано, что множество всех формул, 1-доказуемость которых доказуема в арифметике Пеано, аксиоматизируется с помощью $\epsilon_0$ раз итерированной схемы локальной рефлексии. Также будет показано, что в некоторых случаях доказательство $n$-доказуемости формулы может быть значительно короче доказательства этой формулы с помощью итерированных схем рефлексии.