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

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


Исчисление высказываний.
Определение исчисления высказываний, как и любой формальной системы, следует начинать с задания множества аксиом и правил вывода, обеспечивающих пос­ледовательное их использование при доказательстве истинности заключения.
Доказательством называют конечную последовательность высказываний, каждое из которых является либо аксиомой, либо выводится из одного или более предыдущих высказываний этой последовательности по правилам вывода.
Определение минимально возможного множества аксиом определяет семантическую полноту исчисления, а определение правил, обеспечивающих последовательное использование аксиом и промежуточных высказываний в процессе формирования заключения – метод дедуктивного вывода.
Аксиомы исчисления высказываний.
Определение 1. Аксиомами теории назовем всякие формулы, которые порождают нижеследующие формульные схемы при любом выборе формул

1. 
   
   
2. 
   
   
3. 
   
   
4. 
   
   
5. 
   
   
6. 
   
   
7. 
   
   
8. 
   
   
9. 
   
   
10. 
    
    
11. 
    
    
12. 
    
    
13. 
    
    

Каждая из схем (1)-(13) порождает счетное множество аксиом, если символы заменять конкретными формулами. Поэтому записи (1)-(13) будем называть аксиомными схемами .
Определение 2. Правилом вывода теории называют процедуру перехода от двух формул вида и к одной формуле вида В для любых и .
Это правило называют modus ponens, MP. Правило МР позволяет удалять оператор , поэтому его называют также правилом удаления импликации и обозначают УИ. В случае применения правила МР формулы и называют посылками, а В - заключением этого правила.
4. Формальное доказательство и формальный вывод
Определение 3. Формальным доказательством (в теории ) называется конечная последовательность формул , причем каждая формула этой последовательности либо аксиома, либо получена по правилу МР из каких-либо двух предшествующих формул этой последовательности. Формальное доказательство является доказательством своей последней формулы . Формула В называется формально доказуемой, или формальной теоремой (теории ), если она имеет формальное доказательство.
Утверждение «Формула В формально доказуема в теории » будем обозначать ├_LВ.
Пример 1. Построить доказательство формулы

1. 
   1.
   
2. 
   2.
   
3. 
   3.
   
4. 
   4.
   
5. 
   5.
   
6. 
   6. ОФД (1-5) – определение формального доказательства
   

Обобщим понятие формального доказательства на случай вывода некоторой формулы B из других формул , называемых посылками (гипотезами).