УДК 517.11(075)
ББК 22.12я73
Н53
Первое издание книги было частично поддержано Минвузом России,
гранты 94-1.17-336, программа «Фундаментальные исследования
в естествознании» и «Логические операторы», Новосибирский центр
по математическим наукам, 1996. Второе издание книги было
поддержано фирмой «Новософт», г. Новосибирск
Непейвода, Н. Н.
Н53
Прикладная логика : учебное пособие / Н. Н. Непейвода. —
3-е изд., существ. перераб. и доп. — Москва , Берлин : Директ-Медиа,
2019. — 575 с. : ил. DOI: 10.23681/561272
ISBN 978-5-4499-0126-2
Данное пособие содержит введение в язык современной математики и методы
современной логики, основные важнейшие для приложений и методологии результаты
логики ХХ века, советы по применению методов и методологии логики в информатике
и информационном анализе сложных задач, методологический и философский
анализ следствий приведённых результатов и методов. Впервые в мировой литературе
оно содержит систематическое изложение конструктивной математики с
точки зрения как современной информатики, так и многоуровневого анализа её
успехов и уроков. Его можно использовать совместно с обучающими программами
высокого уровня и программами проверки рассуждений, подобными AGDA.
Рекомендовано Государственным комитетом Российской Федерации по высшему
образованию в качестве учебного пособия для студентов высших учебных заведений,
обучающихся по специальностям «Математика», «Прикладная математика»,
«Лингвистика», «Философия» и «Психология».
Предыдущие версии книги выпущены издательствами УдГУ, 1997 (1-е издание);
НГУПресс, 2000 г. (2-е издание, исправленное и дополненное).
Текст приводится в авторской редакции.
УДК 517.11(075)
ББК 22.12я73
ISBN 978-5-4499-0126-2
© Непейвода Н. Н., текст, 2019
© Издательство «Директ-Медиа», оформление, 2019
Стр.3
Оглавление
Введение
In.1. Что такое современная логика?
In.2. Методологические принципы, на которых основано данное изложение
In.3. Как работать с данной книгой?
In.4. Введение ко второму изданию
In.5. Введение к третьему изданию
I Язык математики
1. Необходимость точного языка в математике
1.1. Как и почему появился яз к математической логики?
1.2. Зачем изучать формальный язык математики?
2. Простейшие высказывания
2.1. Что такое высказывание?
2.2. Математическая интерпретация высказываний
2.3. Предметы и унивёрс. Термы
2.4. Предикаты и элементарные формулы
2.5.
екоторе обозначения
3. Запись высказываний. Логические формулы
x
x
xix
xxiv
xxvii
xxviii
1
2
2
7
13
13
18
19
21
23
26
3 6 Таблицы истинности
30
ii
Стр.5
ОГЛАВЛЕНИЕ
4. Методы перевода с естественного языка на математический и обратно
4 1 Кванторы бласти действия
4.2. "Многоэтажные" кванторы. Дополнительные
ограничения
38
38
40
4.3. «Если на клетке слона увидишь надпись "буйвол", не верь глазам своим» 47
4.4. Таблицы истинности и формулировка отрицаний
4.5. ростейие преобразования классических формул
4.6.
арадокс кучи куч
4.7. Равенство. Единственность и неединственность
5. Базовые математические понятия
5.1. Множества. Диаграммы Эйлера и Венна
5.2. Кортежи, n-ки, наборы, прямые произведения, прямые суммы
5.3. тноени я
51
53
55
56
62
62
71
76
5 7 Графы
102
I I Классическая логика
6. Индукция
115
116
6.2. Об индуктивных определениях
6 3 Трансфинитная индукция и ординал
6.3.1. Построение начального отрезка ординалов
6.3.2. Свойства вполне упорядоченных множеств
6.3.3. Представления ординалов. Действия над ординалами
6.3.4.
7. Введение в синтаксис
121
125
125
127
130
остроение функций рекурсией по определени либо параметру 135
138
7.2. Корректность синтаксических определений
7.3. Свободные и связанные переменные. Подстановка
8. Семантика классической логики
8.2. Теория, модель, логическое следствие
8.3. Теорема о замене эквивалентнх
8.4. Булевы алгебры и алгебраическая семантика
8.5. Языки высших порядков
iii
145
150
155
159
163
164
167
Стр.6
ОГЛАВЛЕНИЕ
9. Семантические таблицы для классической логики
9.1.
9.2.
9.3. Семантические таблицы с кванторами
9.4. Сокраённ е семантические таблиц
9.5. Исчисления традиционного типа
9.6. Секвенции и формализация семантических таблиц
9.7. Семантические таблицы с равенством и для теорий
9.8. Теорема полноты
10. Элементы нестандартного анализа
10.2. естандартная модель
10.3. Hестандартная действительная ось
10.4. естандартне переформулировки
10.5. Суперструктуры и теорема Лося
т таблиц истинности к семантическим таблицам
равила разбиения формул в семантических таблицах
170
170
172
175
180
186
191
195
198
213
217
219
223
227
10.5.1. ксиома выбора, некоторые её следствия и альтернатив . . . . 227
10.5.2. льтрафильтры и структуры
11. Естественный вывод в классической логике
11.1. структуре математических доказательств
11.2. Правила естественного вывода
11.2.1. Общая структура. Импликация и конъюнкция
11.2.2. Дизъюнкция и разбор случаев
231
234
234
236
236
238
11.2.3. Отрицание. Приведение к абсурду и "от противного". A V —A . 239
11.2.4. Hекоторые полезные выводимые правила
240
11.3. Естественный вво д как граф
11.4. равила формулировки отрицанийи согласованность с классической
истинностью
11.5. Теорема полноты естественного вывода
11.6. Логика с равенством и ее полнота
11.7. Метод резолюций и его сравнение с методом
естественного вывода
11.8. Окольные пути как средство сокращения вывода
11.9. есколько слов о язк е ролог
12. Основы теории определений
12.2. Сокрааи е определения
12.3. Теорема рейга об интерполяции
12.4. Теорема Бета об определимости
iv
244
246
250
254
255
261
263
266
267
268
271
Стр.7
ОГЛАВЛЕНИЕ
13. еполнота и не ор ализуе ость
13.1. Теорема Тарского о невыразимости истины
13.2. Аксиоматическое описание вычислимости
13.3. редставимость через доказуемость
13.4. Неполнота
13.5. Вокруг теоремы Гёделя
13.6. Формализация неформализуемых понятий
13.7. онстр
II I Введение в неклассические логики
14. Основы λ-исчисления
14.2. λ-конверсии
14.3. Теорема о сходимости (Чёрча-Россера)
14.4. λ-исчисление
14.5. Комбинаторная логика
14.6. Эквивалентность S, K и λ-исчисления
14.7. Типизация
14.8. Эквивалентность вчислимости и λ
15. Корни неклассических логик
15.1. Корни неклассических логик в традиционной логике
15.1.1. Закон то дества
15.1.2. Закон непротиворечия
15.1.3. Закон исключённого третьего
15.1.4. Закон достаточного основания
15.2. Сила и недостатки классической логики
15.3. Использование доказательств
15.3.1. Сведение новой задачи к уже решенным
15.3.2. Вявление условий, при которх мо но пользоваться данным
утвердением
15.3.3. олучение построения, даег о некоторый результат
15.3.4. роизнесение заклинания, дабы освятить своё либо предло енное
заказчиком реени е
15.4. чём не принято говорить сейчас
16. Интуиционистская логика
16.1.1. Брауэр: идея конструктивности
16.1.2. Формализация и первые интерпретации
16.1.3. Разногласия и нов е идеи
16.1.4. ериод после Брауэра
v
273
273
275
285
291
292
297
302
305
306
308
313
315
316
319
320
323
324
324
324
326
327
328
331
332
333
334
335
336
337
339
339
342
342
343
Стр.8
ГЛВЛЕ Е
16.1.5. Вторая героическая эпоха: математические результаты и
поптки прило ений
16.2. нтерпретация реализуемости
16.3. ормализация Гливенко-Гейтинга
16.4. ервые модели интуиционистской логики
16.5. одели Крипке
16.6. Семантические таблицы для интуиционистской логики
16.7. Полнота семантических таблиц
16.8. Фундаментальные результаты теории доказательств
16.9. Реализуемости и вариации интуиционистских принципов
16.10. нтуиционистская логика и категории
17. Семантики Крипке и базирующиеся на них логики
17.1. ба я идея
17.2. одальные логики и их модели Крипке
17.2.1. Язык и общая конструкция модели
17.3. Временные, динамические и программные логики
18. роблема отрицания
18.3. Логика с сильнм отрицанием
18.4. Логика неполной информации
18.5. снов логики противодействия
18.6. Паранепротиворечивая логика
IV Конструктивные и методологические аспекты логики
19. Конструктивизм
19.2. Соглашения об обозначениях
19.3. Предпосылки конструктивизма
19.4. Появление конструктивизма
19.4.1. Интуиционизм и программа Гильберта
19.5. Базовые принцип и методы конструктивизма
19.5.1. Принцип конечной информации и чум-пространства
19.5.2.
етод провокации и некорректные задачи
19.6. нтуиционистская логика как конструктивная
vi
345
345
351
353
355
359
364
365
369
371
374
374
376
376
17.2.2. Свойства отноения достиимости и конкретные логики . . . 377
17.2.3. Нешкальные логики
378
379
381
18.1. Три стороны классического отрицания и четвёртая — содержательного 381
18.2. инимальная логика
383
384
386
387
388
389
391
392
393
397
400
403
403
410
418
Стр.9
ГЛВЛЕ Е
20. лгорит
и реализуе ость
20.2. Советский конструктивизм
20.3. Недостатки советского конструктивизма
21. Интуиционизм как альтернатива алгоритмическому конструктивизму
21.1.
формализации незнания
21.2. ромеуточные вариант конструктивизма
21.3. одели конструктивных теорий
21.4. Различие вместо равенства
21.5. нализ логических принципов
21.6. еудачная попытка прило ения
22. Доказательства и программы
22.2. Систем вси х типов
22.3. ризраки и классификация выводов
22.4. Теорема о верификации
22.5. Проблема совместимости операторов на примере exit
23. Методологические следствия теорем о неполноте
23.1. бобённ е вчислительные систем
23.2. бобение колмогоровской сло ности
23.3. бобение теоремы Чейтина
23.4. бобённая теорема Гёделя о неполноте
23.5. Алгоритмическая случайность и антиномии Канта
23.6. Закон комитета
23.7. Трёхглавый дракон
23.8. редел Чейтина и парадокс изобретателя
23.9. Следствия для организации творческой работы
23.10Предел Чейтина и языки программирования
24. Прикладная логика
25. Формализация и деформализация
25.2. роцесс реени я задачи
428
430
437
445
445
448
450
451
451
456
459
461
462
463
464
467
467
470
471
472
473
476
477
479
481
483
485
489
490
25.4.2. Вбо р логики
25.4.3. Замена понятий
25.4.4. странение меаи х факторов
25.4.5. Эффективность
vii
493
500
500
501
Стр.10
ГЛВЛЕ Е
25.6. еформализация
25.6.1. Нетривиальность процесса деформализации
25.6.2. спекты деформализации
25.7. Эстетика, эффективность и адекватность
25.8. Следствия и благодарности
би е принцип и вво д . Ванейи е определения
504
504
504
506
508
510
viii
Стр.11
Список иллюстраций
1.1 Схема деятельности информатика и аналитика
2.1 Четр е точки
8
22
5.2
равильная диаграмма Венна
5.3 Правильная диаграмма Венна для неправильного тождества
5.4
еправильная диаграмма Венна
5.5 x — y — целое число
5.6
5.7
5.8 Граф
5.9
иаграммы Гессе двух ваны х пятиэлементнх мно еств
нъекция и накртие, сръекция и ретракция
иаграммы для прямого произведения
5.10 иаграммы для прямой суммы
6.1
редло ение о внутренних углах многоугольника
6.2 Формула и соответствующее ей дерево
66
66
67
76
81
87
103
106
107
119
123
16 2 AA Гейтинг
16.3 Топологическая интерпретация A V —A
16 4 провергаи е модели Крипке
16.5 Сильно опровергаа я модель Крипке
18.1 Ян мос оменский
351
355
357
357
390
ix
Стр.12