Глава 10. Теория доказательства: кваиториые правила
вхождений переменной x вхождениями переменной у. (Например, если a(x) теть F(x, t)& VzG(z, x), то сг(у) теть F(y,t)&VzG(z,y).) Если в (x)
x
возможно, еще от каких-то переменных), и естественно ожидать, что (у)
другим обозначением аргумента.
Так оно и будет, если никакое свободное вхождение x в a(x) не находится в области действия квантора по переменной у. Пусть, например, a(x) теть 3zF(z,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.
Если бы полученное предложение Vy(y = 0 ^ Vx(x = 0)) было истинно, это означало бы, что предикат у = 0 ^ Vx(x = 0) принимает значение И для каждого значения у, в том числе для у = 0; но импликация 0 = 0 ^ Vx(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.
VxVya.(x,y) h VyVxa.(x,y).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
Примечание.
Часть последнего дерева, отвечающая шагам 6—11, по техническим причинам (для того, чтобы дерево поместилось на странице) сдвинута влево, так что под чертой, отвечающей шагу 5, оказались три формулы (на правильном рисунке там должна быть только форму-(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, мы доказали, что их левые и правые части дедуктивно эквивалентны.)
И последнее замечание: можно доказать, что, подобно пропозициональному, предикатное исчисление естественного вывода непротиворечиво.