7. Установление доказуемости формул

Как показывают примеры 6 и 7, применение метода преобразования вывода Г,А├B в вывод Г├АB, описанного в доказательстве МТ3, приводит к «разбуханию» результирующего вывода: если данный вывод содержит k формул, то результирующий вывод – 3k +2 формул. Существуют более «экономные методы». Например, неважно иметь содержащее 161 формулу доказательство формулы (А(ВС))(В(АС)), которое получается трехкратным применением описанного алгоритма к выводу А (В С), В, А├ С (см. пример 6), важно только знать, что эта формула доказуема.

Пример 8.

Установить существование доказательства формулы (А(ВС))(В(АС)).

А(ВС)	1. посылка
В	2. посылка
А	3. посылка
ВС	4. МР(F1,F3)
С	5. МР(F2,F4)
А(ВС), В, А├С	8. ОФВ (1-5)
АС, В├АС	9. ТД(6)
АС├(ВС)(АВС)	10. ТД(7)
├(АС)((ВС)(АВС))	11. ТД(8)

Пример 9.

Установить существование доказательства формулы (АС)((ВС)(АВС)).

АС	1. посылка
ВС	2. посылка
АВ	3. посылка
(АС)((ВС)(АВС))	4. АС8
(ВС)(АВС)	5. МР(F1,F4)
АВС	6. МР(F2,F5)
С	7. МР(F3,F6)
АС, ВС, АВ├С	8. ОФВ (1-7)
АС, ВС├АВС	9. МТ2(8)
АС├(ВС)(АВС)	10. МТ2(9)
├(АС)((ВС)(АВС))	11. МТ2(10)

8. Правила введения и удаления логических операторов

Метатеорема 5 (МТ5).

Для любого конечного множества формул Г и для любых формул А, В, С справедливы правила (введения и удаления), приведенные ниже:

Введение				Удаление
	1	Если Г, А├В, то Г├АВ	ТД, ВИ	2	А, АВ├В	МР, УИ
	3	А, В├АВ	ВК	4,5	АВ├А, АВ├В	УК1,УК2
	6,7	А├АВ, В├АВ	ВД1, ВД2	8	Г, А├С и Г, В├С, то Г, АВ├С	УД
	9	Г, А├В и Г,А├В, то Г├А	RA, ВО	10, 11	А├А А, А├В	УДО СУО
	12	АВ, ВА ├АВ	ВЭ	13	АВ├АВ АВ├ВА	УЭ1 УЭ2

9. Использование правил введения и удаления и мт1 при установлении существования доказательств и выводов в теории l.

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

Методы установления выводимости:

1. построение формального вывода;

2. доказательство существования формального вывода;

3. замена вопроса о выводимости вопросом о следовании в алгебре высказываний.

Методы установления доказуемости:

1. построение формального доказательства;

2. установление существования формального доказательства;

3. замена вопроса о доказуемости вопросом об общезначимости в алгебре высказываний.

Пример 10.

Установить выводимость формулы АВ, В├А

1. Построение формального вывода.

   АВ	1. посылка
   В	2. посылка
   (АВ)(АВ)	3. АС12
   АВ	4. МР(F1,F3)
   (АВ)((АВ)А)	5. АС9
   (АВ)А	6. МР(F4,F5)
   В(АВ)	7.
   АВ	8. МР(F2,F7)
   А	9. МР(F6,F8)

2. Доказательство существования формального вывода.

   АВ, В, А├ В	1. МТ1а
   АВ, В, А├ А	2. МТ1а
   АВ, В, А├ АВ	3. МТ1а
   АВ├ АВ	4. УЭ1
   А, АВ├В	5. МР
   АВ, В, А├ АВ	6. МТ1б(3, 4)
   АВ, В, А├В	7. МТ1б(2, 5, 6)
   АВ, В├ А	8. ВО(1, 7)

3. Замена вопроса о выводимости вопросом о следовании в алгебре высказываний.

АВ, В╞ А

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

противоречие.

Значит, следование является верным. Таким образом, установили данную выводимость.

Пример 11.

Установить доказуемость формулы ├ А(АВ)А

1. Построение формального доказательства.

   (А(АВ) А)((А А(АВ))(А(АВ)А))	1.
   А(АВ) А	2.
   (А А(АВ))(А(АВ)А)	3. МР(F1,F2)
   (ААВ)((А(АВА(АВ)))(АА(АВ)))	4.
   ААВ	5. АС6
   (А(АВА(АВ)))(АА(АВ))	6. МР(F4,F5)
   А(АВА(АВ))	7.
   АА(АВ)	8. МР(F6,F7)
   А(АВ)А	9. МР(F3,F6)

2. Установление существования формального доказательства.

   А├А	1. МТ1а
   А├АВ	2. ВД1
   А, АВ├А(АВ)	3. ВК
   А├А(АВ)	4.МТ1б(1, 2, 3)
   ├АА(АВ)	5. ТД(4)
   А(АВ)├А	6. УК1
   ├А(АВ)А	7. ТД(6)
   АА(АВ), А(АВ)А├ А(АВ)А	8. ВЭ
   ├А(АВ)А	9. МТ1б(5, 6, 7)

3. Замена вопроса о доказуемости вопросом об общезначимости в алгебре высказываний.

╞ А(АВ)А

Докажем общезначимость формулы методом равносильных преобразований.

Будем также учитывать, что АÚИºИ, обозначим данное соотношение (*).

А(АВ)А(А(АВ)А)(АА(АВ))((А(АВ))А)(АА(АВ))(АА(АВ))(АА(АВ))(И(АВ))(ААААВ)(И(АВ))(ИАВ)И ИИ.