Теорема о дедукции

Докажем теперь теорему о дедукции для исчисления предикатов. При этом существенно используется то, что в данном выводе (а) В1, …, Вi формулы В из А1, …, Аm-1, Аm все переменные остаются фиксированными; это условие включено теперь в наше понимание суждения “A1,…, Am-l, Am |- В”. Используем — с некоторыми модификациями и добавлениями — старое доказательство, которое проводилось в логике высказываний.

Если последнее допущение Аm не применяется (в качестве допущения) в данном выводе (а), то мы построим результирующий вывод, просто добавляя к заданному выводу следующие формулы:

l+1′. Bl É (AmÉ Bl) — схема аксиом 1а.

l+2′. AmÉ Bl — MP, l’, l+1.

Поэтому предположим, что последнее допущение Аm используется (как таковое) в данном выводе (а); первое его вхождение обозначим Вn; это значит, что Вn — первая из формул Bl,…, Вl, появление которой в (а) обосновано тем обстоятельством, что она яетсяется последним допущением Аm. Припишем спереди ко всем формулам Вn,…, Вl данного вывода символы “Am É ”; получим

B1,…, Bn-1,AmÉ Bn,…, AmÉ Bl.

Вставлять формулы перед Аm É Вi потребуется только при i = n, …,i. Снова рассмотрим порознь частные случаи, ибо они зависят от того, каким образом оправдывается присутствие Вi, в (а) при каждом i, и опишем, какие вставки нужны в каждом случае.В случаях 1 — 3 доказательство остается неизменным. В случае 4, когда Вi( i>n) получается из Bg и Bh (g, h < i ) no É — правилу, раньше надо было добавить шаги, приводящие от Am É Bg и Аm É Вh к Аm É Вi, где Вg, Вh и Вi соответственно имеют вид A, AÉ В, В. Теперь же если g

BgÉ (AmÉ Bg) — схема аксиом 1а.

AmÉ Bg — MP, g’, -.

Точно так же поступаем, если h

случай 4 так же, как в исчислении высказыавний.

Случай 5.

Вi ( i > n) получается из какой-либо предшествующей формулы Вg ( g < i ) посредством » -правила, т. е. Bg и Вi соответственно имеют вид СÉ А(х), CÉ » xA(x), причем х не входит свободно в С. Если g n, т. е. применение » -правила находится после первого использования Аm ( под именем Вn ) в качестве допущения. Следовательно, x не входит свободно в Аm ввиду условия, что все переменные в данном выводе (а) остаются фиксированными. Согласно ограничению в » правиле, переменная х не входит свободно в С. Значит, х не входит свободно в Аm&С. Используем это для обоснования нового применения » -правила на (k2+1′)-м шаге:

k1′. AmÉ Bg, т.е. AmÉ (CÉ A(x))

k2′. Am& CÉ A(x)

k2+1′. Am& CÉ » xA(x) — » — правило, k2′

k2′. AmÉ (CÉ » xA(x)), т.е. AmÉ Bi

Случай 6.

 

Вi ( i > n ) получается из предшествующей формулы Вg ( g< i ) применением $ -правила. Рассмотрение предоставим читателю. Итак, мы видели, как строить конкретный вывод Аm É В из A1,…, Аm-1. Применения » и $ — правил в этом “результирующем выводе” находятся в соответствии с применениями тех же правил в данном выводе: переменные х соответствующих друг другу применений совпадают, а сами эти применения расположены одинаково по отношению к А1,… ,Аm-1. И так как все переменные в данном выводе остаются фиксированными, то все они фиксированы в результирующем выводе. Значит, А1,…, Аm-1 |- Am É B, что и требовалось доказать.

 

Логика - доступно для всех