Формализация математической теории

Формальная арифметика

Язык и аксиомы. Это — логико-математическое исчисление (или прикладное исчисление первого порядка), формализующее элементарную теорию чисел. Наиболее популярная формализация основана на подходе Пеано, предложенном им в 1889 г. и рассмотренном нами в ранее (пример 26.3). Язык этого исчисления кроме логических связок и равенства содержит нелогическую константу 0, двухместные функциональные символы , одноместный функциональный символ . Термы строятся из константы 0 и переменных с помощью функциональных символов; в частности, натуральные числа изображаются термами вида . Атомарные формулы — это равенство термов; остальные формулы строятся из атомарных с помощью логических связок. В качестве аксиом выбираются логические аксиомы, это аксиомы формализованного исчисления предикатов и следующие нелогические (арифметические) формулы:

где — произвольная формула теории с одной свободной предметной переменной . Последняя формула есть схема аксиом, называемая схемой аксиом индукции.

Средства формальной арифметики оказываются достаточными для вывода теорем, устанавливаемых в стандартных курсах элементарной теории чисел. Более того, формальная арифметика оказывается эквивалентной аксиоматической теории множеств Цермело–Френкеля без аксиомы бесконечности в каждой из этих систем может быть построена модель другой.

Программа Гильберта формализации математики и теорема Гёделя о неполноте

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

Одним из путей выхода из кризиса в основаниях математики в начале XX в., обусловленного обнаружением парадоксов (антиномий) в теории множеств, должен был стать гильбертовский путь формализации математики и логики. Каждая конкретная математическая теория должна быть переведена на язык подходящей формальной системы таким образом, чтобы каждое осмысленное (ложное или истинное) предложение содержательной теории выражалось бы некоторой формулой формальной системы. Тогда естественно было надеяться, что этот метод формализации позволит строить все положительное содержание математических теорий на такой точной и, казалось бы, надежной основе, как понятие выводимой формулы (теоремы формальной системы). Кроме того, такие принципиальные вопросы, как проблема противоречивости математических теорий, решались бы в форме доказательства соответствующих утверждений о формализующих эти теории формальных системах. Поскольку описанные нами формальные системы сами оказываются точными, или, как говорили в школе Гильберта, финитными, математическими объектами, можно было ожидать, что удастся получить финитные доказательства утверждений о непротиворечивости, т.е. доказательства, которые в определенном смысле были бы эффективными, не зависящими от тех мощных средств, вроде абстракции актуальной бесконечности, которые в классических математических теориях как раз и являются причиной трудностей в их обосновании. Но результаты, полученные Гёделем в начале 1930-х гг., привели к краху основных надежд, связывавшихся с этой программой Гильберта. Гёдель доказал следующие две теоремы, получившие общее название "теорема о неполноте формальной арифметики":

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

2) если формализованная арифметика в действительности непротиворечива, то хотя утверждение о ее непротиворечивости выразимо на ее собственном языке, но доказательство этого утверждения средствами, формализуемыми в ней самой, невозможно.

Эта теорема, как и первая, распространяется на всякую непротиворечивую формальную систему, содержащую формальную арифметику.

Доказательство первой теоремы проводится разработанным Гёделем методом арифметизации синтаксиса языка формальной теории, который стал одним из основных методов теории доказательств (метаматематики). Этим методом строится формально неразрешимая формула. Фиксируется нумерация основных формальных объектов (формул, конечных последовательностей формул и т.д.) натуральными числами, такая, что основные свойства этих объектов (быть аксиомой, быть выводом по правилам системы и т.д.) оказываются распознаваемыми по их номерам с помощью весьма простых алгоритмов. Столь же просто вычисляются по номерам исходных данных номера результатов комбинаторных преобразований (например, подстановки терма в формулу вместо переменной). При этом оказывается возможным написать арифметическую формулу , имеющую вид (где — примитивно рекурсивная функция) и выражающую условие: есть номер формулы, которая получается из формулы с номером путем подстановки натурального числа вместо переменной . Если — номер формулы , то формула выражает свою собственную невыводимость. Она и оказывается формально неразрешимой. Отсюда и следует, что в любой непротиворечивой системе с минимальными выразительными арифметическими возможностями имеется истинное, но невыводимое суждение указанного вида. Достаточно подробно доказательство этой теоремы будет изложено позднее после того, как будут изучены основы теории алгоритмов и рекурсивных функций.

Доказательство второй теоремы получается путем формализации доказательства первой и существенно использует особенности арифметизации синтаксиса рассматриваемой системы.

Из первой теоремы Гёделя о неполноте арифметики видно, что (семантическое) понятие истинности в арифметике, а следовательно, и во всей математике нельзя исчерпывающим образом формализовать посредством (синтаксического) понятия доказуемости в какой-либо одной формально-логической системе. Вторая теорема Гёделя о неполноте арифметики показывает, что и основная цель первоначальной программы Гильберта по формализации математики оказывается недостижимой. Эта цель состояла в том, чтобы доказать формальную непротиворечивость арифметики, пользуясь при этом так называемыми "финитными" методами, т.е. лишь такими методами доказательств, которые применяются в самой арифметике. Но всякое разумное уточнение понятия финитного доказательства, по-видимому, формализуемо в формальной арифметике и потому, согласно второй теореме Гёделя, невозможно.

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

Упомянем также еще об одной важной теореме метаматематики, доказанной в 1936 г. американским логиком А.Чёрчем. В ней утверждается, что не существует эффективной процедуры для решения вопроса относительно произвольной формулы формальной теории, содержащей арифметику натуральных чисел, является ли такая формула теоремой теории, т. е. всякая такая формальная теория неразрешима. Из этой теоремы вытекает, в частности, и теорема Гёделя о неполноте. Впоследствии была доказана неразрешимость большого числа формальных теорий, в частности элементарной теории групп, элементарной теории полей.

После этих результатов Гёделя стало ясно, что для решения одного из основных вопросов математики — проблемы непротиворечивости, по-видимому, не обойтись без других, отличных от финитистских, средств и идей. Непротиворечивость формальной системы может быть обоснована только средствами более сильными, чем те, которые формализованы в данной системе. Здесь оказались возможными разные подходы, не для всех математиков в равной степени приемлемые или убедительные, в частности, ввиду существования различных точек зрения на допустимость тех или иных логических средств. В 1936 г. Г. Генцен получил доказательство непротиворечивости формальной арифметики, использующее средство, отсутствующее в арифметике, — так называемую трансфинитную (бесконечную) индукцию до некоторого счетного трансфинитного числа.

Теорема Тарского

Приведем еще одну теорему — теорему А.Тарского об истинности, показывающую, что формальным системам присуща ограниченность еще одного типа. Содержательное понятие истинности, которым мы постоянно пользуемся, также поддается формализации. Понятие истинности в формальной системе определяется относительно другой формальной системы . Эта система должна быть в определенным смысле сильнее системы . В 1956 г. Тарский доказал, что понятие истинности (множество всех истинных предложений, множество истинности предиката) в непротиворечивой формальной теории, включающей формальную арифметику, неопределимо в этой теории.

Таким образом, если теорема Гёделя о неполноте обнаруживает принципиальную ограниченность дедуктивных возможностей любой достаточно богатой системы, то теорема Тарского вскрывает ограниченность выразительных возможностей таких систем.

Перефразируя образное изречение Куайна, можно сказать, что формальные системы попытались проглотить больший кусок онтологии, чем они в состоянии переварить.

Нестандартная модель формальной арифметики и ее некатегоричность

Ранее мы отмечали, что аксиоматическая теория натуральных чисел, построенная на базе системы аксиом Пеано, категорична, т.е. имеет единственную с точностью до изоморфизма модель. С использованием теоремы Гёделя о неполноте формальной арифметики можно доказать существование неизоморфных моделей формальной арифметики. Таким образом, формальная арифметика, основывающаяся на аксиомах, перечисленных ранее, является некатегоричной формальной системой. Этот интересный факт можно объяснить разной трактовкой входящей в обе системы аксиомы индукции. В аксиоме индукции из системы Пеано участвует множество , на которое не накладывается никаких ограничений и которое может рассматриваться как множество истинности произвольного предиката , т.е. множество натуральных чисел, удовлетворяющих любому мыслимому свойству натуральных чисел. В соответствующей аксиоме формальной арифметики за Сможет быть принято не любое свойство натуральных чисел, а лишь такое, которое выразимо средствами данного формализма. Меньшее количество свойств, допустимых в "формальной" аксиоме индукции, априори допускает наличие большего количества объектов (моделей), удовлетворяющих ей. Так и происходит в действительности. Таким образом, различие между этими аксиомами незаметно, пока речь идет о теоремах элементарной теории чисел, и весьма существенно, когда выясняются свойства формальной теории.

Ясно, что моделью формальной арифметики является обычное множество натуральных чисел , в котором и — обычные операции сложения и умножения натуральных чисел.

Пользуясь локальной теоремой Гёделя–Мальцева (см. следствие 29.17 из теоремы 29.16), установим наличие у формальной арифметики одной необычной модели. Она называется нестандартная модель арифметики.

Рассмотрим следующую бесконечную совокупность формул формальной арифметики:

(в последней формуле в правой части равенства слагаемых). Первая из этих формул утверждает, что число делится на 2, вторая — что делится на 3 и т.д., (n-1)-я — что делится на и т.д. Поэтому обозначим эти формулы соответственно: . Рассмотрим далее следующую бесконечную совокупность формул:

Наконец, обозначив через совокупность из девяти аксиом формальной арифметики, рассмотрим следующее множество формул формальной арифметики . Применим к локальную теорему Гёделя–Мальцева. Ясно, что каждое конечное подмножество формул из содержит лишь конечное число формул из и потому имеет модель: его моделью будет обычная система натуральных чисел. Тогда по упомянутой теореме все множество имеет модель. Ее особенностью будет то свойство, что в этой модели будет существовать (натуральное) число, делящееся на все натуральные числа.

Формальные теории числовых систем

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

Первый этап формализации

Выше рассказывалось о формальной арифметике, т.е. о формализации теории натуральных чисел. Здесь будут кратко описаны формальные теории других систем чисел — целых, рациональных, действительных.

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

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

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

Гильберт охарактеризовал множество вещественных чисел как максимальное архимедово упорядоченное поле (т. е. любое поле, являющееся его расширением, уже не архимедово).

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

Проблема М.Я. Суслина

С этой характеристикой системы действительных чисел связана одна из знаменитейших проблем XX в. — проблема М.Я. Суслина. Эта проблема состоит в том, что требуется узнать, сохранится ли указанная характеристика системы действительных чисел, если в ней последнее условие сепарабельности заменить более слабым требованием, называемым условием Суслина: любая система из попарно не пересекающихся непустых интервалов не более чем счётна. Другими словами, будет ли изоморфно системе действительных чисел линейно упорядоченное множество, удовлетворяющее перечисленным выше условиям, кроме, сепарабельности, и условию Суслина.

Судьба этой проблемы, оказалась поистине исторической, и на ее решение потребовалось более 40 лет. Предположение о ее положительном решении получила название гипотезы Суслина. Контрпример к гипотезе (хотя пока и не существующий), т.е. упорядоченное множество, удовлетворяющее всем условиям проблемы! М. Я. Суслина, но не изоморфное действительной прямой, получил названий континуум Суслина. Эта проблема встала в один ряд с континуум-проблемой Кантора, и полное решение их обеих было получено лишь в начале 1960-х гг., когда американский математик П.Коэн открыл принципиально новый метод доказательства, получивший название метода форсинга (вынуждений). (За это открытие он был удостоен в 1966 г. на Международном математическом конгрессе в Москве высшей международной награды, которой удостаиваются ученые-математики, — Филдсовской премии.) Выяснилось, что проблему Суслина, как и континуум-проблему Кантора, вообще невозможно решить в обычном смысле слов — решить проблему, т. е. дать определенный ответ "да" или "нет" на поставленный вопрос. Гипотеза Суслина, как и континуум-гипотеза Кантора, оказалась не зависящей от остальных аксиом теории множеств. Другими словами, возможна теория множеств, в которой гипотеза Суслина справедлива, и возможна теория множеств, в которой эта гипотеза не выполняется. Кроме того, была также установлена взаимная независимость и самих двух гипотез — гипотезы Суслина и континуум-гипотезы Кантора.

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

Углубление формализации: элементарная теория вещественно замкнутых полей

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

где — произвольная формула с одной свободной предметной переменной . Таких формул бесконечно много, и соответствующая формальная аксиома формулируется для каждой из них. Можно показать, что такая схема аксиом не может исчерпать всей силы содержательной аксиомы индукции в том смысле, что нельзя посредством такой схемы (наряду с другими формальными аксиомами формальной арифметики) обеспечить, чтобы единственной с точностью до изоморфизма моделью такой системы аксиом было множество натуральных чисел (что, напомним, обеспечивала содержательная система аксиом Пеано). Тем не менее для многих целей вполне достаточно употреблять эту форму аксиомы индукции.

Аналогично обстоит дело с содержательным свойством полноты поля действительных чисел: всякое ограниченное сверху множество имеет точную верхнюю грань. При его формализации приходится вводить схему аксиом (называемую аксиомой полноты), в которой снова понятие множества заменено на определяющее его свойство

Словесно эту запись можно прочитать так: если существует число, обладающее свойством , и всякое число, обладающее этим свойством, меньше некоторого числа, то существует наименьшее такое число, что все числа, обладающие свойством , меньше его. В связи с такой формализацией возникает естественный вопрос, до какой степени она отражает "полное содержание" исходной аксиомы полноты в ее содержательной теоретико-множественной формулировке. Еще раз отметим, что предоставленный в наше распоряжение формальный язык узкого исчисления предикатов первого порядка не позволяет говорить о множествах как элементах области индивидов. Поэтому, рассматривая множества, мы говорим об определяющих их свойствах, точнее, о выразимых в данном языке свойствах индивидов, а именно вещественных чисел. Например, чтобы сказать, что множество вещественных чисел , обладающих свойством , не пусто, мы пишем просто ; существование верхней грани выражается формулой и т.д. Это и дает приведенную выше формальную запись аксиомы полноты. Вопрос о том, насколько мы при этом отдалились от первичной теоретико-множественной аксиомы полноты, — это по существу, вопрос о том, каков класс множеств, определимых свойствами .

Таким образом, формальная (элементарная) теория вещественных чисел может быть построена на базе системы следующих аксиом:

аксиомы поля;

аксиомы порядка: ,

аксиома полноты (схема аксиом).

Это означает, что система действительных чисел есть полное линейно упорядоченное поле.

Иногда аксиому полноты формулируют в более ограниченном виде — не для произвольного свойства F(x) действительных чисел , а для конкретного свойства: — быть корнем алгебраического многочлена. В этом случае аксиома полноты формулируется так:

где . Или же в этом случае аксиома полноты распадается на две части:

1) (из каждого вещественного числа или противоположного ему числа можно извлечь квадратный корень);

2) (каждый алгебраический многочлен нечетной степени имеет хотя бы один вещественный корень).

Аксиомы поля и аксиомы порядка (т. е. аксиомы линейно упорядоченного поля) и аксиома полноты в одной из двух последних формулировок образуют систему аксиом элементарной теории так называемых вещественно-замкнутых полей.

Разрешимость и абсолютная полнота элементарной теории вещественно-замкнутых полей

Приведенные в предыдущем пункте системы аксиом представляют собой попытки аксиоматизировать совокупность свойств, справедливых в системе действительных чисел. Считается, что самый большой успех аксиоматизации достигнут, если с ее помощью удается обосновать эффективную разрешающую процедуру, т. е. процедуру, которая для любого предложения , сформулированного на данном формальном языке, распознает за конечное число шагов его истинность в подразумеваемой структуре, в данном случае в системе действительных чисел. В 1930-е гг. А.Тарский доказал, что для любого данного суждения о действительных числах, которое может быть выражено на формальном языке элементарной теории вещественно-замкнутых полей, либо само это суждение, либо его отрицание доказуемо в этой теории, т.е. выводимо из ее аксиом. Это означает, что элементарная теория вещественно-замкнутых полей абсолютно полна, а соответствующая система аксиом по существу определяет алгебраические свойства действительных чисел. При этом разрешающая процедура (алгоритм) основана на так называемом методе элиминации (ликвидации) кванторов, который впервые применили Ленгфорд и Пресбургер в 1920-е гг. Этот метод оказался чрезвычайно эффективным и впоследствии нашел многочисленные применения для решения проблемы разрешимости в самых разных разделах математики.

Идея метода элиминации кванторов состоит в следующем. Вначале доказывается, что для любой формулы (рассматриваемой теории первого порядка) вида , где — атомарная формула или отрицание атомарной формулы, найдется такая бескванторная формула , что в данной теории доказуема (выводима) эквивалентность . Основываясь на этом утверждении, к каждой замкнутой формуле (предложению) данной теории может быть применена процедура элиминации кванторов, которая состоит в следующем:

1) превратить самые внутренние кванторы этого предложения в кванторы существования, если они не таковы (пользоваться при этом законами де Моргана);

2) привести область действия каждого из этих кванторов к дизъюнктивной нормальной форме;

3) распределить кванторы существования по дизъюнктивным членам;

4) заменить все ∃-формулы эквивалентными им бескванторными формулами на основании предыдущего утверждения;

5) если полученная формула все еще не является бескванторной, то повторить описанные шаги, начиная с п. 1; в противном случае рассматриваемое предложение превратилось бы либо в истину, либо в ложь.

Таким образом, метод элиминации кванторов сводит логический вопрос о (раз)решении к математическому вопросу о критериях существования решения совершенно определенной задачи. Что касается теории вещественно-замкнутых полей, то решение обсуждаемой проблемы в ней основывается на классической теореме Штурма (доказанной еще в 1829 г.) и доставляющей средство определения числа (вещественных) корней алгебраического многочлена с целыми коэффициентами между двумя заданными границами, а также общего числа корней такого многочлена.

Теорема утверждает, что число корней между и многочлена равно (без учета кратности) числу перемен знака в так называемом ряду Штурма этого многочлена. В удобной для элиминации кванторов форме эта теорема может быть сформулирована следующим образом: для каждого многочлена с целыми коэффициентами имеется такая бескванторная формула , что эквивалентность

выводима из аксиом элементарной теории вещественно-замкнутых полей.

Заслуга А.Тарского состоит в том, что он доказал эту теорему в следующем обобщенном виде: для любой бескванторной формулы найдется такая бескванторная формула , что эквивалентность

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

Но ведь из этой формулы можно удалить кванторы на основании обобщенной теоремы Штурма.

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

Формальная геометрия

В вопросе о понятии математического пространства особенно остро проявляется проблема соотношения математики с окружающей действительностью. Математической наукой о физическом пространстве как раз и является геометрия. Ньютон считал, что основанием для геометрии является практика механики, и в действительности геометрия есть не что иное, как та часть механики в целом, которая точно устанавливает и обосновывает искусство измерения. Следовательно, смысл геометрии заключается в подведении под искусство измерения прочного и достаточно обязательного базиса: необходимо, чтобы математические следствия основных допущений о физическом пространстве можно было проверить фактическим измерением в этом пространстве. Но установление соответствия между математической теорией и эфемерным реальным пространством не является математической задачей. С точки зрения математики задача формализации геометрии выглядит примерно следующим образом. Нужно принять некоторую математическую концепцию реального физического пространства. Поскольку в качестве системы расстояний в евклидовой геометрии принимается поле вещественных чисел, геометрию проще всего понимать, например, по Вейлю — как точечное пространство над соответствующим векторным пространством над полем . Теперь программу формализации (аксиоматизиции) можно сформулировать следующим образом. Выбрав конечное число первичных геометрических понятий (элементов) и отношений между ними, найти такую систему аксиом для этих элементов и отношений, для которой из того, что некоторая элементарная теорема верна для принятого в определения основных понятий, вытекает, что она выводима из принятых аксиом, и, обратно, выводимость влечет истинность. (Здесь, как и обычно, мы называем высказывание элементарным, если оно выразимо в языке первой ступени с рассматриваемыми отношениями на рассматриваемых элементах.) Эта программа аксиоматизации реализуется посредством так называемой координатизации исходного геометрического пространства .

Координатизация геометрического пространства

Хорошо известна модель планиметрической части системы аксиом Гильберта, в которой точкой плоскости является упорядоченная пара действительных чисел, а прямой линией — фактически алгебраическое уравнение первой степени. При ее создании геометрия строится из чисел. Задача координатизации состоит в обратном: построить числовую систему, исходя из геометрии (т.е. из точек и прямых). Точнее, пусть имеется некоторая планиметрия, объектами которой являются элементы двух множеств — множества точек (обозначаются заглавными латинскими буквами) и множества прямых (обозначаются малыми латинскими буквами), для которых справедливы аксиомы Гильберта в их планиметрической части. (При этом основным отношением является отношение инцидентности (принадлежности): — точка принадлежит прямой .) Требуется построить такое поле , изоморфное полю вещественных чисел, чтобы точки в нашей геометрии задавались упорядоченными парами элементов (координатами) из , а прямые — линейными алгебраическими уравнениями.

Из аксиом (1.1)–(1.3) первой группы аксиом системы аксиом Гильберта вытекает существование в нашей планиметрии фигуры, играющей важнейшую роль в процессе ее координатизации. Эта фигура состоит из двух прямых , пересекающихся в точке , и двух отличных от точек и , лежащих соответственно на этих прямых. Элементами поля будут точки прямой . Для точек этой прямой мы введем операции поля — сложение и умножение — геометрически, т.е. определим их через инцидентность, причем точка будет представлять единицу для умножения, а точка — нуль для сложения. Возможность использования этой фигуры для изображения конструкции сложения и умножения точек прямой основана на следующей лемме, которая легко выводится из аксиомы параллельности (V).

Лемма 30.4. Если две различные прямые и пересекаются, то всякая прямая , параллельная , также пересекается с .

Доказательство. Если допустить, что это не так для некоторой прямой , то через точку пересечения прямых и , не принадлежащую прямой , проходит две различных прямых и , не пересекающихся с , что противоречит аксиоме параллельности Евклида.

Теперь определяем сложение точек и прямой с помощью следующих построений. В нашей фигуре проводим прямые:

Тогда , и, следовательно, .

Аналогично определяется умножение точек и прямой с помощью следующих построений. Проводим прямые

Тогда из подобия треугольников и вытекает, что , то есть ( — единичный отрезок).

Можно показать, что так определяемые операции определены корректно и удовлетворяют всем аксиомам поля. Упорядочение в этом поле основывается на геометрическом отношении "между": — точка лежит между точками и . Сначала определяется понятие положительности: . Затем, исходя из гильбертовых аксиом второй группы (аксиомы порядка), устанавливается выполнимость в построенном поле аксиом порядка:

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

Аксиома полноты: пусть и — два непустых множества точек на прямой и пусть имеется точка , такая, что для всех и верно . Тогда имеется такая точка , что для всех и , отличных от , верно .

Из геометрической аксиомы полноты (непрерывности) немедленно следует, что поле, построенное на прямой , полно. Это фактически завершает доказательство того, что построенное поле изоморфно полю вещественных чисел.

Поле, построенное на прямой , можно использовать теперь, для координатизации всей плоскости. Для этого нужно сначала построить поле и на прямой так же, как это сделано на прямой ( — единичная точка на ). Построенные на и поля оказываются изоморфными: изоморфизм осуществляется проектированием параллельно прямой . Теперь каждой точке плоскости мы можем сопоставить упорядоченную пару точек (вещественных чисел), как показано на следующем рисунке.

Остается выразить требование взаимной перпендикулярности осей координат и и равенства единичных отрезков . Это достигается с помощью гильбертовых аксиом III группы — аксиом конгруэнтности отрезков и углов.

Если и — две точки плоскости со своими координатами, то точечное пространство упорядоченных пар можно рассматривать над векторным пространством векторов , в котором скалярное произведение определяется по формуле

В итоге точечное пространство упорядоченных пар оказывается изоморфно исходному евклидову точечному пространству над векторным пространством .

Элементарная теория евклидовой планиметрии

Задача формализации аксиоматической геометрии, построенной, например, на базе системы аксиом Гильберта, снова ставит нас перед проблемой, уже возникавшей при формализации теорий числовых систем: как адекватно выразить содержание аксиомы полноты (непрерывности), в формулировке которой участвуют множества и , в нашем формальном языке первой ступени, как понимать участвующие там множества? Здесь мы снова выбираем тот же выход, что и при формализации теорий числовых систем: мы заменяем множества определяющими их предикатами (свойствами) в языке первого порядка для элементарной геометрии с исходными понятиями по системе Гильберта. Получаемая таким образом в элементарной форме аксиома полноты (а точнее, схема аксиом, называемая схемой Тарского) может быть сформулирована следующим образом: для любых формул и имеем

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

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

Формальный математический анализ

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

Наиболее распространенной из формальных теорий математического анализа является теория Гильберта–Бернайса. Она строится следующим образом. К языку формальной арифметики, описанной в предыдущем пункте, добавляется новый вид переменных , которые рассматриваются как пробегающие множества натуральных чисел. Добавляется новый вид атомарных формул: (" принадлежит множеству "). Логические аксиомы формальной арифметики (т.е. аксиомы формализованного исчисления предикатов) и схема аксиом индукции естественно усиливаются таким образом, чтобы включать в себя формулы расширенного языка. Наконец, добавляется единственная новая схема аксиом — схема аксиом свертывания:

где — формула рассматриваемого языка, не содержащая свободно ; — переменная для натуральных чисел.

Эта теория Гильберта–Бернайса, хотя в ней речь идет лишь о натуральных числах и о множествах натуральных чисел, достаточна для естественной формализации математического анализа. Интересна проблема обоснования непротиворечивости этой теории. Согласно теореме Гёделя о неполноте формальной арифметики для этого необходимо использовать средства, выходящие за пределы формального математического анализа. В 1962 г. К. Спектор доказал непротиворечивость этой теории с помощью остроумной модификации модели Гёделя для интуиционистской арифметики, которая представляет собой некоторое далеко идущее расширение требований интуиционизма. Трудности в попытках доказательства непротиворечивости теории Гильберта —Бернайса связаны с той особенностью аксиомы свертывания этой теории, что в формуле этой аксиомы разрешается свободно использовать кванторы по множествам. Таким образом, при выяснении принадлежности числа у определяемому в аксиоме множеству необходимо использовать наличие всех множеств натуральных чисел, в том числе и определяемого множества . Можно сказать, что аксиома свертывания формального анализа выражает до некоторой степени необходимость актуального существования всех множеств натуральных чисел одновременно (только после этого в формуле могут использоваться кванторы по переменным, пробегающим множество таких множеств). Эта особенность встречается в ряде формальных теоретико-множественных теорий и называется непредикативностью теории. Так что формальный анализ Гильберта–Бернайса является непредикативной формальной теорией.

Имеется эквивалентная формулировка анализа Гильберта–Бернайса, в которой вместо множеств натуральных чисел фигурируют функции, перерабатывающие натуральные числа в натуральные. Для такого вида функции к формальной арифметике добавляются переменные и новый вид термов: ("результат применения к "); логические аксиомы и схема аксиом индукции естественно распространяются на формулы нового языка, и, наконец, добавляется единственная новая схема аксиом, называемая аксиомой выбора анализа:

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

Для устранения непредикативности были предложены различные формальные аксиоматические теории предикативного (или разветвленного) анализа.

Общий взгляд на процесс формализации математической теории

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

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

Один из важнейших вопросов о теории есть вопрос о ее формальной непротиворечивости, который состоит в выяснении того, существует ли в языке такая формула , что сама и ее отрицание являются теоремами теории (что равносильно выяснению вопроса о том, всякая ли формула языка является теоремой теории ). Метаматематический метод доказательства непротиворечивости, предложенный в начале XX в. Гильбертом, состоит в том, что утверждение о непротиворечивости формальной системы рассматривается как высказывание о возможных в этой системе доказательствах. Само же это высказывание уже принадлежит метатеории , которая и исследует это утверждение. Такой подход сводит вопрос о непротиворечивости к вопросу непротиворечивости другой теории . При этом говорят, что непротиворечива относительно . Большое значение имеет вторая теорема Гёделя, которая утверждает, что непротиворечивость формальной теории, содержащей формальную арифметику, невозможно доказать с помощью средств самой рассматриваемой теории (при условии, что эта теория действительно непротиворечива). Примером применения метаматематического метода может служить доказательство Г. Генцена непротиворечивости формальной арифметики, полученное им в 1936 г. и использующее трансфинитную индукцию — средство, выходящее за рамки формальной арифметики.

Существует и другой путь доказательства непротиворечивости формальной системы, идущий через понятие интерпретации и модели. Формальная система называется содержательно (или семантически) непротиворечивой, если существует модель, в которой истинны все теоремы этой системы. Без труда устанавливается, что если формальная система содержательно непротиворечива, то она формально непротиворечива. Для формальных систем, основанных на классическом исчислении предикатов 1-го порядка, справедливо и обратное утверждение (теорема Гёделя о модели): всякая непротиворечивая формальная теория имеет модель. Таким образом, другой способ доказательства непротиворечивости формальной теории состоит в построении ее модели. Но и этот метод является относительным: он устанавливает непротиворечивость одной формальной системы относительно другой, в терминах которой построена модель первой.

Можно, далее, исследовать аналогичным образом и метатеорию , построив формальную систему и изучая уже средствами следующей содержательной теории , которая будет метатеорией по отношению к теории и метаметатеорией по отношению к теории .

О границах аксиоматического метода, метода формализации и логики

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

Эти теоремы Гёделя фактически означали, что истинное утверждение не всегда может быть доказано. Эти логические теоремы по существу разрушали восходящее к Лейбницу и Декарту мнение, будто всякое истинное утверждение подвластно обоснованию методами математического доказательства. Но оставалась надежда, что выводимость ненамного меньше истинности, что недоказуемыми являются лишь экзотические формулы гёделевского типа, в которых зашифрованы утверждения, относящиеся к самим этим формулам. Однако результаты, полученные А.Тарским в 1936 г., окончательно разрушили и эту последнюю надежду (см. более подробно об этом в Заключении).

Конечно, эти результаты, показывающие, что расстояние от доказуемости (выводимости) до истинности столь велико, могут служить солидным основанием для значительной доли пессимизма в оценке роли логики (и в частности, математической логики) в процессе познания окружающего мира и истины. Некоторые определенные философы истолковывают эти результаты как полное отрицание роли логики в процессе познания, считая, что она нужна лишь для придания уже полученным результатам общепонятной и убедительной формы, а сам механизм получения этих результатов совершенно иной. Не следует истолковывать эти результаты и как полный крах формального подхода к математическим теориям. Эти результаты несомненно означают, что первоначальная "максималистская" гильбертовская программа финитистского подхода к обоснованию математики не может быть реализована в полном объеме: нельзя построить математику как некоторую фиксированную совокупность средств, которые можно было бы объявить единственно законными, и с их помощью строить метатеории любых теорий. Невозможность полной формализации содержательно определенных математических теорий — это не недостаток подхода или концепции, а объективный факт, неустранимый никакой концепцией, "суровая правда" об устройстве мира, изучаемого этой теорией. Невозможность адекватной формализации теории означает, что надо либо искать формализуемые ею фрагменты, либо строить какую-то более сильную формальную теорию, которая, правда, снова будет неполна, но, быть может, будет содержать всю исходную теорию.

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