Использование правил введения и удаления и МТ1 при установлении существования доказательств и выводов в теории L

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

Пример 9.

Пример 8.

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

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

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

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

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

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

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

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

Введение	Удаление
É		Если Г, А├В, то Г├АÉВ	ТД, ВИ		А, АÉВ├В	МР, УИ
Ù		А, В├АÙВ	ВК	4,5	АÙВ├А, АÙВ├В	УК1,УК2
Ú	6,7	А├АÚВ, В├АÚВ	ВД1, ВД2		Г, А├С и Г, В├С, то Г, АÚВ├С	УД
Ø		Г, А├В и Г,А├ØВ, то Г├ØА	RA, ВО	10,	ØØА├А А, ØА├В	УДО СУО
~		АÉВ, ВÉА ├А~В	ВЭ		А~В├АÉВ А~В├ВÉА	УЭ1 УЭ2

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

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

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

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

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

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

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

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

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

Дата добавления: 2015-06-27