Гильберт, Бернайс - Основания математики. Теория доказательств (947376), страница 109
Текст из файла (страница 109)
3 аодно ввиду непротиворечивости формализма (Е!) пол ча что формула получается, ра(1)(1, 1, х)=О)=п не может быть выведена в (Хг). Только что доказанное утверждение дает нам приме а иф тической ф нк в см фу ции одного аргумента, однозначно определен ысле традиционной математики, т. е, с содержательным л иной использованием принципа «1ег1нчш поп ба(пг» для целых чисел, и отличающейся от каждой регулярно вычислимой функции хотя бы при одном значении аргумента. Впрочем, эта ф имеет ви д 1«„Я (и, х), где 01(п, а) — рекурсивная формула, и , эта функция с помощью принципа «1ег1шш поп йа1пг» она содержательно определяется как такая функция, которая всякому числу и, находящемуся в отношении И(п, г) по крайней мере с одним числом «„ ставит в соответствие наименьшее из чисел г, обладающих этим свойством, а всякому другому числу ставит в с ствие О. оответ- НЕРАЗРЕШИМОСТЬ ПРОБЛЕМЫ РАЗРЕШИМОСТИ 505 4 а! Имеют место и многие другие теоремы, говорящие о невозможности реализовать те или иные соответствия при помощи регулярно вычислимых функций.
Наиболее значительным результатом этого рода является теорема Алонзо Черча, касающаяся проблемы разрешимости исчисления предикатов, которую мы здесь и рассмотрим. й 3. Невозможность общего решения проблемы разрешимости для исчисления предикатов Проблема разрешимости для исчисления предикатов, рассматриваемая с точки зрения теории доказательств, — в дальнейшем мы будем интересоваться именно этим аспектом данной проблемы— касается исследования формул исчисления предикатов на предмет выяснения их выводимости. Общее решение этой проблемы должно было бы состоять в указании какого-либо общего метода, процедуры, с помощью которой относительно любой конкретной формулы исчисления предикатов можно было бы выяснить вопрос о том, является она выводимой в исчислении предикатов или же нет.
Понятие разрешающей процедуры являетгя неточным. Прояспение понятия разрешимости данного математического вопроса за конечное число шагов как раз и является одной из задач, поставленных Гильбертом перед теорией математического доказательства в его докладе <Аксиоматическое мышление» '). В рассматриваемой ситуации, как и в ряде других аналогичных случаев, задание разрешающей процедуры можно свести к заданию процедуры вычисления некоторой арифметической функции. Действительно, благодаря наличию нашей нумерации исчисления предикатов каждая формула этого исчисления характеризуется ее номером, который всегда может быть легко найден по предъявленной конкретной формуле и по которому, обратно, может быть наидена сама эта формула.
Кроме того, по любому числу можно непосредственно выяснить, является оно номером какой-либо формулы исчисления предикатов или же нет. Требующийся для этого способ мы ранее (в гл. 1!г) облекли в форму рекурсивного определения понятия формулы исчисления предикатов. Если теперь предположить, что в нашем распоряжении имеется способ, позволяющий распознавать выводимость любой конкретной формулы исчисления предикатов, то по любому данному нвм числу мы, во-первых, сможем выяснить, является ли оно вообще 0 поклал прочитав в 19!7 г.
в !(юрина, опубли«ваап в Майн АОБ., 7В, А!» 374, 506 НЕРАЗРЕШИМОСТЬ ПРОБЛЕМЫ РАЗРЕШИМОСТИ ПРИЛОЖЕНИЕ и! номером какой-либо формулы, и если это имеет место, то мы сможем найти соответствующую формулу и по иеи узнать, является ли она выводимой. Если эта формула выводима, мы сопоставим данному числу в качестве значения О, а во всех остальных случаях — число 1.
Тем самым оказывается заданной процедура вычисления значений некоторой арифметической функции одного аргумента, сопоставляющей каждому числу, являющемуся номером какой-либо выводимой формулы исчисления предикатов, значение О, а всем остальным числам — значение 1. И обратно, если бы нам была известна какая-либо процедура вычисления значений подобной функции, то она давала бы способ для распознавания выводимости любои конкретной формулы исчисления предикатов. И вообще, любую арифметическую функцию одного аргумента, которая по отношению к данному дедуктивному формализму г" и к данной нумерации выражений этого формализма обладает ' тем свойством, что ее значение для всякого числа, являющегося номером какой-либо выводимой в г" формулы, равняется О, в то время как для остальных чисел оио равно 1, мы будем называть р азр еш ающей функцией для г", связанной сданной нумерацией выражений этого формализма.
В этих терминах результат только что проведенного рассуждения выглядит следующим образом; общее решение проблемы разрешимости для исчисления предикатов равносильно нахождению способа, позволяющего вычислять значения разрешающей функции для исчисления предикатов, связанной с нашей нумерацией этого исчисления. Теперь мы можем воспользоваться тем, что понятие вычислимой функции было уточнено с помощью понятия регулярно вычислимой арифметической функции одного аргумента. Тогда вопрос о возможности общего решения проблемы разрешимости для исчисления предикатов приобретет следующую более точную формулировку: можно ли для исчисления предикатов и установленной для него нумерации формул указать какую-либо регулярно вычислимую разрешающую функцию? Как показал Черч'), ответ на этот вопрос является отрицательным.
Доказательство Черча мы приведем здесь в несколько измененном виде. Для доказательства нам потребуется следующая ') См, работу Черна: С Ь и г с Ь А. А по(е оп 1Ье Еп(зсЬеыппазргоЫепг.— 3, яушЬо!!с Ьоя!с, 1936, 1, № 1 и исправление к нерп 3. ЗушЬО!!с Ьод!с, 1936, 1, № 3. Другое доказательство, появившееся вскоре после работы Чбрча, принадлежит А. М.
Тьюрингу. Это доказательство основывается на теории машин, впоследствии названных его именем. См, Т и г ! пи А. М. Оп согпрп1аше пшпЬегз, «!63 ап арр!!сацоп 1о Ше Еп1зсье!бппкзргоЫеш,-ргос. Ьопб. Ма1Ь. Бос. Бег. 2, !937, ч2, в особенности см, с. 269 — 266. Лемма.
Не существует регулярно вычислимой функции, которая для формализма (Хоо) была бы раз)тем!агап(ей функцией, связанной с введенной нами нумерацией этого формализма. Эта лемма доказывается при помощи рассуждения Россера'), которое проводится по образцу геделевского уточнения антиномии лжеца: Допустим, что имеется некоторая регулярно вычислимая разрешающая функция для формализма (Еоо). Тогда эта функция представима в (Еоо) соответствующим термом 1(п). Рекурсивная функция 31(й, р, 8.3а), где р — номер переменной а, изображается в (Хоо) некоторым термом б()г)'). Если 1 является номером какого-либо выражения а из (Хоо), то значение терма б(1) является номером того выражения, которое получается из р( в результате замены переменной а всюду, где она входит в Я, цифрой 1.
Пусть 1 является номером формулы 1(б (а)) = О', а ш — номером формулы 1(б (1)) = О'! тогда 6(1) принимает значение ш, а равенство б(1)=ш выводится в (Хоо) Теперь рассмотрим значение терма 1(ш). По нашему предположению 1(п) является разрешающей функцией для (Еоо). Поэтому значение 1(ш) должно было бы равняться О или 1 в зависимости от того, выводится или не выводится в (Уао) формула с номером ш, т. е. формула 1 (б (1)) = О'.
Но ни тот, ни другой случай не могут иметь места. Действительно, если бы терм !(пг) имел значение О, то, с одной стороны, так как фУнкциЯ 1(п) вычислима в (Еоо), Равенство 1(п!) = О должно было бы быть выводимым в (Еоо), а с другой стороны, так как 1(и) является разрешающей функцией для (Еоо), в (~оо) должна была бы быть выводимой формула 1(в (1)) = О', ') См. и о з хе г 3. В. Ех1епз!опз о1 зове 1Ьеогешз о1 ОЫе! апб С)шгсЬ.— зугпьо!!с Ьок!с, 1936, 1, № 3, теорема 111.
') Терм о (А) может быть выбран в (хоо) даже рекурсивным, так как рекурсивное определение фувкции м(аь я, О фигурирует в рекурсивном опрелеле"ня функции «(1, и, г) и тем самым содержится в исходных формулах формализма (7 ), 5О9 ПРИЛОЖЕНИЕ !и НЕРАЗРЕШИМОСТЬ ПРОБЛЕМЫ РАЗРЕШИМОСТИ 4 з! а потому и формула 1(о!) = 0', Но тогда в (Хее) было бы выводимо равенство 0=0', в то время как этот формализм нумерически непротиворечив. А если бы 1(ш) имело значение 1, то, вследствие вычисли- мости 1(п) в (Хзе), в (сее) было бы выводимо равенство 1(н)) =0', а с помощью этого последнего — и формула 1 (в (!)) = 0'. Но тогда вследствие того, что функции 1(и) является разрешающей функцией для (2»з), терм 1(ш) должен был бы иметь значение О, что противоречит сделанному предположению.
Замечание. В приведенном доказательстве леммы использовались только немногие свойства формализма (Езе). На самом деле нами доказан существенно более общий результат, который может быть сформулирован следующим образом: Пусть Р— непротиворечивый дедуктивный формализм, в котором схемы замены и перестановки содержатся в качестве основных или производных схем.
Пусть в Р вычислима такая арифметическая функция одного аргумеюпа, которая для вполне определенной взаимно однозначной нумерации выражений формализма Р и конкретной числовой переменной а любому числу 1, являющемуся номером некоторого вь(ражения К из Р, ставит в соответспьвие номер того выражения, которое получается из К в результате замены переменной а всюду, где она встречается в К, числом 1. 'Тогда для формализма Р и для данной его нумерации не может существовать вычислимой в Р разрешающей функции '). (При этом относительно Р не предполагается, что номера выводимых в нем формул прн какой-либо нумерации образуют область значений какой-либо рекурсивной функции.) Из установленной нами невозможности построения какой-либо регулярно вычнслимой разрешающей функции для формализма (Хзз) мы получим невозможность построения регулярно вычислимой разрешающей функции и для формализма исчисления предикатов'), Для этого мы воспользуемся тем фактом, что при нашей нумерации формализма (сез) номера выводимых в (Езз) формул представляют собой значения некоторой рекурсивной функции 1,(п).
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
