Содержание к диссертации
Введение
Глава I. Теория логического вывода и табличный метод
1.1. Табличный метод и его история развития 17
1.2. Аксиоматический и табличный методы доказательства 31
1.3. Натуральный вывод и табличный метод 38
1.4. Связь табличного и секвенциального методов доказательства . 48
Глава II. Табличные конструкции и их применение в классической логике
II. 1. Семантический период развития табличного метода. Семантические таблицы Э. Бета и модельные множества Я. Хинтикки 77
II.2. Аналитический период развития табличного метода.
II.2.1. Аналитические таблицы Р. Смаллиана 85
II.2.2. Таблицы Фиттинга 115
Глава III. Табличные методы в неклассических логиках
III.1. Методы логического вывода и таблицы в интуиционистской логике
III.1.1. Теоретический анализ методов логического вывода в интуиционистской логике (аксиоматический, натуральный и секвенциальный вывод)
III.1.1.1. Аксиоматические системы интуиционистской логики 121
III.1.1.2. Натуральный вывод в интуиционистской логике 134
IIІ.1.1.3. Секвенциальные системы интуиционистской логики 138
III.1.2. Табличные методы в интуиционистской логике. Семантические таблицы Бета для систем интуиционистской логики 151
III.1.3. Аналитические таблицы для систем интуиционистской логики 159
III.1.4. Усовершенствованная табличная система Мильоли-Москато-Орнаги 176
III.1.5. Расширение табличного метода для интуиционистских логик на модальные системы. Системы Авеллоне-Феррари 181
III.2.Табличные методы в модальной логике
III.2.1. Теоретический анализ методов логического вывода в системах модальной логики (аксиоматический, натуральный и секвенциальный вывод)
III.2.1.1. Аксиоматические варианты систем модальной логики 190
III.2.1.2. Натуральный вывод в модальной логике 194
III.2.1.3. Секвенциальные системы модальной логики 199
III.2.2. Семантический анализ модальной логики методом таблиц. Семантические таблицы Крипке и модельные множества Хинтикки 206
III.2.3. Табличные методы Фиттинга для модальной логики 215
III.3. Применение табличных методов в многозначной логике
III.3.1. Теоретический анализ методов логического вывода в многозначной логике (аксиоматический, секвенциальный)
III.3.1.1. Системы гильбертовского типа в многозначной логике 230
III.3.1.2. Секвенциальные системы многозначной логики 240
III.3.2. Табличные методы в многозначной логике. Аналитические таблицы для систем многозначной логики 247
III.3.3. Табличный метод Карниелли. Систематизация конечнозначных логик через метод таблиц 266
III.3.4. Оптимизация табличного метода Карниелли. Таблицы для множеств-знаков Хэнла 277
III.3.5. Расширение табличного метода для конечнозначных логик на системы интуиционистской логики. Система Баса-Фермюллера 280
III.4. Методы логического вывода и таблицы в релевантной логике.
III.4.1. Теоретический анализ методов логического вывода в релевантной логике (аксиоматический, натуральный и секвенциальный вывод)
III.4.1.1 Аксиоматические системы релевантной логики 289
III.4.1.2. Системы натурального вывода в релевантной логике 300
III.4.1.3. Генценовские логистические исчисления для релевантных систем 303
III.4.1. Таблицы для систем релевантной логики
III.4.1.1. Таблицы для систем 308
III.4.1.2. Таблицы для релевантных систем с мультипликативными связками 315
III.4.1.3. Таблицы с индексированными формулами для релевантных систем 323
Заключение .327
Литература 330
- Связь табличного и секвенциального методов доказательства
- Семантический период развития табличного метода. Семантические таблицы Э. Бета и модельные множества Я. Хинтикки
- Табличные методы в интуиционистской логике. Семантические таблицы Бета для систем интуиционистской логики
- Табличные методы в многозначной логике. Аналитические таблицы для систем многозначной логики
Введение к работе
История логики XX века во многом представляет собой историю развития теории логического вывода. Результатом развития теории логического вывода стали в настоящее время широко известные методы доказательства — аксиоматический, натуральный, секвенциальный и табличный.
В отечественной и зарубежной историко-логической науке табличный метод доказательства до настоящего времени не нашел достойного освещения. Данное исследование рассматривает табличный метод как один из классических и традиционных методов доказательства, к которому, в современной теории логического вывода, несмотря на развитие в нем различных других процедур доказательства, направлений и тенденций, проявляется постоянный и устойчивый интерес. Как процедура доказательства, которая, вообще говоря, является удобной заменой генценовских исчислений, открывает хорошие перспективы исследования как важных теоретических, так и прикладных аспектов логических исчислений, табличный метод сам по себе является проблемой в истории теории логического вывода и вызывает оправданный исследовательский интерес.
Одним из главных преимуществ табличного вывода является то, что в нем наиболее ярко выражается связь, существующая между семантикой и синтаксисом логического исчисления. Особый интерес вызывает то, что именно табличный метод показывает нам те семантические связи, которые лежат в основании синтаксической структуры классической логики. Так
как правила построения табличного вывода соответствуют структуре обычных содержательных рассуждений, то выводы, полученные методом таблиц, оказываются более естественными, чем, выводы в рамках аксиоматического, натурального и секвенциального методов.
Важным и интересным представляется то, что табличные исчисления освобождают нас от необходимости многократного переписывания формул, появляющихся в выводе, что необходимо делать в секвенциальных исчислениях. Это свойство табличных исчислений намного сокращает вывод и делает его простым и ясным. Именно легкость и простота доказательства (при помощи таблиц) дает преимущество их использования во многих областях логики и не только.
Особый интерес вызывает то, что процесс доказательства многих теорем при использовании табличного метода упрощается. Так, Смаллиан пользуясь методом таблиц, доказал Теорему полноты и теорему компактности для классической логики, интерполяционную теорему и Основную теорему.
Отсутствие систематического обзора истории развития табличного метода диктует необходимость данного исследования.
Помимо сказанного о значимости темы в историко-логическом отношении, следует заметить, что результаты представленного исследования могут быть включены в контекст современных нам дискуссий по ряду ключевых вопросов теории автоматического вывода и искусственного интеллекта. Хотя табличный метод возник в логике и создавался для логики, он широко применяется в исследованиях по искусственному интеллекту, в частности в такой его области, как теория и практика автоматического доказательства теорем.
Степень разработанности темы.
Несмотря на отсутствие в нашей стране специальных исследований, посвященных табличному методу как целостному явлению, следует заметить, что отдельные вопросы, связанные с этой темой, рассматривались П.И.Быстровым, В.Н.Костюком, Н.Н.Непейводой, Д.А. Бочваром, В.К. Финном.
В иностранной научной литературе ситуация сложилась существенно иная. Хотя исследований, которые прямо ставили бы своей целью всестороннее рассмотрение истории развития табличного метода, не существует, имеется большое количество работ посвященных различным этапам развития данного метода доказательства. Среди фундаментальных исследований, отметим работы Э.Бета, Дж.Земана, С.Кангера, С.Клини, Р.Смаллиана, М.Фиттинга, С. Лиса, С.Крипке.
Важное значение для понимания табличного метода доказательства имеют исследования посвященные проблемам его применения и использования в неклассических логиках.
Исследования Я. Хинтикки, С.Крипке, П.И.Быстрова, В.Н.Костюка, Н.Н.Непейводы, М.Фиттинга, Э.Бета, С.Кангера, Р.Горе, Ф.Массачи, А.Мазини, Т.Боргуиса, Р.Голдблатта, П.Уолпера посвящены проблемам применения табличного метода доказательства в различных системах модальной логики.
Работы У. Сакона, С.Сурмы, В.Карниелли, Д.А. Бочвара, В.К. Финна, М.Бааза, Г.Фермюллера, Р.Хэнла рассматривают вопрос наиболее эффективного использования метода таблиц в многозначной логике.
Среди работ посвященных применению метода таблиц в интуиционистской логике следует выделить работы Э.Бета, М.Фиттинга, М.Феррари, Р.Мильоли, Р.Дюкхоффа, С.Крипке, А.Авеллоне, У.Москато, М.Орнаги.
Возможность использования табличного метода доказательства в релевантной логике рассматривалась в работах М. Мак-Робби, Н.Белнапа, П.И. Быстрова.
Чрезвычайно ценными для понимания места и роли табличного метода в истории теории логического вывода являются работы, посвященные проблеме использования данного метода в области искусственного интеллекта, в частности в области теории и практики автоматического доказательства теорем.
Среди работ, посвященных данной проблеме, отметим работы Э.Бета, РЛопплестона, И.Кохена, Л.Триллинга, П.Венера, К.Брода, И.Шенфелда, Л.Валлена, С.Ривса, А.Авеллоне, В.Москато, М.Орнаги, Ф.Массачи, П.Мильоли, П.Бонатти, Н.Бааз, Г.Фермюллер, Э.Эдера, Л. Уоллена.
Однако все вышеперечисленные работы посвящены частным проблемам развития табличных методов, поэтому возникла необходимость целостного рассмотрения истории развития табличного метода и применения его в различных логических системах.
Цель и задачи исследования.
Аналитический обзор литературы позволяет утверждать, что в истории современной логики отсутствуют работы, специально посвященные табличному методу доказательства.
Общей целью работы, таким образом, стало восполнение указанного пробела, т.е. исследование табличного метода доказательства как целостного явления в истории логического вывода: определение его хронологических рамок, этапов развития, характерных черт, анализ ключевых проблем и перспектив, связанных с дальнейшим развитием данного метода.
Для достижения сформулированной цели автором решались следующие задачи исследования:
1. Проведение анализа основных концепций и идей, имеющихся по теме исследования в историко-логическои литературе, ограничение хронологических и тематических рамок исследования, определение понятия табличного метода доказательства и уточнение его содержания, представление имеющихся подходов к периодизации этого метода доказательства.
2. Выявление особенностей процесса возникновения и развития табличного метода доказательства, рассматриваемого в связи с другими традиционными методами доказательства — аксиоматическим, натуральным, секвенциальным.
3. Проведение историко-логического анализа основных направлений и тенденций развития теории логического вывода на протяжении XX века.
4. Формирование представлений о наиболее эффективном методе логического вывода в рамках табличного метода доказательства.
5. Исследование причин усиления семантического аспекта логического вывода как теоретического базиса
11сление роли семантики в развитии различных методов доказательства.
6. Анализ новых решений традиционных логических проблем — табличное доказательство Теоремы полноты, Теоремы компактности, интерполяционной теоремы и Основной теоремы: оценка влияния табличного метода доказательства на возникновение новых методов доказательства в теории логического вывода.
7. Определение места и роли табличного метода доказательства в целом в истории теории логического вывода.
Методология исследования.
Автором использовались традиционные методы исследовательской работы: историко-логический анализ исследовательской литературы и сравнительный анализ различных концепций логического вывода.
Вместе с тем, в основу диссертационного исследования положены следующие теоретико-методологические принципы:
1. Исследование табличного метода доказательства как самостоятельного явления в теории логического вывода при одновременном рассмотрении его в контексте преобразования логической традиции (переходе от логик неклассического типа к логикам искусственного интеллекта).
2. Оптимальное (необходимое и достаточное для достижения цели работы) ограничение исследуемого материала, т.е. рассмотрение табличного метода доказательства в его наиболее существенных параметрах, с концентрацией внимания на интересующих нас ключевых моментах эффективного алгоритма поиска вывода. При этом за рамками работы остается
достаточно большое количество систем логического вывода, которые основаны на табличном методе доказательства или близки к нему.
3. Фокусирование внимания на проблемах, связанных с усовершенствованием и автоматизацией процесса вывода, а также рассмотрение этих ключевых вопросов не только в историко-логическом, но и в общефилософском плане.
Положения и выводы, выносимые на защиту:
1. Табличный метод доказательства представляет собой формальную процедуру доказательства, генетически связанную с предыдущими способами доказательства (аксиоматический, натуральный, секвенциальный).
2. Табличному методу доказательства соответствуют следующие хронологические рамки:
Начальный этап развития теории табличного метода доказательства — семантический этап, который составляют семантические таблицы Бета и модели Хинтикки.
Достижение технической простоты и эвристичности табличного метода было целью следующего — аналитического — этапа в развитии табличного метода. Так же как и на предыдущем этапе, эта цель была достигнута независимо друг от друга двумя логиками — С. Лисом и Р. Смаллианом.
Третий этап в развитии табличного метода состоял в использовании его в различных системах неклассических логик.
Современный последний этап развития табличного метода, подразумевает под собой «автоматизацию» табличного метода,
или возможность его применения в автоматическом поиске вывода.
3. Ведущая роль табличного метода доказательства в развитии теории логического вывода обусловлена уникальными особенностями данного метода — оптимальной структурой, а также созданием нового семантического направления развития теории логического вывода, учитывающего потребности современных неклассических логик и логик автоматического вывода.
4. В теории табличного метода доказательства произошло объединение двух путей развития теории логического вывода — синтаксического и семантического, которое не только изменило весь дальнейший ход развития методов логического вывода в XX в., но и продолжает воздействовать на структуру последующих форм доказательства. Табличные методы Бета, Смаллиана, Фиттинга, Лиса и др. являются одним из оснований, на которых строятся новые, более эффективные теории логического вывода.
5. Наибольшим вкладом табличного . метода доказательства в развитие теории логического вывода является: а. одно из главных преимуществ табличного вывода состоит в том, что в нем наиболее ярко выражается связь, существующая между семантикой и синтаксисом логического исчисления. Таким образом, именно табличный метод показывает нам те семантические связи, которые лежат в основании логической (синтаксической) структуры рассматриваемой логики. b. правила построения табличного вывода соответствуют способу обычных содержательных рассуждений, таким образом, выводы, полученные методом таблиц, оказываются более естественными, чем, выводы в рамках аксиоматического, натурального и секвенциального методов доказательства. c. в построении вывода с помощью табличного метода не участвуют более сложные формулы, чем исходная (доказываемая), и каждый шаг построения вывода детерминирован конечным числом альтернатив дальнейших логических шагов. d. процесс доказательства многих базовых теорем при использовании табличного метода упрощается. 6. Проблема алгоритма эффективного поиска вывода относится к числу фундаментальных логико-философских вопросов. Исследование того, как он решается в определенной системе, на определенном этапе развития логики, является одновременно и существенной характеристикой соответствующих системы и этапа развития. Проблема эффективного поиска вывода является своеобразной точкой превращения логик: от логик классического типа к логикам неклассического типа и комбинированным логикам, а от них уже к логикам автоматического типа.
Теоретическое и практическое значение.
Материал диссертации, использованные в ходе исследования методологические подходы и полученные результаты, заключающиеся в разработке теории табличного метода доказательства, позволяет углубить и дополнить понимание специфики процесса развития теории логического вывода, что имеет как теоретическую, так и практическую значимость.
В теоретическом отношении диссертация дает историко-логический анализ табличного метода доказательства, а также является применением описанных выше методологических принципов, позволяющих рассматривать процесс преобразования современной логической традиции в ее существенных параметрах.
В практическом отношении диссертация может служить восполнению пробела в учебной литературе для студентов и аспирантов, обучающихся по философским специальностям, а также студентов математического и психологического факультетов. Содержание и выводы работы могут применяться в преподавании общих и специальных курсов по математической логике.
Апробация исследования
Материал работы на протяжении ряда лет использовался автором при чтении общего курса математической логики и спецкурса «Философия математики» для студентов философского факультета Санкт-Петербургского университета.
Результаты работы представлялись автором в ходе различных научных форумов, среди которых:
1. Первый Общероссийский философский конгресс, Санкт- Петербург, июнь, 1997.
2. Современная логика: проблемы теории, истории и применения в науке, 5 Общероссийская научная конференция. Санкт- Петербург. 19 3. Смирновские чтения: 2 Международная конференция, Москва, 1999
4. Современная логика: проблемы теории, истории и применения в науке, 6 Общероссийская научная конференция. Санкт-Петербург. 2000
5. Современная логика: проблемы теории, истории и применения в науке, 7 Общероссийская научная конференция. Санкт-Петербург. 2002
6. «Дни Петербургской философии», 15-16 ноября. Круглый стол «Философия науки и техники»2002.
7. Смирновские чтения: 4 Международная конференция, Москва, 2003
8. Конференция «Рациональность и вымысел». Санкт-Петербург, 12-14 ноября. 2003.
Основные положения диссертации отражены в публикациях автора.
Структура диссертации. Диссертация состоит из введения, трех глав, заключения и списка литературы.
Связь табличного и секвенциального методов доказательства
Очевидно, что второе доказательство уже не содержит тех ужасных логических «трюков», которые содержались в первом доказательстве.
Таким образом, можно предположить, что значения логических связок в правилах натуральной дедукции фактически являются не классическими, а скорее конструктивными, и именно поэтому простые классические тавтологии с большим трудом доказываются в натуральном выводе, в том смысле, что их самое простое доказательство должно включать в себя такие логические «трюки», которые далеки от естественности. Так как эти правила непосредственно связаны с конструктивным значением логических связок, то когда мы используем эти правила для доказательства интуиционистских тавтологий, доказательство действительно оказывается естественным. Этот пример показывает, что естественный вывод является действительно «естественным» только для интуиционистских тавтологий (но не обязательно для всех из них).
Трудности в доказательстве классических тавтологий в натуральных исчислениях связаны еще и с тем фактом, что формула и ее отрицание не обращаются симметрично в натуральном выводе, в то время как именно это свойство требуется от классического значения логических знаков. Для сравнения приведем пример доказательства неинтуиционистского закона де Моргана методом таблиц, заметив при этом, что табличные правила обращают формулу и ее отрицание симметрично. Пример.
Таким образом, можно сделать предварительный вывод, что табличные доказательства более естественны, чем доказательства, проведенные с помощью правил натурального вывода, так как табличные правила, в отличие от правил натурального вывода, симметрично обратимы относительно отрицания. Однако несомненно, что симметричность табличных правил не является достаточной гарантией того, чтобы табличные правила всегда производили именно такие доказательства, которые естественны с классической точки зрения.
В свете предыдущего обсуждения становится очевидным, что решение вопроса дедуктивной эквивалентности систем натурального вывода табличным системам не будет легким по причине различного отношения к отрицанию в этих двух системах. Однако существует способ, который ведет от доказательства в натуральном выводе к соответствующим табличным доказательствам через эквивалентность обоих доказательству в секвенциальном исчислении. Подробнее об этом можно прочесть в работе Г. Сандхолма35.
Исследование натуральных исчислений приводит Г. Генцена к идее доказательства теоремы о нормальной форме, или Основной теоремы. Генцен пишет: «В основной теореме утверждается, что каждое чисто логическое доказательство может быть приведено к некоторой определенной, хотя и не однозначно, нормальной форме. Наиболее существенное свойство такого нормального доказательства можно выразить так: оно не содержит окольных путей. В него не вводится никаких понятий, кроме тех, которые содержатся в конечном результате и поэтому с необходимостью должны быть использованы для получения этого результата»36.
Так как натуральное исчисление оказалось непригодным для того, чтобы в подходящей форме сформулировать и доказать Основную теорему, Генцен формулирует особое — секвенциальное — исчисление. Секвенциальные исчисления впервые были рассмотрены Г. Генценом37 наряду с натуральными исчислениями. И прежде чем непосредственно рассмотреть секвенциальное исчисление, мы сделаем несколько общих замечаний относительно отличия данного исчисления от системы натурального вывода.
Секвенциальное исчисление, в отличие от системы натурального вывода, не содержит допущений, хотя сохраняет присущее натуральным исчислениям деление способов заключения на введение и удаление логических знаков. Правилам введения логических символов исчисления естественного вывода отвечают фигуры введения в сукцедент, а правилам удаления — фигуры введения в антецедент.
Аналогично выводу в натуральном исчислении, в секвенциальном исчислении используется представление вывода в виде дерева, но здесь при движении вниз по дереву переходят не от формулы к формуле, а от выводимости к выводимости. Таким образом, в этом исчислении происходит «вывод выводимостей». Д. Правиц отмечает: «Доказательство в исчислении секвенций можно рассматривать как инструкцию по конструированию соответствующего натурального вывода... Можно сказать, что доказательство в исчислении секвенций предписывает (в некоторой степени) определенный порядок построения соответствующего натурального вывода. Этот порядок часто не релевантен и только частично отражается в соответствующем натуральном выводе. Таким образом, различные выводы в секвенциальном исчислении могут Там же соответствовать (в указанном смысле) одному и тому же натуральному выводу».
Семантический период развития табличного метода. Семантические таблицы Э. Бета и модельные множества Я. Хинтикки
Если A v В входит в правую часть интуиционистской таблицы, то расщепляем эту таблицу «конъюнктивно» и пишем А в правой части одной из подтаблиц, а В - в правой части другой.
Если входит в левую часть интуиционистской таблицы, то пишем А в правой части этой таблицы, если в правой части уже нет формулы, к которой еще необходимо применять правила.
Несмотря на большую схожесть таблиц-доказательств, построенных Земаном, и таблиц Бета практически все правила обеих таблиц аналогичны, существует различие, которое заключается в том, что таблицы-доказательства основываются на обратимости правил в секвенциальных исчислениях, а таблицы Бета непосредственно связаны с понятием логического следования.
Итак, подводя итог вышесказанному, важно отметить следующие наиболее существенные свойства секвенциальных исчислений.
Во-первых, как и натуральные исчисления, они дают точный анализ логических связок, проясняя, каким образом каждая связка может быть введена в антецедент или в сукцедент секвенции. В натуральном исчислении для каждого логического знака существуют правила введения и удаления, в секвенциальном исчислении существуют только правила введения, а правила удаления принимают форму введения в антецедент. Генцен по-видимому не уделял этому особого внимания и рассматривал различия между двумя формулировками с чисто технической стороны. Во-вторых, их форма подтверждает истинность Основной теоремы: каждое доказательство может быть преобразовано в доказательство, которое свободно от сечения, а эти последние доказательства обладают таким замечательным свойством, как свойство подформульности. С теоретической точки зрения это свойство дает понятие чисто «аналитического» доказательства.
В-третьих, системы без структурных правил вывода, такие как EQ (EQ), Е\ (Е\) Матулиса, G Клини, соответствующие обратимым вариантам секвенциальных исчислений, с точки зрения практического поиска вывода обладают значительными преимуществами. В обратимых секвенциальных исчислениях для любого правила вывода секвенция-заключение выводима только в том случае, если выводимы секвенции-посылки. При этом, переходя от секвенции А, вывод которой мы хотим получить, к секвенциям (или секвенции), из которых А является выводимой по одному из правил, можно быть абсолютно уверенным в том, что в процессе вывода ничего не потеряно и мы не пользуемся такими секвенциями, которые в данном исчислении не являются выводимыми. Системы такого типа предполагают также интересную семантическую интерпретацию, непосредственно связанную с методом семантических таблиц Бета.
Несомненно, секвенциальные исчисления являются одним из самых эффективных методов доказательства, но при этом они обладают одним существенным недостатком. Если формула появляется на каком-то шаге доказательства, то она уже не исчезает и должна многократно переписываться на каждом шаге доказательства или как подформула, или как параметрическая формула. Рїзбавйться от этого недостатка позволяет табличный метод.
В заключении рассмотрим, какими же преимуществами обладает табличный метод по сравнению с другими методами доказательств — аксиоматическим, натуральным и секвенциальным.
Одним из главных преимуществ табличного вывода является то, что в нем наиболее ярко выражается связь, существующая между семантикой и синтаксисом логического исчисления. Таким образом, именно табличный метод показывает нам те семантические связи, которые лежат в основании логической (синтаксической) структуры рассматриваемой логики. Так как правила построения табличного вывода соответствуют структуре обычных содержательных рассуждений, то выводы, полученные методом таблиц, оказываются более естественными, чем, например, выводы в рамках аксиоматического метода. Табличный вывод, так же как и секвенциальный, обладает свойством пбдформульности. В процессе вывода исходная формула разбивается на свои подформулы. Таким образом, в построении вывода с помощью табличного метода не участвуют более сложные формулы, чем исходная (доказываемая), и каждый шаг построения вывода детерминирован конечным числом альтернатив дальнейших логических шагов. Если мы систематически применяем все правила построения табличного доказательства и при этом доказательство существует, то очевидно, что оно обязательно будет найдено. Но если доказательство не существует, тогда процесс построения вывода может никогда не закончиться. В таком случае табличный метод дает нам полуразрешающую процедуру.
На протяжении нашего исследования сравним табличный метод с такими общеизвестными методами доказательств, как аксиоматический, натуральный, секвенциальный в классической и неклассических логиках.
Табличные методы в интуиционистской логике. Семантические таблицы Бета для систем интуиционистской логики
Функции независимы между собой. Если решена задача a ZD b, то не всегда мы имеем решение задачи -па v b. В дальнейшем идеи Гейтинга-Колмогорова были развиты С. Клини, в концепции рекурсивной реализуемости. Первые исчисления интуиционистской логики были рассмотрены в работах В.И. Гливенко2, А.Н. Колмогорова3, Гейтинга4, Генцена5. Данные исчисления еще не содержали четкого конструктивного понимания математических суждений, поэтому позже, как отмечает Н.А. Шанин, «когда проблема конструктивного понимания суждений получила достаточное развитие, интуиционистские логические исчисления получили определенное истолкование. Эти исчисления оказались логическими исчислениями конструктивной математической логики, и в настоящее время их естественно называть конструктивными логическими исчислениями»6.
В СССР исследования в области конструктивной математики и логики начали успешно развиваться в середине 30-х годов XX столетия. Широко известны работы П.С. Новикова, А.А. Маркова, Н.А. Шанина. В дальнейшем, уже в 60-е годы, практически все математики, работающие в области теории доказательств, так или иначе были связаны с конструктивизмом. Как отмечает Г.Е. Минц, «практически все результаты, полученные для классической логики, исследовались затем относительно их интуиционистского применения» . Отметим сначала лишь вкратце (в дальнейшем рассмотрим более детально) некоторые важные результаты, полученные в области конструктивной математической логики.
Конструктивное исчисление с сильным отрицанием и алгоритм выводимости для формул данного исчисления были предложены Н.Н. Воробьевым8.
С.Ю. Маслов, Г.Е. Минц, В.П. Оревков9 доказали, что проблема выводимости неразрешима в конструктивном исчислении предикатов без функциональных знаков для класса формул, содержащих только одну одноместную предикатную переменную. Также В.П. Оревковым10 было доказано, что в конструктивном исчислении предикатов для класса формул типа -1-і V3 проблема выводимости неразрешима.
Конструктивное исчисление предикатов с обратимыми правилами вывода, предложенное Р.А. Плюшкявичюсом11, с точки зрения поиска вывода оказалось значительно более эффективным, чем остальные интуиционистские системы генценовского типа (Gi, G3). Обратимый секвенциальный вариант конструктивного исчисления предикатов с функциональными знаками и равенством предложил СЮ. Маслов . , Первые системы интуиционистской логики имели аксиоматическую форму. Так, система Рн, предложенная Гильбертом, представляет в удобной форме связь между полным аксиоматическим пропозициональным исчислением и интуиционистским пропозициональным исчислением. Таким образом, добавив к позитивному пропозициональному исчислению Гильберта Рр более слабую аксиому или аксиомы, содержащие отрицание, получаем формулировку интуиционистского пропозиционального исчисления Гейтинга. Следующая аксиоматическая формулировка, назовем ее Pls следуя А. Черчу1 , интуиционистского пропозиционального исчисления принадлежит Г. Шольцу и К. Шретеру. Исходными связками в исчислении Р1 являются = , л, v, -» и -і. Исчисление Pls имеет два правила вывода — modus ponens и правило подстановки. Аксиоматическая формулировка минимального пропозиционального исчисления А.Н. Колмогорова и И. Иогансона, назовем ее Р"о следуя Черчу, может быть получена из исчисления Pls заменой двух последних аксиом следующей: {(р z q) z ((р ZD -iq) = -і/?))) — закон приведения к абсурду. Важно отметить, что теоремы интуиционистского пропозиционального исчисления P s или минимального пропозиционального исчисления Pls, которые не содержат отрицания, совпадают с теоремами позитивного пропозиционального исчисления, а те теоремы какого-нибудь из исчислений Р1$, Pls или F, единственной связкой которых является :э, совпадают с теоремами импликативного пропозиционального исчисления. Аксиоматическая формулировка интуиционистского пропозиционального исчисления, предложенная М. Вайсбергом, использует константу /в качестве исходной связки вместо отрицания и добавляет к системе Р аксиому/з р. В заключение этого небольшого обзора аксиоматических систем интуиционистской логики рассмотрим более простую и «экономную» систему интуиционистской (конструктивной) логики, предложенную П.С. Новиковым . Предваряя формальное описание конструктивной системы Новикова, необходимо отметить, что здесь мы уже не можем ограничиться таким минимальным набором связок и логических констант Ои-і, как в классической системе Новикова, которая была рассмотрена нами в главе I. Причиной этого является невыводимость соответствующих теорем о выразимости одних связок через другие без закона исключенного третьего. Поэтому набор связок и логических констант, используемых в конструктивном исчислении, будет значительно расширен.
Табличные методы в многозначной логике. Аналитические таблицы для систем многозначной логики
Отношение между сверхсеквенциями, выводимыми в 2 и секвенциями, выводимыми в конструктивном исчислении G3, определяется следующим образом. Сверхсеквенция (1) называется односукцедентной, если множества Лг+ь ..., J„ попарно не пересекаются.
Теорема. Односукцедентная сверхсеквенция выводима в Q тогда и только тогда, когда хотя бы одна из сопряженных с ней секвенций выводима в G Следовательно, секвенция в сукцеденте которой не более одной формулы, выводима в Q тогда и только тогда, когда она выводима в Gs.
Если внимательно рассмотреть процесс поиска вывода в исчислении Q, то можно прийти к заключению, что он представляет собой лишь одновременное развитие процессов поиска вывода, происходящих в необратимом варианте конструктивного секвенциального исчисления. Однако как отмечает СЮ. Маслов «использование исчисления О приводит к экономии, связанной с возможностью одновременного выполнения для всех этих процессов ряда операций, например применения «снизу вверх» всех правил вывода, но также использование таких операций, как «прополка», «склеивание» и т.д.24».
С точки зрения эффективности поиска вывода равную позицию с обратимыми вариантами выводов занимают несократимые выводы. Подробное описание алгоритма поиска данного вывода для соответствующего конструктивного исчисления было рассмотрено Н.Н. Воробьевым . Суть данного метода заключается в следующем. Выводом в заключениях называется система заключений К рассматриваемая вместе с допустимыми схемами вида однозначно поставленными в соответствие к, каждому заключению, отличному от исходного. Таким образом, вывод в заключениях состоит из заключений и соответствующих им схем. Таким образом, вывод, содержащий систему заключений и соответствующие им схемы, называется несократимым, если любая подпоследовательность системы заключений вместе с соответствующими схемами не является выводом заключения Кк. Первые теоретико-доказательные исследования в области интуиционистской логики А. Гейтинга, Г. Генцена, А.Н. Колмогорова затрагивали только синтаксис интуиционистской логики, не касаясь ее семантики. Семантическую модель для интуиционистской логики впервые предложил Э.В. Бет1. Ему же принадлежит и первая табличная система интуиционисткой логики. Бет предложил ее в форме секвенциального исчисления, в котором, в отличие от секвенциального исчисления LJ Генцена, в сукцеденте секвенции может встречаться более одной формулы. Секвенция А\, Аг, ..., Ат- Ви #2, —, В„ является истинной, если всякий раз, когда модель М выполняет конъюнкции А\, Аг, .., Ат, она также выполняет дизъюнкцию В\, Вг, ..., Вп. Тогда модель М будет контрмоделью для секвенции Am- Bi, Z?2, .-., В„, если она выполнит конъюнкцию А\, Аг, , Ат, хотя не выполнит дизъюнкцию В\, В2,..., Вп.
Табличная система Бета непосредственно связана с интуиционистской системой Gz Клини и системой Гейтинга. Секвенция А\, Аг, ..., Ат является выводимой в системе Бета, если и только если она выводима в интуиционистской системе G$ Клини. Бет предложил также конструктивное доказательство эквивалентности его системы системе Генцена и доказал разрешимость и полноту интуиционистской табличной системы на основе семантического анализа.
Исходя из того факта, что табличное построение интуиционисткои логики Бета является весьма громоздким и трудным для рассмотрения, мы предлагаем более простой вариант этой системы, отличающийся техническими деталями.
Рассмотрим модификацию табличной системы интуиционистской логики Бета — систему LB. Синтаксис системы LB отличается от Ы тем, что LB оперирует с секвенциями, у которых в сукцеденте может быть более одной формулы. Заметим также, что поскольку система может содержать более одной формулы в сукцеденте, то возможны правила утончения и сокращения справа и слева. Правила —»z ,- V и аксиома, включающая ±, определяется секвенциями с по крайней мере одной формулой в сукцеденте, другие правила определяют отношения между секвенциями с множеством формул в сукцеденте.
