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