14-§. Исчисления высказывание. Проблема вывода. Применение понятия доказательство. Исчисление высказываний

Пример 4. Установить существование доказательства формулы .

1. 
   1. Посылка
   
2. 
   B 2. Посылка
   
3. 
   A 3. Посылка
   
4. 
   4.
   
5. 
   C 5.
   
6. 
   8.ОФВ(1-5)
   
7. 
   9.ТД(6)
   
8. 
   10. ТД(7)
   
9. 
   11. ТД(7)
   

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

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

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

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

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

Пример 5. Установить выводимость формулы , .

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

1. 
   1. Посылка
   
2. 
   2. Посылка
   
3. 
   3.AC12
   
4. 
   4.
   
5. 
   5.AC9S
   
6. 
   6.
   
7. 
   7.
   
8. 
   8.
   
9. 
   9.
   

б) Доказательство существования формального вывода.
1. , , 1.MT1a
2. , , 2.MT1a
3. , , 3.MT1a
4. 4.УЭ1
5. A, 5.MP
6. , , 6.MT1б(3,4)
7. , , 7.MT1б(2,5,6)
8. , 8. BO(1,7)
в) Замена вопроса о выводимости вопросом о следовании в алгебре высказываний.
,
Установим верность данного следования методом от противного. Предполагаем, что следование не верно, т.е. при истинных посылках заключение является ложным. Получается следующая система уравнений:
противоречие.
Значит, следование является верным. Таким образом, установили данную выводимость.