Введение к работе
Исследование какого-либо объекта (или класса объектов), первоначально успешно продвигающееся в "глубину", на некоторой стадии достигает "предельной точки", когда обычные усилия уже не приводят к отысканию существенно новых свойств этого объекта.
В этой ситуации часто применяется метод обогащения, при котором изучаемый объект становится частью другого объекта, при этом новый объект наделяется дополнительными атрибутами — отношениями, функциями и пр. В некоторых случаях исходный объект представляет собой собственное подмножество нового объекта, в других — новый объект получается лишь заданием на старом дополнительных атрибутов.
В математике примеров такого рода много. В теории натуральных чисел, например, ряд результатов был получен с помощью комплексных чисел.
Следующие примеры непосредственно связаны с математической логикой: булевы алгебры с операторами; булевы алгебры с выделенными идеалами; языки более высокого порядка; относительно элементарная определимость и др.
В любом случае синтаксическим отражением такого обогащения является расширение языка. Утверждения и понятия, записанные на исходном языке, можно назвать реальными, а утверждения и понятия расширенного языка — идеальными.
Согласно гильбертовской концепции основное назначение идеальных понятий (другое название — экстрапонятия) — либо получение новых реальных знаний об изучаемых объектах, либо более простое обоснование уже известных свойств. Например, к числу реальных утверждений Гильберт относил арифметические формулы вида Vi(/() = g(x)) для вычислимых функций / и д.
При этом первичным требованием к вводимым экстрапонятиям является консервативность, т.е. введенные экстрапонятия не должны изменять объем реальных знаний.
Для пропозициональных логических исчислений экстрапонятиями являются кванторы. Язык первого порядка позволил выразить практически все понятия, необходимые в обычной рабочей математике.
Вместе с тем за эту универсальность первопорядкового языка пришлось расплачиваться. Неполнота и неразрешимость — наиболее известные последствия.
Однако для целого ряда задач универсальный язык не является необходимым. Часто бывает достаточно, не вводя кванторов, ввести некоторые дополнительные логические связки. Эти связки в завуалированном виде должны включать в себя некоторые свойства кванторов, однако сами будут относиться к пропозициональному языку.
Здесь уместно упомянуть современную модальную логику, которая получается из классической двузначной логики введением дополнительных модальных операторов [1, 40]. В рамках модальной логики удается описать чисто логические аспекты разных прикладных теорий, от формальной арифметики Пеано до вопросов прикладной информатики.
Показательными результатами в этой области являются такие, как: исчерпывающее описание свойств оператора доказуемости в классической арифметике Пеано; применение временных логик к доказательству корректности программ.
В результате ряда исследований было выяснено, что классическая двузначная логика не всегда позволяет адекватно описать формально-логическую сторону некоторых прикладных задач. Этим обусловлена необходимость вводить в рассмотрение и неклассические логики.
Среди разнообразия неклассических логик важное место занимает интуиционистская логика, введенная первоначально Л.Э.Я.Брауэром из некоторых философских соображений для обоснования математики, и получившая впоследствии более ясную интерпретацию как логика задач.
У прикладных интуиционистских теорий, таких, как арифметика Гейтин-га, разветвленная теория типов Мартин-Лефа, прототетика и др., базисной логической системой является интуиционистская пропозициональная логика Int. Соответствующее направление исследований заключается в расширении языка Int дополнительными логическими связками и изучении получающихся логик как "самих по себе", так и с точки зрения возможных приложений. Например, в настоящее время группа голландских логиков активно изучает свойства оператора доказуемости в интуиционистской арифметике. На пропозициональном
языке этот оператор представляется как дополнительная одноместная связка.
К настоящему моменту в литературе накопилось большое число примеров логик, полученных из Int расширением языка дополнительной связкой (или связками). Выбор тех или иных связок основывался на различных соображениях. Чаще всего новая связка возникала из некоторого "интересного" или "полезного" понятия, определимого в языке описания конкретной семантики Int. Главный упор в последующих исследованиях делался на построении аксиоматики, изучении свойств и приложений получающихся логик. К этому типу можно отнести работы по следующим направлениям:
модальности (аналоги классических модальностей) в Int: Булл196б, Божич к Дошен1984, Эвальд1986, Серви1977, Сотиров1984, Виллиамсон1992, Вольтер & Захарьящев1997;
временные связки в Int. Каминский1988, Габбай1975, Лопес-Эскобар1985, Нут1975, Раушер1974,1977;
слабая дизъюнкция в логике финитных задач Медведева: Скворцов1983;
сильная конъюнкция Поттингера (Лопес-Эскобар1985);
связки, определимые в интуиционистском второпорядковом пропозициональном исчислении: Габбай1977, Крайзель1981, Трулстра1981;
работа де Йонга1980 о классе интуиционистских связок;
оператор Крайзелп: Гоад1978, Селлуцци1974, Войтыляк1984.
Ряд других работ можно отнести к т.н. синтаксическому подходу. Согласно синтаксической концепции смысл дополнительных связок должен заключаться в описывающих их правилах вывода и аксиомах. При этом интерес исследователей сосредоточен на приложениях и поиске удобных типов семантики. В этом русле находятся работы следующих направлений:
сильное отрицание в Int: Земан19б8, Гуревич1977, Шаталов1977;
связки, определяемые секвенциальными исчислениями: Боуэн1971; Санчис-1973; Кучера1968;
немонотонные операторы: возможность (Габбай1982) и следование (Сер-ви1992);
сюда же можно отнести работу Габбая1978 о понятии классической логической связки.
Приведенный список показывает, что нестандартные интуиционистские связки являются предметом интереса большого числа исследователей. Разнообразие примеров порождает вопрос: какие из нестандартных связок заслуживают рассмотрения?
Проблема выбора тех или иных дополнительных связок лежит за рамками настоящей работы. При фиксированном наборе дополнительных связок возникает обширный класс логик (как правило, континуальный).
Выделив с помощью некоторого условия подкласс логик, можно интересоваться максимальными элементами этого подкласса. Например, если в качестве определяющего условия взять обычную непротиворечивость, то максимальность такого рода известна под названием полноты по Посту.
П.С.Новиков предложил подход к понятию интуиционистской логики с дополнительными связками, при котором базисным свойством является консервативность над Int. Соответственно заслуживающими внимания являются максимальные консервативные над Int логики, в которых дополнительные связки в действительности являются "новыми". В настоящей работе это понятие обозначается термином полнота по Новикову.
Подход П.С.Новикова был впервые изложен в статьях Я.С.Сметанича [3, 4]: формальная система L определяет новую связку по Л.С.Новикову, если L консервативна над Int и не допускает присоединения явных сотношений для дополнительной связки. Первый пример новой связки по Новикову найден Сметаничем, при этом связка оказывается константной, т.е. не зависящей от аргумента.
А.В.Бессонов [5] привел пример исчисления с новой неконстантной связкой и установил континуальность семейства логик, определяющих новую связку по Новикову.
Ссылка на лемму Цорна показывает, что всякая консервативная над Int логика содержится в некоторой полной по Новикову логике, однако такая ссылка ничего не дает в плане эффективного описания как конкретных примеров полных логик, так и всего семейства полных логик.
Проблема Новикова изначально была сформулирована для языка с одной дополнительной одноместной связкой следующим образом: построить явный (т.е. конечно аксиоматизируемый) пример полной логики с новой связкой.
В случае нескольких дополнительных связок понятие новизны естественным образом трансформируется в понятие независимости связок, а сама проблема Новикова переформулируется следующим образом: для данного набора сиязок построить явный пример полной логики, в которой эти связки были бы независимы.
Для конкретной логики проблема Новикова заключается в описании всех ее полных расширений.
Наконец, заключительным пунктом проблемы П.С.Новикова можно считать исчерпывающее описание всего семейства полных по Новикову логик для данного набора дополнительных связок.
Другой подход к понятию интуиционистской логической связки можне назвать семантическим. Его основная идея состоит в трактовке связки как фиксированного способа задания истинности в классе моделей данной логики. Например, в семантике Крипке смысл каждой связки определяется специальным условием вынуждения в конкретном мире.
В классической логике высказываний известно понятие функциональной полноты данного набора связок. Например, набор из отрицания и дизъюнкции функционально полон в семействе всех классических (булевых) связок, трактуемых как функции на двухэлементном множестве истинностных значений. При этом важно то, что класс всех булевых связок определен без ссылки на дизъюнкцию и отрицание, т.е. задан внешним определением.
Для многозначных логик понятие функциональной полноты трактуется аналогичным образом.
Однако в случае интуиционистской логики высказываний конечный адекватный набор истинностных значений невозможен, что было установлено еще К.Гёделем [23]. В связи с этим возникает т.н. проблема характеризации логических связок [26), заключающаяся в отыскании внешнего определения класса связок, в котором изначально подразумеваемый набор оказался бы функцис-
нально полным.
Применительно к модальной логике Д.Скотт [24] пишет: "Имея подходящее определение ..., мы, без сомнения, сможем показать, что единственными логическими операторами (одноместными — прим. авт.) являются -і, ->->, О, О".
С другой стороны, А.Трулстра в статье [25] выражает некоторое сомнение по поводу функциональной полноты набора стандартных интуиционистских связок: "Каждая из этих семантик (семантик интуиционистской пропозициональной логики — прим. авт.) математически намного сложнее, нежели стандартная классическая семантика. Нет оснований полагать, что класс операторов, опре--делимых через -*, V, Л, -і, является дефинициально полным для какой-либо из этих семантик".
Попытка формулировки внешнего определения класса стандартных интуиционистских связок с точки зрения моделей Крипке была предпринята Д.Маккалоу в [6]. Предложенные Д.Маккалоу определения позволяют легко доказать достаточность набора стандартных связок V, Л, —>, -і, однако искусственность самих определений (имеющих чисто синтаксический характер) не дает оснований считать, что проблема характеризации этого набора в указанной работе решена удовлетворительно (отметим, что этот вывод сделан Д.Маккалоу там же). В заключительном параграфе статьи Маккалоу содержится замечание о том, что логические связки не должны различать подобные модели; но эта идея дальнейшего развития не получила.
Цели и задачи диссертации.
Исследование стандартных и нестандартных логических связок интуиционистской логики высказываний с точки зрения:
полноты по П.С.Новикову;
семантической полноты дедуктивной системы в данном классе моделей;
семантической характеризации конкретных наборов связок.
Методология исследований
Первоначальные исследования по семантике неклассических логик велись исключительно на алгебраическом языке. В частности, модели интуиционистской логики и ее расширений представлялись как псевдобулевы алгебры (или алгебры Гейтинга) (Расёва Е. & Сикорский Р. [29]).
Работы С.Крипке по реляционной семантике модальных и интуиционистской логик позволили упростить и визуализировать многие понятия и результаты соответствующей теории.
Интуиционизм как раздел оснований математики нашел свое развитие в работах А.Трулстры, Г.Крайзеля, Д.ван Далена, А.Г.Драгалина и др.
В 70-е годы XX столетия объектом внимания стала чисто логическая проблематика неклассических логик. В этом контексте заметную роль сыграла книга П.С.Новикова [31].
В работах А.В.Кузнецова [32,33, 34,35] были поставлены и частично решены вопросы, специфичные именно для неклассических логик и давшие толчок последующему развитию: полнота, финитная аппроксимируемость, табличность, параметрическая выразимость, шефферовость, арифметическая доказуемость как модальная связка и др.
Усилиями ряда ученых было накоплено много фактов относительно отдельных неклассических логик (некоторые имена упомянуты в предыдущем разделе). По достижении массой фактов некоторого критического значения назрела необходимость выработки более общего взгляда на проблематику. Период первоначального накопления фактов постепенно стал уступать место систематическому анализу не отдельных логик, но всего разноообразия таковых как единого целого (Л.Л.Максимова & В.В.Рыбаков [41]).
Реляционная семантика позволила с помощью шкал строить модели, алгебраическое описание которых является практически необозримым. Мостом между алгебраической и реляционной семантикой явились теоремы о представлении произвольной псевдобулевой алгебры семейством конусов подходящей шкалы и связи между вложениями псевдобулевых алгебр и строго изотонными отображениями (р-морфиэмами) соответствующих шкал (Л.Л.Максимова [42]). Эти тео-
ремы позволили исследовать вопросы интерполяции и определимости в различных неклассических логиках (см. например работы Л.Л.Максимовой [43,44,45]). В нашей работе теорема о представлении и теорема о р-морфизмах являются "краеугольными камнями" всех результатов, касающихся понятия полноты по П.С.Нювикову.
Отмеченная в предыдущем разделе идея задавать интерпретацию дополнительных логических связок с помощью условия вынуждения в моделях Крипке была мредложена Л.Л.Максимовой (см. статью А.В.Бессонова [5]).
Следующим важным понятием является понятие т.н. пгхарактеристпической шкалы. Это понятие с успехом применялось для решения вопросов о допустимости правил вывода в неклассических логиках, о разрешимости V-фрагментов элементарных теорий свободных псевдо- и топобулевых алгебр, решениям уравнений над такими алгебрами (В.В.Рыбаков [36, 37, 38, 39]). Эти результаты были подытожены в монографии В.В.Рыбакова [40]. В нашей работе п-характеристические шкалы непосредственно применяются для построения примеров полных по Новикову логик с несколькими новыми константами и для оценкж общего числа таких логик.
Среди большого числа вопросов, связанных с неклассическими логиками, заметное место занимают вопросы алгоритмического распознавания тех или иных свойств неклассических логик. Положительные примеры (т.е. когда изучаемое свойство Л разрешимо) достаточно редки и основываются чаще всего на явном построении семейства расширений данной логики, удовлетворяющих Л, что позволяет описать эффективный позитивный тест1 для распознавания Л- В качестве примеров можно привести результаты о разрешимости интерполяционного свойства суперинтуиционистских логик (Максимова Л.Л. [43]), свойства анти-табличности расширений логики Геделя-Леба (А.В.Чагров & Л.А.Чагрова [50]).
Для доказательства неразрешимости тех или иных свойств логик применяется техника имитации двухленточных машин Минского (двухрегистровых абаков}. Эта техника была с успехом применена для доказательства алгоритмической неразрешимости целого ряда свойств (дизъюнктивное свойство, таб-
1 термин из книги Дж.Булоса и Р.Джеффри [46].
личность, финитная аппроксимируемость и др.) (Чагров А.В. [49], Захаръящев М.В. к. Чагров А.В [47], Чагрова Л.А. [48]). Эти исследования были подытожены в монографии А.В.Чагрова и М.В.Захарьящева [1]. В нашей работе техника имитации машин Минского применяется для доказательства алгоритмической неразрешимости проблемы консервативности ^-логик для случая двух или более дополнительных констант.
Следующей важной задачей представляется задача о разрешимости данной логики: найти алгоритм распознавания принадлежности произвольной формулы рассматриваемой логике. Одним из наиболее часто упоминаемых- критериев разрешимости является критерий Харропа [51]: если логика конечно-аксиоматизируема и финитно аппроксимируема, то она разрешима. В некоторых случаях удается доказать разрешимость и не финитно аппроксимируемых логик с помощью погружения в разрешимые слабые второпорядковые теории, такие, как слабая арифметика Бюхи или теория Рабина в языке с несколькими одноместными функциями (например, Дж.Бёрджесс [52]).
Следующим важным типом задач является построение аксиоматики логик, заданных семантически, т.е. посредством некоторого класса шкал. Результаты такого типа принято называть теоремами о (семантической) полноте исчисления относительно соответствующего класса шкал. Мы используем следующую методику: по данной непротиворечивой (относительно рассматриваемого исчисления) паре списков формул строится модель, в которой выполняются все формулы "положительной" компоненты и не выполняются все формулы "отрицательной" компоненты. В литературе имеется масса примеров применения этого метода, при этом примеры различаются по степени "участия творческого субъекта" в процессе построения моделей. Понятие канонической модели в этом смысле требует минимального "участия", т.е. все нужные свойства мадели следуют непосредственно из свойств самого исчисления. Недостатком канонических моделей является их необозримость.
Для построения обозримых моделей требуемого вида нужна более высокая степень "участия субъекта" в построении. Пример применения этого метода можно видеть в книге А.Г.Драгалина [30].
Для построения моделей ограниченной мощности в неклассических логиках
применяется метод фильтрации (например, Д.Габбай [57]). В нашей работе вариант метода фильтрации применяется в доказательстве разрешимости логики с константой бесконечного индекса.
Для переноса результатов с одного языка на другой широко применяется метод перевода. Под переводом понимается отображение класса формул одного языка в класс формул другого языка. Типичными примерами являются негативная интерпретация классической логики в интуиционистской, интерпретация интуиционистских формул посредством модальных (например, Максимова Л.Л & В.В;Рыбаков [41]). В нашей работе метод перевода применяется для построения новых примеров полных по П.С.Новикову логик на основе уже имеющихся.
Изучение связок, определимых в языке элементарной теории моделей Крип-ке, основано на понятии элементарного расширения и насыщенной модели (теория моделей первого порядка (Кейслер Дж. & Чэн Ч. [62]). В классической теории моделей 1-го порядка есть ряд теорем, связывающих теоретико-модельные свойства формул с их синтаксическим строением. Примеры: теорема Лося-Тарского показывает, что относительно перехода к подсистемам устойчивы универсальные формулы и только они; относительно строгих гомоморфизмов устойчивы условно экзистенциальные формулы и только они (условно экзистенциальные формулы имеют вид Vx{A(x) -* ЗуВ(,у)) (С.С.Гончаров)). В нашей работе аналогичная методика применяется для получения результатов о харак-теризации некоторых наборов связок как формул, устойчивых (в обе стороны) относительно р-морфизмов моделей Крипке.
Наконец, отметим, что с алгебраической точки зрения дополнительные интуиционистские связки представляют собой операторы на псевдобулеых алгебрах, поэтому данное направление может быть условно обозначено как "псевдобулевы алгебры с операторами". Параллельные ветви классической логики в настоящее время активно развиваются под названиями "булевы алгебры с операторами" (см., например, [56]) и "булевы алгебры с выделенными идеалами" (Д.Е.Пальчунов [53, 54, 55]).
Основные результаты диссертации
Язык интуиционистской логики высказываний Int расширяется путем добавления связок ф = {pi,..., ірп}. Каждая связка
Назовем ф-логикой произвольное множество формул языка С(ф), включающее Int, замкнутое относительно правил modus ponens, подстановки и замены эквивалентных2 для каждой дополнительной связки. ^-Логика L называется консервативной (над Int), если для любой чистой формулы D из D Є L следует D є Int.
Явным соотношением для связки <р{ называем формулу вида
Схемой замены эквивалентных называется множество формул вида
*.
Л ( *+ Ъ) - (D(Pi> .fti) +» Я(«і. . Чш,)). i=i
Если L — ^-логика и Г — множество формул, то через L + T будем обозначать наименьшую по включению ^-логику, содержащую і и Г.
Определение 1. ^-логика L, включающая схему замены эквивалентных, называется полной по Новикову, если она консервативна над Int и для любой формулы A . L <р-логика L + A неконсервативна над Int.
Обратим внимание на то, что П.С.Новиков наличие аксиом замены для дополнительных связок включает в число требований к ^-логикам. Известно, что при наличии аксиом замены правила замены эквивалентных становятся излишними. По видимому, это требование возникло на основе того, что Int содержит аксиому замены эквивалентных для каждой стандартной связки.
Определение 2. Связки
гдля одноместной связки у) v(A*X^iB\ и т.п.
(Pi, ф-лотика L + ipi(pi,. -,Pki) +* А неконсервативна над Int. Другими словами, никакое расширение L, консервативное над Int, не содержит явных соотношений.
Определение 2 можно рассматривать как обобщение известного результата о независимости стандартных связок в Int (Маккинси [7]): при присоединении к Int какого-то явного соотношения, например (р-»д)ч->Л(Л, V, ->)(р, q), образуется собственное расширение Int.
Заметим, что в подавляющем числе работ по нестандартным интуиционистским связкам говорится только об отсутствии явных соотношений в данной ^-логике. П.С.Новиков предложил более сильное условие: не только в данной ^-логике не должно быть явных соотношений, но также и ни в каком ее расширении, консервативном над Int.
Можно отметить аналогию с трактовкой отрицания в известном методе вы-нуждения: условие а вынуждает -*А, если никакое корректное расширение условия а не вынуждает А.
До работ автора не было известно ни одного примера полной по Новикову ^-логики.
Решение первоначальной проблемы Новикова для одной одноместной связки основано на известных примерах: логика Кузнецова и логика Габбая, описывающих варианты т.н. иррефлексивной модальности.
Теорема 1 Логика Кузнецова имеет единственное полное по Новикову расширение, являющееся конечно аксиоматизируемым и разрешимым. Аналогичный факт установлен и для логики Габбая.
Для случая нескольких дополнительных констант <р с использованием понятия п-характеристической модели [40] (в нашей терминологии — универсальной ф-шкалы) установлен следующий результат.
Теорема 2 Каждый конечный конус универсальной ф-шкалы определяет полную по Новикову ф-логику. При этом разным конусам соответствуют разные полные логики.
Каждая полная по Новикову (р-логика, соответствующая конечному конусу, конечно аксиоматизируема и разрешима. Если при этом константы образуют базис псевдобулевой алгебры подконусов выбранного конуса, то эта (р-логика не содержит явных соотношений.
Полностью решен вопрос о числе полных по Новикову логик для констант.
Теорема З В случае двух или более дополнительных констант существует континуум полных по Новикову (р-логик, в которых эти константы независимы. В случае единственной дополнительной константы (<р = {<р}) полные по Новикову (р-логики образуют явно описанную счетную последовательность. Каждая <р-логика из этой последовательности разрешима.
В связи с тем, что консервативность является краеугольным камнем в подходе П.С.Новикова, можно для данного набора связок (р сформулировать алгоритмическую проблему консервативности: по записи формулы А ^5-языка выяснить, является ли ^-логика Int + А консервативной над Int.
Ситуация с алгоритмической проблемой консервативности полностью прояснена:
Теорема 4 Для единственной дополнительной константы проблема консервативности разрешима.
Для двух и более дополнительных констант проблема консервативности неразрешима.
Для единственной одноместной дополнительной связки проблема консервативности неразрешима.
Кроме вышеперечисленного, в работе развит и семантический подход к понятию логической связки, намеченный в работах Маккалоу [6], Скотта [8] и Трулстры [9].
В рамках элементарной теории реляционных моделей в терминах монотонности и устойчивости при определенных отображениях моделей получена ха-рактеризация следующих наборов интуиционистских логических связок:
{V,A,-*,-.}, {V.A.-S-sQ}, {V, A,->,-., г, A}, {Y,A,->,-i,r,-,D}
(здесь О — модальный оператор типа универсальной необходимости, -, г — связки, дуальные связкам —>, -> соответственно)3.
Апробация работы.
Различные разделы работы докладывались на следующих мероприятиях:
Всесоюзные конференции по математической логике (1984, 1986, 1988, 1990, 1992)
2 Всесоюзная конф. по прикладной логике (Новосибирск 1988)
Научно-исследовательский семинар кафедры математической логики и теории алгоритмов МГУ
Logic Colloquhim'94 (Clermont-Fercande, France)
Logic Colloquium'96 (San-Sebastian, Spain)
Всероссийская конференция по логике'96 (Санкт-Петербург)
Goedel'96 (Brno, Czech Republic)
Computer Science Logic'96 (Utrecht, Netherlands)
Advances in Modal Logics'96 (Berlin, Germany)
Logic ColHoquium'97 (Leeds, UK)
Мальцевские чтения'97 (Новосибирск)
Мальцевские чтения'98 (Новосибирск)
Алгебраический семинар КГУ (Красноярск, 1998)
Международная конференция памяти А.И.Мальцева (Новосибирск, 1999)
Международная конференция "Логика и приложения" (Новосибирск, 2000)
'Точные формулировки ниже.