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

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

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

Используя только правила для конъюнкции и импликации, мы не сможем построить вывод формулы 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 не выполнимо.

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

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

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

Дата добавления: 2014-11-29