Исчисления рефлексии и линейность: фрагменты теории бар-индукции

В рамках исследований по основаниям математики эмпирически наблюдается феномен линейности порядка по силе непротиворечивости для естественных теорий. В то же время хорошо известно, что используя подходящие технические приёмы, такие как гёделевская лемма о неподвижной точке, можно строить примеры несравнимых теорий в этом порядке. В данном докладе я расскажу о подходе, позволяющем доказать линейность такого порядка, ограниченного на богатое семейство фрагментов данной теории (в нашем случае теории бар-индукции BI).
Теория BI - это подтеория классической арифметики второго порядка постулирующая, что имеет место принцип трансфинитной индукции для всех полных линейных порядков. В силу классического результата Харви Фридмана она эквивалентна над ACA₀ принципу ω-модельной рефлексии. С точки зрения силы непротиворечивости эта теория эквивалентна теориям KPω и ID₁.
В данном докладе будет рассказано о построении исчисления рефлексии для теории BI. Это исчисление, с одной стороны, позволяет нам с одной стороны произвести ординальный анализ BI и тем самым получить новую теоретико-рефлексивную систему обозначений для ординала Бахмана-Говарда. С другой стороны, мы показываем, что все теории, выразимые в этом исчислении, линейно сравнимы по силе непротиворечивости. При этом техника доказательства является воплощением для случая BI общей схемы: наличие адекватного исчисления рефлексии влечёт линейность порядка по силе непротиворечивости.
Доклад основан на совместной работе с Владом Лазерем.