МЕТАМАТЕМАТИКА

МЕТАМАТЕМАТИКА, теория доказательств, теория доказательства, в широком смысле слова - метатеория математики, не предполагающая никаких спец. ограничений на характер используемых метатео-ретич. методов, на способ задания и объём исследуемой в М. -"математики". Более распространённым и исторически ранним (тем более, что М. вообще была первым примером "метанауки") является следующее, более специальное понимание термина "М.", идущее от Д. Гильберта. Открытие парадоксов (антиномий) в логике и множеств теории выдвинуло в нач. 20 в. задачу перестройки оснований математики и логики на нек-рой основе, исключающей появление противоречий. Программа логицизма предусматривала для этой цели "сведение" математики к логике с помощью аксиоматического метода, но независимо от успешности такого "сведения" для перестроенной т. о. математики (или лежащей в её основе логики) отсутствие известных и невозможность появления новых антиномий могло гарантировать только доказательство их непротиворечивости. Представители математического интуиционизма предлагали столь радикально пересмотреть содержание самого понятия "математика", чтобы повинные (и даже только подозреваемые) в появлении антиномий абстракции клас-сич. математики (как, напр., абстракция актуальной бесконечности) были раз и навсегда изгнаны из неё. Выдвинутая Гильбертом концепция математического формализма, с одной стороны, отказывалась от логицистич. иллюзий о возможности обоснования математики путём "сведения" её к логике, но с другой -решительно не разделяла и интуиционистского скепсиса по отношению к возможностям аксиоматич. построения удовлетворительной в логич. отношении математики. Принимая значит, часть интуиционистской критики по адресу традиционной классич. математики, Гильберт в то же время решил "реабилитировать" аксиоматич. установку: "Ничто не может изгнать нас из рая, который создал нам Кантор",- говорил он. Для этого прежде всего нужна была последоват. формализация подлежащих обоснованию мате-матич. теорий (аксиоматической теории множеств, аксиоматич. арифметики), т. е. представление их в виде исчислений (формальных систем), для к-рых "чисто формально" следует определить понятия аксиомы (формулы нек-рого спец. вида), вывода (последовательности формул, каждая из к-рых получается из предыдущих по строго фиксированным правилам вывода), доказательства (вывода из аксиом) и теоремы (формулы, являющейся заключит, формулой нек-рого доказательства), чтобы затем, пользуясь нек-рыми "совершенно объективными" и "стопроцентно надёжными" содержательными методами рассуждений, показать недоказуемость в данной формальной теории противоречия (т. е. невозможность ситуации, при к-рой её теоремами оказывалась бы к.-л. формула и её отрицание). Совокупность таких "объективных" и "надёжных" (во всяком случае, неуязвимых со стороны интуиционистского критицизма) методов и должна была составить М. (теорию математич. доказательства). Комплекс ограничений, налагаемых на допустимые в М. методы, Гильберт охарактеризовал как ф и н и-т и з м: в ещё более радикальной форме, нежели интуиционизм, эта "финитная установка" запрещает использование каких бы то ни было "метафизических" ссылок на бесконечные ("инфинитные") совокупности. Ограничениям этим не удовлетворяют, напр., такие важные метатеоретич. результаты, как теорема К. Гёделя о полноте исчисления предикатов и теорема Л. Лёвенхейма - Т. Ско-лема об интерпретируемости любой непротиворечивой теории на области натуральных чисел, поскольку используемое в них понятие общезначимости формулы исчисления предикатов определяется с помощью "нефинитного" представления о "совокупности всех возможных интерпретаций" (поэтому эти мета-теоремы, строго говоря, не принадлежат к М., в связи с чем их часто относят к металогике или к т. н. теоретико-множественной логике предикатов). Однако (мета )теоремы о непротиворечивости исчисления высказываний и исчисления предикатов удалось получить в русле "финитной установки", т. е. строго метаматематич. путём. И всё же гильбертовская программа в её полном виде оказалась неосуществимой: Гёдель (1931) показал, что никакая непротиворечивая формализация математики не может охватить всей классич. математики (и даже всей формальной арифметики) - в ней непременно найдутся т. н. неразрешимые, т. е. выразимые на её языке, но не доказуемые и не опровержимые её средствами (хотя и содержательно истинные) формулы. Примером такой формулы является формула, утверждающая свою собственную недоказуемость; задать формулу со столь парадоксальной на вид интерпретацией Гёделю удалось с помощью придуманного им остроумного приёма - своего рода арифметич. кодирования ("гёде-левской нумерации") символов, формул и последовательностей формул формальной системы, однозначно приписывающего каждому элементу системы "тёде-левский номер". Благодаря такой "ариф-метизации синтаксиса" Гёделю удалось представить не только предикаты рассматриваемой формальной системы, но и относящиеся к ней метаматематич. предикаты ("быть формулой", "быть доказательством", "быть теоремой" и т. п.) посредством нек-рых арифметических предикатов. Утверждение этой т. н. первой теоремы Гёделя доказывается теперь с помощью рассуждения, чрезвычайно близкого к т. н. парадоксу Ришара и вообще к парадоксам типа "Лжеца" ("я лгу") и вариантам антиномии Б. Рассела ("брадобрей, бреющий всех тех и только тех жителей деревни, к-рые не бреются сами" и т. п.). В качестве следствия из этой теоремы получается вторая теорема Гёделя, согласно к-рой непротиворечивость любой непротиворечивой формальной системы, содержащей арифметику натуральных чисел, не может быть доказана средствами, формализуемыми в этой системе. В этих теоремах Гёделя говорится, т. о., не только о свойствах рассматриваемой формальной системы, но и о нек-рых метаматематич. свойствах, так что они являются даже не метатеоре-мами, а, строго говоря, м е т а м е т а-теоремами. Из них вытекает неосуществимость "финитистской" программы Гильберта: не только вся математика, но даже арифметика натуральных чисел не допускают формализации, к-рая была бы одновременно полной и непротиворечивой; к тому же весь аппарат финитизма выразим средствами интуиционистской арифметики, из чего, в силу второй теоремы Гёделя, следует невозможность фи-нитистского доказательства непротиворечивости арифметики. (Ещё один фундаментальный результат М.- т. н. теорема А. Чёрча о неразрешимости арифметики и исчисления предикатов, согласно к-рой не существует алгоритма распознавания доказуемости для формул соответствующих исчислений.)

В нек-ром смысле теоремы Гёделя можно было воспринимать как "конец М.", но, свидетельствуя об ограниченности финитизма, формализма и связанной с ними гильбертовской программы, а также аксиоматич. метода в целом, эти теоремы в то же время послужили мощным стимулом поиска средств доказательств (в частности, доказательств непротиворечивости) более сильных, чем финитные, но и в определённом смысле конструктивных. Одним из таких методов явилась т. н. трансфинитная индукция до первого недостижимого конструктивного трансфинита; этот путь позволил получить доказательство непротиворечивости арифметики (Г. Генцен, В. Аккерман, П. С. Новиков, К. Шют-те, П. Лоренцен и др.). Др. примером может служить т. н. ультраинтуиционистская программа обоснования математики, позволившая получить абсолютное (не пользующееся редукцией к к.-л. др. системе) доказательство непротиворечивости теоретико-множественной системы аксиом Цермело - Френкеля.

Лит.: Гильберт Д., Основания геометрии, пер. с нем., М.- Л., 1948, добавл. 6 -10; К ли ни С. К., Введение в метаматематику, пер. с англ., М., 1957; его же, Математическая логика, пер. с англ., М., 1973; К а р р и X. Б., Основания математической логики, пер. с англ., М., 1969, гл. 2 - 3; Генцен Г., Непротиворечивость чистой теории чисел, пер. с нем., в кн.: Математическая теория логического вывода, М., 1967, с. 77 -153; Н а г е л ь Э., Ньюмен Дж., Теорема Гёделя, пер. с англ., М., 1970; Тарский А., Введение _в логику и методологию дедуктивных наУк, пер. с англ , М., 1948; God el К., TJber formal unent scheidbare Satze der Principia Mathematica und verwander System. I, "Monatshefte Mathe-matic Physik", 1931, Bd 38, S. 173-98; R о s s е г В., Extensions of some theorems of Godel and Church, "Journal Symbolic Logic" 1936, v. 1, № 3; Т а г s k i A., Logic, semantics, metamathematics, Oxf., 1956.

Ю. А. Гостев.