Гильберт, Бернайс - Основания математики. Теория доказательств (947376), страница 84
Текст из файла (страница 84)
Каждому такому вхождению рассматриваемой переменной е, в выражение 6(а„..., а,) в рамках нашей нумерации соответствует вхождение номера этой переменной, — возможно, несколько раз умноженного на 3 — в качестве показателя степени некоторого простого числа, а замене переменной и; цифрой 1; соответствует замена номера этой переменной значением выражения 2. 3 '. Поэтому искомое функциональное выражение 1(п„..., а,) можно получить, имитируя средствами нашей нумерации построение выражения 6(а„..., а„); при этом всюду, где переменная а; (1=1, ..., с) входит, — возможно, с несколькими штрихами — в качестве аргумента какой-либо формульной переменной, предикатного символа или функционального ' '.
знака н где в соответствии е этим в изображающем 6(п„..., а,) арифметическом выражении в качестве показателя степени при каком-либо простом числе фигурирует номер этой переменной аь— быть может, умноженный на какую-либо степень числа 3,— мы; должны вместо 'номера этой переменной и, подставить выражение .' 2.3 '. Пусть, например, 6(а, Ь) представляет собой импликацию е(а-мс:,а" +Ь. Тогда 1(а, Ь) будет представлять собой выражение 30, уто,!ззо,пз з 11то.!зтз !тз !' ' ' !Зз з Функциональное выражение 1(а,, ..., а,), построенное указанным способом для выражения 6(а„..., а„) нз (Хп) со свободными индивидными переменными и„..., а„мы будем называть а р ифметическим функциональным выражением, сопоставленным выражению 6(а,, ..., а) относительно переменных и„..., а,.
При этом указание «относительно переменных и„..., а,» может быть опущено, если рассматриваемое выражение никаких других свободных индивидных переменных не содержит. Проверяя для (Ер) третье условие на выводимость'), мы постоянно будем использовать эту конструкцию. Сначала мы применим ее для того, чтобы придать этому условию другую редакцию, опираясь на следующее обстоятельство: Если с — номер выражения из (Хп), содержащего переменную г, а й(с) — сопоставленное этому выражению относительно переменной с арифметическое функциональное выражение, то в (Ем) выводимо равенство') з(е(т 14 2.3с) й(с), В силу этой выводимости рассматриваемое нами условие на выводимость равносильно следующему: Если 1(и) — рекурсивный терм, содержащий единственную переменную и, а й (а) — арифметическое функциональное выражение, сопоставленное равенству ((а) = 0 (относительно переменной а), то формула ! (и) = 0-м Зха (х, й (и)) выводима в (ЕР).
Поясним это условие на каком-нибудь простом примере. Возьмем в качестве 1(и) терм и+О. Тогда роль й(а) будет играть выражение 70.11( " "') 13' Требуется найти вывод формулы и+О= О-мосха(х, й(и)). Но эта формула переводима в формулу :-)ха(х, й(0)), а) См. с. 355. ') В етом нетрудно убедиться с помопаю определения функции 21»; см. е.
37!. 13 Д Гнаьоарт п Бернайс звт звв ВЫХОД ЗА РАМКИ ТЕОРИИ ДОКАЗАТЕЛЬСТВ [Гл. у ФОРМАЛИЗАЦИЯ АРИФМЕТИЧЕСКОГО ФОРМАЛИЗМА а значит, и в формулу Лх8(х, 70 11» '"'з' 13»). Значение выражения У0.1Р [[*.[з' 13» является номером формулы 0+0 О. Если обозначить этот номер буквой и, а буквой ш обозначить номер списка формул, состоящего из двух формул а+О= а и О+ 0 0 (первая из которых является одним из рекурсивных равенств для сложения, а вторая получается из первой в резуль- тате подстановки вместо переменной а), то формула Е» (ш, и)— а потому и 6(ш, и) — будет выводима в (УР), Но из нее получается формула :-)хк[(х, и).
Таким образом, в этом весьма частном случае выполнимость рас- сматриваемого условия установлена. Теперь мы убедимся, что искомая выводимость имеет место всегда. Прежде всего мы напомним смысл высказывания, которое формализуется посредством формулы ((т) 0-«-Вх6(х, й(т)), где ((т) — рекурсивный терм с единственной переменной т, а й (а)— арифметическое функциональное выражение, сопоставленное равен- ству ((а) =0 относительно переменной а.
Зто высказывание может быть сформулировано следующим образом: «Еели для какой-либо цифры 1 значение терма ((1) равно О, то равенство выводимо в (ЕР)». Содержательная истинность этого утверждения усматривается следующим образом: Любое вычисление значения рекурсивного терма без переменных в рамках рекурсивной арифметики может быть формализовано выводом равенства, указывающего результат этого вычисления. В этом вь[воде в качестве исходных формул используются рекурсивные равенства для рекурсивных функций, прямо или косвенно фигурирующих в этом терме, и аксиомы равенства. При этом использование этих формул производится с помощью подстановок и схем заключения.
Если к используемым рекурсивным равенствам, не являющимися равенствами для сложения и умножения, добавить их выводы, то из любого такого вывода в рамках рекурсивной арифметики получится некоторый вывод в формализме (ХР). В самом деле, рекурсивные функции, за исключением сложения и умножения, в формализме (7 ) вводятся посредством явных определений и, как мы знаем, рекурсивные равенства, соответствующие этим функциям, выводимы на основе этих определений. Таким образом, задача искомого доказательства заключается в том, чтобы показать, что применение только что проведенного метаматематического рассуждения к любому рекурсивному терму [(а) может быть формализовано в (2Р) выводом соответствующей формулы [(т)=0-Р'ЗЛЗ(х, й(л[)).
3 а меч ание. Отличие искомого доказательства от только что проведенного рассуждения будет заключаться в том, что в данном рассуждении содержательная всеобщность распространяетсп как на терм [(а), так и на цифру й а в искомом доказательстве содержательная всеобщность будет распространяться только на терм [(а), тогда как всеобщность в отношении цифры 1 заменится некоторой формальной всеобщностью, которая выразится в появлении переменной л[ в зависящей от ааданного терма [(а) формуле, вывод которой ищется.
Сначала мы докажем следующую лемму: Если некоторая выводимая в формализме (ХР) формула содержит переменные а,, ..., Аи а й(АМ ..., «,) представляет собой арифметическое функциональное выражение, сопоставленное этой формуле относительно переменных ам ..., а„то формула Чхб(х, й(а„..., а,)) тоже выводима в (ХР). Для доказательства мы воспользуемся сделанным ранее замечанием'), что для любого простого числа р, большего или равного 3, в (ЕР) выводима формула Эха(х, й) «-Эха(х, з[*(й, 2 р, 2 3')). Применяя это замечание нужное число раз, мы получаем, что для произвольных простых чисел р„..., р„ббльших или равных 3, и для произвольных отличных друг от друга свободных инднвидных переменных а„..., а«в (Х ) выводима формула :-)х8 (х, й) -Р "=)х8 (х, з[* (з[ «(...
... (З1~(й, 2 Рм 2 3«~), 2 Р„2 3'»), ...), 2 Р«, 2-3")). Если в эту формулу вместо й мы подставим номер и какой-либо выводимой в (2 ) формулы, то посылка Зхк)(х, п) окажется выво- > см. «, звз, 13* выход зА Рамки тео~ии доказательств 1ГЛ. Ч % з! ФОРМАЛИЗАНИЯ АРИФМЕТИЧЕСКОГО ФОРМАЛИЗМА ззз димой формулой, и поэтому выводимой будет и формула Эхб (х, з1Ф(з1Ф (...(З(Ф (и, 2 Г„2 3'1)„2 р„2 3"з), ...), 2 р„, 2 3"')). Следовательно, для доказательства нашей леммы достаточно убеиться в выводимости в (ЕР) равенства З1Ф (З(Р (... (З(Р (П, 2 р„2. 3"1), 2 1„2 3"з), ... - е 2 р„2.3'~)=й(а„..., а,) в предположении, что и является номером некоторого выражения Я из (Х,„), содержащего переменные а„..., а,, числа 2 В„...
..., 2.р, суть номера этих переменных, а 8(а„..., а,) — арифметическое функциональное выражение, сопоставленное выражению Я относительно этих переменных. Мы немедленно получим вывод указанного равенства (с использованием аксиом равенства), если сумеем вывести равенства з(Р(1; о 2 р;, 2 3")=1; (1=1, ..., Г), где 1з представляет собой цифру и, а 1, при 1=1, ..., т означает арифметическое функциональное выражение, сопоставленное выражению Я относительно переменных а„..., аь Но вывод этих равенств может быть получен на основании рекурсивного определения функции з(Р (лз, й, 1), если вспомнить структуру выражений 1; (1=0, ..., Г) и учесть, что индукцией по а может быть выведено равенство З1Ф(2 3', Ь, 1) =2 3, (Как мы помним, схема индукции в формализме (ХР) является производной.) Таким образом, наша лемма доказана.
Чтобы несколько облегчить ее применения, мы введем два сокращения. Одно из них будет заключаться в том, что выражение формализма (7 ), имеющее внд Зхб(х, 1), мы будем обозначать посредством 6(1). Далее, мы условимся,- что если Я вЂ” выражение из (ХР), а 1 — арифметическое функциональное выражение, сопоставленное выражению Я относительно всех входящих в него свободных индивидных переменных, то это функциональное выражение, фигурирующее в качестве аргумента формулы 6, мы будем записывать в виде заключенного в фигурные скобки выражения Я.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
