Натуральное исчисление высказываний и предикатов

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

Сформулируем правила вывода, которые могут быть рассмотрены как дедуктивные принципы исчисления высказываний. Все правила можно подразделить на правила введения (обозначаются с помощью нижнего индекса «в» после знака соответствующей логической константы) и правила исключения логических символов (обозначаются с помощью нижнего индекса «и»). Также все правила можно подразделить на однопосылочные (над чертой пишется одна формула) и двухпосылочные (над чертой пишутся через запятую две формулы). Основными правилами натурального исчисления высказываний будут:

– правило введения конъюнкции;

– правило исключения конъюнкции;

– правило введения дизъюнкции;

– правило исключения дизъюнкции;

– правило введения импликации ( C – последняя посылка);

– правило исключения импликации;

– правило введения отрицания ( C – последняя посылка);

– правило исключения отрицания.

Каждое правило содержит указание на тип необходимых посылок (символы метапеременных A, B и C, стоящие над чертой) и тип заключения (символы соответствующих метапеременных, стоящие под чертой). Сам вывод обозначен в данном случае сплошной одинарной чертой. Если даны формулы того вида, которые указаны посылками, то каждое правило разрешает записать под чертой формулу того вида, которая указана заключением правила.

Правило введения конъюнкции является двухпосылочным. Оно позволяет в случае наличия двух произвольных формул A и B объединить их в конъюнкцию – . Также двухпосылочным является правило исключения дизъюнкции, позволяющее при наличии дизъюнкции и отрицания одного из членов дизъюнкции перейти ко второму члену дизъюнкции.

Правило исключения конъюнкции является однопосылочным и позволяет при наличии формулы вида перейти к одному из членов конъюнкции. Правило введения дизъюнкции также является однопосылочным и позволяет при наличии формулы A ( B ) перейти к формуле .

Своеобразие правил введения импликации и введения отрицания заключается
в том, что формула C в заключениях этих правил – это не любое выражение, а последнее допущение в некотором рассуждении, т. е. формулировки этих правил соотносят их
с конкретным рассуждением. Правило введения импликации позволяет по любой формуле B перейти к импликации вида , где C – последнее допущение, а на место консеквента помещается формула B. Данное правило выражает теорему дедукции.

Правило введения отрицания позволяет при обнаружении в рассуждении двух противоречащих друг другу формул ( ) перейти к формуле (отрицание последнего допущения). Таким образом, правило введения отрицания разрешает вводить отрицание последней посылки, если зафиксировано наличие двух противоречащих друг другу формул.

Применение всех указанных правил возможно только в отношении главных логических констант.

Вывод и доказательство в натуральном пропозициональном исчислении .
Посредством правил можно строить формальные рассуждения двух видов – выводы
и доказательства.

Вывод – непустая конечная линейно упорядоченная последовательность формул , удовлетворяющая двум условиям:

а) каждая является посылкой либо получена из предыдущих формул по одному из правил вывода;

б) если применялось правило введения импликации (теорема дедукции) или правило введения отрицания, то все формулы, начиная с последней посылки и вплоть до результата применения данного правила, должны быть исключены из дальнейших шагов вывода (исключенные посылки обозначаются вертикальной чертой), так как означенные правила являются непрямыми. Если имеется последовательность формул и в этой последовательности неисключенными посылками являются формулы , а последняя формула последовательности графически совпадает с формулой B, т. е. имеет место отношение графического равенства ,
то данная последовательность называется выводом формулы B из посылок Наличие выводимости обозначается при помощи выражения , где « » – метазнак выводимости. Если множество формул Г
содержит формулы то имеется и вывод формулы B из множества формул Г, что обозначается записью .

Доказательство – вывод из пустого множества посылок. Последняя формула в доказательстве называется доказуемой формулой (теоремой).

Пусть имеется доказательство и пусть формула B находится в отношении графического равенства с формулой Данная последовательность и есть доказательство формулы B. Выражение «B является теоремой» записывается так:

Вывод строится в виде линейной последовательности записанных друг под другом формул. Каждая формула последовательности в обязательном порядке нумеруется. Анализом вывода называется указание основания появления формулы в выводе. Формула может присутствовать в последовательности либо потому, что она является посылкой, либо она была получена из предыдущих формул по одному из правил натурального исчисления.

Пример 1. Допустим, что требуется обосновать метаутверждение о выводимости формулы s из посылок и Таким образом, нам необходимо обосновать метутверждение . Как мы знаем, для обоснования необходимо построить вывод, в котором последняя формула графически совпадала бы с формулой r, а посылками оказались бы в точности формулы и Ею является следующая последовательность:

(1) – посылка;

(2) – посылка;

(3) – посылка;

(4) p – посылка;

(5) q – из (1), (4);

(6) r – из (2), (5);

(7) s – из (3), (6).

Анализ этой последовательности показывает, что она удовлетворяет условиям, а потому является выводом, так как каждая формула является либо посылкой (1)–(4), либо получена посредством применения правил (5)–(7).

Эвристики. Построение выводов и доказательства является творческой задачей. Она состоит в нахождении нужной последовательности содержательных утверждений.
В случае доказательства необходимо начинать с поиска посылок. Это связано с тем, что доказательство есть обоснование выводимости метаутверждения из пустого множества посылок. Брать можно любые посылки, но в дальнейших шагах вывода, применяя правила, нужно исключить все лишние посылки. В этом случае применяются эвристики, т. е. своего рода рекомендации, позволяющие уменьшить число переборов, сделав выбор посылок неслучайным.

Пусть обосновывается метаутверждение о выводимости вида

Тогда в качестве посылок необходимо взять все формулы которые уже предложены как посылки. Далее выбор дополнительных посылок осуществляется в соответствии со следующими эвристическими правилами.

Первая эвристика. Формула, которая стоит справа от знака « », является целью вывода. В этой формуле необходимо выделить главный знак. Если им является импликация, то антецендент данной импликации берется в качестве дополнительной посылки, а новой целью вывода становится получение оставшейся от формулы ее консеквента. В нашем случае это формула в которой антецендентом является формула а консеквентом формула вида В этом случае присоединяется к основным посылкам в качестве дополнительной. Первая эвристика в обязательном порядке применяется до тех пор, пока не будет получена формула, не имеющая импликации в качестве главного знака. В нашем случае таковой является формула B. На этом работа по первой эвристике заканчивается. В итоге мы можем осуществить вывод вида

Формула B и есть цель вывода, к которой надо стремиться. Если этой цели удается достигнуть, то тогда все дополнительные посылки устраняются последовательным применением правила введения импликации.

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

Вторая эвристика. Данная эвристика применяется в том случае, если в результате применения первой эвристики не удалось получить импликативную формулу.
В таком случае в качестве дополнительной посылки берется отрицание формулы B. Тем самым осуществляется переход к доказательству от противного.Посылки в этом случае примут вид:

Целью будет вывод двух формул вида D и Ø D (т. е. противоречия). В случае, если это удается сделать, то применяется правило Ø _в, которое позволяет получить двойное отрицание последней формулы – , исключив при этом дополнительную посылку Применяя далее правило Ø _и, можно получить формулу B и тем самым обосновать выводимость:

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

Вывод, в котором применяется правило введения отрицания, называется косвенным выводом или выводом от противного.

Третья эвристика. Эта эвристика применяется только после первой и только в случае, если имеется формула вида или же отрицание дизъюнкции . В первом случае в качестве дополнительной посылки берется формула и после этого, применяя правило исключения дизъюнкции, получаем формулу B. Во втором случае в качестве посылки берется формула A, затем по правилу введения дизъюнкции строится формула, противоречащая отрицанию дизъюнкции. Вообще получение противоречия остается целью до тех пор, пока не будет устранена посылка, в силу принятия которой мы перешли к доказательству от противного.

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

(1) – посылка по 1-й эвристике;

(2) – доп. посылка по 2-й эвристике;

(3) – доп. посылка по 3-й эвристике;

(4) – из (3) по ;

(5) – из (2), (4) по ;

(6) – из (5) по ;

(7) – из (1), (6) по ;

(8) – из (7) по ;

(9) – из (2), (8) по ;

(10) – из (9) по ;

(11) – из (1), (10) по .

Анализ показывает, что последовательность удовлетворяет условиям (1) и (2) понятия вывода, а потому является выводом. Последняя формула графически совпадает с той формулой, которую необходимо было получить в заключении.

Пример 4. Попытаемся обосновать, что формула выводима из пустого множества посылок. Обосновывающей будет следующая последовательность:

(1) – посылка по 1-й эвристике;

(2) – посылка по 1-й эвристике;

(3) – посылка по 1-й эвристике;

(4) – посылка по 1-й эвристике;

(5) ­ – из (1), (4) по ;

(6) – из (2), (4) по ;

(7) – из (3), (5) по ;

(8) – из (6), (7) по ;

(9) – из (3), (8) по ;

(10) – из (2), (9) по ;

(11) – из (1), (11) по .

Анализ данной последовательности показывает, что она представляет собой доказательство формулы В качестве посылок были взяты формулы (1)–(4). Из этих формул на шаге (7) была получена формула , противоречащая формуле r. Это позволило применить правило введения отрицания, согласно которому в выводе можно записать отрицание последней посылки. Применив на шагах(9), (10) и (11) правило введения импликации, получили искомую формулу. Тем самым доказательство требуемого заключения завершено.

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