Решение. Построить вывод в ИП для формулы х А у (А(х

Примеры

Пример 3.3

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

В более традиционной (но менее точной) записи это высказывание имеет вид: х А(х) у А(у).

Строим вывод:

х А(х)А(у), (а)

это пример схемы аксиом (ип2);

у (х А(х)А(у)), (б)

по правилу (Gen) из (а), структурное требование выполняется, так как (а) – не гипотеза (а аксиома ИП);

у (х А(х)А(у))(х А(х)у А(у)), (в)

это пример схемы аксиом (ип12) (существенно, что х А(х) не содержит свободно у);

х А(х)у А(у) (г)

вытекает из (б) и (в) по правилу (MP).

Соответствующее дерево вывода имеет вид:

Пример 3.4

Привести краткое обоснование пяти допустимых структурных правил вывода в ИП).

Дата добавления: 2014-01-06