Гильберт, Бернайс - Основания математики. Логические исчисления и формализация арифметики (947375), страница 86

Просмтор этого файла доступен только зарегистрированным пользователям. Но у нас супер быстрая регистрация: достаточно только электронной почты!

Текст из файла (страница 86)

Все ати выводы основываются на элементарном исчислении со свободными переменными. Если же эа основу взять исчисление предикатов, то тем более получится, что все формулы системы аксиом (В) могут быть выведены из системы аксиом, состоящей из второй аксиомы равенства, формулы 0 ~ О, рекурсивных равенств для функций 6 (и) и а — ' Ь и аксиомы индукции, т. е. из системы формул ! а = Ь е- (А (а) — ~ А (Ь)), 0' Ф О, 6(О)=О, 6 (и') = и, а — 'О=а, а — ' и' = 6 (а — ' и), ( А(0) 61~а(А (а) -+ А(а')) — +- А(а) с добавленным явным определением а Ь ° Ь вЂ” а~О.

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

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

е. 371 и далее. енного герма таким образом, чтобы при аамене данного функционального знака этим термам формулы, посредством которых вводится этот функциональный знак, переходили в выводимые (т. е. в выводимые в исходном формализме). В этом смысле слова формализм системы (В) расширяется унее введением функции 6 (и) при помощи рекурсивных равенств 6 (0) = О, 6 (и') = п. Под формализмом системы (В)мыприэтомпонимаем систему аксиом (В) с включением всех тех соглашений, на которые опирается применение этих аксиом, а также всех тех правил образования термов и формул и проведения доказательств, которые допускаются этими соглашениями. В этом формализме всякий терм представляет собой либо цифру, либо переменную, либо переменную, снабженную штрихами.

Таким образом, явное определение 6 (и) с помощью терма могло бы иметь только вид 6 (п) = а(1), где а — либо символ О, либо какая-нибудь переменная, Терм а() должен был бы содержать переменную и, потому что в противном случае при замене 6 (и') выражением а(О равенство 6(п') =и должно было бы перейти в формулу, выводимую средствами системы (В), т.

е. оказалось бы выводимым равенство а(1) = и. Но тогда средствами системы (В) можно было бы вывести и формулы а(1) = О, а(1) = 0' (так как по предположению а не содержит переменной и), а тем самым и формулу 0' = О. Но мы знаем, что эта формула, являющаяся ложной, не может быть выведена средствами системы (В).

Таким образом, а могло бы быть только переменной и, и, значит, наше явное определение тогда имело бы вид 6 (п) = п(1). Но этот случай тоже не мон1ет иметь места; действительно, если бы это равенство представляло собой соответствующее явное определение, то для 6 (и') в качестве замены получалось бы и(1~') $ з) НРедстлвимость РекуРсиВных Функции (гл, уы РЕКУРСИВНЫЕ ОПРЕДЕЛЕНИЯ и тогда средствами системы (В) можно было бы вывести равенство п($+1) = п, получающееся в результате этой замены иэ второго рекурсивного равенства для 6 (и). Но тогда было бы выводимо и равенство 0((»1) — О между тем как эта формула является ложной.

Таким образом, функция 6 (и) действительно пе допускает явного определения в формализме системы (В). И тем не менее совокупность высказываний, изобразимых в формализме системы (В) посредством формул '), не претерпевает никакого расширения. Действительно, функциональное отношение, изображаемое равен- ством 6(а) =Ь, может быть выражено без функционального знака 6 формулой (а = 0 дг Ь = О) )/ а = Ь'. Именно, если мы сокращенно обоаначим эту формулу посредством В (а, Ь), то из аксиомы (»1) непосредственно могут быть выведены В (О, 0), В (и', п); из этих формул при помощи схемы индукции можно будет полу- чить ЛхВ (а, х), а с помощью формул (Р,), (Р,) и второй аксиомы равенства мы получим В (а, Ь) дг В (а, с) -»- Ь = с.

Эти две формулы выражают тот факт, что отношение В (, ) В (а Ь) всякому значениго переменной а однозначно сопоставляет то единственное значение переменной Ь, для которого имеет место В (а, Ь), а омлы фру В(0, 0), В(п', и) вы ражают тот факт, что это соответствие, рассматриваемое как ф нкция, удовлетворяет рекурсивным равенствам дл ( ). У Только что приведенные выводы осуществляются беа испол- ьзования функции 6 (и). Если нге дополнительно присоединить рекурсивные равенства для 6 (и), то индукцией по а мы получим 1) заметим, что формула, принадлежащая формализму системы,' ), ыгз св 1 не обнзатзльно должна быть выводимой формулой.

эквивалентность 6 (а) = Ь В (а, Ь), которая в прямом виде выражает тот факт, что 6 (а) равно тому числу Ь, которое находится к а в отношении В (а, Ь). Из этой эквивалентности с помощью аксиом равенства (т. е. с использованием формулы ба)) из гл. У) ') можно, далее, получить формулу А (6 (а)) э1 х (В (а, х) -» А (х)), при помощи которой любая формула, построенная с использованием функционального знака 6( ° ), может быть переведена в такую формулу, в которой этот функциональный знак не встречается.

Между прочим, с исключением функционального знака 6( ° ) из формул можно связать (что из предшествующего непосредственно не усматривается) исключение функции 6 (и) иа выводов; иначе говоря, в выводе формулы, не содержащей функционального знака 6( ), мы всегда сможем обойтись без использования функции 6 (и). То, что это действительно имеет место, в дальнейшем моягно будет извлечь из одной весьма общей логической теоремы об устранимости понятия зтот, который», доказательство которой будет приведено в следующей главе з). Рассмотренная нами связь мепгду равенством 6(а) =Ь и формулой В(а, Ь) поаволяет сделать следующие выводы относительно цифр, являющихся значениями фигурирующих здесь переменных: Если й— цифра, а г — значение, которое получается в ревультанге вычисления 6 (й), то формула В(й, г) является истинной и в то же самое время выводимой средствами системы (В).

А если и — цифра, отличная от г, то формула В(й и) является ложной, а ее отрицание выводимо средствами сиспгемы (В). Такое же положение вещей, с каким мы сталкиваемся здесь в связи с функцией 6 (и), имеет место и в отношении функции ') Сы. с. 2(4. з) Поскольку мы ограннчкзазысн рассмотренном таких доказательств, заключктзльныз формулы которых нз содержат форыульных пзрзызнных, ыы можем доказать устранкыость функции 6 (л) также н с помощью ыоднфнкзцкн разработанного з гл. ч1 метода редукции. 432 РБКУРСИВНЫБ ОПРБДБЛБНИЯ [ГЛ, Ч11 а (а, Ь), которую мы в нашей рекурсивной арифметике ввели посредством явного определения 1) а (а, Ъ) = зяп ((а †' Ь) + (Ь вЂ ' а)) с помощью функций а + Ь, а — ' Ъ и эдп п.

Относительно этой функции мы тоже мо1кем утверждать, что ока не допускает явного определения с помощью какого-либо терма, построенного из переменных и символа 0 при помощи штрих- символа. Но равенство а (а, Ъ) = с может быть заменено формулой (а = Ь бе с = О) 1[' (а ~ Ь й с = 0 ), принадлежащей формализму системы (В). К этой формуле упомянутое определение фупкции а (а, Ь) ведет кас ке непосредственно, а лишь через выводимые из него формулы а = Ь -ь а (а, Ь) = О, а чь Ь -е. сь (а, Ь) = 0'. Эти формулы определяют функцию а (а, Ь) в том смысле, что для любых двух цифр 3 и 1 (в зависимости от того, равны эти цифры или различны) они дают.

возможность вывести либо равенство а (3, 1) = О, либо равенство и(3, 1) = 0' и тем самым дают возможность формализовать вычисление значений этой функции. Если равекство и(а, Ь)=с замепить формулой (а=Ъбес 0) Ч'(а~Ьетес=ОР), которую мы для краткости обозначим посредством ьэ (а, Ь, с), то определяющие а (а, Ь) формулы перейдут в формулы а = Ь -+ Ж (а, Ь, 0), а~б-ь.[е (а, Ь, 0~), которые могут быть выведены с помощью формулы а а. е) См.

с. 391. икядстлвимость РккуРсивных фуккция Кроме того, о помощью аксиом равенства могут быть выведены формулы 6 (а, Ь, с) бе а = Ь -е. с = О, [е (а, Ь, с) ое а ~ Ь ь. с = 0'. Полученные четыре формулы показывают, что формула [е (а, Ь, с) находится к равенству а(а, Ь) = с в отношении, совершенно аналогичном тому, в котором ранее рассмотренная нами формула к) (а, Ь) находится к равенству 6 (а) = Ь. В частности, получается, что для каждой тройки цифр т, 3, 1, в которой 1 совпадает со значением а т, 3), средствами системы (В) может быть выведена формула ) (а, ы й)=[ можно представить, 'формулой Я(а...

Ь,, [) этого формализма в том смысле, что при каждом замещении меккых ии пере- а, ..., й, [ а, ..., $, [ цифрами ') Уб~~ы~, ыр делающее предстааикость, кы выбираем как можно окве слабым, чтобы утверждение о непредстаэимости было как можно более 23 Д. Гальбере, п. вераебе ьэ(т,б, 1) и что если 1 отлично от значения ы (т 3) то теми жа с средствами мон1ет быль выведена формула [(6 (т, 3, 1). Рассмотрение примеров этих двух функций, присоединение которых к формализму системы (В) хотя и расширяет запас термов > но ие изменяет запаса изобразимых отношений, иаводит кас па мысль дать следующее уточнение понятия существенного расширения (речыщет о расширении формализма путем присоединения какой-либо функции).

Характеристики

Список файлов книги