• A
  • A
  • A
  • АБB
  • АБB
  • АБB
  • А
  • А
  • А
  • А
  • А
Обычная версия сайта

Статья

Исчисление для схем рефлексии и спектры консервативности

Успехи математических наук. 2018. Т. 74. № 4. С. 3-52.

Строго позитивные логики в последнее время привлекают внимание специалистов благодаря их сочетанию эффективности и приемлемой выразительности. Язык исчисления рефлексий RC состоит из импликаций между формулами, составленными из пропозициональных переменных и константы “истина” лишь с помощью связки конъюнкции и модальностей, интерпретируемых в арифметике Пеано как ограниченные равномерные схемы рефлексии. Мы расширяем язык RC дополнительным семейством модальностей, соответствующих операторам, которые сопоставляют данной арифметической теории T её фрагмент, аксиоматизированный всеми теоремами T арифметической сложности Π0n для каждого n>0. Мы показываем, что эти операторы, в некотором точном смысле, не представимы в полном языке модальной логики. Мы формулируем модальную систему RC∇, расширяющую RC, которая корректна и, по нашей гипотезе, полна относительно указанной интерпретации. Показано, что в этой системе выразимы итерации схем рефлексии вплоть до любого ординала <ε0. Далее, мы предлагаем нормальную форму для формул фрагмента RC∇ без переменных. На основе нормальных форм показывается алгоритмическая разрешимость данного фрагмента и его полнота относительно арифметической семантики. В заключительной части работы рассматриваются несколько естественных характеризаций алгебры Линденбаума–Тарского для замкнутого фрагмента RC∇ и для её двойственной шкалы Крипке. Элементы этой алгебры находятся в естественном соответствии с последовательностями теоретико-доказательственных Π0n+1-ординалов для ограниченных фрагментов арифметики Пеано, так называемых спектров консервативности, а также с точками известной модели Крипке, введённой К. Н. Игнатьевым.