Гильберт, Бернайс - Основания математики. Теория доказательств (Гильберт Д. - Основания математики и прочие работы), страница 7

г подстановкам. Действительно, з ф , из формулы Я-+ 6(а) такой, что переменная а вст ечается указана в кач р чается в ней только там, где она тате подстановки мы п качестве аргумента, а х не вхо ит мы получим формулу дит в 6(а), в резуль- Я-ь6(е )6(х)), которая вместе с формулой ))гх6(х) 6(е, )6(х)), получающейся подстановкой из (ва) дает н фо а т нам формулу Я -ь гэгх6 (х). Аналогичным образом из формулы 6(а)-ь Я такой, что а встречается в ней только там, г в качестве аргумента, а там, где она указана становки мы получим фо х не входит в 6(а), и формулу ( ), в результате под- 6 (е„6 (х)) -ь Я, которая вместе с формулой :-)х6 (х) 6 (а 6 (х)), получающейся подстановкой из ( ) о из (ез), дает нам формулу Эхб (х) -э- Я. У Р стью включает в себя все исчисление д ние пре окатов в целом.

ще одно преимущество введения е-си что в результате е-символа заключается в том те присоединения к исчислению и е Ф ию ~р~д~псат~~ е-симиенужным ь-правило: е-символ пол- ста тельно ля юб й ф у ( ) таков, что выводимы отио" ф у д нственности, выводима, в част ей форм лы е и , ула х (х). С другой сто сны изф ности, мы получаем фо рмулу роны, из формулы (е„) подстановкой эху((х)- Я(е„я(,)), а следовательно, и форм Я (в„Я (х)), гильвяэтов з-снмвол и -оормилд ф лч, которая получается из Результирующей фор „)лы ь-схемы, примененной к формуле Я(с), после замены входящего в нее ь-символа соответствующим е-символом'). Однако, в то время как ь-символ приложим лишь к таким формулам, для которых выведены соответствующие формулы единственности, е-символ может быть определен для произвольной формулы, содержащей свободную переменную. В заключение мы получим, используя е-символ и е-формулу„ некоторую общую формализацию операции символьного решения э) Именно, если мы хотим применить эту операцию к формуле БвЯ(о, ..., Е, и), где а, ..., Š— фигурирующие в ней свободные переменные, то нам достаточно лишь воспользоваться (выводимой с помощью ачрормулы) формулой (еа) ЗхА(х)-ь.А (е А(х)), из которой подстановкой (и, возможно, переименованием переменных) мы получим формулу :-)ир((п, ..., Е, и)- Я(п, ..., Е.

е„Я(а, ..., Е, и)). Эта последняя после введения явного определения ((а, ..., Й) =е„Я(а, ..., й, и) совместно о формулой ЗвЯ(а, ..., Е, и) даст пам формулу Я(а, ..., Е, ((а, ..., Е)). Замечание. Чтобы формально воспользоваться этим явным определением ((а, ..., й), нам нужно обратиться к аксиомам равенства. В том случае, если в рассматриваемом формализме аксиом равенства в нашем распоряжении нет, это явное определение мы можем воспринимать как некоторое правило замены, согласно которому выражения е Я (о, ..., Е, н) и Е (о, ..., Е) всюду могут быть заменены друг другом.

Вообще, следует обратить внимание на тот факт, что если явное определение имеет вид некоторого правила замены, то ') Эта роль е.символа становится очевидной, если принять во внимание его содержательный смысл. В самом деле, в случае предиката л(с), выполншошегося хотя бы для одного обьекта иэ его индивидиой области, а.терм вгм(г) представляет собой объект, для которого этот предикат выполняется, в значит, для предиката К (с), выполняюшегося для одного-единственного объекта, данный терм будет изображать именно этот объект; но этот же самый объект изображается и мтермом ьзя (з).

з) См. с. 23, йе ИСКЛЮЧЕНИЕ СВЯЗАННЫХ ПЕРЕМЕЬ!НЫХ 1ГЛ 1 независимо от того, является это определение равенством или эквивалентностью, введенный этим определением символ всегда можно исключить из любого доказательства, в заключительной формуле которого этого символа нет. При этом предполагается, что выполнено условие, имеющее место в отношении всех явных определений; а именно, что фигурирующие в определяемом выражении переменные и только они являются аргументами определяемого символа '). Таким образом, мы видим, что е-символ в силу своей характеризации посредством Р-формулы позволяет добиться троякого эффекта: во-первых, он вместе с определениями (е,) и (е,) доставляет в наше распоряжение соответствующие формулы и схемы для кванторов; во-вторых, он заменяет собой ысимвол и, в-третьих, он сводит символьные решения к явным определениям.

Эти свойства е-символа, из-за которых он и был введен Гиль- бертом в теорию доказательств, мы теперь используем для целей намеченной нами программы исследований'). С одной стороны, мы убедимся, что если в основу рассмотрения положить исчисление предикатов, то переход от какой-либо системы собственных аксиом (В) к соответствующей системе аксиом в разрешенном виде (В') представляет собой консервативный способ расширения этого формализма в том смысле, что любая формула исходного формализма, выводимая средствами системы (В'), будет выводиться также и из аксиом системы (8).

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

Теоремы эти в измененном таким образом порядке мы будем называть первой и второй е-теоремами. -Обе эти теоремы будут относиться к любому формализму Р, который получается из исчисления предикатов в результате добавления к его символам е-символа и некоторых дополнительных индивидных, предикатных и функциональных символов, а к числу исходных формул е-формулы н ряда не содержащих е-символа собственных аксиом з1)ы ..., '111, Для всякого такого формализма р эти теоремы формулируются следующим образом.

37 ДОКАЗАТЕ.ЧЬСТВО ПЕРВО1Ч з-ГЕОРГМЫ 1 з1 ео ем а 1 (первая е-теорема). Пусть СР— выводимая в Р о мгла, нг содержащая связанных пгрелзгннььг, и пусть аксиомы ч), ..., ' бгз исполь. ц! может быть выведена из аксиом мула ' л ж только говения связанных пере пе лгенных, пг. е, средствами одного ментарного исчисления со свободными переменными. 2 ! - орема). Луста Се — выв имая в Теорема вторая е-те ена г ла, не сооеажащач е-символов. Тогда СУ может быть выв из ',, ..., гВ б спользования е-символа средствам и из аксиом '!)н ..., 1 ез ис В ачестве следствия нз первой е-теоремы мы пол к ю, совершенно не связанную с е-симво р лом тео ем — ее мы дующую, б элементарном выводе.

,ем называть теоремой о ео ем а 3. Если из системы собственных аксиом, не годер. нных, с едствами исчисления предикатов оо а связанных од б срд и одного только элементарного исчисления со сво ными ными ). 1 Мы займемся пока доказательством пер " - р вой е-тео емы. Вторая е-теорема получится затем в ка качестве следствия из примыкающих к этому доказательству рассуждений'). дк 3.

Доказательство пеРвой е-теоРемы ) По готовка. Доказательство первой е-теоремы мы начнем ал одготовка. к ий. В о мулировке этой с нескольких подготовительных редукци . т о емы предполагается, что заключи тельная мула рассмате р риваемого вывода не содержит связанн р ых пе еменных. е ограничивая общности, можно считать, что она не содержит также и З без а гументов дедуктивно равна всякой друго переменной ез арг те повсеместной замены о м ле, получающейся из нее в результате по с чавшаяся формульная переменная с одним аргум изв ьный терм; причем, если рассматри р у ваемая м ла не содерол е ктивное авенство может жит связанных переменных, то это дедукт ') См т.

1, гл. !7!1, с. 357 — 353 нлн Приложение 1, с. 465 н далее. а) См. с. 25 н далее. частным сл чаем одной более общей тео") Эта теорема аалкетса также часгн к то ю Э нк теннус уста Рамы об исчислении пРеднкатогь отоРУ раооты 51е п1 н з Е. ВЬег баз 1п1ырыпцюплрт 1ещ Хашепшеог1е.— Ас1а Асабет1ае АЬоепцз Ма1Ь. е1 РЬуз., з) См. с, 167 н далее, ЬВ ИСКЛЮЧЕНИЕ СВЯЗАННЫХ ПЕРЕМЕННЫХ 1гл 1 38 доклзлтельство певвои -тео~емы быть установлено уже в рамках одного только исчисления высказываний '). Пусть теперь из формулы Ж в результате замен указанного типа, произведенных для каждой встречающейся в ней формульной переменной без аргументов, получается формула ат,; пусть, далее, (вз — формула, получающаяся нз 6з в результате замены каждой встречающейся в (Вг индивидной переменной каким-либо вновь введенным индивидным символом и каждой формульной переменной с аргументами каким-либо новым предикатным символом с тем же числом аргументов.