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

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

	 |– F
(ВП)
	 {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))



2.29 Найдите вывод p  r из p  q и q  r.

2.30 Найдите вывод r из p & q и p  (q  r).

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

2.31 p  (q  p).

2.32 p  ((p & q)  q).

2.33 ((p & q)  r)  (p  (q  r)).

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

Определение 19 (Истинность секвенций). Секвенция  |– F тождественно истинна, если  влечёт F.^*

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

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

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

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

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

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

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

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

	 { F } |– 
(В¬)
	 |– ¬F

	 { ¬F } |– 
(У¬)
	 |– F

	 |– F    |– ¬F
(В)
	 |– 

	 |– 
(У)
	 |– F

Выведите секвенции:

2.39 {¬¬p} |– p.

см. Решение

2.40 {p} |– ¬¬p.

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

2.41 ¬(p & ¬p).

2.42 (p & ¬p)  q.

Определение 21 (Истинность секвенций). Секвенция  |–  тождественно истинна, если  не выполнимо.

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

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

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