Решение

Правило 1 – из гипотезы A и ввиду АA по (MP) AА.

Правила 2 – 4 – тривиально допустимы. Вывод, обосновывающий секвенцию выше черты, обосновывает и секвенцию ниже черты;

Правило 5 – из B, AC по теореме о дедукции BАC. Отсюда и из ГА по правилу добавления Г, BАC; Г, BА. Применяя (MP), получим Г, BC.

Пример 3.5

Доказать логические правила техники естественного вывода в ИП (см. с. 59-60).

Решение

Приведем доказательства некоторых из правил (остальные доказываются аналогично).

-введение. Это есть в точности теорема о дедукции.

-удаление. Из данных выводов ГA, ГAB вывод для ГB получим с помощью (MP).

Ú-введение. Имеем: ГA. Кроме того,AAÚB (это аксиома). По (MP) ГAÚB.

Ú-удаление. Из данных Г,AC; Г,BC по теореме о дедукции ГAC и ГBC. Кроме того, (AC)((BC)(AÚBC)) (это аксиома). Дважды применяя (MP), получим: ГAÚBC. По закону тождества (и правилу добавления) Г,AÚBAÚB. По (MP)Г,AÚBC.

-удаление. Из Г,A(y)C по теореме о дедукции следует, что ГA(y)C. По правилу обобщения Гy(A(y)C) (здесь существенно, что y не входит свободно в Г). Имеем аксиому y(A(y)C)(y(A(y)C)). По (MP) Гy A(y) C. Аналогично x A(x) yA(y). Отсюда Г,xA(x)yA(y). Следовательно, по (MP) Г,xA(x) C.

-введение. Из Г, AВ и Г, BA по теореме о дедукции ГAB, ГBA, Г(AB)(BA), что и означает по определению эквивалентности ГAB.

Пример 3.6

Доказать в ИП, что AÚBØ(ØAØB).

Решение

Согласно -введению достаточно установить AÚB Ø(ØAØB) и Ø(ØAØB) AÚB.

Начнем с первой секвенции. Слева у нее стоит дизъюнкция, поэтому, разбирая случаи согласно Ú- удалению, достаточно установить два факта:

AØ(ØAØB) и BØ(ØAØB).

Установим только первый, второй устанавливается симметрично. Для вывода отрицания Ø(ØAØB) достаточно допустить ØAØB и вывести противоречие, т.е. использовать Ø-введение. Противоречие будет состоять в выводе A и ØA. Итак, для вывода AØ(ØAØB) с помощью Ø-введения достаточно установить: A,ØAØBA и A,ØAØBØA.

Первая секвенция выводима по закону тождества. Для вывода второй согласно -удалению достаточно показать: A,ØA,ØBØA, что также следует из закона тождества.

Теперь установим: Ø(ØAØB)AÚB. Здесь наше рассуждение будет косвенным. Согласно Ø-удалению достаточно установить: Ø(ØAØB)

ØØ(AÚB). А для этого согласно Ø-введению следует, допустив Ø(AÚB), вывести противоречие.

Мы докажем:

Ø(ØAØB),Ø(AÚB) Ø(ØAØB) и Ø(AÚB)ØAØB.

Первая секвенция, очевидно, выводима по закону тождества. Вторую секвенцию получим по -введению. Достаточно вывести:

Ø(AÚB)ØA и Ø(AÚB)ØB.

Мы выведем первую секвенцию, вторая выводится симметрично. Используя
Ø- введение, достаточно вывести:

Ø(AÚB),AØ(AÚB) и Ø(AÚB),AAÚB.

Но первая из этих секвенций очевидна, а вторая получается с помощью
Ú-введения из Ø(AÚB),AA.

Пример 3.7

Вывести AÚØA.