Правила для конъюнкции и импликации

G |– F G |– G (В&)     G |– F & G	G |– F & G (У&)     G |– F G |– F & G   G |– G
G È { F } |– G (ВÉ)     G |– F É G	G |– F G |– FÉ G (УÉ)     G |– G

В каждом из этих пяти правил вывода, одно или два выражения над горизонтальной чертой представляют ``посылки'', к которым правило может быть применено, и выражение под чертой представляет ``заключение'' которое выводится по этому правилу. Правила В& и ВÉ – ``правила введения'' конъюнкции и импликации; У& и УÉ – ``правила удаления''. Подставляя конкретные формулы вместо метапеременных F и G и конкретные конечные множества формул вместо метапеременной G некоторое правило вывода, мы получаем пример этого правила. Например,

{q, r} |– p {p Ú q, r} |– q

{q, r, p Ú q} |– p & q

есть пример правила введения конъюнкции.

Пример простого вывода. Выведем формулу q из посылки p & q. Этот вывод получается за один шаг с помощью второго правила удаления конъюнкции.

	{q} |– q
(У&)
	{p & q} |– q

Правило введения посылки

Используя только правила для конъюнкции и импликации, мы не сможем построить вывод формулы p & q из множества посылок {p, q}. Действительно, формулу {p, q} |– p & q мы можем получить с помощью правила (В&) из формулы {p, q} |– p и формулу {p, q} |– q. Однако ``очевидные'' формулы {p, q} |– p и {p, q} |– q мы не сможем вывести. У нас нет правила, позволяющего выводить формулу из некоторого множества посылок, если она выводится из более узкого множества. Это правило вывода назовём правилом введения посылки.

	G |– F
(ВП)
	G È {G} |– F

Пример вывода. Мы приводим вывод p É ((p É q) É (p & q)) из пустого множества посылок:

	{p} |– p (ВП)     {p,p É q} |– p       {p} |– p (ВП)     {p,p É q} |– p   {p É q} |– p É q (ВП)     {p,p É q} |– p É q (УÉ)     {p,p É q} |– q
(В&)
	{p,p É q} |– p & q (ВÉ)     {p} |– (p É q) É (p & q) (ВÉ)     Æ |– p É ((p É q) É (p & q))

Корректность правил вывода

Истинность секвенций.Секвенция G |– F тождественно истинна, если G влечёт F.

Корректность правил вывода.Правило вывода корректно, если для каждого примера этого правила посылки которого являются тождественно истинными, его заключение также тождественно истинно.

А) Правило введения посылки корректно.

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

В) Правило введения конъюнкции корректно.

Г) Правило удаления импликации корректно.

Д) Правило введения импликации корректно.

Правила для отрицания и правила противоречия

Следующие четыре правила вывода – правила введения и удаления отрицания ``правило сведения к противоречию'' и ``правило противоречия''.

G È { F } |– ^ (В)     G |– F	G È { F } |– ^ (У)     G |– F
G |– F G |– F (В^)     G |– ^	G |– ^ (У^)     G |– F

Истинность секвенций.Секвенция G |– ^ тождественно истинна, если G не выполнимо.

Е) Правило удаления отрицания корректно.

Ж) Правило введения отрицания корректно.

З) Правило противоречия корректно.

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

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

G |– F (В Ú)     G |– F Ú G

G |– G   G |– F Ú G

	G |– F Ú G G È F |– C G È G |– C
(У Ú)
	G |– C

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

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

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

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

1)(p Ú q) É (q Ú p).

2)(p Ú p) º p.

3) p É ((p Ú q) º q).

4)(p & (q Ú r)) º ((p & q) Ú (p & r)).

5) p º p.

6)(p Ú q) º (p & q).

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

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