Гильберт, Бернайс - Основания математики. Теория доказательств (947376), страница 80
Текст из файла (страница 80)
Однако мы не будем здесь этим заннматься. †Вмес того чтобы тра.сформировать формулу (р,) е (и',), люжно было бы также добавить н качестае новой аксиомы формулу А (рх ) А (х)) -л. лухА (х) н опустить схемы ла) н (б), Тогда формулы А (р«) А (х)) -л УХА (х) 'лхА х) — л А (Р,А (х)) В этом случае будет логично исключить квантор и в формуле ()лз), взяв в качестве аксиомы вместо этой формулы переводимую в нее формулу (Ра) ) А (12„А (х)) -ь р, А (х) = О. Аксиомы для )л-символа, если взять в качестве аксиомы формулу а Ф О -1- Чх (х' = а) и ввести надлежащее определение для символа е- или (, позволяют не брать в качестве исходной формулы аксиому индукции.
о м л , взяв При этом целесообразно слегка изменить и формулу (р,), вместо нее переводимую в нее формулу А (а) -ь 11 А (х) ( а'. Выводимость аксиомы индукции вытекает из того ранее уже потом и аксиома отмечавшегося факта, что схема индукции, а пото у индукции, выводима средствами исчисления предикатов из двух равенства ()2). В этом выводе аксиомы для е-символа могут быть заменены аналогичными им формулами для р-символа, т.
е. форм лой;) и (р А(а)- рхА(х) чь а'. Но последняя из этих формул с помощью аксиомы равенства ()а) и формулы ) (а(а) выводится из формулы ()лз), а формула ) (а( а) получается из первого рекурсивного равенства для сложения а+О=а, если предикатный символ ( определить с помощью эквивалентности а ( Ь Ух (Ь+ х чь а), которая выводится из эквивалентностей а( Ь 1(Ь (а), а~Ь Чх(а+х=Ь).
Ф ормализм, м, к которому мы таким образом приходим, содер- 1 и п авила исчисжит переменные, снмволы, исходные формулы и прав ления предикатов) кроме того, к ним добавляются следующие символы и аксиомы: выступали бы а качестве обращений формул лл«хА (х) -л А (о) н А (о) -л ЭХА (х). Втн дее пары фопмул соотеетстауют формулам сс-Группыл нз работы дж, фон Неймана: хоп гестапо з. Енг Н11ьсг1зсйеп Веже1зщеоые.— Ма1й.
Е., 4 21 ФОРМАЛИЗАЦИЯ АРИФМЕТИЧЕСКОГО ФОРМАЛИЗМА 367 ВЫХОД ЗА РАМКИ ТЕОРИИ ДОКАЗАТЕЛЬСТВ 1гл. и знак равенства с аксиомой ()е) а = Ь- (А (а) -ь А (Ь)); индивидный символ 0 и штрих-символ с аксиомами с числовыми а'чьО, а'=Ь'-ьа=Ь н а~О-ьЧх(х'=а); венствами символы для сложения и умножения с рекурсивными и ра- а+О=а, а 0=0, а+Ь'=(а+Ь)', а Ь'=а Ь+а; символы а ~ Ь и а( Ь с эквивалентностями а~Ь Лх(а+х=Ь) и а(Ь Ух(Ь+хчьа) и )ь-символ с аксиомами (Р') А (а) -~ А ()г„А (х)), (Рз) А (а) — )з,А (х) ( а' (Р.') 1 А ОА„А (х)) -ь Р„А (х) = О.
Кроме того, с помощью явных ап еделений нительно введены - б какне-ли о новые ф нк ио ре елений могут быть дополнальных знаков представляют собой некото олы. и определения при введении ф н фу кциосо ои некоторые Равенства у предикатных символов — эквивалентности. П и это в качестве переменных для арг ментов вво ль д д тельно об ин иви ные пе еменные. р ные. Ввиду соглашений относил о о щего вида явных определений з), вы а в правых частях опре ), выражения, стоящие пре щ Равенств или эквивалентностей, пределяю их аргументов определяемых символо . ны иметь никаких других свободных пе еменных, к Р , кроме писанный таким образом а ифметиче р скин форм лиз в даль смотрим более подробно и убедимся чт дл ются ния еих теорем Геделя о неполноте').
') См. т. 1, с. 357 или Приложение 1, с. 465 и далее. з) Мы могли бы взять несколько более який ж~ узк» формализм, воспользоваввости фор алин ~а (2 ) ф что при оассмот н р могут быть исключены (метоормульные пепеменные мо ечи. случае, когда мы опираемс гл, т.; см. с. 275 — 283, 286— тики исчисления пр а у рнфметизапию л~етаматемая на уже имеюш юся а упрощениям. икатов, зто едва ли привело бы к каким-нибудь Предположение а,)') для этого формализма выполняется, так как он содержит в себе исчисление предикатов, а также аксиомы равенства и аксиому а'чьО и так как в нем явно определены рекурсивные функции, для которых соответствующие рекурсивные равенства являются выводимыми формулами.
Таким образом, нам остается проверить выполнение условия б,), а также трех условий 1 — 3 на выводимость'), Для этого в первую очередь требуется ввести подходящую нумерацию нашего формализма. б) Построение нумерации формализма (Еп). Чтобы получить нумерацию этого формализма, мы начнем с имеющейся у нас нумерации исчисления предикатов, которая в свое время была распространена также на цифры и на функциональные знаки '). Приведем краткую сводку основных фактов, касающихся этой нумерации.
В качестве номеров для связанных нндивидных переменных мы взяли простые числа, ббльшие или равные 7; в качестве номеров для свободных индивидиых переменных -те же числа, умноженные на 2; в качестве номеров для формульных переменных без аргументов †же числа, умноженные на 10; в качестве номера для цифры 1 — число 2 31. Функциональный знак с г аргументами мы изобразили функцией б ае* ... а", а формульную переменную с г аргументами— фУнкцией 10 пез ....ч", где Ч„ ..., 4е — попаРно Различные пРостые числа, большие или равные 7, а вместо переменных а,, ..., а, должны подставляться номера аргументов. Логические связки мы изобразили следующим образом: отрицание — умножением на 3; конъюнкцию-функцией 1 20.7" 11', дизъюнкцию — функцией 2 20 7е 11з; импликацию — функцией 4 20 7' 11з; эквивалентность — функцией 8 20 7'1Р; кванторы всеобщности и существования с переменной 5 — функциями 50 4е И 100 Ча СООтВЕтСтВЕННО (ЗДЕСЬ 4 — НОМЕР ПЕрЕМЕННОй 5, а ВМЕСТО переменной а должен подставляться номер того выражения, на которое распространяется изображаемый квантор).
Чтобы из этой нумерации получить нумерацию для системы (Х„), мы сопоставим )ь-символу с переменной 5 функцию 25 аа, в которой 4 — номер переменной х, а вместо переменной а должен подставляться номер того выражения, на которое распространяется изображаемый )з-символ. Для изображения суммы ') См. с, 354. ') Сч с 35о н далее з] См. с.
267 в далее. ВЫХОД ЗА РАМКИ ТЕОРИИ ЛОКАЗАТЕЛЬСТВ )гл ч ФОРМАЛИЗАЦИЯ АРИФМЕТИЧЕСКОГО ФОРМАЛИЗМА и произведения мы возьмем функции 5 !1э.13' и 5 11' 17', что соответствует нашему прежнему соглашению об изображении функциональных знаков, а для изображения предикатных символов =, ~ и ~ мы возьмем функции 70 !1' 13', 70 11' 17е и 70 13'. 17' соответственно.
Отметим, что такое изображение данных трех предикатных символов не вступает в коллизию с нашим способом изображения формульных переменных. Действительно, наименьшим числом, которое по нашим соглашениям может быть номером какого-либо выражения, является число 2 (номер цифры О). Если 1 н 1 суть номера каких-либо выражений, то значение любого из выражений 70 11' 13', 70 11' 17' и 70 13~ 17' не может быть номером какой-либо формульной переменной без аргументов; но оно не может быть и номером формульной переменной с аргументами, потому что в этом случае оно должно было бы делиться на 7", где и — число, являющееся номером некоторого выражения и поэтому большее 1.
Что касается изображения штрих-символа, то мы должны учитывать то обстоятельство, что любая цифра в арифметическом формализме представляет собой либо символ О, либо выражение, получаю1цееся из символа 0 в результате (однократного или многократного) применения к нему штрих-символа, Учитывая имеющуюся уже нумерацию цифр, мы будем изображать применение штрих-символа к какому-либо квазитерму умножением номера этого квазитерма на 3. При этом для нумерации цифр достаточно будет приписать символу 0 номер 2. Зто изображение штрих-символа не вступает в коллизию с изображением отрицания, так как отрицание применяется только к таким выражениям, которые либо сами являются формулами, либо получаются из формул в результате замены свободных индивидных переменных связанными.
Эти выражения, которые мы будем называть квазиформулами, в нашей нумерации характеризуются тем, что их номера делятся на 10. Поэтому умножение на 3, примененное к номеру какого-либо выражения, изображает или отрицание или применение штрих-символа в зависимости от того, делится этот номер на 10 или же нет.
Для полного задания нумерации теперь нам недостает только соглашения относительно способа описания символов, вводимых явными определениями !как мы помним, в формализме (У,„) допускаются только такие (не считая основных) функциональные знаки и предикатные символы, которые вводятся 'с помощью явных определений!. Это обстоятельство доставляет нам известные трудности, поскольку мы хотели бы иметь возможность изобразить свойство числа быть номером терма или соответственно формулы с помощью рекурсивного предиката. Но эти трудности мы можем устранить, сделав номер символа, вводимого посредством явного определения, зависящим от номера определяющего его выражения ').
С этой целью мы условимся, что ао всяком явном определении в качестве аргументов определяемого т-местного символа всегда будут браться переменные с номерами 2.!оз, 2.!Яе, ..., 2 !о,эз, стоящие друг за другом в указанном порядке, так что место (-го аргумента определяемого символа всегда будет занимать перемен- ная с номером 2 (Я~+1. А теперь мы примем соглашение, что г-местный функциональный знак или предикатный символ, вво- димый посредством явного определения с определяющим выра- жением, имеющим номер и, будет изображаться функциеи 5 з" (р" ....(э" или функцией 70 ф ... !р'1, соот. '!и ' пФ1' пФ„ Я+1-1 ветственно. Это не будет вступать в конфликт с изображениями символов , =, «=. и ( с помощью функций, Действительно, наиболь- шим простым делителем у этих изображений является чис ло 17, т. е. (о„в то время как при изображении явно определенных символов простое число !'„по крайней мере равно )озм так как определяющее выражение содержит не менее одной свободной переменной, и потому его номер самое меньшее ра авен !4.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
