Решение

C этой целью допустим xA(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(ØAB).

Решение

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

1) A, ØA, ØBA,

2) A, ØA, ØBØA,

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

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

5) A(ØAB) ( -введение дважды).

Пример 3.10

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