Современные проблемы использования табличных методов в логике

Краткое описание

Оглавление

Введение...6

Глава I. Теория логического вывода и табличный метод

1.1. Табличный метод и его история развития...17

1.2. Аксиоматический и табличный методы доказательства...31

1.3. Натуральный вывод и табличный метод...38

1.4. Связь табличного и секвенциального методов # доказательства...48

Глава II. Табличные конструкции и их применение в классической логике

ИЛ. Семантический период развития табличного метода. Семантические таблицы Э. Бета и модельные множества

Я. Хинтикки...77

Ц.2. Аналитический период развития табличного метода.

П.2.1. Аналитические таблицы Р. Смаллиана...85

И.2.2. Таблицы Фиттинга...115

Глава III. Табличные методы в неклассических

логиках

III. 1. Методы логического вывода и таблицы в

интуиционистской логике

IH.1.1. Теоретический анализ методов логического

вывода в интуиционистской логике (аксиоматический,

натуральный и секвенциальный вывод)

Ш. 1.1.1. Аксиоматические системы интуиционистской

логики...121

Ш. 1.1.2. Натуральный вывод в интуиционистской

логике...134

Ш. 1.1.3. Секвенциальные системы интуиционистской

логики...138

III. 1.2. Табличные методы в интуиционистской логике. Семантические таблицы Бета для систем

интуиционистской логики...151

Ш.1.3. Аналитические таблицы для систем

интуиционистской логики...159

III. 1.4. Усовершенствованная табличная система Мильоли-

Москато-Орнаги...176

Ш.1.5. Расширение табличного метода для интуиционистских логик на модальные системы. Системы Авеллоне-Феррари...181

Ш.2.Табличные методы в модальной логике

Ш.2.1. Теоретический анализ методов логического вывода в системах модальной логики (аксиоматический, натуральный и секвенциальный вывод) Ш.2.1.1. Аксиоматические варианты систем модальной

логики...190

Ш.2.1.2. Натуральный вывод в модальной

логике...194

Ш.2.1.3. Секвенциальные системы модальной

логики...199

1П.2.2. Семантический анализ модальной логики методом таблиц. Семантические таблицы Крипке и модельные множества Хинтикки...206

Ш.2.3. Табличные методы Фиттинга для модальной

логики...215

Ш.З. Применение табличных методов в многозначной

логике

Ш.З Л. Теоретический анализ методов логического

вывода в многозначной логике (аксиоматический,

секвенциальный)

Ш.З. 1.1. Системы гильбертовского типа в многозначной

логике...230

Ш.З. 1.2. Секвенциальные системы многозначной

логики...240

Ш.З.2. Табличные методы в многозначной логике. Аналитические таблицы для систем многозначной

логики...247

Ш.3.3. Табличный метод Карниелли. Систематизация

конечнозначных логик через метод таблиц... .266

Ш.З.4. Оптимизация табличного метода Карниелли.

Таблицы для множеств-знаков Хэнла...277

Ш.З.5. Расширение табличного метода для конечнозначных логик на системы интуиционистской

логики. Система Баса-Фермюллера...280

Ш.4. Методы логического вывода и таблицы в

релевантной логике.

Ш.4.1. Теоретический анализ методов логического

вывода в релевантной логике (аксиоматический,

натуральный и секвенциальный вывод)

Ш.4.1.1 Аксиоматические системы релевантной

логики...289

Ш.4.1.2. Системы натурального вывода в релевантной

логике...300

Ш.4.1.3. Генценовские логистические исчисления для

релевантных систем...303

Ш.4.1. Таблицы для систем релевантной логики

Ш.4.1.1. Таблицы для систем ?"_,_., R^-, ЯМ-,_ ...308

Ш.4.1.2. Таблицы для релевантных систем с

мультипликативными связками...315

Ш.4.1.3. Таблицы с индексированными формулами для

релевантных систем...323

Заключение...327

Литература...330
Введение

ВВЕДЕНИЕ

ОБЩАЯ ХАРАКТЕРИСТИКА РАБОТЫ Актуальность темы исследования.

История логики XX века во многом представляет собой историю развития теории логического вывода. Результатом развития теории логического вывода стали в настоящее время широко известные методы доказательства — аксиоматический, натуральный, секвенциальный и табличный.

В отечественной и зарубежной историко-логической науке табличный метод доказательства до настоящего времени не нашел достойного освещения. Данное исследование рассматривает табличный метод как один из классических и традиционных методов доказательства, к которому, в современной теории логического вывода, несмотря на развитие в нем различных других процедур доказательства, направлений и тенденций, проявляется постоянный и устойчивый интерес. Как процедура доказательства, которая, вообще говоря, является удобной заменой генценовских исчислений, открывает хорошие перспективы исследования как важных теоретических, так и прикладных аспектов логических исчислений, табличный метод сам по себе является проблемой в истории теории логического вывода и вызывает оправданный исследовательский интерес.

Одним из главных преимуществ табличного вывода является то, что в нем наиболее ярко выражается связь, существующая между семантикой и синтаксисом логического исчисления. Особый интерес вызывает то, что именно табличный метод показывает нам те семантические связи, которые лежат в основании синтаксической структуры классической логики. Так

как правила построения табличного вывода соответствуют структуре обычных содержательных рассуждений, то выводы, полученные методом таблиц, оказываются более естественными, чем, выводы в рамках аксиоматического, натурального и секвенциального методов.

Важным и интересным представляется то, что табличные исчисления освобождают нас от необходимости многократного переписывания формул, появляющихся в выводе, что необходимо делать в секвенциальных исчислениях. Это свойство табличных исчислений намного сокращает вывод и делает его простым и ясным. Именно легкость и простота доказательства (при помощи таблиц) дает преимущество их использования во многих областях логики и не только.

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

Отсутствие систематического обзора истории развития табличного метода диктует необходимость данного исследования.

Помимо сказанного о значимости темы в историко-логическом отношении, следует заметить, что результаты представленного исследования могут быть включены в контекст современных нам дискуссий по ряду ключевых вопросов теории автоматического вывода и искусственного интеллекта. Хотя табличный метод возник в логике и создавался для логики, он широко применяется в исследованиях по искусственному

интеллекту, в частности в такой его области, как теория и практика автоматического доказательства теорем.

Степень разработанности темы.

Несмотря на отсутствие в нашей стране специальных исследований, посвященных табличному методу как целостному явлению, следует заметить, что отдельные вопросы, связанные с этой темой, рассматривались П.И.Быстровым, В.Н.Костюком, Н.Н.Непейводой, Д.А. Бочваром, В.К. Финном.

В иностранной научной литературе ситуация сложилась существенно иная. Хотя исследований, которые прямо ставили бы своей целью всестороннее рассмотрение истории развития табличного метода, не существует, имеется большое количество работ посвященных различным этапам развития данного метода доказательства. Среди фундаментальных исследований, отметим работы Э.Бета, Дж.Земана, С.Кангера, С.Клини, Р.Смаллиана, М.Фиттинга, С. Лиса, С.Крипке.

Важное значение для понимания табличного метода доказательства имеют исследования посвященные проблемам его применения и использования в неклассических логиках.

Исследования Я. Хинтикки, С.Крипке, П.И.Быстрова, В.Н.Костюка, Н.Н.Непейводы, М.Фиттинга, Э.Бета, С.Кангера, Р.Горе, Ф.Массачи, А.Мазини, Т.Боргуиса, Р.Голдблатта, П.Уолпера посвящены проблемам применения табличного метода доказательства в различных системах модальной логики.

Работы У. Сакона, С.Сурмы, В.Карниелли, Д.А. Бочвара, В.К. Финна, М.Бааза, Г.Фермюллера, Р.Хэнла рассматривают вопрос наиболее эффективного использования метода таблиц в многозначной логике.

Среди работ посвященных применению метода таблиц в интуиционистской логике следует выделить работы Э.Бета, М.Фиттинга, М.Феррари, Р.Мильоли, Р.Дюкхоффа, С.Крипке, А.Авеллоне, У.Москато, М.Орнаги.

Возможность использования табличного метода доказательства в релевантной логике рассматривалась в работах М. Мак-Робби, Н.Белнапа, П.И. Быстрова.

Чрезвычайно ценными для понимания места и роли табличного метода в истории теории логического вывода являются работы, посвященные проблеме использования данного метода в области искусственного интеллекта, в частности в области теории и практики автоматического доказательства теорем.

Среди работ, посвященных данной проблеме, отметим работы Э.Бета, РЛопплестона, И.Кохена, Л.Триллинга, П.Венера, К.Брода, И.Шенфелда, Л.Валлена, СРивса, А.Авеллоне, В.Москато, М.Орнаги, Ф.Массачи, П.Мильоли, П.Бонатти, Н.Бааз, Г.Фермюллер, Э.Эдера, Л. Уоллена.

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

Цель и задачи исследования.

Аналитический обзор литературы позволяет утверждать, что в истории современной логики отсутствуют работы, специально посвященные табличному методу доказательства.

10

Общей целью работы, таким образом, стало восполнение указанного пробела, т.е. исследование табличного метода доказательства как целостного явления в истории логического вывода: определение его хронологических рамок, этапов развития, характерных черт, анализ ключевых проблем и перспектив, связанных с дальнейшим развитием данного метода.

Для достижения сформулированной цели автором решались следующие задачи исследования:

1. Проведение анализа основных концепций и идей, имеющихся по теме исследования в историко-логической литературе, ограничение хронологических и тематических рамок исследования, определение понятия табличного метода доказательства и уточнение его содержания, представление имеющихся подходов к периодизации этого метода доказательства.

2. Выявление особенностей процесса возникновения и развития табличного метода доказательства, рассматриваемого в связи с другими традиционными методами доказательства — аксиоматическим, натуральным, секвенциальным.

3. Проведение историко-логического анализа основных направлений и тенденций развития теории логического вывода на протяжении XX века.

4. Формирование представлений о наиболее эффективном методе логического вывода в рамках табличного метода доказательства.

5. Исследование причин усиления семантического аспекта логического вывода как теоретического базиса

11

табличного метода доказательства, осмысление роли семантики в развитии различных методов доказательства.

6. Анализ новых решений традиционных логических проблем — табличное доказательство Теоремы полноты, Теоремы компактности, интерполяционной теоремы и Основной теоремы: оценка влияния табличного метода доказательства на возникновение новых методов доказательства в теории логического вывода.

7. Определение места и роли табличного метода доказательства в целом в истории теории логического вывода.

Методология исследования.

Автором использовались традиционные методы исследовательской работы: историко-логический анализ исследовательской литературы и сравнительный анализ различных концепций логического вывода.

Вместе с тем, в основу диссертационного исследования положены следующие теоретико-методологические принципы:

1. Исследование табличного метода доказательства как самостоятельного явления в теории логического вывода при одновременном рассмотрении его в контексте преобразования логической традиции (переходе от логик неклассического типа к логикам искусственного интеллекта).

2. Оптимальное (необходимое и достаточное для достижения цели работы) ограничение исследуемого материала, т.е. рассмотрение табличного метода доказательства в его наиболее существенных параметрах, с концентрацией внимания на интересующих нас ключевых моментах эффективного алгоритма поиска вывода. При этом за рамками работы остается

12

достаточно большое количество систем логического вывода, которые основаны на табличном методе доказательства или близки к нему.

3. Фокусирование внимания на проблемах, связанных с усовершенствованием и автоматизацией процесса вывода, а также рассмотрение этих ключевых вопросов не только в историко-логическом, но и в общефилософском плане.

Положения и выводы, выносимые на защиту:

1. Табличный метод доказательства представляет собой формальную процедуру доказательства, генетически связанную с предыдущими способами доказательства (аксиоматический, натуральный, секвенциальный).

2. Табличному методу доказательства соответствуют следующие хронологические рамки:

Начальный этап развития теории табличного метода доказательства — семантический этап, который составляют семантические таблицы Бета и модели Хинтикки.

Достижение технической простоты и эвристичности табличного метода было целью следующего — аналитического — этапа в развитии табличного метода. Так же как и на предыдущем этапе, эта цель была достигнута независимо друг от друга двумя логиками — С. Лисом и Р. Смаллианом.

Третий этап в развитии табличного метода состоял в использовании его в различных системах неклассических логик.

Современный последний этап развития табличного метода, подразумевает под собой «автоматизацию» табличного метода,

13

или возможность его применения в автоматическом поиске вывода.

3. Ведущая роль табличного метода доказательства в развитии теории логического вывода обусловлена уникальными особенностями данного метода — оптимальной структурой, а также созданием нового семантического направления развития теории логического вывода, учитывающего потребности современных неклассических логик и логик автоматического вывода.

4. В теории табличного метода доказательства произошло объединение двух путей развития теории логического вывода — синтаксического и семантического, которое не только изменило весь дальнейший ход развития методов логического вывода в XX в., но и продолжает воздействовать на структуру последующих форм доказательства. Табличные методы Бета, Смаллиана, Фитганга, Лиса и др. являются одним из оснований, на которых строятся новые, более эффективные теории логического вывода.

5. Наибольшим вкладом табличного . метода доказательства в развитие теории логического вывода является:

а. одно из главных преимуществ табличного вывода состоит в том, что в нем наиболее ярко выражается связь, существующая между семантикой и синтаксисом логического исчисления. Таким образом, именно табличный метод показывает нам те семантические связи, которые лежат в основании логической (синтаксической) структуры рассматриваемой логики.

14

b. правила построения табличного вывода соответствуют способу обычных содержательных рассуждений, таким образом, выводы, полученные методом таблиц, оказываются более естественными, чем, выводы в рамках аксиоматического, натурального и секвенциального методов доказательства.

c. в построении вывода с помощью табличного метода не участвуют более сложные формулы, чем исходная (доказываемая), и каждый шаг построения вывода детерминирован конечным числом альтернатив дальнейших логических шагов.

d. процесс доказательства многих базовых теорем при использовании табличного метода упрощается.

6. Проблема алгоритма эффективного поиска вывода относится к числу фундаментальных логико-философских вопросов. Исследование того, как он решается в определенной системе, на определенном этапе развития логики, является одновременно и существенной характеристикой

соответствующих системы и этапа развития. Проблема эффективного поиска вывода является своеобразной точкой превращения логик: от логик классического типа к логикам неклассического типа и комбинированным логикам, а от них уже к логикам автоматического типа.

Теоретическое и практическое значение.

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

15

понимание специфики процесса развития теории логического вывода, что имеет как теоретическую, так и практическую значимость.

В теоретическом отношении диссертация дает историко-логический анализ табличного метода доказательства, а также является применением описанных выше методологических принципов, позволяющих рассматривать процесс преобразования современной логической традиции в ее существенных параметрах.

В практическом отношении диссертация может служить восполнению пробела в учебной литературе для студентов и аспирантов, обучающихся по философским специальностям, а также студентов математического и психологического факультетов. Содержание и выводы работы могут применяться в преподавании общих и специальных курсов по математической логике.

Апробация исследования

Материал работы на протяжении ряда лет использовался автором при чтении общего курса математической логики и спецкурса «Философия математики» для студентов философского факультета Санкт-Петербургского университета.

Результаты работы представлялись автором в ходе различных научных форумов, среди которых:

1. Первый Общероссийский философский конгресс, Санкт-Петербург, июнь, 1997.

2. Современная логика: проблемы теории, истории и применения в науке, 5 Общероссийская научная конференция. Санкт-Петербург. 1998

16

3. Смирновские чтения: 2 Международная конференция, Москва, 1999

4. Современная логика: проблемы теории, истории и применения в науке, 6 Общероссийская научная конференция. Санкт-Петербург. 2000

5. Современная логика: проблемы теории, истории и применения в науке, 7 Общероссийская научная конференция. Санкт-Петербург. 2002

6. «Дни Петербургской философии», 15-16 ноября. Круглый стол «Философия науки и техники»2002.

7. Смирновские чтения: 4 Международная конференция, Москва, 2003

8. Конференция «Рациональность и вымысел». Санкт-Петербург, 12-14 ноября. 2003.

Основные положения диссертации отражены в публикациях автора.

Структура диссертации. Диссертация состоит из введения, трех глав, заключения и списка литературы.

17

Глава I. Теория логического вывода и табличный метод 1.1. Табличный метод и его история развития

Табличный метод — формальная процедура доказательства, которая на сегодня существует во многих вариантах и для различных логик. Однако табличный метод имеет также несколько характерных свойств, которые практически никогда не изменяются.

Таблица для формулы X — это упорядоченное дерево, в котором точки есть формулы и которая построена следующим образом.

Сначала рассмотрим структуру, определяющую неистинность формулы. Для этого вводятся два знака: Т и F. Обозначенными будут считаться соответственно формулы вида FX и ТХ, где X — формула. Тогда FX — структура, которая определяет неистинность X. Таким образом, табличное доказательство начинается с FX.

Далее нам необходимы правила для разбиения обозначенных формул на подформулы. Для простоты ограничимся логическими связками =э и -I. Значение отрицания очевидно. Из Т —X получается FX, из F —X получаем ТХ. Эти правила могут быть представлены следующим образом:

T-JC F-JC

FX ТХ

Правила для = более сложные. Из таблиц истинности известно, что если X z Y является ложным, то X является истинным, a Y ложным. Если X z Y истинно, то либо X ложно, либо Y истинно. Это подразумевает разделение на два случая.

Список литературы