Строго позитивные логики в последнее время привлекают внимание специалистов благодаря их сочетанию эффективности и приемлемой выразительности. Язык исчисления рефлексий RC состоит из импликаций между формулами, составленными из пропозициональных переменных и константы "истина" лишь с помощью связки конъюнкции и модальностей,интерпретируемых в арифметике Пеано как ограниченные равномерные схемы рефлексии. Мы расширяем язык RC дополнительным семейством модальностей,соответствующих операторам, которые сопоставляют данной арифметической теории Т её фрагмент, аксиоматизированный всеми теоремами Т арифметической сложности Лn 0 для каждого n > 0. Мы показываем, что эти операторы, в некотором точном смысле, не представимы в полном языке модальной логики. Мы формулируем модальную систему RCΔ, расширяющую RC, которая корректна и, по нашей гипотезе, полна относительно указанной интерпретации. Показано, что в этой системе выразимы итерации схем рефлексии вплоть до любого ординала < εo. Далее, мы предлагаем нормальную форму для формул фрагмента RCΔ без переменных. На основе нормальных
展开▼
