Решение

Согласно -удалению достаточно вывести (AA). С этой целью по -введению допустим, что (AA), и получим противоречие: (AA) A, (AA) A.

Для вывода первой секвенции (-введение) допустим A и получим противоречие: (AA),A (AA), (AA),A AA.

Первая из этих секвенций очевидна, а вторая получается -введением. Аналогично, для получения секвенции: (AA) A достаточно вывести секвенции (AA),A (AA), (AA),A AA, которые доказываются аналогично.

Пример 3.8

Вывести x A(x)  x A(x).

Решение

C этой целью допустим x A(x) и выведем  x A(x), т.е. выведем: x A(x)  x A(x). Для этого согласно -удалению выберем новую переменную у и установим A(y)  x A(x). Это можно сделать с помощью - введения:

A(y), x A(x) A(y) и A(y), x A(x) A(y).

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

Пример 3.9

Доказать A (A B).

Решение

Расположим доказательство в технике естественного вывода прямым образом, «сверху вниз»:

1. A, A, B A,

2. A, A, B A,

3. A, A B (-введение из 1. и 2.),

4. A, A B (-удаление из 3.),

5. A (A B) ( -введение дважды).

Пример 3.10

Доказать правило подстановки в технике естественного вывода в ИП.

Решение

Пусть для простоты Г есть список _, . Из _, A по -удалению A, а по -введению A. По правилу обобщения ( A).

Далее, (( A) ( A))' есть аксиома; штрихом здесь обозначена подстановка ( ).

По (MP) ( A)', или, что то же самое, .

Далее, по -введению . По (MP) , что и требовалось доказать.

Задачи

3.2. Являются ли выводами в ИП следующие последовательности:

а) ;

б) , , где - одноместный предикатный символ;

в) ,

,

?

3.3. Каким требованиям должна удовлетворять формула , чтобы следующая последовательность была выводом в ИП:

а) , ;

б) , ?

3.4. Построить выводы формул:

а) ;

б) ;

в) .

3.5. Являются ли следующие последовательности формул выводами из Г= , где не содержит свободных вхождений :

а) , ;

б) , ,

, , если и не содержат свободных вхождений ?

3.6. Построить выводы из Г= следующих формул:

а) ;

б) .

Индивидуальное задание (контрольная работа) правила выполнения и оформления индивидуального задания

При выполнении контрольной работы следует строго придерживаться следующих правил.

1. Выбор варианта для контрольной работы осуществляется в соответствии с порядковым номером в списке группы (во избежание недоразумений рекомендуется согласовать номер варианта с преподавателем). В соответствии с номером варианта из каждого задания 1-8 выбирается своя задача.

2. Контрольная работа оформляется в тонкой тетради чернилами любого цвета (кроме красного). Для замечаний рецензента оставляются поля. На обложке тетради указывается шифр академической группы, фамилия, имя, отчество студента, его учебный шифр (серия и номер зачетной книжки), домашний адрес, а также наименование дисциплины.

3. Решения задач следует располагать в порядке следования номеров задач, указанных в задании, сохраняя номера задач и записывая исходные условия.

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

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