О некоторых результатах о принципах рефлексии в арифметике

Для достаточно выразительных теорий T и классов формул C естественным образом может быть определен принцип равномерной рефлексии RFN_C(T) утверждающий, что всякая C-формула следует из утверждения о своей доказуемости в теории T. В этом докладе пойдет речь о некоторых результатах о принципах рефлексии для арифметики первого и второго порядка. Классический результат С. Фефермана утверждает, что всякое истинное утверждение языка арифметики первого порядка следует из итерированного принципа рефлексии RFN^α(PA), для подходящего рекурсивного ординала α. В настоящем докладе я приведу простое доказательство этого результата. Для этого будет доказано, что всякое рекурсивно перечислимое расширение T теории PA может быть аксиоматизировано как PA+TI(≺), где TI(≺) это схема арифметической трансфинитной индукции для подходящего рекурсивного линейного порядка ≺ (притом ≺ является вполне упорядочиванием если и только если T истинная теория). Также речь пойдет о последовательностях теорий T_0,T_1,... таких, что каждая T_i доказывает RFN_C(T_{i+1}). В частности, для класса Π¹₁-формул в качестве C и Π¹₁-коректного расширения ACA₀ в качестве T_0, таких цепей не существует. Тем самым мы можем естественным образом приписывать ординалы Π¹₁-рефлексивного ранга корректным Π¹₁-корректным расширениям ACA₀. Будет рассказано о взаимоотношение Π¹₁-рефлексивных рангов теорий и Π¹₁ теоретико-докзательственных ордниналов. Доклад частично основан на совместной работе с Джеймсом Волшем.