Содержание к диссертации
Введение
Глава 1. О метаматематике -логик 15
1.1 Метаматематика чистых шкал и логик 15
1.2 О иредтабличных суперинтуиционистских логиках 21
1.3 Метаматематика -шкал и -логик 24
Глава 2. Классификационные теоремы для полных по Новикову расширений иредтабличных суперинтуиционистских логик 31
2.1 Пополнения LC: классификация, примеры с одной и двумя константами и явные соотношения в них 31
2.2 Пополнения LI: классификация, примеры с одной и двумя константами и явные соотношения в них 39
2.3 Пополнения L3: классификация, примеры с одной константой и явные соотношения в них 49
Глава 3. Вопросы аксиоматики и алгоритмической разрешимости 59
3.1 Построение канонической модели 59
3.2 Аксиоматика полных по Новикову расширений иредтабличных суперинтуиционистских логик 67
3.3 О некоторых алгоритмических вопросах 77
Список литературы
- О иредтабличных суперинтуиционистских логиках
- Пополнения LI: классификация, примеры с одной и двумя константами и явные соотношения в них
- Пополнения L3: классификация, примеры с одной константой и явные соотношения в них
- Аксиоматика полных по Новикову расширений иредтабличных суперинтуиционистских логик
О иредтабличных суперинтуиционистских логиках
В этом параграфе приводятся необходимые сведения из метаматематики 2-логик и -шкал (изложение адаптировано для языка с несколькими константами и опирается на [13], [21], [38]).
Напомним, что к пропозициональному языку добавляется набор дополнительных логических констант Tp = {tpi, p i, Рп}] получается класс Fm(Tp) формул расширенного язьжа, при этом формулы из Fni были названы чистыми.
Формулы без переменных называются константными, Fmc(Tp) — класс константных формул.
Понятие подстановки переносится на расширенный язык: s(pi) = pi для всех ifi Є Тр.
Определение 1.3.1. Тр-Логикой называется множество L формул расширенного язьжа, включающее Int и замкнутое относительно правил modus ponens и подстановки [13, с. 155].
Через L + А обозначим наименьшую -логику, включающую логику L и содержащую формулу А (А є Fm(Tp)).
Рукописное начертание букв для логик, шкал и классов шкал будет указывать на связь с расширенном языком, прямое начертание — на связь с чистым языком.
Определение 1.3.2. Будем говорить, что Тр-логика L является консервативным расширением си. логики L, если L С и для всякой чистой формулы А из А Є следует А є L.
Определение 1.3.3. Явным соотношением для константы pi назовем формулу вида (pi г В, где подформула В не содержит pi (но может содержать константы, отличные от pi).
Тр-Логика L называется полным по Новикову расширением логики L, если L консервативна над L и для любой формулы А Є Fm(Tp): не принадлежащей , -логика L + А неконсервативна над L (то есть не допускает присоединения никакой новой формулы).
Если Тр = {(/?}, то явное соотношение имеет вид р - В для некоторой чистой формулы В. Тогда можно сказать, что определяет новую константу в L. Подход Новикова к понятию новой константы адаптирован А. Д. Яшиным [38]: понятие новизны трансформируется в понятие независимости констант.
Определение 1.3.4. Будем говорить, что -логика определяет новые независимые логические константы в L, если консервативна над L и для любого явного соотношения tpi - В -логика + (fii - В является неконсервативной над L (другими словами, не допускает присоединения никаких явных соотношений для дополнительных констант). Напомним формулировку проблемы Новикова для си. логики L: построить явные примеры полных над L Тр-логик с независимыми константами [проблема-минимум)] описать класс всех полных по Новикову Тр -логик (проблема-максимум). Следующая теорема является формальным обоснованием корректности постановки проблемы полноты по Новикову для произвольной логики L.
Однако этот результат ничего не дает в плане эффективного описания как конкретных примеров полных логик, так и всего семейства полных логик. Определение 1.3.5. Обобщенной Тр-шкалой называется структура вида (\,3;Ф), где (W,S) — обобщенная шкала, Ф = (Фі,...,Фп) — набор конусов из S, которые также будем называть константами. О каких константах идет речь, будет ясно из контекста.
Как и в случае обобщенных шкал, под конечными обобщенными р-шкалами всегда будем понимать обобщенные -шкалы, удовлетворяющую условию S = ConW. Аналогично, любую р-шкалу (W; Ф) можно естественным образом отождествить с обобщенной -шкалой (W, ConW] Ф). Обобщенную -шкалу будем иногда называть просто -шкалой, если ее тип ясен из контекста.
Определение 1.3.6. Оценкой переменных в Тр-шкале /І = (И7, S; Ф) называется отображение v: Var — S.
На стандартные связки оценка распространяется, как описано выше. Для новых констант для любой v полагаем v(pi) := Ф , і Є [l,n].
Конусы для интерпретации констант на обобщенной -шкале /І = (W, S] Ф) можно задавать также с помощью понятия цвета [1].
Определение 1.3.7. Цветом называется произвольное подмножество множества р (всего существует 2П цветов). Цветом точки х обобщенной -шкалы /І называется множество со1(ж) := {рі Є р \ х lb pi\. В случае одной константы точку х назовем окрашенной, если х Є Ф, и соответственно неокрашенной, если х . Ф.
Понятия модели, истинности формулы в модели, общезначимости формулы в Тр-шкале и в классе р-шкал определяются аналогично.
Класс М = {(И ,5І;ФІ) і Є І)} -шкал будем называть характеристическим для L, если таковым является класс обедненных (без выделенных конусов) шкал М = {(И , Sp) \ і Є /)}. Определение 1.3.8. р-Логикой класса Ж обобщенных -шкал называется множество С(М) {Лє Fm{p) I V/i Є M : /І = А}. Замечание 1.3.1. Из вышесказанного следует, что для любой с. и. логики L по крайней мере одно консервативное расширение существует. В самом деле, по теореме 1.1.3 логика L характеризуется некоторым классом обобщенных шкал; введем в каждой шкале этого класса набор выделенных конусов каким-либо образом, получим характеристический класс обобщенных р-шк&л и его -логику L. При этом чистый фрагмент совпадает с L.
В работе [13] рассмотрено расширение пропозиционального языка произвольным набором р дополнительных логических связок произвольной местности. Модели 2-логик в таком языке названы посредством р-п.б.а.7 то есть псевдобулевыми алгебрами с заданными на них дополнительными операторами; доказана теорема о моделируемости р-логик классами -п.б.а. В нашем частном случае эта теорема формулируется следующим образом
Пополнения LI: классификация, примеры с одной и двумя константами и явные соотношения в них
В настоящем параграфе мы покажем, что любая консервативная над L1 (/?-логика включена в некоторую -логику, задаваемую подходящим кон-финальным классом конечных -вееров.
В работе [23] дано описание полных по Новикову расширений логики L1 для случая одной константы. В настоящем параграфе мы приведем аналогичные результаты для случая п констант.
Пусть точка 2о — корень Fm: а точки ai, с&2,..., ат образуют крышу веера Fm. Обозначим полные прообразы точек сц через WQ := h l({ao}), Wi := h l({a ) для і = [l,m]. Прообраз крыши веера Fm обозначим через W := [J 1 Wi. Из определения р-морфизма получаем, в частности, что W Є S.
Поскольку число возможных цветов равно 2П, множество W{ разбивается на дизъюнктные непустые компоненты в количестве от 1 до 2П. Компоненту, содержащую точку х Є Wi можно записать так: (здесь &j обозначает теоретико-множественное дополнение). Лемма 2.2.4. Имеет место равенство Wi \ Ф = Wi П (—Ф ) для У г Є [l,m] и Vj Є [l,n]. Доказательство. Включение D следует из того, что — Ф С Ф - (согласно определению операции псевдодополнения на конусах).
Докажем обратное включение. Рассмотрим точку х Є Wi такую, что Наконец, в предположении х у точки х и у не могут принадлежать разным компонентам разбиения конуса W. В самом деле, если у Є Х и ж ф. X/, то х у (напомним, что компоненты являются элементами п.б.а. S). При этом х Є VK, о ф W. Получили - -цепь о х у, что невозможно.
Конусность. Пусть f(x) Ь в веере F/. Это означает, что /(ж) = ао, т.е. х Є Wo и 6 совпадает с некоторым af. В силу леммы 2.2.6 точка х видит компоненту X/, т.е. VK П X/ 0- Значит, найдется у х такая, что
Корректность этого определения следует из следствия 2.2.3 и из определения отношения равноцветности. Таким образом получили if-веер jF/ и желаемый -морфизм. Теоре ма 2.2.1 доказана. Следствие 2.2.7. Пусть М — произвольный L2-характеристический класс обобщенных If-шкал. Тогда существует конфинальный класс Э if-вееров такой, что Э М.
Доказательство. Зафиксируем натуральное число т. В силу L2-xa-рактеристичности класса Ж найдутся порожденная из некоторой шкалы этого класса корневая подшкала (W, S; Ф) и р-морфизм h: (W, S) —» Fm. По основной лемме найдется -веер JF/ (где т / т 2П) и -морфизм (И ;Ф)Л$.
Натуральный ряд содержит бесконечное число попарно не пересекающихся интервалов вида [m, m-2n]. Для каждого из этих интервалов найдется (/2-веер JF/, где / Є [т т 2П]. Все такие jF/ и образуют искомый класс JF. П
В заключение этого параграфа сформулируем следующий результат. Предложение 2.2.8. Полные по П. С. Новикову расширения логики L2 в языке с несколькими константами характеризуются подходящими конфинальными классами Jf-вееров. п. 2. Прототипы и классификация полных по Новикову расширений логики L1 Определение 2.2.1. Прототипом JF будем называть f-веер JF = (F; Фі, Ф2,..., Фп), все максимальные точки которого имеют разные цвета.
Далее максимальные точки -веера JF будем рассматривать вместе с их цветами. Пример 2.2.1. В случае двух констант один из прототипов выглядит так:
Пусть JF — прототип и а — точка крыши -веера 3\ Обозначим через Э , а] класс -вееров, полученный из У размножением точки а с сохранением цвета этой точки. Например, при размножении левой точки в веере из предыдущего примера -веера этого класса будут иметь такой вид:
Лемма 2.2.9. Любой Lp-веерр -морфно отображается на некоторый прототип. Действительно, склеивание всех равноцветных точек крыши в одну является искомым -морфизмом. Сразу получаем, что в прототипе 3 и классах вида Э З , а] истинны одни и те же константные формулы. То есть имеет место Следствие 2.2.10. Для каждой точки а из крыши веера У имеет место равенство &с(3) = (9 3 , а}).
Доказательство. Если крыши прототипов неизоморфны, то в одной из них, например, в крыше веера Эд, найдется точка а, не имеющая цветового аналога в крыше веера 3 - Тогда получаем 3 = - Со1(а) и Эд \/= -iCol(a). Если же крыши изоморфны, то различны цвета корней этих шкал, то есть найдется константа, истинная в одной из них и не истинная в другой.
Для двух классов [JF, а] и [JF, 6] аксиома неразложимости Irr(b) выполнена в первом классе и не выполнена во втором, и наоборот, Irr(a) выполнена во втором и не выполнена в первом. Таким образом, -логики классов, полученных размножением разных точек одного прототипа, различны. Пример 2.2.2. Рассмотрим прототип, один из Тр-вееров класса [JF, 2i] и один из If-вееров класса SFfjF, 0] :
Рассмотрим произвольный конфинальный класс Э -вееров. По лемме 2.2.9 каждый / веер этого класса -морфно отображается на некоторый прототип. Поскольку число прототипов конечно, найдется конфинальный подкласс 2 С Уі, в котором все члены имеют один и тот же прототип Э . Теперь работаем с Э : в его прототипе конечное число точек, поэтому для этого класса существует конфинальный подкласс Э С Э и точка а из крыши прототипа JF, такие, что Э содержит шкалы со сколь угодно большими прообразами точки а.
В каждом веере из Э склеим все равноцветные точки крыши в одну, кроме тех точек, которые являются прообразами точки а. Получим класс 3 = Э . Кроме того, имеем Э 4 Q Э [3,а\. С другой стороны Э [3,a] = Э . Поэтому (9 , a]) = (9. Таким образом, любая консервативная над L2 -логика включена в какую-то -логику вида ( (3 , а)). Все -логики такого вида различны.
Пополнения L3: классификация, примеры с одной константой и явные соотношения в них
В силу теоремы 1.3.2 существует характеристический класс Ж обобщенных (/ шкал такой, что = (М). Согласно предыдущему разделу, (М) С (Х) ), где Т — некоторый конфинальный подкласс класса Т . Дальнейшие рассуждения зависят от того, (/9-даймонде каких видов преобладают в классе Т .
Если Т содержит конфинальный подкласс Т (/ даймондов типа «f-нигде», то по прямой теореме сравнения if -логик (Х)) С (Х) ), а по лемме 2.3.7 получим L(JD") = «С1, откуда С А Если Т содержит конфинальный подкласс (/9-даймондов типа «f-везде», то, аналогичным образом, С 2. Если Т содержит бесконечный подкласс (/ даймондов типа «if в топе», то С Д Если Т содержит бесконечный подкласс (/ даймондов типа «if везде, кроме корня», то С А Пусть ни один из предыдущих случаев для Т не выполнен, то есть каждый (/9-даймонд из Т имеет в миддле как окрашенные, так и неокрашенные точки.
Если в Т имеются (/ даймонды со сколь угодно длинными неокрашенными частями миддла, образующие конфинальный подкласс Т , то L С (Х) ). В каждом (/ даймонде из Т окрашенные точки миддла можно «подклеить» к топу (см. пример 2). Получим класс ТУ" типа «ip в топе» такой, что !D D , следовательно, по прямой теореме сравнения (/9-логик L{T ") С (D "). С другой стороны, Т " конфинален в Т поэтому по лемме 2.3.7 /(D ") = 3, следовательно, L С А
Если же в Т имеются (/9-даймонды со сколь угодно длинными окра шенными частями миддла, образующие конфинальный подкласс Т , то сно ва имеет место L С (Х) ). Далее в каждом из этих (/9-даймондов неокра шенные точки миддла можно «склеить» в одну (см. пример 1), получив подкласс Т (/9-даймондов типа «tp везде в миддле, кроме одной точки» та кой, что Ю" Ю ", откуда (") С (! ") и, кроме того, Ю " С D5. В силу конфинальности класса Т)" и леммы 2.3.7 получаем, что (D ") = 5, откуда С 5.
Сначала покажем, что В Є А Предположим противное. Тогда найдутся некоторый (/ даймонд (Ї) ;Ф), где Ъ\ = {,mi,... ,mn,r}; Ф = { ,m2,... , mn} и некоторая оценка v : г (р) = Р, v( p) = Ф. Найдется точка х данного (/ даймонда такая, что х Є (Р 2 Ф) П ((Ф D Р) D Р) и ж (Фи -Р). Откуда имеем: (1) ж Є Р D Ф; (2) х Є (Ф D Р) э Р; (3) ж Ф; (4) ж —Р. Из (4) получаем t Є Р, а из (3) получаем, что х = т\ или ж = г. Ясно, что в любом случае т\ ф Р, потому что в противном случае ті Є Ф по (1), чего быть не может. С другой стороны, для любого у ті имеем у ф Ф или у Є Р, откуда ті Є Ф 2 Р, значит по (2) получаем ті Є Р, что приводит к противоречию.
Теперь покажем, что В . А Приведем пример (/ даймонда класса Т с заданной на нем оценкой, в котором формула В опровергается, поэтому
Таким образом, существует ровно пять полных по Новикову расширений с. и. логики L3. Более точно, каждая консервативная над L3 tp-логика включена в одну из попарно несравнимых ip-логик «С1, 2, 3, 4, А Глава 3. Вопросы аксиоматики и алгоритмической разрешимости
В предыдущей главе была дана исчерпывающая классификация полных по Новикову расширений предтабличных суперинтуиционистских логик. В этой главе дается явная аксиоматика гильбертовского типа для каждого из указанных расширений соответствующей иредтабличной с. и. логики в язьже с одной константой.
К каждому из рассматриваемых исчислений можно добавлять некоторые формулы в качестве дополнительных аксиом исчисления. Исходя из цели данного параграфа, дополнительные аксиомы для каждого из исчислений будем выбирать из следующего списка:
Пусть J — некоторое исчисление, полученное добавлением в какое-то из исчислений LC, L2, L3 некоторых схем аксиом из списка 1- 9.
В исчислении J выводом из множества гипотез Г называется конечная последовательность формул i, 2, , Bi такая, что для любого і (1 і /) В І есть либо аксиома, либо гипотеза из Г, либо получается из двух предшествующих формул последовательности по правилу вывода modus ponens. Формула А выводима из Г в исчислении J (обозначение Г \-у А), если существует вывод из Г, заканчивающийся формулой А. Если 0 Ьд А, то говорят, что формула А выводима в J (обозначение Ьд А). хМьі рассматриваем вариант бесподстановочного вывода [10], то есть под аксиомой понимаем частный случай схемы аксиом. Теорема 3.1.1 (о дедукции). Г, A bj В тогда и только тогда, когда Г bj А — В. Доказательство этой теоремы аналогично доказательству соответствующей теоремы для Int (см. [4]). Исчисление J называется противоречивым, если Ьд А Л -іА для некоторой формулы Л. Заметим, что противоречивость J равносильна выводимости любой формулы в J. Часть этих исчислений, содержащих в том числе аксиомы списка 1 — 9 приведенного выше списка, являются противоречивыми, например исчисления, содержащие формулы 1 и 2. Для дальнейших рассуждений нам понадобится следующее Предположение. Рассматриваемое в общем виде исчисление J предполагается непротиворечивым, то есть не все формулы выводимы.
Аксиоматика полных по Новикову расширений иредтабличных суперинтуиционистских логик
Доказательство (от противного). Пусть 3 — одно из исчислений Ji,..., 5- Зафиксируем формулу Л, невыводимую в 3. Пара (0; А) непротиворечива, значит, найдется тип а: А Є а1, откуда, по лемме 3.1.11, в канонической -(/9-модели (Ж, v) в точке сг имеем сг I/ Л. Рассмотрим корневую подмодель Ж7 с наследуемой оценкой if. В силу теоремы 1.1.4 Жа \/= А.
Теперь покажем, что для каждого исчисления 3 = 3k для к Є [1,5], корневая ушкала Ж7 имеет цветовой тип JF .
Если max vtc", то в Зі цветовой тип точки а — « р — нигде» — соответствует максимальным точкам вееров класса «tp — нигде». В J 2 цветовой тип точки сг — «(/2-везде» — соответствует максимальным точкам вееров класса «tp — везде». Для 3s цветовой тип точки сг — «tp — во всех точках крыши» — соответствует максимальным точкам вееров класса «tp — во всех точках крыши». Для J4 и 5 цветовой тип точки сг не важен, так как в классах jF и JF есть (/9-веера как с окрашенными, так и с неокрашенными точками крыши. Пусть сг — точка глубины 2. Тогда Ж7 является веером, возможно с бесконечным числом точек крыши. Пусть J = Ji, тогда чр есть аксиома исчисления Зі. По лемме 3.1.8, получим Ф = 0, то есть Ж7 имеет тип «tp — нигде». Пусть 3 = 3 i, тогда tp есть аксиома исчисления Зі- По лемме 3.1.8, получим Ф = Ма, то есть Ж7 имеет тип «tp — везде». Пусть 3 = 3%. Пусть т а, тогда тах т в силу аксиомы bd,2, отсюда, по лемме 3.1.10, получим (р Є т. Так как —і—чр — аксиома исчисления з? т0 -1-К/9 Є т и, по лемме 3.1.4, получим -і(/9 Є г1, то есть крыша (/9-веера Ж7 полностью окрашена.
Покажем, что a \f (р. Предположим противное. Пусть р Є т. Тогда найдутся тип т а и формула А такая, что А Є а1 и А Є т. Из аксиомы получаем (A V -іА) Є т. По лемме 3.1.4, имеем А Є а0 или — А Є о-0, но первый случай невозможен в силу непротиворечивости типа а, во втором случае -і А Є т, что тоже невозможно в силу непротиворечивости типа т. Поэтому р . сг, то есть Ж7 имеет тип «р — во всех точках крыши».
Пусть J = 4- По лемме 3.2.5, существует не более одной точки т а такой, что р Є т. Убедимся, что хотя бы одна такая точка существует. Поскольку d((i) = 2, то найдутся т а и формула А такая, что А Є а1 и А Є т. Из аксиомы (р V -кр) — (А V -vl) получаем, что (/9 V -кр Є о-1 и (/9 Є о-0. По лемме 3.1.4, из -і(/9 Є о-1 получим, что найдется я а такой, что р Є я. Откуда Ж7 имеет тип «р — в единственной точке крыши».
Пусть J = 5- По лемме 3.2.6, существует не более одного т а такого, что -і(/9 Є т. Все дальнейшие рассуждения аналогичны рассуждениям предыдущего абзаца. Ж7 имеет тип «р — во всех точках крыши, кроме одной».
Таким образом, для каждого из пяти исчислений Ji,..., J5, если J& \/ А, существует р-веер соответствующего цветового типа, в котором формула А опровергается.
В каждом из пяти рассматриваемых случаев Жа может иметь бесконечное число точек крыши. Сделаем переход от бесконечного веера к конечному, применив известный метод фильтрации [30] и отвлекаясь от конкретного вида полученной модели Жа.
Рассмотрим бесконечный р-веер W = (И-7, Ф) с корнем о одного из пяти рассматриваемых типов с заданной на нем оценкой v переменных из Var. Зафиксируем конечный набор переменных р = {pi,... ,ps}.
Зададим на множестве точек крыши W отношение эквивалентности х у: v Pi для всех рі Є p. (3.2) Свойства рефлексивности, транзитивности, симметричности выполнены. Тогда крыша (/ веера W разбивается не более чем на 2S+1 классов эквивалентности И-7!,..., W/. Далее строим конечный веер Fi = {r,cui,..., о;/}, на котором задаем выделенный конус Ф следующим образом: Доказательство проводим индукцией по построению формулы В(ср]р). Для константы tp и переменных списка р оба утверждения вытекают непосредственно из определений (3.1)-(3.6). Проведем шаг индукции для формулы вида В\ — 2, предполагая оба утверждения леммы для В\ и 2 верными. Докажем (1). Пусть wk \\-и В\ — В2. В силу максимальности точки wk получаем wk \fu В\ или wk \\-и 2- По предположению индукции Ух Є Wk : х \fv В\ или Ух Є х \\-v В ї- Отсюда Ух Є Wk : ж lhw В\ — 1.
Пусть Зх Є И7 : ж Wv В\ — В2. Для подразумеваемой точки х Є И7/; в силу ее максимальности имеем х \fv В\ или х Wv В2. Из первого получаем -Ух Є Wk : х \\ v Bi (в силу законов внешней логики), из второго, по индукционному предположению, получаем Ух Є Wk : х \\-v 2- По предположению индукции имеем Wk \у и В\ или Wk \\ и В2: из чего, в силу максимальности Wk, вытекает Wk \\ и В\ — B i Докажем (2). Пусть г \fu i 2- Найдется z г : z \\-и В\ и z \fu В2.
Если z = г, то, по предположению индукции (утверждение 2), получаем о \\-v В\ и о \fv В2, то есть о \fv В\ — 2- Если Z Г, ТО Z = Wk для некоторого к и Wk \\ и В\ и Wk \у и В2- В силу предположения индукции (утверждение 1) получаем Ух Є Wk : х \\-v В\ и Зх Є Wk : х \fv В2. Отсюда Зх Є Wk : х \\ v В\ и х \fv В2, поэтому о \fv В\ — В2.
В обратную сторону аналогично. Заметим также, что если исходный tp-веер W относится к одному из указанных пяти типов, то и полученный из него tp-веер jF/ имеет тот же цветовой тип. Завершим доказательство теоремы о полноте. Пусть формула А не содержит других переменных, кроме как из списка р: и невыводима в исчислении J&. По описанному выше, существует tp-веер к-го цветового типа, опровергающий А. По лемме 3.2.8, существует конечный веер цветового типа к, опровергающий А, то есть JF = А, что и требовалось доказать.
Таким образом, для каждого из пяти исчислений Ji,..., J4, если J& \/ А, существует (/9-даймонд соответствующего цветового типа, в котором формула А опровергается.
В каждом из четырех рассматриваемых случаев Ж7 может иметь бесконечное число точек миддла. Сделаем переход от бесконечного даймонда к конечному, применив известный метод фильтрации [30] и отвлекаясь от конкретного вида полученной модели Жа.
Рассмотрим бесконечный (/ даймонд W = (И-7, Ф) с корнем о одного из пяти рассматриваемых типов с заданной на нем оценкой v переменных из Var. Зафиксируем конечный набор переменных