Непейвода Н.Н. - Прикладная логика [2017, PDF, RUS]

Введение ix
0.1. Что такое современная логика? . . . . . . . . . . . . . . . ix
0.2. Методологические принципы,
на которыx основано данное изложение . . . . . . . . . . xviii
0.3. Как работать с данной книгой? . . . . . . . . . . . . . . . xxv
0.4. Введение ко второму изданию . . . . . . . . . . . . . . . xxix
Часть I. Язык математики 1
1. Необходимость точного языка в математике 3
1.1. Как и почему появился язык математической логики? . . 3
1.2. Зачем изучать формальный язык математики? . . . . . . 9
2. Простейшие высказывания 15
2.1. Что такое высказывание? . . . . . . . . . . . . . . . . . . 15
2.2. Математическая интерпретация высказываний . . . . . . 21
2.3. Предметы и универс. Термы . . . . . . . . . . . . . . . . 22
2.4. Предикаты и элементарные формулы . . . . . . . . . . . 25
2.5. Некоторые обозначения . . . . . . . . . . . . . . . . . . . 27
3. Запись высказываний. Логические формулы 31
3.1. Связка ‘и’ . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
3.2. Связка ‘или’ . . . . . . . . . . . . . . . . . . . . . . . . . 33
3.3. Связка ‘следует’ . . . . . . . . . . . . . . . . . . . . . . . 33
3.4. Связка ‘тогда и только тогда’ . . . . . . . . . . . . . . . . 35
3.5. Связка ‘не’ . . . . . . . . . . . . . . . . . . . . . . . . . . 35
3.6. Таблицы истинности . . . . . . . . . . . . . . . . . . . . 35
3.7. ‘Для всеx’ . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
3.8. ‘Существует’ . . . . . . . . . . . . . . . . . . . . . . . . . 37
3.9. Ограниченные кванторы . . . . . . . . . . . . . . . . . . 38
4. Методы перевода с естественного языка
на математический и обратно 45
4.1. Кванторы. Области действия.
Свободные и связанные переменные . . . . . . . . . . . . 45
4.2. “Многоэтажные” кванторы.
Дополнительные ограничения . . . . . . . . . . . . . . . 46
4.3. «Если на клетке слона увидишь надпись “буйвол”,
не верь глазам своим» (Козьма Прутков) . . . . . . . . . 56
4.4. Равенство. Единственность и неединственность . . . . . 60
4.5. Таблицы истинности и формулировка отрицаний . . . . 66
4.6. Простейшие преобразования классическиx формул . . . 68
5. Базовые математические понятия 73
5.1. Множества. Диаграммы Эйлера и Венна . . . . . . . . . 73
5.2. Кортежи, n-ки, наборы, прямые произведения,
прямые суммы . . . . . . . . . . . . . . . . . . . . . . . . 84
5.3. Отношения . . . . . . . . . . . . . . . . . . . . . . . . . . 90
5.4. Функции . . . . . . . . . . . . . . . . . . . . . . . . . . . 99
5.5. Фактор-множества . . . . . . . . . . . . . . . . . . . . . . 116
5.6. Графы . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 121
5.7. Диаграммы . . . . . . . . . . . . . . . . . . . . . . . . . . 127
5.8. Слова . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 135
Часть II. Классическая логика 137
6. Индукция и определения 139
6.1. О разныx видаx индукции . . . . . . . . . . . . . . . . . . 139
6.2. Об индуктивныx определениях . . . . . . . . . . . . . . . 146
6.3. Трансфинитная индукция и ординалы . . . . . . . . . . . 151
6.3.1. Построение начального отрезка ординалов . . . . 151
6.3.2. Свойства вполне упорядоченных множеств . . . . 154
6.3.3. Представления ординалов.
Действия над ординалами . . . . . . . . . . . . . 157
6.3.4. Определение функций рекурсией
по определению либо параметру . . . . . . . . . . 163
7. Введение в синтаксис 167
7.1. Синтаксис логического языка . . . . . . . . . . . . . . . . 167
7.2. Свободные и связанные переменные. Подстановка . . . . 183
8. Семантика классической логики 189
8.1. Интерпретация языка конечныx типов . . . . . . . . . . . 190
8.2. Теория, модель, логическое следствие . . . . . . . . . . . 194
8.3. Теорема о замене эквивалентныx . . . . . . . . . . . . . . 200
8.4. Булевы алгебры и алгебраическая семантика . . . . . . . 201
8.5. Языки высшиx порядков . . . . . . . . . . . . . . . . . . 204
9. Семантические таблицы для классической логики 209
9.1. От таблиц истинностик семантическим таблицам . . . . 209
9.2. Правила разбиения формул в семантическиx таблицах . 211
9.3. Семантические таблицы с кванторами . . . . . . . . . . . 214
9.4. Сокращенные семантические таблицы . . . . . . . . . . 219
9.5. Исчисления традиционного типа . . . . . . . . . . . . . . 225
9.6. Секвенции и формализация семантическиx таблиц . . . . 233
9.7. Семантические таблицы с равенствоми для теорий . . . . 238
9.8. Теорема полноты . . . . . . . . . . . . . . . . . . . . . . . 242
9.9. Сечения . . . . . . . . . . . . . . . . . . . . . . . . . . . . 249
10. Элементы нестандартного анализа 260
10.1. Историческое введение . . . . . . . . . . . . . . . . . . . 260
10.2. Нестандартная модель . . . . . . . . . . . . . . . . . . . . 266
10.3. Нестандартная действительная ось . . . . . . . . . . . . 269
10.4. Нестандартные переформулировки . . . . . . . . . . . . 274
10.5. Суперструктуры и теорема Лося . . . . . . . . . . . . . . 278
10.5.1. Аксиома выбора, некоторые ее следствия
и альтернативы . . . . . . . . . . . . . . . . . . . 279
10.5.2. Ультрафильтры и структуры . . . . . . . . . . . . 283
11. Естественный вывод в классической логике 288
11.1. О структуре математическиx доказательств . . . . . . . . 288
11.2. Правила естественного вывода . . . . . . . . . . . . . . . 291
11.2.1. Общая структура. Импликация и конъюнкция . . 291
11.2.2. Дизъюнкция и разбор случаев . . . . . . . . . . . 293
11.2.3. Отрицание. Приведение к абсурду
и “от противного”. A ∨ ¬A . . . . . . . . . . . . . 295
11.2.4. Некоторые полезные выводимые правила . . . . . 297
11.2.5. Кванторы . . . . . . . . . . . . . . . . . . . . . . . 297
11.3. Естественный вывод как граф . . . . . . . . . . . . . . . 301
11.4. Правила формулировки отрицаний и согласованность
с классической истинностью . . . . . . . . . . . . . . . . 304
11.5. Теорема полноты естественного вывода . . . . . . . . . . 309
11.6. Логика с равенством и ее полнота . . . . . . . . . . . . . 315
11.7. Метод резолюций и его сравнение
с методом естественного вывода . . . . . . . . . . . . . . 316
11.8. Окольные пути как средство сокращения вывода . . . . . 323
11.9. Несколько слов о языке Пролог . . . . . . . . . . . . . . . 326
12. Основы теории определений 330
12.1. Определения в математике . . . . . . . . . . . . . . . . . 330
12.2. Сокращающие определения . . . . . . . . . . . . . . . . . 331
12.3. Теорема Крейга об интерполяции . . . . . . . . . . . . . 333
12.4. Теорема Бета об определимости . . . . . . . . . . . . . . 336
13. Неполнота и неформализуемость 339
13.1. Теорема Тарского о невыразимости истины . . . . . . . . 339
13.2. Аксиоматическое описание вычислимости . . . . . . . . 342
13.3. Представимость через доказуемость . . . . . . . . . . . . 354
13.4. Неполнота . . . . . . . . . . . . . . . . . . . . . . . . . . 361
13.5. Вокруг теоремы Гёделя . . . . . . . . . . . . . . . . . . . 364
13.6. Формализация неформализуемыx понятий . . . . . . . . 370
Часть III. Введение в неклассические логики 379
14. Основы λ-исчисления 381
14.1. Основы λ-языка . . . . . . . . . . . . . . . . . . . . . . . 381
14.2. λ-конверсии . . . . . . . . . . . . . . . . . . . . . . . . . 384
14.3. Теорема Черча-Россера . . . . . . . . . . . . . . . . . . . 391
14.4. λ-исчисление . . . . . . . . . . . . . . . . . . . . . . . . . 393
15. Корни неклассических логик 395
15.1. Корни неклассическиx логик в традиционной логике . . 395
15.1.1. Закон тождества . . . . . . . . . . . . . . . . . . . 395
15.1.2. Закон непротиворечия . . . . . . . . . . . . . . . 397
15.1.3. Закон исключенного третьего . . . . . . . . . . . 400
15.1.4. Закон достаточного основания . . . . . . . . . . . 400
15.1.5. Алгебраические законы логики . . . . . . . . . . 401
15.2. Сила и недостатки классической логики . . . . . . . . . . 404
15.3. Использование доказательств . . . . . . . . . . . . . . . . 405
15.3.1. Сведение новой задачи к уже решенным . . . . . 407
15.3.2. Выявление условий, при которых можно
пользоваться данным утверждением . . . . . . . 408
15.3.3. Получение построения,дающего
некоторый результат . . . . . . . . . . . . . . . . 410
15.3.4. Произнесение заклинания, дабы освятить
свое либо предложенное заказчиком решение . . 411
16. Интуиционистская логика 412
16.1. Создание интуиционистской логики . . . . . . . . . . . . 412
16.1.1. Брауэр: идея конструктивности . . . . . . . . . . 412
16.1.2. Интуиционизм и программа Гильберта . . . . . . 415
16.1.3. Формализация и первые интерпретации . . . . . 418
16.1.4. Разногласия и новые идеи . . . . . . . . . . . . . 419
16.1.5. Период после Брауэра . . . . . . . . . . . . . . . . 421
16.1.6. Вторая героическая эпоха:
математические результаты и попытки
приложений . . . . . . . . . . . . . . . . . . . . . 423
16.2. Интерпретация Колмогорова . . . . . . . . . . . . . . . . 423
16.3. Формализация Гейтинга . . . . . . . . . . . . . . . . . . . 430
16.4. Первые математические модели
интуиционистской логики . . . . . . . . . . . . . . . . . . 432
16.5. Модели Крипке . . . . . . . . . . . . . . . . . . . . . . . 434
16.6. Семантические таблицы
для интуиционистской логики . . . . . . . . . . . . . . . 438
16.7. Полнота семантическиx таблиц . . . . . . . . . . . . . . 442
16.8. Фундаментальные результаты теории доказательств . . . 443
16.9. Реализуемости и вариации
интуиционистскиx принципов . . . . . . . . . . . . . . . 444
16.10.Интуиционистская логика и категории . . . . . . . . . . 447
16.11.О формализации незнания . . . . . . . . . . . . . . . . . 449
17. Семантики Крипке и базирующиеся на них логики 452
17.1. Общая идея . . . . . . . . . . . . . . . . . . . . . . . . . . 452
17.2. Модальные логики и иx модели Крипке . . . . . . . . . . 455
17.2.1. Язык и общая конструкция модели . . . . . . . . 455
17.2.2. Свойства отношения достижимости
и конкретные логики . . . . . . . . . . . . . . . . 456
17.2.3. Нешкальные логики . . . . . . . . . . . . . . . . . 457
17.3. Вариации на тему модальностей и Крипке . . . . . . . . 458
17.3.1. Временные, динамические и
программные логики . . . . . . . . . . . . . . . . 458
18. Проблема отрицания 459
18.1. Три стороны классического отрицания
и четвертая — содержательного . . . . . . . . . . . . . . 459
18.2. Минимальная логика . . . . . . . . . . . . . . . . . . . . 461
18.3. Логика с сильным отрицанием . . . . . . . . . . . . . . . 463
18.4. Логика неполной информации . . . . . . . . . . . . . . . 465
18.5. Основы логики противодействия . . . . . . . . . . . . . . 466
18.6. Паранепротиворечивая логика . . . . . . . . . . . . . . . 467
19. Доказательства и программы 469
19.1. Изоморфизм Карри-Xоварда . . . . . . . . . . . . . . . . 469
19.2. Системы высшиx типов . . . . . . . . . . . . . . . . . . . 472
19.3. Призраки и классификация выводов . . . . . . . . . . . . 472
19.4. Теорема о верификации . . . . . . . . . . . . . . . . . . . 474
19.5. Проблема совместимости операторовна примере exit . . 476
Литература 479
Предметный указатель 482
Персоналии 489