ДОКАЗАТЕЛЬСТВ ТЕОРИЯ, метаматематика

— наука, изучающая формализованные математические теории и доказательства в них. Ввел ее нем. математик Д. Гильберт (1862—1943) в рамках предложенной им программы обоснования математики путем доказательства непротиворечивости. В настоящее время Д. т. изучает более широкий круг вопросов, относящихся к структуре формализованных доказательств. Центральным для Д. т. является установленное Гильбертом различие между действительными» матем. предложениями, имеющими содержательный смысл, и «идеальными» предложениями, которые сами по себе не обязательно допускают истолкование, но позволяют сокращать доказательства действительных предложений. В качестве действительных предложений Гильберт выделял финитные предложения, т. е. утверждения о равенстве и различии конструктивных объектов (результатов конструктивных процессов). Отличительным признаком финитных предложений является отсутствие в них конструкций, связанных с актуальной (завершенной) бесконечностью, т. н. трансфинитных конструкций, напр., «для каждого натурального числа», «существует натуральное число», «то натуральное число, которое обладает свойством 5» и т. п. Проблема обоснования математики была бы решена, если бы удалось указать общий метод исключения идеальных предложений из доказательства действительных предложений. Гильберт заметил, что для этого, в свою очередь, достаточно финитными средствами доказать непротиворечивость математики, т. е. утверждение о том, что ни для какого предложения А нельзя доказать как А, так и отрицание А (или утверждение о недоказуемости . Он указал и подход к решению этой задачи, остающийся до сих пор основным методом Д. т.: следует сделать объектом изучения саму рассматриваемую матем. теорию и установить, что среди ее теорем нет ф-лы . С этой целью теория формализуется: перечисляются ее исходные понятия и матем. аксиомы (это же делается и при использовании аксиоматического метода в др. областях математики), а также осн. логические понятия и допустимые правила перехода. Такое перечисление определяет формальную систему или формализм. Изучаемая средствами Д. т. формальная система наз. предметной теорией, а относящаяся к ней часть Д. т. - ее метатеорией. С точки зрения метатеории, предметная теория является набором бессодержательных символов, аналогичных, папр., позициям в шахматной игре. Классическим примером применения этого способа рассмотрения является теорема двойственности в проективной геометрии: из каждой теоремы снова получается теорема после взаимной замены слов «точка» и «прямая». Гильберт надеялся на возможность полной формализации всей математики (или значительной ее части) и финитного доказательства непротиворечивости полученной формальной системы. Эти надежды были опровергнуты (1931) двумя теоремами австр. математика К. Гёделя (р. 1906), являющимися осн. результатами Д. т.: 1) в любой достаточно богатой непротиворечивой формальной системе найдется формально неразрешимое предложение, т. е. ф-ла, которую нельзя ни доказать, ни опровергнуть средствами этой системы; 2) при несколько более сильных предположениях такой ф-лой является утверждение о непротиворечивости системы. В частности, если считать, что средствами формализованной арифметики можно провести все финитные рассуждения, то непротиворечивость арифметики не доказуема финитными средствами. Вслед за теоремами Гёделя был получен другой важный результат Д. т. - теорема Чёрча о существовании неразрешимых систем, т. е. таких систем, для которых невозможен единый общий метод (алгоритм), который по каждой ф-ле в конечное число шагов решает, является ли она теоремой рассматриваемой системы.

Теоремы Гёделя выявили, во-первых, необходимость рассмотрения иерархий формальных систем, т. к. в каждой конкретной формальной системе есть формально неразрешимые предложения, и, во-вторых, неизбежность различных методов доказательства непротиворечивости. Вопросы, связанные с доказательствами

непротиворечивости, занимают в современной Д. т. центр, место, т. к. результаты, полученные при их изучении, и используемые при этом методы находят приложение как в самой Д. т., так и в др. областях матем. логики. В частности, многие доказательства непротиворечивости решают задачу приписывания смысла некоторым идеальным предложениям. Один из осн. методов доказательства непротиворечивости состоит в том, что естественная формализация рассматриваемой системы заменяется искусственной (см. Генцена формальные системы), содержащей выделенное правило (сечение), причем вид остальных правил таков, что невозможен вывод противоречия , не содержащий сечения. После этого доказывают, что из выводов числовых равенств можно устранить сечение, откуда и следует непротиворечивость. Трансфинитный элемент (он должен быть в силу второй теоремы Гёделя) появляется в доказательстве устранимости сечения следующим образом: каждому выводу сопоставляется некоторое трансфинитное порядковое число; определяется операция, сопоставляющая любому выводу числового равенства, содержащему сечение, некоторый вывод того же равенства, имеющий меньшее порядковое число. После этого устранимость сечения получается применением правила трансфинитной индукции (к финитному предикату). Доказательство непротиворечивости некоторой системы С генценовским методом обычно выявляет порядковое число а, характеризующее С в следующем смысле: можно таким образом конструктивно определить вполне-упорядочение R натуральных чисел по типу а, что в С доказуема вполне-упорядоченность любого собственного отрезка R; непротиворечивость С доказуема трансфинитной индукцией по для какого вполне-упорядочения натуральных чисел по типу в С не доказуема вполне - упорядоченность. Доказательство непротиворечивости классической арифметики, которое предложил нем. математик Г. Генцен (1936), дает для этой системы характеристику 80; для предикативного анализа (см. Предикативность) характеристическим оказывается первое сильно критическое порядковое число. Важным способом применения генценовских методов является использование полуформальных систем, содержащих т. н. неэлементарные правила вывода, напр., правило бесконечной индукции (правило Карнапа): если для любого натурального N выводимы , то выводимо и . В полуформальных системах сечение часто устранимо не только из выводов числовых равенств, но и из выводов произвольных ф-л.

Второй метод доказательства непротиворечивости, который сформулировал К. Гёдель в 1941 (опубликовано 1958), вводит трансфинитный элемент не в виде трансфинитной индукции, а через употребление конструктивных функционалов конечных типов. Функционалы типа «0» — это натуральные числа, функционалы типа (0 0) — это числовые ф-ции, а функционалы типа — это отображения числовых ф-ций в натуральные числа; вообще функционалы типа перерабатывают функционалы типа а в функционалы типа . Гёдель описывает перевод арифм. формул в ф-лы типа более простого вида), где переменные для функционалов, и доказывает, что для каждой выводимой в арифметике ф-лы можно указать такой примитивно рекурсивный функционал , что формула со свободной переменной выводима в бескванторной системе Т, правилами которой являются правила вычисления значений примитивно рекурсивных функционалов и индукция. Так как переводами числовых равенств являются они сами, отсюда и из непротиворечивости системы Т следует непротиворечивость арифметики. Американский математик К. Спектор (1930—61) дал доказательство непротиворечивости классического анализа методом Гёделя; при этом было использовано новое правило определения функционалов — правило бар-рекурсии. Однако обоснование этого правила проводится средствами, приемлемыми далеко не для всех математиков. Метод Гёделя был применен для вычисления характеристического числа подсистемы интуиционистского анализа с бар-индукцией типа 0.

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

Доказательство непротиворечивости обычно дает интерпретацию некоторых классов ф-л рассматриваемой системы С в более простой системе т. е. операцию я, сопоставляющую каждой ф-ле А рассматриваемого класса «бесконечную дизъюнкцию» (последовательность) ф-л системы , такую, что, во-первых, финитные предложения не меняются; во-вторых, для любых А к В по любому выводу В из А в С к по любому можно указать такое что выводимо из (А) в . Второе условие соответствует рассуждению: если верно то при любом верно а поэтому при каждом найдется такое j, что верно . В частности, если в качестве А взять стандартное выводимое предложение получаем: если В выводимо в С, то для некоторого . выводимо в Если взять в качестве В стандартное ложное предложение то получим, что противоречивость влечет противоречивость С. Если ф-лы системы считаются действительными предложениями, то интерпретация решает задачу приписывания смысла доказуемым ф-лам системы С.

Самый характерный пример интерпретации — гёделевская интерпретация ф-л арифметики, играющей роль С, ф-лами бескванторной системы Т, играющей роль . Аналогичные интерпретации дают и др. доказательства непротиворечивости методом Гёделя. Доказательства непротиворечивости методом Генцена дают интерпретацию экзистенциальных ф-л в бескванторной арифметике ординально рекурсивных функций. Метод -подстановок дает интерпретацию отсутствием контрпримера, отличающуюся от гёделевской интерпретации употреблением функционалов лишь типа которые можно определять с помощью не только примитивных, но и трансфинитных рекурсий. Один из первых примеров интерпретации дает теорема Эрбрана: каждая ф-ла классического исчисления предикатов разлагается, согласно этой теореме, в «бесконечную дизъюнкцию» ф-л классического исчисления высказываний. Сравнивая конструктивные (см. Логика конструктивная) и неконструктивные системы, используют интерпретацию классических систем в конструктивных путем вставки двойного отрицания. Имеется также интерпретация конструктивного (интуиционистского) исчисления высказываний в модальном исчислении Льюиса . Для анализа структуры конструктивных систем используют интерпретацию реализуемости, позволяющую сводить конструктивные системы к классическим. Модификации этой интерпретации дают возможность устанавливать необходимые условия выводимости существования и дизъюнкции (если в конструктивной арифметике выводима дизъюнкция замкнутых ф-л, то выводима и одна из этих ф-л). Многие метаматем. теоремы легко доказуемы для систем без сечения, поэтому представляют интерес доказательства устранимости сечения и др. метаматем. результатов, не являющиеся сами метаматематическими. Одним из первых примеров такого рода было доказательство теоремы Эрбрана, содержащееся в доказательстве теоремы Гёделя о полноте. В последнее время такой подход был применен для анализа конструктивных, интуиционистских и модальных систем, а также для доказательства устранимости сечения из простой теории типов. В приложениях к др. областям матем. логики оказались полезными обобщения метаматем. результатов на бесконечно длинные формулы.

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

В последнее время, особенно после исследований амер. математика П. Коэна, доказавшего (1963) независимость континуум-гипотезы и аксиомы выбора от остальных аксиом множеств теории, возрос интерес к проблеме независимости аксиом. Методы Д. т. широко применяют в теор. обоснованиях алгоритмов доказательства теорем на ЭВМ. Здесь существенную роль играют теоремы о специализации формы доказательства и о перестройках доказательств, напр., дедукционная теорема и интерполяционная теорема.

Лит.: Новиков П. С. Элементы математической логики. М., 1973; Клини С. К. Математическая логика. Пер. с англ. М., 1973 [библиогр. с. 451—465]; .