Гильберт, Бернайс - Основания математики. Теория доказательств (947376), страница 73
Текст из файла (страница 73)
Однако это определение может быть всего лишь описательным, т. е. без указания эффективного построени я соответствующего числа. Прн соответствующем выборе Определений условие в") будет выполняться для формализма арифметики, а также для формализма анализа и объемлющих их формализмовв). Мы теперь покажем, что из предположений а)-в) и ве) относительно формализма Р и рассматриваемой нами нумерации в сочетании с допущением гх) следует выводимость в Р некоторого противоречия. Действительно, из предположений б), в) и в*) получается, что свойство числа пз «быть номером некоторого герма с число- х) См с 322 и далее ») Для простоты мы снова предполагаем, ето числовые переменные, е твкже символы для предикзтв ревенсгвв и для арифметической функции следования совпадают с употреблявшимися ранее.
Кроме того, мы предполвгаем, что номер терни 1 всегда меньше номера терме 1'. Эти несущественные добевкн н допущениям в) — в) в дальнейшем специально оговариваться не будут. ') Например, оно выполняется для рмелизмв, описанного в книге Р. Керн»ив: Сегпвр Ц. 1.ой1»сне Бун1зх ег Бргзсйе.— %1еп, 1934 ноднвзвеннем «Бр)нейе Пь Этот формализм представляет собой теорию типов о включением аксиом Пеево н формвлизецни понятия наименьшего числе. ВЫХОД ЗА РАМКИ ТЕОРИИ ДОКАЗАТЕЛЬСТВ !гл. ч Г АИИЦЫ ИЗОЕРАЗИМОСТИ И ВЫВОДИМОСТИ ГРА И 4 (1 вой переменной а в качестве единственной свободйой переменной» является рекурсивным предикатом. Обозначим его через 5(т). Рассмотрим номера термов а, а', ..., а(').
Все эти номера обладают свойством 5 и являются попарно различными. Номер терма а(') в его зависимости от е изображается некоторой рекурсивной функцией в(п). Для этой функции выполняются неравенства и ~в (и) и в (л) в(,п'). Кроме того, имеет место й (» (и)). Последовательность цифр, обладающих свойством )у, можно изобразить — в порядке их возрастания — с помощью некоторой рекурсивной функции 1(п), Именно, 1(п) можно определить рекурсивными равенствами ') 1(0)= Ы!и й(х), к < в (в) 1(л') = Ы(п (5 (х) 6(1(п) (х). к (в (з') Для этой функции справедливы следующие (выводимые в рекурсивной арифметике) формулы: 1(п)-= в (и), 1(п) (1(и'), и =1(п), 5 (1(п)). Согласно предположению а) функция 1(п) изображается в Р некоторым термом 1(п) таким, что единственной его свободной переменной является числовая переменная п.
Последовательность значений термов Е(0), Е(0'), Е(0"), ... представляет собой перечисление номеров всех тех термов в Р, которые имеют а в качестве единственной свободной переменной. Таким образом, последовательности Е(0), Е(0'), Е(0"), ... соответствует некоторое перечисление (с повторениями) ф,(а), зрз(а), ... всех арифметических функций, представимых в Р с помощью каких-либо термов с единственной свободной переменной а.
При этом для всякой цифры и значение терма Е(п) является номером некоторого терма (н(а) в Р'), изображающего функцию зрв с аргументом а. Если в этот терм вместо а подставить цифру и, то номер получающегося при этом терма будет (в силу характеристического свойства функции 6(л, !)з)! значением терма 6(Е(п), и). Поэтому на основании свойства функции е(л) [допущение г,)]е), з) Относительно фуннннн М!и см. с. 274 н далее.
з) Инденс и в Ен Унвзыввет только нв ззвнснмасть РзссмвтРнвземага термв от и. з) См. с. 324. е) См, с. 329 н далее, получается, что в Р выводимо равенство е (6 (Е(п), п)) = Ев (и). (ф (л)) может быть представлена в Р Номер этого терма должен в р б Е Если Е (О), Е (0~) Е (Оь) Пусть, например, это будет (Р). н) — номер герма (е(6(Е(р), р)))' то на основе характеристического сво" у йства ф нкции 6(Й, !) в Р выводимо равенство 6(Е(р), р)=н(, откуда с помо омощью аксиом равенства выводится формула е (6 (Е (р), р)) = е (н)). С другой стороны, в силу х у характеристического свойства функ- ции е(п), в Р выводимо равенство е(п()=(е(6(Е(р), р)))'.
Но два последних равенства, взятые друг с другом, дают (6(Е(!), р)) =(е(6(Е(р), р)))', в то время как в силу пр предположения а) в Р выводима формула е (6 (Е (р), р)) Ф (е (6 (Е (р), р)))'. , фо мализм Р содержит противоречие. мализм, удовлетворяющий условиям а) — в, и в, нем вр щ у )) го типа'). В их рассмотрении вместо нашего е гие предположения а допу- допущения в) взяты некоторые другие и (цение в") заменено более слабы . у м.
Рез льтат этого рас авторы применяют к пост оенным А. Черчем и п и станавливают непротиворе- системам логистики и на этом пути устанавли чивость указанных систем. о можно было бы получить несколько прон(е. Именно, быча бы лссмвтрнввть терм (е (з(а а)))' рмв е(е(е(а), а)))' достаточно была бы рлссм Но мы хотели здесь прояснить связь между получен В Т))е 1псонмыевс о! сж1жн !с~~~! — Н. В.
Тье Рвезбох с! 13 Ьсс 1941 30 454 — 5! 6 , 3. См. также Снегу К1еепе впб мсззее. — Тевпз. А(вег. Мвбь сс., 336 выход зА РАмки твопии доклзктгльств / 1гя. о Прежде чем закончить это изложение семантичйских парадоксов и их формальное усиление, мы хотели бы,йодчеркнуть еще одно обстоятельство. Результаты, касающивбя невозможности формального изображения понятия истинрого высказывания и понятия значения выражения, определяю«него число, в формализованных языках (дедуктивных формализмах), были получены при некоторых общих предположениях относительно этих формализмов, Они справедливы лишь в том смысле, что эти понятия, будучи отнесены к рассматриваемым формализованным языкам, не могут быть изображены внутри самих этих языков. Между тем они никоим образом не исключают возможности изображения этих понятий в рамках каких-либо объемлющих формализованных языков.
Более того, такая возможность имеется, по всей видимости, в самом общем смысле, И, действительно, формальное изображение этих понятий может быть осуществлено, с одной стороны, аксиоматическим путем, а с другой, — с помощью соответствующих явных определений. Что касается формализации понятия истинного высказывания при помощи явных определений (определений истинности), то такие определения для различных систем исчисления классов и исчисления предикатов (включая и исчисления второй ступени) были проведены Тарским '). Для одного формализма теории типов с включением арифметических аксиом Р.
Карнап') дал набросок определения истинности, изложенный на естественном языке. Это определение может быть формализовано в рамках некоторой логистической системы, обладающей достаточными изобразительными возможностями. В предьщущих главах мы уже познакомились с различными примерами определений истинности, сформулированных иа естественном языке. Такими определениями являются определения верифицируемости'), сформулированные нами для ряда формализмов. Встречающиеся при рассмотрении проблемы разрешимости определения понятий общезначимости и выполнимостии также можно рассматривать (со ссылкой на какой- либо формализм, в рамках которого могут быть формально изображены общезначимость и выполнимость формул исчисления предикатов) как определения истинности или же фрагменты таких определений.
В дальнейшем мы рассмотрим пример одного такого формализованного определения истинности '). ') В его уже пнтнрованном сочинении; «1»ег Фнкгие1««ьек«ИГ!и Всп !огп»а11ыег1еп зргасиеп». ') Сагпнр й. Е1п С»й!113«е!1»нгнепп1п Шг и!е зй1»е Вег «11м»!»сйсп М»1пе»п»1по — Моп»ЬЬ, М»1п. Рву»., 1935, 42, № 1. »7 См. т. 1, с. 294, 303, 307, 336, 339, 343, 360, 363, 441, 449. ») См. с. 406 — 411, зи ГРАницы изовРАзимости и ВИВОдимости 337 Замечание.
Термин определение истинности сам по себе не должен вводить нас в соблазн. Мы не должны ожидать от такого определения философского объяснения понятия истины. Напротив, в большинстве случаев речь здесь идет лишь о некотором уточнении того понимания формул, которое и без того лежит в основе обычного использования формализма, и задача такого определения заключается в том, чтобы выразить это понимание в общем виде, в его зависимости от структуры рассматриваемой формулы. Впрочем, определения истинности, как правило, не допускают какого-либо 4инитного истолкования.
б) Первая теорема Геделя о неполноте. От антиномии лжеца к упоминавшимся в начале этой главы теоремам Геделя нас приводит рассмотрение одной модификации этой антиномии и применение к ней метода формального уточнения. Эта модификация заключается в том, что мы рассматриваем высказывание, выражающее свою собственную недоказуемость. Если некто произносит фразу: «предложение, которое я сейчас произношу, не может быть получено в результате какого-либо доказательства», то предположение о том, что зто предложение может получиться в результате некоторого доказательства, ведет к противоречию. Таким образом, это предположение должно быть отвергнуто.
Но тогда получается, что имеет место именно то, о чем говорится в этом предложении и, значит, это предложение получается в результате некоторого доказательства. Поначалу складывается впечатление, что мы добавили к антиномии лжеца лишь ненужное осложнение. Но для формального уточнения произведенная нами модификация оказывается очень существенной„так как относительно дедуктивного формализма понятие р е з у л ь т а т а д о к а з а т е л ь с т в а имеет более элементарный характер, чем понятие истинного высказывания. Для формализма исчисления предикатов мы в свое время показали, что с помощью соответствующей нумерации отношение между списком формул и формулой Я, указывающее, что этот список является выводом формулы Я, изображается рекурсивным отношением Об(т, п) между номером этого списка и номером формулы Л ').
Способ, с помощью которого мы получили это изображение, показывает, что возможность такого рекурсивного изображения отношения между числом гп, являющимся номером какого-либо списка формул, представляющего собой некоторый вывод, и числом н, являющимся номером заключительной формулы этого вывода, не обусловлена какнми-то специфическими особенностями исчисления предикатов, а имеет место для любого достаточно 4] См, с. 296.
ззв выход зА РАмки тео~ии доказательств, [гл. и ГРАницы изОБРАзимости и Выводимости 339 $ и четко очерченного дедуктивного формализма. Позйсе мы еще убедимся в рекурсивной изобразимости этого отнрй)ения специально в применении к арифметическому формализМ)~. Гедель установил рекурсивную нзобразимость упомянутого отношения для одного формализма, получающегося из системы, изложенной в Рг1пс|р1а п1а()гегпа(!са, ' в результате отказа от различения ступеней, замены аксиомы бесконечности аксиомами Пеано, а также некоторых упрощений. Системы аксиоматической теории множеств при их формализации приводят нас к дедуктивным формализмам, для которых — при подходящей нумерации— отношение номера списка формул, являющегося выводом, к номеру его заключительной формулы также выражается рекурсивным образом ').
Поэтому при формализации модифицированной антиномии лжеца не может быть речи о том, чтобы при определенных общих предположениях относительно дедуктивного формализма, включая и предположение о его непротиворечивости, доказывать невозможность формализации понятия результата доказательства. Напротив, мы с самого начала положим в основу нашего рассмотрения обратное предположение, что при нашей нумерации отношение «число т является номером некоторого вывода формулы с номером и» допускает определенное рекурсивное изображение. Это предположение является усилением нашего прежнегодопущения относительно рассматриваемого дедуктивного формализма Р.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
