Пропозициональный вывод

Существует другое определение следования, которое выглядит совершенно отличающимся от данного выше, но в действительности эквивалентное ему. В соответствие с этим определением,  влечёт F, если F может быть выведено из  с использованием определенного набора ``правил вывода''. Первое определение, основанное на интерпретации, – ``семантическое'', второе, основанное на понятии вывода – ``синтаксическое'' или ``дедуктивное''.

О корректности, полноте и разрешимости

Выводы в логике высказываний – наш основной объект изучения до конца данной части.

Вывод строятся из конструкций, которые называются ``секвенциями''.

Определение 15 (Секвенция). Секвенция – это выражение вида  |– F (``F при посылках '') или  |–  (``посылки  противоречивы''), где F – формула и  – конечное множество формул. ^*

Мы определим, какие секвенции рассматриваются ``начальными'', и опишем несколько ``правил вывода'' для порождения новых секвенций из секвенций, порождённых ранее. Начальные секвенции называются аксиомами.

Определение 16 (Аксиомы). Аксиомы в исчислении высказываний имеют вид

{ F } |– F.

Мы определим 12 правил вывода, и удобно вводить их постепенно.

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

Определение 17 (Дерево доказательства). Дерево доказательства определим рекурсивно:

1. Деревом доказательства является пустое дерево доказательства, состоящее только из корня – аксиомы.

2. Пусть T1, ..., T_k – деревья доказательства с корнями R1, ..., R_k. Тогда

   T1 ... T_k

   

3. (где  – некоторая секвенция) – дерево доказательства, если  может быть получена из R1, ..., R_k с помощью одного из правил вывода. Корнем такого дерева является .

Определение 18 (Доказуемая секвенция). Если существует дерево доказательства с корнем R, то R называют доказуемой секвенцией. Если этот корень имеет вид  |– F, то говорят о выводе формулы F из .

В соответствие с дедуктивным определением следования говорят, что F следует из , если существует вывод F из подмножества .

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

	 |– F    |– G
(В&)
	 |– F & G

	 |– F & G
(У&)
	 |– F

 |– F & G

 |– G

	 { F } |– G
(В)
	 |– F  G

	 |– F    |– F G
(У)
	 |– G

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

{q, r} |– p   {p  q, r} |– ¬q

{q, r, p  q} |– p & ¬q

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

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

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



2.26 Найдите вывод q & p из p & q.

см. Решение

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

2.27 (p & p)  p.

2.28 (p & p)  p.