О пропозициональных исчислениях, представляющих понятие доказуемости

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

Содержание
Введение

Глава 1. Интуиционистская логика доказательств

1.1. Язык

1.2. Логика іЬР

1.3. Семантика Крипке

1.4. Арифметическая семантика

Глава 2. Позитивный фрагмент нолимодальной логики доказуемости

2.1. Позитивный фрагмент системы СЬР

2.2. Семантика Крипке для СЬР+

2.3. Случай одной модальности

2.4. Сложность фрагмента СЬР+
Литература

Введение
Первая глава диссертации посвящена рассмотрению интуиционистской логики доказательств 1ЬР. Логика доказательств ЬР [4] введена С. Н. Артёмовым и в настоящее время активно исследуется. ЬР является расширением исчисления высказываний в языке, представляющем доказательства как формальные объекты. Термы, выражающие доказательства, строятся из констант и переменных с помощью операций, соответствующих естественным операциям над выводами. Получаемые формулы вида £: Т1 предполагают толкование «£ есть доказательство Т>>. Логика ЬР полна относительно арифметики Пеано РА при интерпретации £: Р арифметической формулой «£* есть вывод Р* в арифметике Пеано».
Интуиционистская арифметика НА — наиболее известная теория, формализующая понятие конструктивного доказательства. В силу известных теорем Р. Соловея [32], логикой доказуемости классической арифметики РА является логика Гёделя-Лёба СЬ. Вопрос о логике доказуемости теории НА, впервые поставленный А. Виссером [33], длительное время остается открытым [13]. Кроме того, —в частности, в связи с последним вопросом — представляет интерес отыскание логики доказательств теории НА. Так, подходящим образом определенная интуиционистская логика доказательств позволяет выразить допустимые в НА пропозициональные правила [22], которые, вследствие интуиционистского характера этой теории, не являются непременно выводимыми.
Ранее исследовалась [5] интуиционистская логика доказательств 1ЬР, определяемая как фрагмент ЬР с интуиционистскими пропозициональными аксиомами вместо классических. Однако, логика 1ЬР не полна относительно интуиционистской арифметики НА и, таким образом, не решает вопроса о

логике доказательств этой теории.
Проблема построения арифметически полной интуиционистской логики доказательств рассматривалась С. Н. Артёмовым и Р. Имхофф [6]. В указанной работе ими вводится базовая интуиционистская логика доказательств ПЗЬР и интуиционистская логика доказательств ПР. В отличие от гЬР, логика 1ВЬР не содержит операций над термами, представляющими доказательства. Там же определена естественная арифметическая интерпретация логики ПЗЬР в НА и доказаны корректность и полнота 1ВЬР относительно этой интерпретации, а также выдвинута гипотеза полноты 1ЬР относительно надлежащей интерпретации в НА. Мы доказываем эту гипотезу. Соответствующие результаты опубликованы в работе автора [17].
Кроме того, в настоящей диссертации предложена семантика Крипке для логик 1ВЬР и 1ЬР, развивающая подход А. Мкртычева [27] и М. Фиттин-га [19] к построению моделей логики доказательств. Доказаны соответствующие теоремы о полноте и корректности, а также получен ряд следствий из них.
Во второй главе диссертации рассматривается фрагмент полимодальной логики доказуемости СЬР в некотором обедненном языке. Интерес к логике СЬР и этому ее фрагменту вызван, прежде всего, приложениями к теории доказательств.
Л. Д. Беклемишев предложил [9] новый подход к ординальному анализу арифметических теорий, основанный на понятии градуированной алгебры доказуемости, т. е. алгебры Линденбаума рассматриваемой теории, обогащенной операторами доказуемости (или непротиворечивости). Пусть Ст означает алгебру Линденбаума теории Т. Предполагая Т достаточно сильной, введем операторы на Ст:
(п)т' [А1] |~» [п-Сопт(А)],

Предикат доказательств —это примитивно рекурсивная арифметическая формула Prf [ж, у, такая что при всех <р Е £на> *“на Ф имеет место тогда и только тогда, когда найдется число п € и, для которого N (= Prf (п, г(рп).
Предикат доказательств Prf (ж, у) нормальный, если выполнены следующие условия:
(конечность) для всех кЕш множество Т (к) {I | Prf (к,1)} конечно и функция Хк.г{1 | I е Т (к)}п рекурсивная тотальная;
(объединимость) для всех к, I 6 со найдется п 6 ш, такое что Т (к) U Т (I) С Т(п).
Любая примитивно рекурсивная формула, выражающая примитивно рекурсивный [30] предикат
Proof (к, I) “к есть номер вывода в НА,
содержащего предложение с номером I"
является, как легко видеть, нормальным предикатом доказательств.
Лемма 1.4Л. Если Prf (ж, у) нормальный предикат доказательств, то существуют рекурсивные тотальные функции т: и2 —> и, а: ш2 —> ш, с: и —> и, и fn: ui —У и) для всех п € ш, такие что для любых чисел k,l € ш и предложений ср, ф G Prf (к, г<р —> ф'1) —> (Prf (I, г<рп) —) Prf (m (к, Г), гфп));
Prf (к, rip~l) —> Prf (а (к, /), Пр“1); Prf (,I, г<рп) —> Prf (а (&, 1),Г(/Г>);
Prf (fc, Пр"1) -> Prf (с (A:), rPrf (к,гip"1)"1);
Prf (к, г<р~') -> Prf (/„ (/с), фИ если 6 Vn(XA).