Гильберт, Бернайс - Основания математики. Теория доказательств (947376), страница 77
Текст из файла (страница 77)
В случае выполнения этого условия непротиворечивость формализма будет сохраняться и при добавлении таких исходных формул, которые могут быть выведены из формул, верифицируемых в только что указанном широком смысле этого слова. Пусть, например, у нас имеется формула эйхЗуэчи'Зо)1 (х, у, и, о), изображающая высказывание, которое с помощью введения двух вычислимых функций 1(а) и й(а, Ь) может быть в фннитном смысле усилено до утверждения: «для любых чисел г и ( имеет место отношение 6(1, ((1), (, й(1, 1))».
Тогда формула Я(а, 1(а), Ь, й(а, Ь)) верифицнруема, а формула чгхЭуУДЭОЯ(х, у, и, о) выводится нз этой формулы. Если, теперь, какой-либо арифмети- ческий формализм будет удовлетворять сформулированному выше минимальному требованию внешней непротиворечивости, то его непротиворечивость не нарушится ни при добавлении в качестве исходной формулы верифицируемой формулы е((а,)(а), Ь, й(а, Ь)), ') См. т.
1, с. 72.— Что касается соотношения между ы-непротнворечн- востью н внешней непротиворечивостью, то безусловно можно счнтзгь, что нн первая нз ннх не следует нз второй, нн вторая нз первой, ВЫХОД ЗА РАМКИ ТЕОРИИ ДОКАЗАТЕЛЬСТВ [ГЛ. Ч $ и ГРАИИЦЫ ИЗОБРАЗИМОСТИ И ВЫВОДИМОСТИ 383 ни при добавлении формулы ЧхйуУИЛО91(х, у, и, О). Мы упомянем также следующие, касающиеся внешней непротиворечивости результаты, которые могут быть извлечены из наших предшествующих доказательств: 1.
Из теоремы, полученной нами в результате формального усиления теоремы Геделя о полноте'), вытекает, что если некоторая система аксиом первой ступени непротиворечива в рамках исчисления предикатов, то оиа останется непротиворечивой также и после формализации в ней какого-либо содержательно правильного рассуждения, по крайней мере если эта формализация возможна в каком-нибудь арифметически непротиворечивом формализме. 2. Параллельно с тем доказательством непротиворечивости, которое мы в начале гл.
П провели с помощью нп-теоремы для рассматривавшегося там ограниченного формализма арифметики '), была установлена и внешняя непротиворечивость этого формализма (в смысле сформулированного нами минимального требования). Действительно, мы установили, что полученное доказательство непротиворечивости остается в силе и в случае присоединения к этому формализму правила, позволяющего добавлять верифицируемые исходные формулы, а также вводить с помощью верифицируемых аксиом новые функциональные знаки.
Вп рочем, этот дополнительный результат получается, как легко заметить, и с помощью другого, изложенного в гл. П, метода доказательства непротиворечивости, использующего п оцедуру цифровых замен. ь щего пров) Вторая теорема Геделя о неполноте. В рассуждении, с помощью которого была получена первая теорема Геделя о неполнотеа), формализация модифицированной антиномии лжеца произведена не полностью. Правда, предложение, говорящее о своей собственной недоказуемости изображается в нем некот ф муло[[, а именно формулой ) 6 (т, 8(Р, В)) или соответственно переводимой в нее формулой ) 6 (т, 9).
Но затем следует неформальное доказательство, с помощью которого мы убеждаемся, что в рассматриваемом нами формализме г' — к которому относятся предположенные свойства формулы 6 (ти, и) и рекурсивной функции 8(й, 1), а также задание цифр р и е — формула 16(лт, [[) невыводима, если этот формализм непротиворечив, и что, с другой стороны, при выполнении этого условия для любой цифры я[ дима в г". отношение ) 6(п[, [[) выполняется и формула ) 6(а ) в ») См.
с. 284 и 3[8 — 3!9. ») См. с. 79 и далее. а) См. е. 339 и далее, Однако формальное имитирование этой антиномии может быть продвинуто дальше. И это тоже было сделано Геделем. Действительно, рассуждение, показывающее, что в случае непротиворечивости формализма г для каждой цифры я! имеет место отношение ) 6([я, 9), при известных предположениях, которые мы в дальнейшем укажемт), может быть формализовано с помощью некоторого вывода в Р: именно, формула ) 6(т, ч) (с переменной т) может быть выведена из формулы [1, выражающей утверждение о непротиворечивости г" в следующей его редакции: «Никакая формула формализма г" не может быть выведена в этом формализме вместе со своим отрицанием». А теперь на основе этого вывода, который вскоре будет рассмотрен более подробно, получается, что в случае непротиворечивости формалнзма г не может существовать формализованного в г" доказательства этой непротиворечивости, т.
е. вывода я Р уже упоминавшейся нами формулы 5. Действительно, из такого вывода в сочетании с выводом, упомянутым ранее, получилось бы, что выводима формула ) 6 (т, ч), а относительно нее мы ранее убедились, что в случае непротиворечивости г" она не может быть выведена в этом формализме. Этим доказательством, показывающим, что в случае непротиворечивости г формула м, выражающая эту непротиворечивость, не будет выводима в г", формализация модифицированной антиномии лжеца достигает своего полного завершения. В самом деле, эта невыводимость как раз и представляет собой то, что в четко очерченных дедуктивных формализмах соответствует противоречию, получающемуся при изложении данной антиномии в рамках естественного языка.
Возможность избежать этого противоречия, которая ввиду указанной невыводимости имеется в дедуктивных математических формализмах, в обиходном языке отсутствует потому, что в нем правила логического следования не являются абсолютно установленными, а мыслятся как обосновываемые с помощью разумных соглашений. Тем самым заранее исключено, чтобы корректно проводимые доказательства при отсутствии ложных посылок давали противоречие. Поэтому при рассуждении в рамках естественного языка всякое допущение, приводящее нас к заключению о доказуемости некоторого предложения вместе с его отрицанием, тем самым оказывается 'ложным, в то время как при формальных рассуждениях в рамках какого-либо математического формализма соответствующее рассуждение еще требует добавления посылки, которая выражала бы предположение о непротиворечивости этого формализма.
3 а меча и не. Заметим, что преодоление противоречия при формализации модифицированной антиномии лжеца происходит ') [[опуи~еяии а,) и з«) и условия иа иыаодимость (см, с. 354 — 3551. 12 д. Гиаьаерп П. Вера«а« выход зл глмки твогин доклзлтвльств 1гл ч существенно иначе, чем при формализации первоначальной антиномии. В то время как при формальном имитировании первоначальной антиномии противоречие устраняется тем, что определенное словосочетание нашего языка оказывается непереводимым на язык формализма, в случае модифицированной антиномии все входящие в рассмотрение языковые термины допускают соответствующее изображение в формализме, и здесь устранение противоречия основывается на том, что некоторый способ рассужде.
ния, допустимый при аргументации в рамках естественного языка, становится недопустимым после того, как мы переведем его на язык формализма. Теперь речь пойдет о том, чтобы убедиться, что яри определенных предположениях вывод формулы ) 6(т, з) изформулы й:, формализующей утверждение о непротиворечивости формализма Р, оказывается осуществимым в Р. Что касается формулировки этих предположений, то мы сначала обобшим допущение ае) '), добавив предположение, что формализм Р содержит кванторы вместе с соответствующими им формальными способамн умозаключений. Так, вместо допущения а,) у нас появится следующее более сильное допущение: а,) Формализм Р содержит символы и переменные рекурсивной арифметики и исчисления предикатов, за исключением, быть может, формульных переменных; каждая формула, выводимая средствами рекурсивной арифметики и не содержащая формульных переменных, выводима также и в Р, а каждый производимый средствами исчисления предикатов переход от одной формулы формализма Р к другой производим также и в Р.
Условие б;) е), которое неявно использовалось уже при построении формулы ) 6(т, «)), теперь будет заменено следующим, более общим требованием: б,) Имеется нумерация выражений формализма Р, обладающая следующими свойствами: Номер отрицания формулы с номером п изображается в его зависимости от и некоторой рекурсивной функцией е(п).
Номер формулы, получающейся из формулы с номером в результате повсеместной замены переменной а цифрой 1, изображается в его зависимости от 1 и 1 некоторой рекурсивной функцией б(й, 1). Существует рекурсивная формула 6(т, и), не содержащая отличных от т и и переменных и обладающая тем свойством, что цифра и является номером некоторой выводимой в Р формулы тогда и только тогда, когда можно указать цифру пе такую, что имеет место отношение 6(пе, и).
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
