Правила для дизъюнкции

Оставшиеся три правила вывода – правила введения и удаления дизъюнкции:

	 |– F
(В )
	 |– F  G

 |– G  |– F  G

	 |– F  G  F |– C  G |– C
(У )
	 |– C

Здесь F и G – формулы, и C – либо формула, либо .

Теперь описание системы вывода для логики высказываний завершено.^*

Мы рекомендуем строить деревья доказательства, начиная с корней (т.е. с формул, которые надо вывести) и постепенно нарашивая дерево, добиваясь, чтобы конечными формулами в дереве были аксиомы.

О том, как строить дерево доказательства.

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

2.46 (p  q)  (q  p).

2.47 (p  p)  p.

2.48 ¬p  ((p  q)  q).

2.49 (p & (q  r))  ((p & q)  (p & r)).

2.50 ¬¬p  p.

2.51 ¬(p  q)  (¬p & ¬q).

2.52 Оба правила введения дизъюнкции корректны.

2.53 Правило удаления дизъюнкции корректно.

Корректность и полнота логики высказываний

Теорема корректности. Если существует вывод F из , тогда  логически влечёт F.

Теорема полноты. Для любой формулы F и любого множества формул , если  влечёт F, тогда существует вывод F из подмножества .

Полнота логики высказываний (для другого множества правил вывода) была установлена Емилем Постом в 1921 году.