Аксиоматическое построение теорий

Для доказательства некоторого утверждения, необходимо оттолкнуться от других утверждений (предположений). Условно представим каждое утверждение в виде окружности, а стрелками пометим какие утверждения использовались при его доказательстве. Так как возможных утверждений очень много (вообще говоря бесконечно много), такое спагетти взаимосвязей может оказаться очень запутанным.

Однако, замечательным образом в этом переплетении, обычно, можно навести порядок. Оказывается, что существует только несколько исходных утверждений (аксиом) из которых выводятся все остальные. Другими словами, из конечного набора утверждений удаётся получить бесконечное число других утверждений. Это замечательное свойство математических и физических теорий называется аксиоматическим методом.

Геометрия Евклида была по-видимому первой теорией, сформулированной в аксиоматическом виде. Сначала перечислялись "очевидные", принимаемые без доказательств утверждения - аксиомы, а затем, при помощи логического вывода, получались другие утверждения - теоремы. Впрочем, логический вывод был достаточно неформальный, часто опирающийся на интуитивную очевидность. По образному выражению Владимира Успенского это были психологические доказательства, т.е. рассуждения, убедительные на столько, что вы готовы других людей убеждать при помощи этих же рассуждений.

Со временем возникла потребность так формализовать построение теории и доказательства теорем, чтобы ни какие незаметно привнесённые "очевидности" не портили её логическую стройность. В частности, по-возможности необходимо отказаться от естественного языка с присущей ему неоднозначностью. Блестящим примером подобного подхода явились "Основания геометрии" и последующие работы Давида Гильберта. При этом все объекты теории и взаимосвязи между ними обозначаются формальными символами, а логический вывод сводится к "перестановке" этих символов по заранее определённым правилам.

✦ Аксиомы "хорошей" теории обладают свойствами независимости, непротиворечивости и полноты. Независимость означает, что ни одну из аксиом нельзя вывести из других. Если это удаётся сделать, система аксиом уменьшается, пока не останутся полностью независимые утверждения. Непротиворечивость - предполагает, что в теории нельзя вывести некоторое утверждение и одновременно с этим доказать его отрицание. Противоречивая теория приносит мало пользы и необходимо избегать таких теорий. Наконец, полнота системы аксиом означает, что с их помощью можно доказать или опровергнуть любое утверждение, которое формулируется в рамках данной теории. Если утверждение (и его отрицание) не выводимо из аксиом, его можно к ним добавить. В "хорошей" теории множество аксиом должно оставаться конечным.

Полную и непротиворечивую теорию нельзя изменить, добавив к уже существующим аксиомам новую. При этом или система аксиом перестанет быть независимой, или в теории возникнут противоречия (если добавлено отрицание выводимого из исходных аксиом утверждения).

✦ Теоремы теории можно разбить на классы зависимостей, отбирая в каждый класс теоремы, выводимые из данной группы аксиом. Например, пусть есть 3 аксиомы $A_1,A_2,A_3$. Если теорема $T_1$ выводима из $A_1,A_2$ и не требует аксиомы $A_3$, она помещается в класс $\{A_1,A_2\}$. В некотором смысле аксиомы содержат в себе некоторую " аксиоматическую информацию", которая требуется для вывода данной теоремы. Чем "информативнее" теорема, тем больше аксиом необходимо задействовать для её вывода. Иногда может оказаться, что теорема принадлежит сразу двум классам, например $\{A_1,A_2\}$ и $\{A_1,A_3\}$. Это означает, что информация в аксиомах $A_2$ и $A_3$, необходимая для теоремы, частично перекрывается.

В принципе можно перечислить подмножество теорем, которые не требуют для своего доказательства некоторой аксиомы. Эти теоремы образуют, вообще говоря, неполную теорию. Однако, такая теория может оказаться достаточно содержательной и, как мы видели на примере вывода преобразований Лоренца, более общей, чем та, которая следует из полного набора аксиом. Добавление неиспользуемой аксиомы приводит к новым теоремам, которые являются более жёсткими (определёнными). Так, утверждение о том, что время абсолютно, т.е. во всех системах отсчёта течёт одинаковым образом, является более жёстким, чем допущение различного хода времени для различных наблюдателей. Большая общность теории как раз означает, что в ней допускаются явления (формулируемы в виде утверждений), которые отвергаются в частной теории, в результате добавления "ограничивающих" аксиом.