4.3. Корректность исчисления предикатов

Теорема 43. Всякая выводимая в исчислении предикатов формула является общезначимой.

C Для исчисления высказываний проверка коррект-

ности была тривиальной | надо было по таблице проверить, что все аксиомы (1) { (11) являются тавтологиями. С этими аксиомами и сейчас нет проблем. Но в двух следующих аксиомах есть ограничение на корректность подстановки, без которого они могут не быть общезначимыми. Естественно, это ограничение должно быть использовано и в доказательстве корректности, и это потребует довольно скучных рассуждений | тем более скучных, что сам факт кажется ясным и так. Тем не менее такие рассуждения надо уметь проводить, так что мы ничего пропускать не будем.

Итак, пусть фиксирована сигнатура , а также некоторая интерпретация этой сигнатуры. Всюду далее, говоря о термах и формулах, мы имеем в виду термы и формулы этой сигнатуры, а говоря об их значениях, имеем в виду значения в этой интерпретации.

Лемма 1. Пусть u и t | термы, а | переменная. Тогда

[u(t= )]( ) = [u]( + ( 7→[t]( )))

для произвольной оценки .

Напомним обозначения: в левой части мы подставляем t вместо в терм u, и берём значение получившегося терма на оценке . В правой части стоит значение терма u на оценке, которая получится из , если значение переменной изменить и считать равным значению терма t на оценке .

В сущности, это утверждение совершенно тривиально: оно говорит, например, что значение sin(cos( x)) при x = 2 равно значению sin(y) при y = cos(2). Но раз уж мы взялись всё доказывать формально, докажем его индукцией по построению терма u. Если терм u есть переменная, отличная от , то ни подстановка, ни изменение

оценки не сказываются на значении терма u. Для случая u = получаем [t]( ) слева и справа. Если терм получается из других термов применением функционального символа, то подстановка выполняется отдельно в каждом из этих термов, так что искомое равенство также сохраняется. Лемма 1 доказана.

Аналогичное утверждение для формул таково: Лемма 2. Пусть ' | формула, t | терм, а | пе-

ременная, причём подстановка t вместо в формулу ' корректна. Тогда

['(t= )]( ) = [']( + ( 7→[t]( )))

для произвольной оценки .

Поясним смысл этой леммы на примере. Пусть является единственным параметром формулы ', а c | константа. Тогда формула '(c= ) замкнута; лемма утверждает, что её истинность равносильна истинности ' на оценке, при которой значение переменной есть элемент интерпретации, соответствующий константе c.

Доказательство леммы проведём индукцией по построению формулы '. Для атомарных формул это утверждение является прямым следствием леммы 1. Кроме того, из определения истинностного значения формулы и из определения подстановки ясно, что если утверждение леммы 2 верно для двух формул '1 и '2, то оно верно для их любой их логической комбинации (конъюнкции, дизъюнкции и импликации); аналогично для отрицания.

Единственный нетривиальный случай | формула, начинающаяся с квантора. Здесь наши определения вступают в игру. Пусть ' имеет вид . Есть два принципи-

ально разных случая: либо является параметром формулы ' (т. е. формулы ), либо нет. Во втором случае

'(t= ) совпадает с ', а изменение значения переменной в оценке не влияет на значение формулы ', так что всё сходится. Осталось разобрать случай, когда является параметром формулы (отсюда следует, что

не совпадает с ). По определению корректной подстановки, в этом случае переменная не входит в терм t и

=m[ (t=)]( + ( 7→m)) =

=m[ ]( + ( 7→m) + ( 7→[t]( + ( 7→m)))):

Мы воспользовались определением подстановки, определением истинности ( m означает конъюнкцию по всем

элементам из носителя интерпретации) и предположением индукции для формулы . Теперь надо заметить, что переменная не входит в t по предположению корректности, и потому значение терма t не изменится, если заменить + ( 7→m) на . Далее, и различны, по-

этому два изменения в можно переставить местами. Используя эти соображения, можно продолжить цепочку равенств:

=m[ ]( + ( 7→[t]( )) + ( 7→m)) =

=[ ]( + ( 7→[t]( ))) =

=[']( + ( 7→[t]( )));

что и требовалось. Случай формулы вида разбирается аналогично, надо только m заменить на m. Лем-

ма 2 доказана.

Теперь уже ясно, почему формула

' → '(t=)

будет истинна на любой оценке (если подстановка кор-

ректна). В самом деле, если левая часть импликации истинна на , то ' будет истинна на любой оценке 0, ко-

торая отличается от лишь значением переменной . В частности, ' будет истинна и на оценке + ( 7→[t]( )),

что по только что доказанной лемме 2 означает, что правая часть импликации истинна на .

Общезначимость формулы

'(t=) → '

доказывается аналогично.

Нам осталось проверить, что правила вывода сохраняют общезначимость. Для правила MP это очевидно (как и в случае исчисления высказываний). Проверим это для правил Бернайса. Это совсем несложно, так как здесь нет речи ни о каких корректных подстановках.

Пусть, например, формула → ' общезначима и пе-

ременная не является параметром формулы . Проверим, что формула → ' общезначима, то есть истин-

на на любой оценке (в любой интерпретации). В самом

деле, пусть истинна на оценке . Тогда она истинна и на любой оценке 0, отличающейся от только значением

переменной (значение переменной не влияет на истин-

ность , так как не является параметром). Значит, и формула ' истинна на любой такой оценке 0. А это в

точности означает, что ' истинна на оценке , что и

требовалось.

Для второго правила Бернайса рассуждение симметрично. Пусть формула ' → общезначима и перемен-

ная не является параметром формулы . Покажем, что формула ' → общезначима. В самом деле, пусть

её левая часть истинна на некоторой оценке . По опре-

делению истинности формулы, начинающейся с квантора существования, это означает, что найдётся оценка 0,

которая отличается от только на переменной , для которой [']( 0) истинно. Тогда и [ ]( 0) истинно. Но пе-

4.4. Выводы в исчислении предикатов

Примеры выводимых формул

Прежде чем доказывать теорему Гёделя о полноте исчисления предикатов, мы должны приобрести некоторый опыт построения выводов в этом исчислении.

•Прежде всего отметим, что возможность сослаться на теорему о полноте исчисления высказываний и

считать выводимым любой частный случай пропозициональной тавтологии сильно облегчает жизнь. Например, пусть мы вывели две формулы ' и и хотим теперь вывести формулу ( ' ). Это просто:

заметим, что формула (' → ( → (' ))) являет-

ся частным случаем пропозициональной тавтологии (а на самом деле и аксиомой) и дважды применяем правило MP.

• Другой пример такого же рода: если формула ' → → выводима, то выводима и формула ¬ → ¬', поскольку импликация

(' → ) → (¬ → ¬')

является частным случаем пропозициональной тавтологии.

•Ещё один пример: если выводимы формулы ' → и → , то выводима и формула ' → , поскольку формула

(' → ) → (( → ) → (' → ))

является частным случаем пропозициональной тавтологии.

• Для произвольной формулы ' выведем формулу

x ' → x ':

В самом деле, подстановка переменной вместо себя всегда допустима, поэтому формулы x ' → ' и

' → x ' являются аксиомами. Остаётся воспользоваться предыдущим замечанием.

• Для произвольной формулы ' выведем формулу

y x ' → x y ':

→ y '. Теперь заметим, что левая часть имплика-

ции не имеет параметра x, а правая часть не имеет параметра y, так что можно применить два правила Бернайса (в любом порядке) и добавить справа квантор x, а слева | квантор y.

• Предположим, что формула ' → выводима, а |

произвольная переменная. Покажем, что в этом случае выводима формула ' → . В самом деле,

формула ' → ' является аксиомой. Далее выво-

дим (с помощью пропозициональных тавтологий и правила MP) формулу ' → ; остаётся восполь-

зоваться правилом Бернайса (левая часть не имеет параметра ).

•Аналогичным образом из выводимости формулы ' → следует выводимость формулы ' → ,

только надо начать с аксиомы → , затем получить ' → , а потом применить правило Бернайса.

• Таким образом, если формулы ' и доказуемо эквивалентны (это значит, что импликации ' → и → ' выводимы), то формулы ' и также

доказуемо эквивалентны. (Аналогичное утверждение верно и для формул ' и .)

Теперь несложно доказать и более общий факт: замена подформулы на доказуемо эквивалентную даёт доказуемо эквивалентную формулу (см. с. 190).

•Выведем формулу x A(x) → y A(y) (здесь A |

одноместный предикатный символ). Это несложно: начнём с аксиомы x A(x) → A(y), в ней левая часть

не имеет параметра y и потому по правилу Бернайса из неё получается искомая формула. Этот пример показывает, что связанные переменные можно

переименовывать, не меняя смысла формулы (подробнее об этом мы скажем в разделе 4.6.)

•Выведем формулы, связывающие кванторы всеобщности и существования:

' ↔ ¬ ¬';' ↔ ¬ ¬':

Напомним, что ↔ мы считаем сокращением для ( → ) ( → ), так что нам надо вывести четыре формулы.

Начнём с формулы ' → ¬ ¬'. Имея в виду правило Бернайса, достаточно вывести формулу ' → → ¬ ¬'. Тавтология (B → ¬A) → (A → ¬B) позволяет вместо этого выводить формулу ¬' → → ¬', которая является аксиомой.

В только что выведенной формуле ' → ¬ ¬'

можно в качестве ' взять любую формулу, в том числе начинающуюся с отрицания. Подставив ¬'

вместо ', получим

¬' → ¬ ¬¬';

где ¬¬' доказуемо эквивалентна ' и потому может

быть заменена на '. После этого правило контрапозиции (если из A следует ¬B, то из B следует ¬A)

даёт

' → ¬ ¬':

Выведем третью формулу: ¬ ¬' → '. По правилу Бернайса достаточно вывести ¬ ¬' → ',

что после контрапозиции превращается в аксиому

¬' → ¬'.

Четвёртая формула получится, если заменить в третьей ' на ¬' и применить контрапозицию.

Выводимость из посылок

В исчислении высказываний важную роль играло понятие выводимости из посылок и связанная с ним лемма о дедукции (с. 50). Для исчисления предикатов ситуация немного меняется. Если разрешить использовать посылки наравне с аксиомами безо всяких ограничений, то утверждение, аналогичное лемме о дедукции, будет неверным. Например, из формулы A(x) можно вывести формулу x A(x) (как мы видели на с. 165 при обсужде-

нии правила обобщения). Но импликация A(x) → x A(x)

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

ки являются замкнутыми формулами. Пусть ` | произвольное множество замкнутых формул рассматриваемой нами сигнатуры . (Такие множества называют теориями в сигнатуре .) Говорят, что формула A выводима из `, если её можно вывести, используя наравне с аксиомами формулы из `. Как и для исчисления высказываний, мы пишем ` ` A. Выводимые из ` формулы называют

также теоремами теории `.

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

`| множество замкнутых формул, а A | замкнутая формула. Тогда ` ` (A → B) тогда и только тогда, когда

`{A} ` B.

Доказательство проходит по той же схеме, что и для исчисления высказываний (с. 50): к формулам C1; : : : ; Cn, образующим вывод Cn = B из ` {A}, мы приписываем

посылку A и дополняем полученную последовательность

(A → C1); : : : ; (A → Cn)

до вывода из `. Отличие от пропозиционального случая в том, что в выводе могут встречаться правила Бернайса. Например, от выводимости формулы

A → ( → ')

надо перейти к выводимости формулы

A → ( → ')

174 Исчисление предикатов [гл. 4]

(в которой переменная не является параметром формулы ). Это несложно сделать, если заметить, что в силу пропозициональных тавтологий можно перейти от A → ( → ') к (A ) → ', затем применить правило

Бернайса (это законно, так как переменная не является параметром формулы , а формула A замкнута по предположению). Получится выводимая из ` формула

(A ) → ';

и остаётся вернуть A из конъюнкции в посылку. Сходным образом рассматривается и второе правило

Бернайса. Если выводима формула A → (' → ); то в

силу пропозициональных тавтологий выводима формула ' → (A → ); к которой можно применить правило Бер-

найса и получить ' → (A → ); после чего вернуть A

назад с помощью пропозициональной тавтологии. Лемма о дедукции доказана.

Отметим теперь несколько полезных свойств выводимости из посылок.

•Если ` ` A и `0 `, то `0 ` A. (Очевидно следует из определения.)

•Если ` ` A, то существует конечное множество `0 `, для которого `0 ` A. (Вывод конечен и

потому может использовать лишь конечное число формул.)

•Если ` конечно и равно { 1; : : : ; n}, то ` ` A равносильно выводимости (без посылок) формулы

( 1 : : : n) → A:

В самом деле, если { 1; : : : ; n} ` A, то многократное применение леммы о дедукции даёт

`1 → ( 2 → (: : : ( n → A) : : :));

иостаётся воспользоваться надлежащей пропозиональной тавтологией. (В обратную сторону рассуждение также проходит без труда.)

•Комбинируя три предыдущих замечания, приходим

к такому эквивалентному определению выводимости из посылок: ` ` A, если найдутся формулы

1; : : : ; n `, для которых

` 1 → ( 2 → (: : : ( n → A) : : :)):

Это определение имеет смысл и для формул с параметрами, так что если уж определять выводимость из посылок с параметрами (чего обычно избегают), то именно так.

Понятие выводимости из посылок позволяет переформулировать теорему о корректности исчисления предикатов.

Говорят, что интерпретация M сигнатуры является моделью теории `, если все формулы из ` истинны в M.

Теорема 44 (о корректности; переформулировка) . Все теоремы теории ` истинны в любой модели M теории `.

C Если формула A является теоремой теории ` (т. е.

`` A), найдутся формулы 1; : : : ; n `, для которых

`1 → ( 2 → (: : : ( n → A) : : :)):

По теореме о корректности (в уже известной нам форме) эта формула будет истинна во всех интерпретациях, в частности в M. Поскольку 1; : : : ; n истинны в M, то и формула A истинна в M (на любой оценке). B

В следующих задачах | и только в них | знак ` по-

нимается в описанном выше смысле (в посылках допускаются параметры).

95. Пусть ` | множество произвольных (не обязательно замкнутых) формул. (а) Пусть существует «вывод» некоторой формулы ', в котором наравне с аксиомами используются формулы из `, при этом все применения правил Бернайса предшествуют появлению формул из `. Покажите, что ` ` '.

Покажите, что верно и обратное утверждение. (б) Покажите, если в «выводе» формулы ' наравне с аксиомами используются формулы из `, но правила Бернайса не применяются по переменным, свободным в `, то ` ` '.

Аналогичное рассуждение позволяет доказать и другое утверждение, которое нам потребуется:

Лемма о добавлении констант . Пусть формула ' неко-

торой сигнатуры выводима в исчислении предикатов расширенной сигнатуры 0, полученной из добавлени-

ем новых констант. Тогда ' выводима и в исчислении предикатов сигнатуры .

Доказательство. Пусть формула ', не содержащая новых констант, имеет вывод, в котором новые константы встречаются. Как их оттуда удалить? Легко понять, что их можно заменить на свежие переменные, не входящие в вывод, и он останется выводом, но уже без новых констант. Лемма доказана.

На самом деле эта лемма верна для произвольного расширения сигнатуры (можно добавлять не только константы, но и функциональные символы любой валентности, а также предикатные символы). Чтобы удалить новые символы из вывода, поступаем так. Все термы вида f(: : :), где f | добавленный функциональный символ, мы заменяем на новую переменную (можно взять одну и ту же переменную для всех новых символов и всех их вхождений). Все атомарные формулы с новыми предикатными символами заменяем на какую-либо замкнутую формулу (одну и ту же; какая именно формула, роли не играет).

98. Проведите это рассуждение подробно.

Таким образом, мы можем говорить о выводимости формулы, не уточняя, в какой именно сигнатуре (содержащей все использованные в формуле предикатные и функциональные символы) мы ищем её вывод.

Если принять теорему о полноте, по которой выводимость равносильна общезначимости, независимость выводимости от сигнатуры становится очевидной: истинность формулы не зависит от интерпретации символов, которые в неё не входят. (Если интерпретировать отсутствующие в формуле символы как постоянные функции и предикаты, мы приходим к синтаксическому рассуждению, упомянутому выше.)