12.10. Метаматематика

Формализация логики была начата (если не считать первых попыток Лейбница) в середине XIX в. работами Дж.Буля (1815-1864) и закончена к началу XX в. главным образом благодаря работам Шредера, К.С.Пирса, Фреге и Пеано. В фундаментальном труде Рассела и Уайтхеда «Principia Mathematica» (вышел в 1910 г.) уже используется формализованный язык, который, если не считать несущественных вариаций, является общепринятым по настоящее время. Этот язык мы описали в главе 6, теперь мы дадим краткий набросок формализации логического вывода.

Существует несколько эквивалентных друг другу формальных систем логического вывода. Мы остановимся на самой компактной. Она использует всего одну логическую связку — импликацию ? и один квантор — квантор общности ?. Зато она включает логическую константу, которая изображается символом 0 и обозначает тождественно ложное высказывание. Используя эту константу, можно описать отрицание высказывания p как p ? 0, а из отрицания и импликации легко построить и остальные логические связки. Квантор существования выражается через отрицание и квантор общности, таким образом, наш сжатый язык эквивалентен полному языку, рассмотренному в главе 6.

Формальная система (языковая машина) содержит пять схем аксиом и два правила вывода. Схемы аксиом таковы:

A1. p ? (q ? p).

A2. [p ? (q ? r)] ? [(p ? q) ? (p ? r)].

A3. [(p ? 0) ? 0] ? p.

A4. (?x)[p ? q(x)] ? [p ? (?x)q(x)].

A5. (?x)q(x) ? q(t).

Здесь р, q, r — произвольные высказывания: в схемах А4 и А5 запись q(x) означает, что выделена одна из свободных переменных, от которых зависит высказывание q; запись q(t) означает, что вместо этой переменной подставлен произвольный терм t; наконец, в схеме А4 предполагается, что переменная х не входит свободно в высказывание р.

Выражение «схема аксиом» означает, что высказывание, имеющее вид одной из формул А1 — А5, рассматривается как логическая аксиома. Легко убедиться, что эти аксиомы соответствуют нашей интуиции. Схемы А1 — A3 затрагивают только исчисление высказываний, и их истинность можно проверить по таблицам истинности логических связок. Оказывается, что они истинны всегда независимо от того, какие истинностные значения принимают высказывания р, q и r. Схема А4 гласит, что если q(x) следует при любом х из высказывания р, которое от х не зависит, то из р следует справедливость q(x) при любом х. Схема А5 — это фактически определение квантора общности: если q(x) верно для всех х, то оно верно и для любого t.

Правила вывода можно кратко записать следующим образом:

МР.p | p ? qqGN.p(x)(??)p(?)

Здесь над чертой стоят посылки, а под чертой — заключения. Первое правило (носящее по традиции латинское название modus ponens) гласит, что если есть две посылки: высказывание p и высказывание, утверждающее, что из p следует q, то в качестве заключения мы выводим высказывание q. Второе правило — правило обобщения (generalization) основано на том, что если удалось доказать некое высказывание p(x), содержащее свободную переменную х, то можно заключить, что это высказывание будет верно при любом значении этой переменной.

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

D = (d₁, d₂, ..., d_n)

такая, что d_n совпадает с q и каждая формула d_i, есть либо формула из множества посылок X, либо логическая аксиома, либо заключение, полученное по правилам вывода из предыдущих формул d_j. Когда мы рассматриваем аксиоматическую теорию, то в качестве множества Х фигурирует совокупность всех аксиом данной теории, а логический вывод некоторой формулы есть ее доказательство.

Итак, доказательство формулы само стало формальным объектом, формулой определенного вида (последовательность логических высказываний), вследствие чего возникла возможность чисто синтаксического исследования доказательств как свойств некоторой языковой машины. На эту возможность указал Д.Гильберт (1862–1943), крупнейший математик XX в., который вместе со своими учениками и заложил основы нового направления. Гильберт ввел понятие метаязыка и назвал новое направление метаматематикой. Термин метасистема, который мы ввели в начале книги (и который сейчас является общепринятым), возник в результате обобщения терминологии Гильберта. Действительно, переход к исследованию математическими средствами математических доказательств – яркий пример крупномасштабного метасистемного перехода.

Основная цель, которую преследовала программа, намеченная Гильбертом, это доказательство непротиворечивости различных систем аксиом. Система аксиом называется противоречивой, если из нее можно вывести некоторую формулу q и ее отрицание ¬q. Легко показать, что если существует хотя бы одна такая формула, т. е. если теория противоречива, то из нее можно вывести любую формулу. Поэтому для аксиоматической теории вопрос о непротиворечивости системы аксиом, на которых она основана, имеет чрезвычайно большое значение. Этот вопрос допускает чисто синтаксическую трактовку: можно ли из заданных формул (наборов знаков), действуя по заданным формальным правилам, получить заданный формальный результат? Из такой постановки вопроса и исходил Гильберт; затем оказалось, что существуют и другие важные свойства теорий, которые можно исследовать синтаксическими методами. На этом пути было получено много интереснейших и важнейших результатов, главным образом негативного характера; однако мы не можем здесь на них останавливаться.