- •Ф.К. Алиев, и.А. Юров
- •Введение
- •Основные способы задания двоичных функций
- •1.1. Табличный способ задания
- •1.2. Геометрический способ задания
- •1.3. Задание двоичных функций формулами
- •Основные способы задания двоичных функций (продолжение)
- •2.1. Нормальные формы двоичных функций
- •2.2. Многочлен Жегалкина и действительный многочлен двоичной функции
- •2.3. Теорема о разложении в ряд Фурье
- •Полнота и замкнутость. Критерий полноты системы. Функционально полные системы. Замкнутые классы булевых функций
- •3.1. Полнота и замкнутость. Функционально полные системы
- •3.2. Замкнутые классы булевых функций
- •3.3. Критерий полноты системы булевых функций
- •4.1. Псевдобулевы функции
- •4.2. Функции k-значной логики
- •5.1 Минимизация двоичных функции
- •5.2. Геометрическая интерпретация минимизации днф
- •6.1. Метод Квайна — Мак-Класки нахождения сокращённой днф двоичной функции
- •6.2. Метод нахождения тупиковых днф
- •6.3. Метод Петрика нахождения тупиковых днф
- •Алгебраические системы
- •7.1. Алгебраические системы. Булевы алгебры
- •7.2. Изоморфизм алгебраических систем
- •Алгебры высказываний. Предикаты и операции над ними
- •8.1. Основные логические операции и их свойства
- •8.2. Предикаты и операции над ними
- •Исчисление предикатов
- •9.1. Общее понятие о логическом исчислении
- •9.2. Формулы алгебры предикатов
- •9.3. Равносильность формул. Основные отношения равносильности
- •9.4. Использование равносильностей для упрощения формул
- •9.5. Построение исчисления предикатов
- •9.6. Выводимость и доказуемость формул
- •9.7. Семантика исчисления предикатов
- •Понятие о теории моделей
- •Элементы теории алгоритмов
- •11.1. Основные требования к алгоритмам
- •11.2. Машина Тьюринга и функции, вычислимые по Тьюрингу
- •11.3. Машины произвольного доступа и вычислимые функции
- •Частично рекурсивные функции и их вычислимость
- •Вычислимость суперпозиции
- •Вычислимость рекурсии
- •Вычислимость минимизации
- •Нумерация наборов чисел и слов
- •Нормальные алгоритмы
- •Нумерация алгоритмов
- •1. Нумерация машин Тьюринга
- •2. Нумерация мпд-программ
- •Универсальные функции
- •Алгоритмически неразрешимые проблемы
- •16.1. Алгоритмически неразрешимые проблемы
- •16.2. Примечательные алгоритмически неразрешимые проблемы
- •Характеристики сложности вычислений
- •Характеристика сложности вычислительных задач
- •18.1. Классы сложности p и np и их взаимосвязь
- •18.3. Основные np-полные задачи. Сильная np-полнота
- •Список Литературы
9.6. Выводимость и доказуемость формул
Определение 9.16. Выводом формулы А из конечного или бесконечного множества формул Т в исчислении α называется конечная последовательность формул
А1, А2, …, An,
в которой An = A и каждая из формул Ai, i = 1, …, n является или аксиомой, или формулой из Т (исходной формулой), или получается по некоторому правилу вывода из предыдущих формул этой последовательности.
Если существует вывод формулы А из множества формул Т исчисления α, то говорят, что в α А выводима из Т и пишут
Т ├─ А, или В1, В2, …, ВК ├─ А,
α α
если Т = {В1, В2, …, ВК}. При этом формулы из Т называют посылками вывода.
Особо важным является случай, когда Т — пустое множество.
Определение 9.17. Формула из А языка α , выводимая в исчислении α из пустого множества формул, называется доказуемой формулой, или теоремой исчисления α, а сам вывод формулы А из пустого множества формул называется ее доказательством. Если формула А доказуема в исчислении α, то пишут
├─ А.
α
Так как у нас исчисление α фиксировано, то букву α будем опускать и писать просто
Т ├─ А; В1, В2, …, ВК ├─ А; ├─ А.
Очевидно, что при выводах и доказательствах формул можно использовать не только аксиомы и исходные формулы, но и любые доказанные ранее формулы.
Дальше нас будут интересовать вопросы о характеризации доказуемых формул и формул, выводимых из заданного множества, вопросы о непротиворечивости и полноте исчисления α. Предварительно приведем доказательства некоторых формул и вспомогательных правил вывода. При этом последовательности формул, являющиеся доказательствами или выводами, будем записывать в столбик, указывая справа их происхождение (номер аксиомы, номер правила вывода, порядковые номера исходных формул и т.п.).
Теорема 9.18. ├─ А А для любой формулы А.
Доказательство.
1. |
(А ((В А) А)) ((А (В А)) (А А)). |
(I2) |
2. |
А ((В А) А). |
(I1) |
3. |
(А (В А)) (А А). |
(I, 1, 2) |
4. |
А (В А). |
(I1) |
5. |
А А. |
(I, 3, 4) |
Теорема 9.19. Если А — любая формула и В — доказуемая формула, то ├─ А В.
Доказательство получается и добавлением к доказательству формулы В аксиомы I1 и формулы А В, получаемой из В и аксиомы I1 по правилу I.
Теорема 9.20. ├─ АВ ВА для любых формул А, В.
Доказательство.
1. |
(АВ В) ((АВ А) (АВ ВА)). |
(II3) |
2. |
АВ В. |
(II3) |
3. |
(АВ А) (АВ ВА). |
(I, 1, 2) |
4. |
АВ А. |
(II1) |
5. |
АВ ВА. |
|
Заменяя в доказательстве теоремы 9.20 II1 II3 соответственно аксиомами III1 – III3, получим доказательство следующей формулы.
Теорема 9.21. ├─ А В В А для любых формул А, В.
Теорема 9.22. ├─ для любой формулыА(х), содержащей свободные вхождения переменной х.
Доказательство.
1. |
А(х) х А(х). |
(V2) |
2. |
(А(х) х А(х)) . |
(IV3) |
3. |
. |
(I, 1, 2) |
4. |
. |
(I, 1, 3) |
Даже из приведенных простейших примеров видно, что задача построения доказательств формул является сложной и зачастую весьма искусственной. То же относится и к построению выводов. Попытайтесь, для примера построить вывод
AC D ├─ A (C D).
Для облегчения этой работы сначала доказывают ряд вспомогательных правил вывода, которыми затем можно заменять целые куски выводов или доказательств.
Ряд наиболее распространенных вспомогательных правил вывода можно получить из так называемой теоремы дедукции. Однако и ее формулировка и доказательство в общем случае сложны. Мы пока рассмотрим один ее ослабленный вариант.
Теорема 9.23 (об ограниченной дедукции). Пусть Т — произвольное множество формул, и А, В — произвольные формулы. Если T, A├─ B и существует вывод формулы В из T {A}, в котором не используются правила -введения и -удаления, то T ├─ A B.
Доказательство. Пусть В1, В2, …, Вm = B есть вывод формулы В из T {A}, в котором не используются правила -введения и -удаления. Докажем утверждение теоремы индукцией по длине вывода m.
Пусть m = 1. Тогда В является или аксиомой, или посылкой. Если В — аксиома, то она, очевидно, доказуема, и по теореме 9.19 имеем ├─ A B для любой формулы А. Пусть В — посылка. Если В = А, то T ├─ A B следует из теоремы 9.18. Если же В Т, то можно указать следующий вывод формулы А В из Т:
1. |
В (А В) |
(I1) |
2. |
В |
(посылка) |
3. |
А В |
(I, 1,2) |
Допустим, что теорема верна при m n, и докажем ее для m = n + 1. В этом случае по условию формула В будет или аксиомой, или посылкой, или непосредственным следствием двух предыдущих формул Bi, Bj по правилу заключения. Если В — аксиома или посылка, то T ├─ A B устанавливается точно так же, как и при m = 1. Пусть В получается из Bi, Bj по правилу заключения, т.е. BJ = Bi -> B. Так как i < n, j < n, то по предположению индукции имеем: T ├─ A Bi, T ├─ A (Bi B). Применяя теперь к формулам A (Bi B), A Bi и к аксиоме I2
(A (Bi B)) ((A Bi) (A B))
дважды правило заключения, получим формулу А В. Теорема доказана.
Докажем теперь ряд вспомогательных правил вывода, обозначая в них буквами А, В, С произвольные формулы α.
Правило умножения формул:
A, B ├─ AB.
Вывод:
1. |
(A A) ((A B) (A AB)) |
(II3) |
2. |
A A |
|
3. |
(A B) (A AB) |
(I, 1, 2) |
4. |
B (A B) |
(I1) |
5. |
B |
(посылка) |
6. |
A B |
(I, 4, 5) |
7. |
A AB |
(I, 3, 6) |
8. |
A |
(посылка) |
9. |
AB |
(I, 7, 8) |
Правило силлогизма:
A B, B C├─ A C.
В ы в о д. Согласно теореме дедукции достаточно показать, что A B, B C, A├─ C, причем существует вывод С, не использующий правил -введения и -удаления. Таким выводом может служить последовательность формул: А, А В, В, В С, С. Для ее получения дважды применяется правило заключения к посылкам.
Аналогично доказываются следующие правила.
Правило умножения посылок: |
A (B C)├─ AB C |
Правило разделения посылок: |
AB C ├─ A (B C) |
Правило перестановки посылок: |
A (B C)├─ B (A C) |
Правило умножения заключений: |
A B, A C├─ A BC |
Правило сложения посылок: |
A C, B C├─ A B C |
Правило введения посылки: |
A├─ B A |
Правило контрапозиции: |
A B├─ B A |
Правило де Моргана: а) ├─, б)├─.
Вывод правила а):
1. |
AB -> A |
(II1) |
2. |
AB -> B |
(II2) |
3. |
(правило контрапозиции, 1) | |
4. |
(правило контрапозиции, 2) | |
5. |
(правило сложения посылок, 3, 4) | |
6. |
(посылка) | |
7. |
(1, 5, 6) |
Вывод правила б):
1. |
(III1) | |
2. |
(III2) | |
3. |
(правило контрапозиции, 1) | |
4. |
(правило контрапозиции, 2) | |
5. |
(IV2) | |
6. |
(IV2) | |
7. |
(правило силлогизма, 3, 5) | |
8. |
(правило силлогизма, 4, 6) | |
9. |
(правило умножения заключений, 7, 8) | |
10. |
(правило контрапозиции, 9) | |
11. |
(IV2) | |
12. |
(правило силлогизма, 10, 11) |
Правило -отрицания:
а) ├─(следует непосредственно из теоремы 9.6.7);
б) ├─.
Вывод правила б):
1. |
(V1) | |
2. |
(правило контрапозиции, 1) | |
3. |
(IV1) | |
4. |
(правило силлогизма, 2, 3) | |
5. |
(III, 4) | |
6. |
(правило контрапозиции, 5) | |
7. |
(IV1) | |
8. |
(правило силлогизма, 6, 7) |
Правило -отрицания: а) ├─;
б) ├─.
Докажите в качестве упражнения.
Правило противоречия: ├─В (из противоречия выводима любая формула).
Выведем произвольную формулу В из , используя при этом любую доказуемую формулуR, например, А А.
1. |
A (R A) |
(I1) |
2. |
(IV3) | |
3. |
(правило силлогизма, 1, 2) | |
4. |
(правило умножения посылок, 3) | |
5. |
| |
6. |
(правило контрапозиции, 5) | |
7. |
(правило силлогизма, 4, 6) | |
8. |
(IV2) | |
9. |
(правило силлогизма, 7, 8) | |
10. |
(посылка) | |
11. |
B |
(1, 9, 10) |
Правило (закон) исключенного третьего: ├─ .
Доказательство (снова используем доказуемую формулу R):
1. |
(III1) | |
2. |
(III2) | |
3. |
(правило контрапозиции, 1) | |
4. |
(правило контрапозиции, 2) | |
5. |
(IV1) | |
6. |
(правило силлогизма, 4, 5) | |
7. |
(правило умножения заключений, 7, 8) | |
8. |
(правило противоречия и теорема дедукции) | |
9. |
(правило силлогизма, 7, 8) | |
10. |
(правило контрапозиции, 9) | |
11. |
(IV1) | |
12. |
(правило силлогизма, 10, 11) | |
13. |
(IV2) | |
14. |
(правило силлогизма, 12, 13) | |
15. |
R |
|
16. |
(1, 14, 15) |
Воспользуемся вспомогательными правилами вывода для доказательства еще одного частного случая теоремы дедукции.
Теорема дедукции 9.24 (для замкнутой формулы).
Если Т произвольное множество формул, В — произвольная, А — замкнутая формулы и T, A├─ B, то T├─ A B.
Доказательство. Производится так же, как теоремы об ограниченной дедукции. В дополнение нам необходимо лишь рассмотреть два случая (при m = n + 1):
а) В получается по правилу -введения из формулы Bi;
б) В получается по правилу -удаления из формулы Bi.
В случае «а» имеем: Bi = C D(x), B = C x D(x), причем С не содержит свободных вхождений х. По предположению индукции имеем:
T├─ A (C D(x)).
Дополним вывод формулы A (C D(x)) следующими формулами до вывода формулы А В:
AC D(x) (правило умножения посылок)
AC x D(x) (правило -введения)
A (C x D(x)) = A B (правило разделения посылок)
В случае «б»: Bi = C(x) D, B = x C(x) D, где D не содержит свободных вхождений х. По предположению индукции
T├─ A (C(x) D).
Отсюда, используя правила перестановки посылок и -удаления, получим:
T├─ C(x) (A D);
T├─ x C(x) (A D);
T├─ A (x C(x) D) = A B.
Теорема доказана.
Укажем одно следствие теоремы дедукции.
Следствие. Если Т — любое множество формул, А — замкнутая, В — любая формулы и T, A├─ , то T├─ .
Доказательство. По теореме дедукции T├─ A . Применяя правило контрапозиции, получим T├─ . Из правила де Моргана «а» и закона исключенного третьего следует, что ├─ , для любой формулы В. Следовательно, T├─ .