Некоторые алгоритмические вопросы для формальных систем со свойством интернализации выводов

• Автор: Крупский, Николай Владимирович
• Шифр специальности: 01.01.06
• Научная степень: Кандидатская
• Год защиты: 2006
• Место защиты: Москва
• Количество страниц: 80 с.

0.1 Введение

1 Отраженная логика доказательств

1.1 Основные определения

1.2 Конструкция наименьшей модели

1.3 Отраженный фрагмент логики доказательств

1.4 Сложность фрагментов логики доказательств

2 Типизация термов в рефлексивной комбинаторной логике

2.1 Определение правильно построенных формул ВСІ—,

2.2 Типизация подтермов

2.3 Типы в ВСІ ,

2.4 Соответствие между правильно построенными формулами и типами

2.5 Восстановление типов
3 Выводимость в рефлексивной комбинаторной логике
3.1 Выводимость из гипотез в ВС1__*
3.2 Устранение сечения в ВСЬТс
3.3 Разрешимость ВССГс
3.4 Оценки сложности

0.1 Введение.
Под свойством интернализации выводов для формальной системы Т ниже понимается ее способность формализовать рассуждения про свои собственные выводы и их связь с выводимыми ими формулами. Типичным примером формализма такого рода является формальная арифметика первого порядка РА (арифметика Пеано). Гёделевская нумерация синтаксиса РА (см. [15], [11]) позволяет определить инъективное кодирование формул и выводов натуральными числами таким образом, что предикат доказательств
“ж есть код вывода формулы с гёделевским номером у”
оказывается выразимым арифметической формулой .Рг/(ж, у). При этом для любой арифметической формулы <р справедливо
РА ~ (р <^> РА Н Рг/(п, г<рп) для некоторого натурального числа п.
(Здесь п — нумерал, соответствующий числу п, а г<р~1 — гёделевский номер формулы <р.)
Множество всех теорем РА вида Рг/(п, г<рп) образует отраженный фрагмент РА. Фактически, он уже содержит формулировки всех доказуемых в РА утверждений, но в несколько иной форме и с дополнительной информацией про их выводы. В то же время он существенно проще множества всех теорем РА. Естественный выбор деталей кодирования приводит к выражению предиката доказательств посредством Д 1-формулы. Это обеспечивает разрешимость отраженного фрагмента, в то время как множество всех теорем РА неразрешимо.
Аналогичное наблюдение имеет место для всех рекурсивно аксиоматизируемых расширений Т теории РА истинными (в стандартной модели арифметики) формулами. Факт разрешимости отраженного фрагмента теории Т является следствием разрешимости отношения

“d есть вывод формулы <р” для теории Т, а сама теория Т неразрешима ввиду существенной неразрешимости РА (см. [15]). Поэтому отраженный фрагмент устроен проще всей теории Т. Заметим, что это рассуждение использует факт неразрешимости теории Т и неприменимо в случае разрешимых теорий. Для ряда разрешимых формализмов вопрос о сравнении проблем разрешения для теории и сс отраженного фрагмента остается открытым.
Логика доказательств LP С.Н. Артёмова [1], [2], [3], [5], [6] является примером разрешимой пропозициональной логики со свойством интернализации выводов. В языке LP присутствуют выражения двух видов — термы, или полиномы доказательств (proof polynomials), и формулы. Термы строятся из переменных и констант первого вида (“по доказательствам”) с помощью унарной операции “!” (верификация) и бинарных операций (аппликация, применение modus ponens), “+” (объединение доказательств). Формулы строятся из пропозициональных переменных (второго вида) с помощью булевых связок и дополнительного конструктора квазиатомарных формул действующего по следующему правилу:
если t — терм, a F — формула, то t:F является формулой. Логика доказательств LP задается следующим исчислением: Аксиомы:
АО Аксиомы классической логики высказываний в языке LP,
A1 t:F -> F,
А2 t:(F -* G) —> (s:F -> (t ■ s):G),
A3 t.F —► (f + s):F, sF —► (t + s):F,
A4 t:F ->!f:(f:F).
Правила вывода :
(MP) F -> G, F h G,

с-шаблонов определяются аналогично (6). Это размеченные формулы следующих видов (соответственно):
Определение 3.1.2 Будем рассматривать секвенции вида Г =г» где F € ЬРт, а Г является конечным мультимножеством размеченных формул. Секвенция называется правильно построенной, если F и все члены Г являются типами. Секвенциальный вывод назовем правильно построенным, если все секвенции в нем правильно построены. Секвенциальное исчисление БС1_Тс определяется следующим образом:
Аксиомы: все секвенции вида Р, Г =>■ Р, где Р есть типовая переменная р1 или размеченная формула вида Ьс: (7.
Правила:
(р - (<7 -> Н)) - —► <7) ^ > Я)),
(10)
F^G)Г^Я
Г ^ F -> С

Г => А (Яг) Г 1А: А