Новые константы в предтабличных суперинтуиционистских логиках

В исследовании какого-либо объекта (или класса объектов) при отыс- кании существенно новых свойств этого объекта часто применяется метод обогащения, при котором изучаемый объект становится частью другого объ- екта, при этом новый объект наделяется дополнительными атрибутами — отношениями, функциями и прочее. В некоторых случаях исходный объект представляет собой собственное подмножество нового объекта, в других — новый объект получается лишь заданием на старом дополнительных атри- бутов.
Синтаксическим отражением такого обогащения является расширение языка. Утверждения и понятия, записанные на исходном языке, можно на- звать реальными, а утверждения и понятия, использующие дополнительные атрибуты — идеальными. Например, к числу реальных понятий Д. Гиль- берт относил понятие алгоритмически вычислимой функции. К реальным утверждениям он относил формулы вида ∀x(f(x) = g(x)) с вычислимыми функциями f и g. Мотивировка — любой частный случай этого равенства проверяется явно за конечное число шагов.
Пусть T — базовая теория в базовом языке S. Основа языка S — ре- альные понятия; основа теории T — аксиомы и правила вывода реального языка. Добавление к базовому языку новых символов (например, функци- ональных, константных, предикатных), иначе говоря, введение в язык S идеальных понятий, или экстрапонятий, расширяет (другими словами — обогащает) его до языка S′ : S ⊆ S′. Соответственно, введение в базовую тео- рию T дополнительных аксиом (и, возможно, правил вывода) расширяет ее до теории T′ : T ⊂ T′. При этом новые аксиомы, или экстрааксиомы, от- ражают свойства экстрапонятий и их взаимосвязь с реальными понятиями. В математике примеров такого рода много. В теории натуральных чисел, например, ряд результатов был получен с помощью теории комплексных
3
чисел. В алгебре примером такого рода является задача о разложении мно- гочлена x4 + 1 = 0 на множители над полем действительных чисел (есть два способа решения: первый подразумевает отыскание комплексных кор- ней, второй — выделение полного квадрата). Примерами из математической логики являются булевы алгебры с операторами, языки более высокого по- рядка, относительно элементарная определимость и другие.
Заметим, что при произвольном расширении теория T′ может ока- заться противоречивой, даже если T была непротиворечива. Поэтому важ- нейшее требование для такого расширения теорий — получаемая теория должна быть консервативна над исходной теорией, то есть экстрапонятия и новые аксиомы не должны нарушать базовую теорию:
A∈S, T′⊢A T⊢A
(если утверждение реального языка выводимо в расширенной теории, то и в реальной теории оно должно быть выводимо).
Согласно Гильберту, основное назначение экстрапонятий — получение новых реальных, теорем, а также более ясное доказательство уже известных теорем. Иначе говоря, экстрапонятия повышают выразительную силу языка и упрощают доказательства прежних теорем.
Для пропозициональных исчислений экстрапонятиями являются, на- пример, кванторы. Язык первого порядка позволил выразить практически все понятия, нужные для работы в привычных разделах математики. След- ствием такой универсальности стали, например, неразрешимость логики первого порядка, неполнота арифметики, неформализуемость логики вто- рого порядка.
Тем не менее, для решения ряда задач был найден промежуточный ва- риант — вместо кванторов использовать дополнительные пропозициональ- ные связки, отражающие некоторые свойства кванторов. Известные связки
4

модальной логики 2 , ♦ являются экстрапонятиями для языка классической двузначной логики.
Однако, классическая двузначная логика не всегда позволяет адекват- но моделировать некоторые прикладные задачи (например, в теоретической информатике). В связи с этим возникла необходимость применять и неклас- сические логики. Первым важнейшим примером таковых является инту- иционистская пропозициональная логика (Int), введенная первоначально Л.Э.Я. Брауэром, впоследствии формализованная А. Гейтингом, и истол- кованная А. Н. Колмогоровым в работе [36] как логика задач (подробнее об Int см., например, [11]). Кроме того, полезными, по разным соображениям, оказались и расширения Int, названные впоследствии суперинтуиционист- скими (с.и.) логиками.
П. С. Новиков1 в конце 50-тых годов ХХ века поставил задачу о новых логических связках как экстрапонятиях для языка со стандартным логиче- скимисвязками ∨,∧,→,¬.Я.С.Сметаничпривелточныеформулировки подхода Новикова к понятию новых логических связок в суперинтуицио- нистских логиках в работах [14,15].
Одним из примеров, рассмотренных Я. С. Сметаничем, является рас- ширение Int дополнительной одноместной связкой, удовлетворяющей акси- омам
φ(p) ↔ φ(q); ¬¬φ(p); φ(p) → (q ∨ ¬q).
Первая из трех аксиом показывает, что смысл φ(·) не зависит от ар- гумента, то есть можно рассматривать φ как логическую константу. Кроме того, можно рассматривать не одну, а несколько дополнительных логиче- ских констант (помимо стандартных констант 0 «ложь», 1 «истина»).
1в дальнейшем фамилия «Новиков» будет означать исключительно «П.С. Новиков».
5

В настоящей работе будут рассмотрены только дополнительные логи- ческие константы. Для этого случая подход Новикова адаптируется следу- ющим образом.
Язык чистой пропозициональной логики основан на пропозицио- нальных переменных V ar = {p0, p1, p2, . . .}; пропозициональных связках: ∨,∧,¬,→,↔(эквиваленцияпонимаетсякакp↔q (p→q)∧(q→p)); пропозициональных константах: 0 и 1. Обычным образом строится множе- ство Fm формул этого языка.
Добавим к исходному языку дополнительный набор констант φ = {φ1, φ2, …, φn}. Получим класс F m(φ) формул расширенного языка.
φ-Логикой будем называть множество формул языка F m(φ), включа- ющее Int и замкнутое относительно правил modus ponens и подстановки. φ-Логика L называется консервативным расширением с. и. логики L, если L включено в L и для всякой чистой формулы A из A ∈ L следует A ∈ L.
φ-Логика L определяет новые независимые константы в с. и. логи- ке L, если L является консервативной над L и не допускает никакого явного соотношения ни для какой дополнительной константы (явное соотноше- ние — формула вида φi ↔ B, где B не содержит φi). Другими словами, при добавлении явного соотношения к L нарушается консервативность над L.
φ-Логика L называется полным по Новикову расширением логики L, если L консервативна над L и не допускает присоединения никакой новой формулы (в смысле предыдущего определения).
Проблема Новикова для с. и. логики L формулируется следующим об- разом:
– построить примеры φ-логик, определяющие новые независимые кон- станты для L, и примеры полных φ-логик для L (проблема минимум);
– дать исчерпывающее описание семейства полных по Новикову рас- ширений L и выяснить в каких из них дополнительные константы незави- симы (проблема максимум).
6

Известно, что семейство с. и. логик имеет мощность континуума [19], поэтому естественным представляется рассмотрение проблемы Новикова для таких с.и. логик, которые по тем или иным причинам уже находи- лись в поле зрения исследователей. В настоящей работе проблема Новикова рассматривается применительно к предтабличным суперинтуиционистским логикам.
Напомним, что табличной называют с.и. логику, которая характери- зуется конечным числом конечных шкал. Предтабличной называют с. и. ло- гику, которая сама табличной не является, но любое ее собственное расши- рение оказывается табличным.
Из работы [6] известно, что всякая предтабличная суперинтуиционист- ская логика финитно аппроксимируема. Л.Л. Максимова, используя этот результат, в работе [8] показала, что предтабличных суперинтуиционист- ских пропозициональных логик ровно три: LC, L2, L32. Предтабличность первой логики была доказана в [28], остальных двух — в [34].
Цель диссертации:
1) получить исчерпывающее описание семейства всех полных по Но- викову расширений каждой из предтабличных с. и. логик в языке с несколь- кими дополнительными константами и исследовать каждое пополнение на наличие явных соотношений;
2) построить явную аксиоматику гильбертовского типа для из ука- занных расширений исследуемых логик в языке с одной дополнительной константой;
3) исследовать каждое из пополнений на алгоритмическую разреши- мость;
2Отметим, что для L2 и L3 используются и другие обозначения: в работе [8] указано, что логика L2 эквивалентна логике LP2, а логика L3 эквивалентна логике LQ3. Логики LP2 и LQ3 рассматривались в работе [33]. Здесь мы будем придерживаться обозначений, введенных Л. Л. Максимовой.
7

4) исследовать массовую проблему распознавания консервативности φ-логик над LC, L2, L3 на предмет алгоритмической разрешимости.
Диссертация состоит из введения, трех глав по 3 параграфа, списка литературы, включающего 50 наименований. Общее число страниц диссер- тации — 84. Номер теоремы, леммы и др. включают последовательно номер главы, параграфа и порядковый номер в параграфе. Для примеров, опреде- лений, замечаний предусмотрена отдельная нумерация, которая включает номер главы, номер параграфа и порядковый номер примера, определения, замечания в параграфе соответственно. Некоторые параграфы разбиты на пункты, пронумерованные по порядку в каждом параграфе отдельно. Ис- пользуются обозначения: — «по определению равносильно»; := — «по определению равно»; [1, m] — натуральные числа от 1 до m включительно.
Основные результаты диссертации связаны с получением ответов на сформулированные выше вопросы.
1) для LC и L2 дано семантическое описание всех полных по Новикову расширений в терминах классов конечных φ-цепей с раскраской (LC) и конечных φ-вееров с раскраской (L2); для L3 подобное описание дано для случая одной константы;
2) дана аксиоматика гильбертовского типа для всех полных по Но- викову расширений логик LC и L2, а также для 4-х полных по Новикову расширений логики L3 для случая одной константы;
3) установлена алгоритмическая разрешимость каждого пополнения указанных трех с. и. логик, а так же алгоритмическая проблема распозна- вания консервативности.
В первой главе приведены необходимые сведения о метаматематике φ-логик. Результаты, полученные в процессе работы, приведены с их дока- зательствами.