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

Определение 4. Формальным выводом формулы В из посылок называется конечная последовательность формул , заканчивающаяся формулой B ( ), причем каждая формула этой последовательности

1. 
   или одна из посылок ,
   
2. 
   или аксиома,
   
3. 
   или формула, полученная из некоторых двух предшествующих формул этой последовательности по правилу МР.
   

Если существует формальный вывод формулы В из формул , то формула В называется формально выводимой из формул , и обозначается так: ├В, или Г├В, где Г = { }.
Очевидно, что доказательство - частный случай формального вывода из пустого множества посылок.
Пример 2. Построить вывод формулы

1. 
   1. Посылка
   
2. 
   2. Посылка
   
3. 
   3. Посылка
   
4. 
   4.
   
5. 
   5.
   
6. 
   6.
   
7. 
   7.
   
8. 
   8.
   
9. 
   9. ОФВ (1-8) – определение формального вывода
   

Свойства отношений выводимости.
Метатеорема 1 (МТ1).

1. 
   
   
2. 
   Если
   

Метатеорема 2 (МТ2).
Пусть Г- любое множество формул. Тогда:
а) если Г тo Г, B частности,
b) если тo
Следствия:
а) если
b) если тo
Метатеорема 3 (МТ3), теорема дедукции (ТД), правило введения импликации (ВИ).
Пусть Г - любое множество формул. Тогда:

1. 
   если Г, , то Г В частности,
   
2. 
   если , то .
   

Следствия.

1. 
   если , , то В частности,
   
2. 
   если , , то