Глава 10. Теория доказательства: кваиториые правила

вхождений переменной x вхождениями переменной у. (Например, если a(x) теть F(x, t)& VzG(z, x), то сг(у) теть F(y,t)&VzG(z,y).) Если в (x)

x

возможно, еще от каких-то переменных), и естественно ожидать, что (у)

другим обозначением аргумента.

F

деленным на множестве натуральных чисел и означающим, что число, стоящее на первом месте, больше числа, стоящего на втором ме-

x

x

очевидно, тождественно истинен). Если мы теперь подставим в формулу 3zF(z, x) вместо переменной x переменную у и в полученной формуле 3zF(z, у) заместим предикатный символ F тем же самым двуместным предикатом, мы получим тот же одноместный предикат, что и раньше, но от переменной у. Однако если мы подставим в формулу 3zF(z,x) вместо переменной x переменную z и в полученной формуле 3zF(z, z)

F

и прежде, то получится уже не предикат, а предложение (очевидно, ложное) «Существует такое натуральное число, которое больше самого себя». Произошло это потому, что свободное вхождение заменяемой

x

на которую мы ее заменили, так что после замены свободное вхождение стало связанным.

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

Понятно, что если переменная у вообще те входит в формулу a(x), то подстановка переменной у вместо переменной x в формулу a(x) корректна. Для упрощения формулировок полезно также считать, что любая

(x) x

сто себя самой. Такая подстановка, разумеется, корректна.

2.

12) Если M h a(x) и перемен- 13) Если подстановка переменная x те входит свободно ни ной y вместо переменной x в одну формулу из M, то корректна, то Vra(x) h a(y) M h Vxa(x) (удаление общности); (введение общности);

14) Если подстановка перемен- 15) Если M, a(x) h у и переменной y вместо переменной x ная x не входит свободно ни корректна, то a(y) h Зга(x) в одну формулу из M и в (введение существования); формулу у, то M, Зга(x) h у

(удаление существования).

Сокращенно эти правила будут обозначаться BV, W, В З УЗ.

V З V З

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

если, фиксировав произвольный элемент заданного множества, мы доказали, что он (при некотором условии M) обладает свойством A, то

M

все элементы данного множества (введение общности);2

из утверждения «Все элементы данного множества обладают свой- Ay yA

yA

y

A

(введение существования);

y

A

вии M) утверждение О, то это утверждение будет следовать (при усло- M

A

V3

x те входила свободно в формулы из M, обеспечивает произвольность элемента x: если бы какая-нибудь формула J3(x) Є M содержала свобод-

xx

(x)

3x

M, 3x (x) I

элемент x обладает свойством A, то тот же самый x должен обладать и свойством C. О смысле требования, чтобы в правилах W и В3 подстановка у вместо x была корректной, мы уже говорили: при несоблюдении

( у)

(x)

Задача. Убедитесь, что при отказе от ограничительного требования в одном из новых правил стали бы доказуемыми (без изменения осталь-ных правил) следующие формулы:

Vy(F(у) ^ VxF(x)) — при отказе от требования в правиле BV; Vx3yF(x, у) ^ 3yF(у, у) — при отказе от требования в правиле W; VyF(у, у) ^ 3xVyF(x, у) — при отказе от требования в правиле В3; Vx(3xF(x) ^ F(x)) — при отказе от требования в правиле У3.

Из каждой формулы этой задачи можно получить ложное предложение, заместив предикатный символ подходящим конкретным предика-

F( x)

предикатом, определенным на множестве целых чисел и означающим x = 0.

F(x, у)

предикатом, означающим x < у (получится предложение, означающее, что существует целое число, меньшее самого себя), или в третьей заместить тот же символ предикатом, означающим x = у (получится предложение, означающее, что существует целое число, равное всем целым

F(x)

в первой (получится предложение, также означающее, что все целые числа равны нулю). (Все предикаты можно считать определенными на множестве целых чисел; подробности предоставляются читателю.)

Замечание. Если вспомнить, что кванторы общности и существования можно понимать как «бесконечную конъюнкцию» и «бесконечную

дизъюнкцию» (см. замечание в пункте 3 главы 7), то станет ясно, что правила введения и удаления общности и существования — это, в сущности, распространенные на «бесконечный случай» правила введения и удаления конъюнкции и дизъюнкции. (Чтобы убедиться в этом для правила ВК, нужно заметить, что оно равносильно следующему услов- M h M h M h &

3. В деревьях вывода применение новых правил изображается аналогично применению старых. Именно: для безусловных правил ВЗ и W соответствующие элементарные шаги вывода изображаются точно так же, как для прочих безусловных правил; сходным образом изображается

V

( x) Vx ( x)

в отличие от безусловных правил здесь нужно следить, чтобы зеле-

( x)

переменной x; применение прав ила УЗ изображается аналогично применению УД—ему отвечает горизонтальная черта, снизу от которой записывается формула у, а сверху — Зга(x) и та же формула у, причем она должна быть корнем дерева, среди зеленых листьев которого име-

(x) M

(x)

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

xy

менные.

Пример 1.

VxVm(x, y) yy

Vya(x, y) yy a(x, y) BV

Vx«(x, y) BV

VyVx (x, y) Пример 2. ЗxЗyQL(x,y) h ЗУЗга(x,y).

Зга (x,y) „і

ЗуЗга(x,y) [ЗУа(x,y)](4) уз

^ ЗуЗга(x, y) ЗxЗyol(x, y) y^

ЗуЗга(x, y)

Пример 3. Vx—a(x) I 3xa(x).

Vx— ( x) 1n —a(x) W Kx)](3) yo

Л [3xa (x)](4) уз

4 ?—BO

3x (x)

Пример 4. —3xa.(x) I Vx—a.(x).

[«(x)](3)

'л

2 3xa(x) —3xa(x)

— (x)

4-

Vx— (x)

Пример 5. 3x—a(x) I Vxa(x).

[Vxa (x)](3)

a(x) [—a (x)](4)

3 Л

^ —Vxa (x) 3x—a (x)

—Vx (x)

Пример 6*. —Vxa(x) I 3x—a(x).

t [—«(x)](3)

3x—a (x) [—3x—a (x)](k)

Опущенные фрагменты этого дерева (замененные пунктирными линиями) аналогичны примеру 1 из главы 9. Шагу, на котором устраняется промежуточное допущение Sx—v.(x), для большей ясности приписан условный номер к.

Неконструктивность последней из доказанных выводимостей озна-чает, что если мы доказали, что некоторым свойством не могут обладать все элементы какого-то множества, отсюда еще не вытекает, что мы можем указать пример элемента, не обладающего этим свойством. Это можно проиллюстрировать следующим примером. Действительное число называется алгебраическим, если оно является корнем некоторого уравнения вида f (x) = 0, где f(x)—многочлен с целыми коэффициентами. Создатель теории множеств Г. Кантор (Georg Cantor, 1845—1918) дал простое и изящное доказательство того факта, что не все действительные числа — алгебраические, установив, что алгебраических чисел в некотором смысле «меньше», чем всех действительных. Отсюда следует, что существуют неалгебраические числа (математики называют их трансцендентными). Но такое доказательство существования трансцендентных чисел неконструктивно: из него не получается ни одного конкретного примера трансцендентного числа. Конструктивное доказательство было дано Ж. Лиувиллем (Joseph Liouville, 1809—1882): он установил, что играющие в математике важную роль числа e и % трансцендентны.

Другой пример: если о каком-то русском писателе мы знаем из достоверных источников, что он писал не только по-русски, но ни одно его произведение, написанное не на русском языке, не сохранилось, то мы не можем утверждать, что располагаем конструктивным доказательством существования таких произведений.

Читателю рекомендуется, учитывая замечание в конце пункта 2 этой главы, убедиться, что доказательства выводимостей примеров 3, 4 и 5 совершенно аналогичны доказательствам выводимостей примеров 2, 3 и 4 из главы 9. (Но для выводимости примера 6 мы дали доказательство, непохожее на пример 5 из главы 9 и более сложное. Полезно попытаться объяснить, почему аналогия здесь «не проходит», а также дать для примера 5 из главы 9 доказательство, аналогичное только что приведенному для примера 6.)

Если мы вспомним теперь определение дедуктивной эквивалентности формул (глава 8, пункт 8) и основные равносильности логики предикатов (глава 7, пункт 3), то мы увидим, что в примерах 1—6 мы фактически доказали дедуктивную эквивалентность левых и правых частей основных равносильностей групп I и II. То же самое можно сделать и для равносильностей групп III и IV.

Выводимости следующих восьми примеров будут отвечать равно- сильностям группы III. Из них выводимости примеров 8—13 имеют место .лишь при условии, что формула |3 не содержит свободных вхо- x

ограничений.

Пример 7. Vx(a(x)&p) I Vxa.(x)&J3.

Пример 8. Vxa(x)&p I Vx(a(x)&p).

Пример 9*. Vx(a(x) vp) I Vxa(x) vp.

Пример 10. Vxa(x) vp I Vx(a(x) vp).

Пример 11. 3x(a(x)&p) I 3xa(x)&p.

Пример 12. 3xa(x)&p I 3x(a(x)&p).

Пример 13. 3x(a(x) vp) I 3xa(x) vp.

Пример 14. 3xa(x) vp I 3x(a(x) vp).

Мы докажем сейчас выводимости примеров 7, 9, 11 и 12. (Остальные четыре читатель может попытаться доказать самстоятельно.)

Доказательство выводимости примера 7:

Vx(ot(x)&p)

a(x)&P Vx(ot(x)&P)

ot(x) a(x)&p

Vxa (x)

Vxa(x) & p

Доказательство выводимости примера 9:

I ( )](5) I ffl(,,) niffiMULУО ^.WIW Ьй(11) тв 2 3^!Lac 4W.(,)vp) w

к a(x) а[ж) ot(x) vp VJT

6 ot(x) EV gVx(a(x) vp)jp] (11) TE УД

Vxa(x) ВД 9 ^ ВД 10 ИТ

J Vxot(x) Vp A Vxot(x) Vp A pV^p VJT

Vra(x) vp A

Примечание.

(x)

Доказательство выводимости примера 11: |ot(x)&p] (5)

2 *(x) В3 3 |ot(x)&p](5) ук

4 3xQ-(x) Р_вк

^ Зга(x) & p 3x(ot(x) &p) y^

Зга(x) & p

Доказательство выводимости примера 12:

Зга(x) & р VT/- 1 о р ja(x)](5) _вк

3 q(x)&p ш 43га(ж)&_уК 3x(ot(x) &р) Зга(x)

3x(a(x)&p)

x

V

для применимости правила УЗ.

Неконструктивность выводимости примера 9 станет очевидной, если взять в качестве р предложение 3x^0.(x). В этом случае, если имеется регулярный способ, позволяющий для каждого элемента x0 рассматриваемого нами множества M проверить, удовлетворяет ли он условию a(x0), то мы можем для каждого x0 Є M конструктивно обосновать дизъюнкцию a(x0) V3x^a(x), т.е. обосновать один из ее членов: если

предложение a(x0) окажется истинным, будет обоснован первый член дизъюнкции, а если оно окажется ложным — второй. Тем самым будет конструктивно обосновано предложение Vx(a(x) vp). Но отсюда не по-

Vx (x) v

в этом убедиться, обратимся к гипотезе Гольдбаха—Эйлера (см. пункт 4

x

( x)

x

и через р — предложение 3x—a(x). Для каждого натурального числа, очевидно, можно проверить, представляется ли оно в виде суммы двух простых чисел, так что предложение Vx(a(x) vp) конструктивно обосновано и его конструктивное обоснование получается очень легко. Но

Vx (x) v

проблемы Гольдбаха—Эйлера!

Выводимости следующих двух примеров, отвечающие основным рав-

у

(x) у x

(x)

Пример 15. Vxa(x) I Vya(у). Пример 16. 3га(x) I 3уа(у). Доказательство выводимости примера 15:

x ( x) / \ У V

a(y) BV Vya(у)

Выводимость примера 16 читатель может попытаться доказать сам.

Задача. Доказать следующие выводимости:

Vxa(x) I 3xa(x);

3yVxa(x,y) I Vx3ya(x, y);

Vx(a(x)&f3(x)) I Vxa(x)&Vxp(x);

Vxa(x)&Vxp(x) I Vx(a(x)&p(x));

3x(a(x) vp(x)) I 3xa(x) v3xp(x);

3xa(x) v 3xp(x) I 3x(a(x) vp(x));

Vxa(x) vVxp(x) I Vx(a(x) vp(x));

3x(a(x)&p(x)) I 3xa(x)&3xp(x);

Vx(a(x) ^ p(x)) I Vxa(x) ^ Vxp(x);

Vx(a(x) ^ p(x)) I 3xa(x) ^ 3xp(x).

4. В пункте 8 главы 8 мы заметили, что понятие доказуемости в пропозициональном исчислении естественного вывода совпадает по объему с понятием тождественной истинности: формула логики предложений доказуема в этом исчислении тогда и только тогда, когда она тождественно истинна. Аналогичный факт имеет место и для предикатного исчисления естественного вывода: формула логики предикатов доказуема в нем тогда и только тогда, когда она всюду истинна. Это утверждение называется теоремой о полноте исчисления предикатов.5

Что касается связи между понятиями дедуктивной эквивалентности и равносильности, то она для предикатного исчисления естественного вывода такова же, как для пропозиционального: две формулы логики предикатов дедуктивно эквивалентны в (предикатном) исчислении естественного вывода тогда и только тогда, когда они равносильны. (Для основных равносильностей логики предикатов, перечисленных в главе 7, мы доказали, что их левые и правые части дедуктивно эквивалентны.)

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