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

	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

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