Гильберт, Бернайс - Основания математики. Теория доказательств (947376), страница 76
Текст из файла (страница 76)
2. Для всякого неиротиворечивога дедуктивного формализма Р, удовлетворяющего условиям ат), б1) и б;) и содержащего квантор 1) См. т. 1, с. 395 н далее. з) В данном частном случае, когда рекурсивная формула Э(т, л) нзо- брвжвет отношение вокззуеностн, искомую функцню Ь(л) можно получить несколько более про«тын способом. В этом случае формула ~В(т, л) имеет внд ЯЗ,(т) й(ч(т, Л(т))= — л), где З,(т) — некоторый рекурсивный преднквт, т. е.
ореднквт, представимый некоторым равенством Ь, (т) =О, где Ь, (т) — рекурсивная функция. Поэтому, если п является номером какой-либо доказуемой формулы, то рекурсивный терм и зйп(Ь«(т))+т (т, Л(т)) ° зйн (Ьт(т)) со свободной переменной т двет'пересчет (с повторениями) номеров выводнмык в д формул.
') Например, это требовзнне будет выполнено, если ножно уквзвть такую Рекурсивную формулу В (1, т, л), не содержзшую отличных от 1, т н и пеРеменных, что цнфрв ю является номером некоторого вывода формулы с но. нзроы в тогда н только тогда, когда отношзнне й(1, зь в) имеет место для некоторой цифры 1. В этом можно убедиться, воспользовзвшнсь внесю только что нсвользоввнного пересчета числовых нвр рекурсивным пересчетом числавых троек. 348 ВЫХОД ЗА РАМКИ ТЕОРИИ ДОКАЗАТЕЛЬСТВ 1гл.
Р 4 П гнкницы изовРАзимости и выводимости всеобщности вместе с Относящимися к нему формальными способами умозаключений, можно указать такую рекурсивную функцию ((т), что ни формула 'чх(((х) =- 0), ни ее отрицание не будут выводимы в г, (Из невыводимости формулы )>Ух(~(х)=0), в частности, следует, что для любой цифры ( формула ((() =0 является истинной и выводимой в г.] Поэтому каждый обладающий достаточными изобразительными возможностями и достаточно четко очерченный формализм является дедуктивно незавершенным; точнее говори, существуют предложения, причем да>не предложения рекурсивной арифметики, которые формулируемы в нем, но дедуктивно неразрешимы.
Если же удастся доказать непротиворечивость этого формализма р, то найдется такое предложение рекурсивной арифметики, которое хотя и будет доказуемым, но не будет формально доказуемым в г". Действительно, если формализм г" непротиворечив, то предложение, изображаемое рассматриваемым нами равенством ((т) = О, в силу доказанной теоремы о неполноте будет истинным. Поэтому любой дедуктивный формализм, для которого удается провести доказательство его непротиворечивости, не может содержать в себе запас всех возможных доказательств арифметических предложений.
Если даже отвлечься от трудностей, связанных с проблемой установления непротиворечивости, то и тогда — уже в силу констатированной нами дедуктивной незавершенности любого обладающего достаточными изобразительными возможностями и достаточно четко очерченного дедуктивного формализма — идея характеризации математики как дедуктивного формализма, время от времени выдвигавшаяся различными логистическими системами, представляется бесперспективной *).
Излагая наше представление об исходной проблематике и о целевой установке теории доказательств, мы с самого начала избегали введения идеи о какой-либо всеобъемлющей системе математики в каком-либо философски принципиальном смысле слова. Более того, мы удовольствуемся тем, что реально существующую систематику анализа и теории множеств мы охарактеризуем как дающую нам подходящие рамки для упорядочения геометрических и физических дисциплин. Этой цели может служить и такой формализм, который не является дедуктивно вполне завершенным.
Наша точка зрения, согласно которой при построении системы анализа и теории множеств на основе содержательной установки речь идет об образовании идей, экстраполирующих действитель- *) у авторов «ита«пеета໠— Прим, яе>>ев, ность, тоже хорошо согласуется с незавершенностью этой системы; способы умозаключений этой системы ориентированы в сторону представления о завершенной, окончательно определенной действительности и представляют собой формальное выражение этого представления. Но отсюда вовсе не следует, что порождаемая этими способами умозаключений дедуктивная (метаматематически оформленная) структура должна обладать свойством абсолютной завершенности.
Разумеется, в известной степени она наверняка обладает методической завершенностью, а именно той завершенностью, в силу которой мы при обычных способах рассуждений, применяемых в анализе и теории множеств, так сказать, сами по себе остаемся в области этого формализма, и такой степени завершенности вполне хватает для той цели, которой служит этот дедуктивный формализм. И все же возникает некоторая другая проблематика, если принять во внимание то вытекающее из теоремы Геделя соображение, что финитное доказательство непротиворечивости формализма анализа и теории множеств позволило бы нам получить фииитное доказательство некоторого арифметического предложения, невыводимого в указанном формализме.
Выглядит несколько парадоксальным, что при доиазательстве арифметических предложений методы финитной теории доказательств в определенном отношении превосходят методы анализа и теории множеств. Это приводит нас к проблеме выяснения границ применимо. сти финитных методов и одновременно с этим к проблеме разумного ограничения методической установки теории доказательств.
В дальнейшем мы более подробно займемся этими вопросами.— С результатом Геделя связана еще одна точка зрения, которую П. Финслер в своей работе «Формальные доказательства и разрешимость» ') высказал за несколько лет до геделевского исследования формально неразрешимых предложений. Интересно, что уже в этой работе Финслер высказал тезис о том, что в любом четко определенном и обладающем достаточными изобразительными возможностями формализованном языке могут быть сформулированы такие предложения, которые в этом формализме дедуктивно неразрешимы, между тем как с содержательной точки зрения они являются истинными, Разумеется, аргументация, с помощью которой Финслер обосновывает свое утверждение (она представляет собой некоторую модификацию парадокса Ришара), не может быть использована в теории доказательств') и само зто утверждение является ») г1п»!вг Р. Р««п>а1« Вся«1»е ппа Еп1»«ЬЫВЬ»г««11.— МА1Ь.
с., 1926, 25, ') Формализмы, которые рассмвтривает Февсяер, обяадвют такими бельшиии семантическими и»обраэнтельиыми возможностями, что в них может быть получен обыкновенный парадокс Ришара. Финслер ие считает этот яа- ВЫХОД ЗА РАМКИ ТЕОРИИ ДОКАЗАТЕЛЬСТВ 1гл. ч ГРАИИЦЫ ИЗОБРАЗИМОСТИ И ВЫВОДИМОСТИ з и лишь некоторым аналогом теоремы Геделя, так как оно формулируется в совсем других предположениях. Но во всяком случае заслуживает серьезного внимания та имеющая принципиальное значение мысль, которую Финслер— со ссылкой на существование в достаточно богатых выразительными возможностями формализованных языках дедуктивно неразрешимых предложений — выдвинул здесь на первый план, связав ее с вопросом о непротиворечивости.
Он подчеркнул, что доказательство непротиворечивости какого-либо формализма в обычном смысле этого слова еще не дает .никаких гарантий от противоречий, потому что противоречие может заключаться в формальной выводимости отрицания некоторого выразимого в данном формализме, но не выводимого предложения, которое, однако, с содержательной точки зрения может быть признано истинным. Теорема Геделя показывает, что это соображение применимо и к формализмам, рассматриваемым в теории доказательств, причем даже в том случае, когда в основу рассмотрения кладется финитная точка зрения. Действительно, возьмем какой-либоформализм г", удовлетворяющий условиям а,) и б;) и содержащий квантор всеобщности, и на основании этой теоремы построим такую одноместную рекурсивную функцию ((т), для которой в случае непротиворечивости этого формализма равенство ((1) = 0 истинно при любой цифре 1 и невыводима формула ч(х(1(х) =О).
Если к исходным формулам этого формализма добавить формулу ) »1х(1(х) =О), то полученный формализм Р,— в предположении, что в исходном формализме г" действует дедукционная теорема') — будет обладать тем свойством, что с доказательством не противоречивости г" будет получаться и его непротиворечивость. Несмотря на непротиворечивость г"ы выводимая в г"з формула ) Чх(1(х) = О) в данном случае будет изображать отрицание истинного высказывания, и эта непротиворечивость формализма г", будет утрачена, если мы добавим к г", в качестве формальной аксиомы изображение некоторого истинного высказывания, которое дается формулой эчх(((х) =О). редок« воэннкэюшнм в таком формализме е необходимостью, э рассматривает его лишь кэк противоречие, возникающее вследствие недорээуменнн, Прн этом под форм ел немом Фннелер понимает нечто совсем отлкчное от того, что нод этим понимается в теории доказательств; з именно, формвлнзм понимается нм всего лищь кзх придание словзм, грэммэтнчеекнм формам н еостэвным конструкциям определенных значений, нэ основе которых для любого конкретно предънвленного текста е помощью нэдлежэшего рвзборэ можно решить вопрос о том, выражает лн он какое-либо еодержэнне (нлн, соответ.
«твенно, чтб именно он выражает).— Из рассуждений Фннслерэ совершенно не вытекэет, что формальна нерээрешнмые нредложеннк могут возникать н в формализмах, рэссмэтрнвземых в теории докэззтельств. з) См. т. 1, с. 194 — 199. Но от непротиворечивого в полном смысле этого слова дедуктивного формализма арифметики мы будем требовать, чтобы никакая выводимая в нем формула не была отрицанием формулы, изображающей какой-либо факт, устанавливаемый финитно.
Это требование мы будем называть условием внешней не- и р о т и в о р е ч и в о с т и. Мы указывали на него уже и ри нашем первоначальном изложении теории доказательств '). Правда, фигурирующее здесь понятие финитно устанавливаемого факта является неточным. В качестве более точного минимального требования внешней непротиворечивости для арифметических формализмов можно выдвинуть следующее: непротиворечивость формализма должна сохраняться при добавлении к нему каких угодно верифицируемых формул в качестве исходных; причем эти формулы могут строиться как из символов рассматриваемого формализма, так и из каких-нибудь вновь вводимых функциональных или преднкатных символов (в последнем случае верифицируемость формул должна устанавливаться на основе специально добавляемой процедуры нахождения истинностных значений элементарных формул, построенных из этих символов и цифр). Замечание.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
