Метаматематика

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

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

Лит.: Гильберт Д., Основания геометрии, пер. с нем., М—Л., 1948, добавл. 6—10; Клини С. К., Введение в метаматематику, пер. с англ., М, 1957; его же, Математическая логика, пер. с англ., М, 1973; Карри Х. Б., Основания математической логики, пер. с англ., М, 1969, гл. 2—3; Генцен Г., Непротиворечивость чистой теории чисел, пер. с нем., в кн.: Математическая теория логического вывода, М, 1967, с. 77—153; Нагель Э., Ньюмен Дж., Теорема Геделя, пер. с англ., М, 1970; Тарский А., Введение в логику и методологию дедуктивных наук, пер. с англ., М, 1948; Gödel ., Über formal unent scheidbare ätze der Principia Mathematica und verwander System. , "Monatshefte Mathematic Physik", 1931, Bd 38, . 173—98; Rosser В., Extensions of some theorems of Gödel and Church, "Journal Symbolic Logic", 1936, v. 1, № 3; Tarski A., Logic, semantics, metamathematics, Oxf., 1956.

Ю. А. Гастев.

	Copyright © 1999-2023 Oval.ru, All Rights Reserved.