 |
Законы снятия и введения двойного отрицания, вывод на основе противоречивых гипотез
|
|
|
|
Лемма о снятии отрицания с гипотезы
Пусть имеется доказательство из множество формул Гамма и множества отрицаний Х выводится Y и из Гамма и отрицания Х выводится отрицание Y, тогда из Гамма выводится Х.
Доказательство:
Теорема: закон снятия двойного отрицания.
Из двойного отрицания Х выводится Х.
Доказательство:
Теорема: об опровержении гипотез.
Из доказательства противоречия на основе гипотез можно получить опровержение любой из этих гипотез на основе остальных.
Если из Гамма и Х выводится Y, из Гамма и Х выводится отрицание Y, то из Гамма выводится отрицание Х.
Доказательство:
Закон введения двойного отрицания
Из Х выводится двойное отрицание Х.
Теорема вывода на основе противоречий
Если бы можно было доказать противоречие, то можно было бы и доказать все что угодно.
Из Х и отрицания Х выводится Y
Доказательство.
Независимость высказывания
Аксиомы являются независимыми, если их нельзя друг из друга вывести. То есть взять одну аксиому и вывести ее из других. Речь идет об аксиомах, относящихся к разным схемам. Схемы аксиом исчисления высказываний L независимы.
Доказательство.
В процессе доказательства будем пользоваться одним приемом. Будем находить такое свойство, которым обладают все схемы аксиом, кроме выбранной и показывать, что это свойство сохраняется при применении правила вывода.
Докажем, что А1 не выводимо из А2 и А3. Для этого зададимся специальной интерпретацией. Будем считать, что пропозициональные символы могут принимать значения 0, 1 и 2. при этом операции отрицания и импликации определяются так
| А | Отрицание А |
| А | В | А-В |
Схемы тождественно равны нулю. А схема аксиом А1 – нет.
|
|
|
Покажем, что МР сохраняет свойство тождественного равенства нулю. Строка где В тоже равно 0. Значит схема аксиом А1 не выводится из А2 и А3.
Покажем, что А2 не выводится из А1 и А3. поступаем точно также, только используем другие таблицы.
| А | Отрицание А |
| А | В | А-В |
Показываем независимость А3 от А1 и А2. Можно было бы вновь составить таблицы, но найдем другое свойство. Введем операнд h(F), который в формуле F стирает все отрицания. Если применить этот оператор к схемам аксиом А1 и А2, они останутся тавтологиями. Так в них отрицания нет вообще. Если применить к схема аксиом А3, то h(A3)=((отр В имп отр А) имп ((отр В имп А) имп В))=(В имп А)имп((В имп А) имп В
Подставим В=А, получим (А имп А) имп ((А имп А) имп А)=А.
Из тавтологии мы получили не тавтологию.
Покажем, что свойство формулы оставаться тавтологией после применения оператора h сохраняется правилом МР.
H(А имп В)=H(А)имп H(B)
После применения оператора h, h(А имп B) тавтология, h(A) тоже тавтология, следовательно h(B) тоже тавтология. Свойство оставаться тавтологией после применения оператора h сохраняются выводом оператора МР. Так как А3 не тавтология после применения оператора h, то А3 не зависит от А1 и А2.
Альтернативные исчисления высказывания
1. Система Гилберта и Алкермана 1938
Дизъюнкция и отрицание.
А имп В=отр А или В
(А или А) имп А
А имп (А или А)
А или В имп В или А
(В имп С) имп (А или В имп А или С) правило МР
2. исчисление Россера 1953
конъюнкция отрицание
А имп В=отр(А и отр В)
А имп (А и А)
А и В имп В
(А имп В) имп (отр (В и С) имп отриц (С и А)) правило МР
|
|
|
3. схема исчисления Клини
конъюнкция, дизъюнкиция, отрицание, импликация
1 А имп (В имп А)
2 (А имп (В имп С))имп ((А имп В) имп (А имп С))
3 А и В имп А
4 А и В имп В
5 А имп (В имп (А и В))
6 А имп (А или В)
7 В имп (А или В)
8 (А имп В) имп ((В имп С) имп ((А или В) имп С))
9 (А имп В) имп ((А имп отр В) имп отр А)
10 Отр отр А имп А
4. Классическое исчисление
1, 2, 3, 4, 5, 6, 7, 8 совпадают
9 (отр А) имп(А имп В)
10 (отр В имп (отр А)имп ((В имп А) имп (отр В)))
11 А или отр А
|
|
|
