Игошин Математическая логика и теория алгоритмов (1019110), страница 73
Текст из файла (страница 73)
Столь же просто вычисляются по номерам исходных данных номера результатов комбинаторных преобразований (например, подстановки терма в формулу вместо переменной). При этом оказывается возможным написать арифметическую формулу В(а, Ь), имеющую видна, Ь) = 0 (где 7— примитивно рекурсивная функция) и выражающую условие: Ь есть номер формулы, которая получается из формулы с номером а путем подстановки натурального числа а вместо переменной ж Если р — номер формулы (Ъ'Ь)(- В(х, Ь)), то формула (чЬ)(- В(р, Ь)) выражает свою собственную невыводимость. Она и оказывается формально неразрешимой.
Отсюда и следует, что в любой непротиворечивой системе с минимальными выразительными арифметическими возможностями имеется истинное, но невыводимое суждение указанного вида. Достаточно подробно доказательство этой теоремы будет изложено в 5 37 после того, как будут изучены основы теории алгоритмов и рекурсивных функций. Доказательство второй теоремы получается путем формализации доказательства первой и существенно использует особенности арифметизации синтаксиса рассматриваемой системы. Из первой теоремы Геделя о неполноте арифметики видно, что (семантическое) понятие истинности в арифметике, а следовательно, и во всей математике нельзя исчерпывающим образом формализовать посредством (синтаксического) понятия доказуемости в какой-либо одной формально-логической системе. Вторая теорема Геделя о неполноте арифметики показывает, что и основная цель первоначальной программы Гильберта по формализации математики оказывается недостижимой.
Эта цель состояла в том, чтобы доказать формальную непротиворечивость арифметики, пользуясь при этом так называемыми «финитными» методами, т.е. лишь такими методами доказательств, которые применяются в самой арифметике. Но всякое разумное уточнение понятия финитного доказательства, по-видимому, формализуемо в формальной арифметике и потому, согласно второй теореме Геделя, невозможно. Гильберту и представителям его школы для выполнения гильбертовской программы удалось доказать строго финитными методами непротиворечивость весьма широкой подсистемы арифметики; подсистема эта имеет лишь тот недостаток, что принцип индукции формулируется в ней в ослабленной форме, что пре- 292 пятствует применению его к квантифицированным, предложениям.
Вторая теорема Геделя показывает, что такой частичный неуспех гильбертовской школы объясняется отнюдь не недостатком изобретательности ее представителей, а, как выяснилось впоследствии, объективной картиной явления. Напротив, теперь мы знаем, что они продвинулись в этом направлении настолько далеко, насколько это вообще было возможно, Упомянем также еще об одной важной теореме метаматематики, доказанной в 1936 г.
американским логиком А.Черчем. В ней утверждается, что не существует эффективной процедуры для рещения вопроса относительно произвольной формулы формальной теории, содержащей арифметику натуральных чисел, является ли такая формула теоремой теории, т.е. всякая такая формальная теория неразрешима. Из этой теоремы вытекает, в частности, и теорема Геделя о неполноте. Впоследствии была доказана неразрешимость большого числа формальных теорий, в частности элементарной теории групп, элементарной теории полей. После этих результатов Геделя стало ясно, что для решения одного из основных вопросов математики — проблемы непротиворечивости, по-видимому, не обойтись без других, отличных от финитистских, средств и идей.
Непротиворечивость формальной системы может быть обоснована только средствами более сильными, чем те, которые формализованы в данной системе. Здесь оказались возможными разные подходы, не для всех математиков в равной степени приемлемые или убедительные, в частности, ввиду существования различных точек зрения на допустимость тех или иных логических средств. В 1936 г. Г. Генцен получил доказательство непротиворечивости формальной арифметики, использующее средство, отсутствующее в арифметике, — так называемую трансфинитную (бесконечную) индукцию до некоторого счетного трансфинитного числа.
Теорема Тарского. Приведем еще однутеорему — теорему А. Тарского об истинности, показывающую, что формальным системам присуща ограниченность еще одного типа. Содержательное понятие истинности, которым мы постоянно пользуемся, также поддается формализации. Понятие истинности в формальной системе Т определяется относительно другой формальной системы Т'. Эта система Т' должна быть в определенным смысле сильнее системы Т. В 1956 г. Тарский доказал, что понятие истинности (множество всех истинных предложений, множество истинности предиката) в непротиворечивой формальной теории, включающей формальную арифметику, неопределимо в этой теории.
Таким образом, если теорема Геделя о неполноте обнаруживает принципиальную ограниченность дедуктивных возможностей любой достаточно богатой системы, то теорема Тарского вскрывает ограниченность выразительных возможностей таких систем. 293 Перефразируя образное изречение Куайна, можно сказать, что формальные системы попытались проглотить больший кусок онтологии, чем они в состоянии переварить.
Нестандартная модель формальной арифметики и ее некатегорич ность. В 527 мы отмечали, чтоаксиоматическая теория натуральных чисел, построенная на базе системы аксиом Пеано, категорична, т.е. имеет единственную с точностью до изоморфизма модель.
С использованием теоремы Геделя о неполноте формальной арифметики можно доказать существование неизоморфных моделей формальной арифметики. Таким образом, формальная арифметика, основывающаяся на аксиомах, перечисленных ранее, является некатегоричной формальной системой. Этот интересный факт можно объяснить разной трактовкой входящей в обе системы аксиомы индукции. В аксиоме индукции из системы Пеано участвует множество М, на которое не накладывается никаких ограничений и которое может рассматриваться как множество истинности произвольного предиката г(х), т.е. множество натуральных чисел, удовлетворяющих любому мыслимому свойству Рнатуральных чисел.
В соответствующей аксиоме формальной арифметики за г" может быть принято не любое свойство натуральных чисел, а лишь такое, которое выразимо средствами данного формализма. Меньшее количество свойств, допустимых в «формальной» аксиоме индукции, априори допускает наличие большего количества объектов (моделей), удовлетворяющих ей. Так и происходит в действительности. Таким образом, различие между этими аксиомами незаметно, пока речь идет о теоремах элементарной теории чисел, и весьма существенно, когда выясняются свойства формальной теории.
Ясно, что моделью формальной арифметики является обычное множество натуральных чисел йг, в котором О' = 1, х' = х+ 1 и +, . — обычные операции сложения и умножения натуральных чисел. Пользуясь локальной теоремой Геделя — Мальцева (см. следствие 29.17 из теоремы 29.16), установим наличие у формальной арифметики одной необычной модели.
Она называется нестандартная модель арифметики. Рассмотрим следующую бесконечную совокупность формул формальной арифметики: (Эу)(х= у+ у), (Эу)(к= у+у+у), ..., (Эу)(х= у+ у+ ... +у), ... (в последней формуле в правой части равенства п слагаемых). Первая из этих формул утверждает, что число х делится на 2, вторая — что х делится на 3 и т.д., (и — 1)-я — что х делится на и и т.д. Поэтому обозначим эти формулы соответственно: 2~х, З~х, ..., 294 л~х, ...
Рассмотрим далее следующую бесконечную совокупность формул: Ео = ((ЗхН2~г), (Эх)(2)х л 3!х), ..., (Зх)(2!х л 31х л ... л л)х), ...). Наконец, обозначив через У. совокупность из девяти аксиом формальной арифметики, рассмотрим следующее множество формул формальной арифметики Е1 = ь 0 уо. Применим к Е, локальную теорему Геделя — Мальцева. Ясно, что каждое конечное подмножество формул из Х, содержит лишь конечное число формул из Уо и потому имеет модель: его моделью будет обычная система натуральных чисел.
Тогда по упомянутой теореме все множество Е, имеет модель. Ее особенностью будет то свойство, что в этой модели будет существовать (натуральное) число, делящееся на все натуральные числа. О формальных теориях числовых систем. Вопрос о природе понятия числа никогда не стоял на обочине магистрального пути математических исследований во все времена. Математика, достигнув того или иного уровня в своем развитии, неизменно обращалась к своим основам, где центральную роль всегда играло понятие числа. Во второй половине Х(Х в. в связи с необходимостью обоснования математического анализа и приведения в систему огромного количества результатов, полученных в этой области математики, числа снова оказались в центре внимания математиков.
Математика ХХ в. и прежде всего значительно развившаяся математическая логика еще выше подняли уровень требований к строгости обоснования основ математической науки и в первую очередь понятия числа. Потребовалось создание формальных аксиоматических теорий основных систем чисел. Ведь в конечном итоге математика не интересует природа чисел и вопрос о том, откуда они берутся. Его интересует, каковы свойства этих чисел, и желательно перечисление всех таких свойств чисел, из которых чисто логически вытекали бы все теоремы соответствующей математической дисциплины и в первую очередь математического анализа. Первый этап формализации.