Аксиоматизация доказуемой 1-доказуемости

В докладе будут рассмотрены доказуемо 1-доказуемые предложения и связанные с ними теории. Более точно, для произвольной пары теорий T и S изучается множество всех таких предложений φ, для которых в теории T доказуемо, что предложение φ является 1-доказуемым в теории S, то есть, T ⊢ [1]_S(φ). Данное множество предложений представляет из себя некоторую теорию, расширяющую S. Будет дана аксиоматизация этой теории в терминах итерированных схем локальной рефлексии над S, а также рассмотрен вопрос о распространении данного результата на понятия доказуемой n-доказуемости для n > 1.