Гильберт, Бернайс - Основания математики. Теория доказательств (947376), страница 70

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

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

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

Это обстоятельство, которое может нас озадачить, находит принципиальное объяснение в одной теореме Геделя о дедуктивных формализмах, первым объектом применения которой является формализм арифметики. Выводы, которые влечет за собой эта теорема, вынуждают нас расширить область допустимых неформальных рассуждений, употребляемых в теории доказательств, по сравнению с тем, что до сих пор допускалось при фактической реализации нашей финитной точки зрения.

ГЛАВА Ч ПРИЧИНЪ|, ВЪ|ЗЫВАЮЩИЕ НЕОБХОДИМОСТЬ РАСШИРЕНИЯ МЕТОДИЧЕСКИХ РАМОК ТЕОРИИ ДОКАЗАТЕЛЬСТВ В |. Границы нзобразимостн н выводнмостн в дедуктивных формализмах Метод арифметизации метаматематики был разработан Геделем в целях доказательства двух весьма общих теорем, выражающих тот факт, что всякий логнко-математический формализм, с одной стороны, четко очерченный, а с другой стороны, не слишком узкий, является дедуктивно незавершенным. Основная идея геделевского доказательства этих теорем заодно доставляет нам и метод, позволяющий произвести математическое уточнение некоторых логических и теоретико-множественных парадоксов, из числа тех, в которых существенную роль играет соотношение между обозначением и обозначаемым и для которых в последнее время получило права гражданства название семантических парадоксов, илн же семантических антиномий.

Принципиальная сторона геделевского метода в наиболее простой форме проступает именно тогда, когда мы начинаем прилагать этот метод к упомянутым антиномиям, н потому мы в первую очередь займемся рассмотрением этих приложений. а) Антиномия лжеца; теорема Тарского о понятии истинности; парадокс Рипйара. Одним из простейших семантических парадоксов является парадокс лжеца.

Парадокс этот был известен уже древним грекам. Суть его заключается в том, что из высказывания, утверждающего свою собственную ложность, вытекает противоречие. Если некто говорит: «сейчас я лгу» или, более подробно, «я высказываю сейчас утверждение, которое является ложным», то в силу языковой формы, в которую облечено это высказывание, оно носит характер некоторого утверждения.

Предположение, что это утверждение является истинным, ввиду содержания этого высказывания немедленно приводит нас к заключению, что оно является ложным. Поэтому, согласно принципу гебпсПо ай аЬзпгапгп, это утверждение является ложным. Но это означает, что в тот момент времени, когда это высказывание произносится, то, о чем в нем говорится, верно.

Следовательно, данное высказывание выражает истинное утверждение. Тем самым П д. Гнаьберт, и. Бернайс 323 ГРАИИЦЫ ИЗОБРАЗИМОСТИ И ВЫВОДИМОСТИ 411 ВЫХОД ЗА РАМКИ ТГОРИИ ДОКАЗАТВЛЬСТВ [ГЛ. ч мы пришли к противоречию. (Заметим, кстати, что закон исклю. ченного третьего при этом не использовался.) Мы не хотели бы вдаваться здесь в философскую дискуссию по поводу этой антиномии, о которой уже много говорилось и писалось '). Во всяком случае, в обиходном языке парадокс этот вызывает определенную трудность, так как он показывает, что оперирование с грамматически правильно построенным предложением по обычным правилам умозаключений иногда может привести к противоречию.

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

Допустим, что формализм Р и рассматриваемая нумерация удовлетворяют следующим условиям: а) Функции, отношения, предложения и способы умозаключений рекурсивной арифметики (включая и соответствующие средства исчисления высказываний) изобразимы в Р. б) С помощью рассматриваемой нумерации свойства выражений формализма Р и отношения между ними, формулируемые в терминах внешнего вида этих выражений, изображаются рекурсивными предикатами, а выполняемые над этими выражениями формальные операции изображаются рекурсивными функциями. в) Имеются переменные некоторого специального вида, называемые числовыми переменными. Некоторые извыражений формализма Р выделены в качестве термов.

К термам, в частности, относятся числовые переменные и цифры. Всякая рекурсивная функция изображается в Р некоторым термом, г) Иа лнтервтуры но этому вопросу см., в частности, дискуссию между П. Фннслером н Х. ггнппсом: Р1пв! ег Р., 1. г р р а Н. ОЬег Ше Еовнпн чоп Рагадох!еп.— РРЛ!ов. Апге!Хег, П од., 1927, № 2, работу Р. Караева: Сагн а р Гг. Ег!е Апнпопнеп нпб б1е упчо11а1апб!К!ге!! бег Магиепга1иг. — Мопами.

Ма!М Риув., 1934, 41 № 2, а также работу Э. Стенвуса: 91е п1нв Е. 0аа Ргошсгн бег 1оелвсиен Аонноннеп (днссертапнн, Хельсинки, 1949, Сопнпеп1а. 1гопев Риуэ!со Мащеюа!!сае Х!ч' 1! оос, ос!со!. Репгцса). а аргументы этих функций изображаются числовыми переменными. Если в терме, содержащем какую-либо числовую переменную, ее заменить каким-либо термом, то при этом снова получается некоторый терм (разумеется, при условии отсутствия коллизий между связанными переменными).

Некоторые из выражений формализма Р выделены в качестве ф о р м у л. Равенство любых двух термов является формулой, и потому любое рекурсивное отношение изобразимо в Р некоторой формулой. При замене в формуле входящей в нее числовой переменной каким-либо термом — если при этом не возникает коллизий между связанными переменными — снова получается некоторая формула. Отрицание любой формулы является формулой. Любое выводимое выражение является формулой. Замечание.

Характеризуя определенные выражения из Р в качестве термов или формул, мы будем предполагать, что имеется способ, который для каждого выражения, принадлежащего Р, проверял бы, является ли оно термом (или соответственно формулой). Что касается этих подготовительных предположений, то они носят довольно общий характер. Они выражают примерно ту мысль, что формализм Р обладает некоторым минимальным запасом изобразительных и дедуктивных возможностей, что обращение с символьными выражениями в Р определено достаточно строго и что этот формализм обнаруживает определенное сходство с рассматривавшимся нами до сих пор формализмом арифметики.

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

Это допущение может быть сформулировано следующим образом: г) Имеется формула й)((а) с числовой переменной а в качестве единственной свободной переменной, обладающая тем свойством, что если и представляет собой номер некоторой формулы 6 без свободных переменных, то в Р выводимы импликации йг! (и) -~'Л и Я -э. Й! (п). 324 выход за гхмки твогии доклзатяльств 2гл. ч ггАницы изовг»зимости и выводимости 4 Н На основе предположений а) — г) мы получаем следующий аналог парадокса лжеца: Сначала из предположений б) и в) мы заключаем, что существует рекурсивная функция, зависящая от двух аргументов, которая номеру всякого выражения К из Р и всякой цифре ( ставит в соответствие номер выражения, получающегося из К в результате замены переменной а всюду, где она входит в это выражение, цифрой 2.

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

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