При обсуждении проблемы формальной аксиоматики мы подчеркивали, что при выводе теорем из аксиом первоначальные термины рассматриваются как лишенные смысла: либо им вообще не приписывается никакого значения, либо же значение, которое они имеют, не принимается во внимание. Сказать же, что они обладают некоторым смыслом, играющим роль в процессе доказательства теорем, значит сказать, что для этих теорем важны некоторые свойства первоначальных терминов; помимо тех, что фигурируют в аксиомах. Но тогда описания этих дополнительных свойств следует сформулировать как дополнительные аксиомы.
Евклиду в “Началах” не удалось описать в его “аксиомах и постулатах” все свойства, используемые им в действительности. Его доказательства сопровождаются многочисленными чертежами. И понадобилось немало времени, чтобы прийти к очевидной для нac мысли, что на самом деле чертежи не должны быть существенной частью самого процесса доказательства: они либо облегчают процесс поиска доказательства, либо помогают следить за ходом доказательства, либо, наконец, способствуют запоминанию доказательств. На практике, однако, чертежи иногда служат источником информации, существенной для самого доказательства. Последнее обстоятельство можно проиллюстрировать на печаль-
ном примере “теоремы”, в которой “доказывается”, что каждый треугольник —равнобедренный. От многих доказательств Евклида такие “доказательства” отличаются лишь использованием чуть искаженных чертежей.
Используемые Евклидом “скрытие” допущения были выявлены уже в новейшее время и зафиксированы в виде аксиом Пашем , Гильбертом и другими. Скажем, среди аксиом системы Гильберта имеется следующая (сформулированная впервые Пашем ): если прямы, лежащая в плоскости некоторого треугольника и пересекающая одну из его сторон, не проходит через вершину треугольника, противолежащую данной стороне, то она пересекает одну из остальных сторон этого треугольника. На наших чертежах это так, но в тексте Евклида нет ничего, что позволило бы доказать, что это обязательно должно быть так. Изящное изложение евклидовой геометрии средствами формальной аксиоматики с явной формулировкой всех принимаемых, допущений дано Гильбертом в его “Основаниях геометрии” .
Обратившись снова к формальной аксиоматике, мы видим, что, кроме первоначальных терминов, самих по себе смысла не имеющих, в проведении выводов используется еще смысл слов ecтecтвенного языка. Но мы уже видели, что различные теории могут отличаться друг от друга не только принятыми в них математическими допущениями, но и логическими средствами. Поэтому, чтобы понятие теоремы, данной теории стало совершенно точным, нам придется в качестве следующего шага проделать процедуру, примененную ранее к первоначальным терминам, и по отношению ко всем словам, используемым в доказательствах . Иными словами, проводя точку зрения формальной аксиоматики, мы должны отвлечься от смысла всех входящих в доказательства слов и проводить выводы исключительно на основе точно сформулированных правил, относящихся лишь к форме ( а не к содержанию ) предложений. Логика, используемая в процессе вывода в формальной аксиоматике, как раз и должна быть зафиксирована в виде таких правил, по крайней мере частично; частично же эта логика может быть выражена посредством логических аксиом.
Такая полная формализация была бы неосуществимой если бы формализуемая теория формулировалась на естественном языке ( скажем, на русском или английском ): нерегулярности и однозначности, присущие словам и выражениям естественных языков, сильно осложнили бы эту задачу.
Фактически современная математика с большой выгодой пользуется специальными символизмами но, как правило часть ее предложений, в том числе используемых в процессе логического вывода, выражена обычными языковыми средствами. Символическая запись равенств не только весьма экономна, но и представяет значительные удобства для различных преобразований ( скажем, из х+5 = 2 получаем х==2—5, а затем и х = — 3), которые, хотя и имеют содержательное обоснование, но на практике обычно производятся быстро, без задержек на обдумывание и обоснование каждого шага. Фактически это полуформальный способ рассуждений, в значительной мере обусловливающий мощь современной математики.
Полная формализация, которую мы собираемся провести, чтобы осуществить замыслы Гильберта и достичь некоторых других целей, получается путем сочетания обычной символики, приятой в современной математике, с символическим построением логики, идущим от работ Буля, Пирса, Фреге, Уайтхеда и Рассела и других авторов. Пользуясь обеими этиими идеями, мы строим полностью символический язык для формализуемой теории. Для этого языка мы точно определяем синтаксис ( посредстэом правил образования ) и логику ( посредством правил вывода, или правил преобразования ). То что получается в результате, мы будем называть формальной системой, или формализмом, или логистической системой . Сам этот метод, приводящий к уточнению понятия теории, иногда называют логистическим методом.
Обсуждение свойств некоторой формальной системы, в том числе точное ее описание (т. е. определение правил образования и преобразования) и исследование относящихся к ней результатов, мы производим в некоторой другой теории (средствами другого языка), которую назовем ее метатеорией (а этот другой язык — метаязыком). Саму же формальную систему мы будем называть предметной (или объектной) теорией (и соответственно употреблять термины “предметный язык” или язык-объект ). Изучение свойств формальной системы, проводимое содержательными математическими методами в рамках метаязыка, мы будем называть метаматематикой, или теорией доказательств.
В качестве метаязыка мы будем пользоваться обычным русским языком, причем пользоваться содержательным образом, т. е. на основе смысла слов, а не с помощью формальных правил введение и употребление, которых потребовало бы создания метаязыка). Поскольку в обслуживающей метаматематику части русского языка предметом обсуждения являются только такие “осязаемые материи”, как символы, последовательности символов и т. п. элементы предметного языка, то эта часть языка в интересующих нас контекстах оказывается свободной от тех присущих естественному языку неясностей, которые и обусловили потребность в формализации.
Поскольку формальная система получается ( как правило ) в результате формализации некоторых разделов обычной неформальной или полуформальной математики, то символы, формулы и прочие элементы такой формальной системы истолковываются (интерпретируются) в терминах соответствующей неформальной или полуформальной математики. Совокупность значений, приписанных таким образом символам, формулам и прочим элементам формальной системы, мы будем называть ее (подразумеваемой, или естественной, или стандартной) интерпретацией. Если мы не знаем этой интерпретации, данная формальная система не представляет для нас интереса. Но в метаматематике, в соответствии с ее задачами, формальная система должна изучаться именно как таковая, т. е. просто как система символов, лишенных всякого смысла, а ее интерпретация не должна приниматься во внимание. Когда мы говорим об интерпретации, мы не занимаемся метаматематикой.
Кроме того, как мы уже говорили в предыдущем параграфе, согласно программе Гильберта, метаматематика должна пользоваться лишь так называемыми “финитными” методами, которые являются интуитивно убедительными.
Мы рассматриваем изучаемый нами язык как “формальную систему”, только если это символический язык (а не часть какого-либо естественного языка, скажем русского или английского) и если для него определены точно аксиомы и правила вывода (а не просто введены такие теоретико-модельные понятия, как “общезначимость” и “следование”). Мы называем язык, используемый при изучении какого-либо предметного языка, “метаязыком” (или “синтаксисом”) только если в нем используются лишь финитные методы (хотя некоторые авторы и придерживаются более расширительного понимания термина “метаязык”, не связывая его непременно с указанным ограничением ). Таким образом, введенные выше термины “предметный язык” и “язык исследователя” имеют более широкое значение, чем соответственно “формальная система” и “метаязык”.
Выше мы применяли термин “теория доказательств” в несколько более широком смысле, чем имел в виду Гильберт, которому мы далее намерены следовать; фактически мы не фиксировали точно никакого символического языка.
Пользуясь подходящими определениями (сформулированными применительно к символическому языку) понятий “элементарной формулы” (“атома”) исчисления высказываний, {“элементарного предикатного выражения” (“иона”) исчисления предикатов или элементарного функционального выражения” (“мезона”) исчисления предикатов с функциональными символами в качестве основы для определения понятия “формулы” (или определений понятий “терма” и “формулы”), придем к формальной системе исчисления высказывании, исчисления предикатов или исчисления предикатов с равенством. В результате этой процедуры все доказанные выше теоремы становятся метаматематическими теоремами, за исключением тех, в чьих формулировках используются понятия “общезначимости” и “следования” для исчисления предикатов (с равенством или без), определения которых нефинитны.
Объявленная Гильбертом цель спасти классическую математику от парадоксов с помощью доказательства ее непротиворечивости предполагала создание формальных систем, охватывающих ( элементарную ) арифметику (т. е. теорию натуральных чисел, а также, быть может, аналогичных “систем” из объектов), анализ (т. e. теорию действительных чисел и т. п)и ,по-видимому, также более широкие разделы математики. Однако уже метаматематические проблемы, связанные с арифметикой, оказались столь трудными, что именно к арифметическим ( и подобным им ) системам было обращено главное внимание Гильберта и его школы на протяжении двух десятилетий (1920—1940 гг.).
Помимо прочего, у метаматематических исследований есть еще поле приложений, связанных с построением и изучением “машинных языков” (и “языков программирования”) для использования в современных быстродействующих вычислительных машинах. Информация должна вводиться в вычислительную машину в виде абсолютно стандартных последовательностей символов, записанных налейте, перфокартах или еще как нибудь и не требующих для своего прочтения ни малейшего размышления. Для формирования таких последовательностей символов надо разработать точные синтаксические правила, подобные тем правилам, которые впервые стали объектом математического исследования в рамках гильбертовской метаматематики.