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

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

Здесь 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 из G, тогда G логически влечёт F.

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

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