С большинством математических теорий дело обстоит так же, как в нашем первом примере: никто не может однозначно ответить, виновны подозреваемые или нет. Но не удивляйтесь, когда мы скажем, что всегда можно выбрать аксиомы так, чтобы теория была полной: для этого система аксиом должна содержать все истинные высказывания. В этом случае все доказательства будут выполняться в одну строчку, так как всё, что мы захотим доказать, уже будет аксиомой. Почему бы нам не поступить именно так, ведь полные теории — это настоящий рай для логиков?
Всё доказуемое будет совпадать с истинным, а доказательства будут максимально короткими. Однако множество всех возможных истинных высказываний слишком велико, чтобы его можно было выбрать в качестве множества аксиом. Нас интересует не столько длина доказательств, сколько возможность проверить их корректность каким-либо автоматическим методом. Так как в доказательстве каждое утверждение является либо аксиомой, либо выводится из предыдущих с помощью правил, чтобы узнать, доказывает ли перечень высказываний некоторую теорему, мы должны иметь возможность подтвердить, что некоторое высказывание является аксиомой. И если мы включим в систему слишком много аксиом, подобная проверка потребует бесконечно много времени.
Система аксиом называется рекурсивно перечислимой, когда подобного не происходит, то есть когда за конечное число шагов можно доказать, является ли произвольное утверждение аксиомой. Критерий рекурсивной перечислимости становится препятствием на пути «жадного» логика, который хочет доказать все больше и больше теорем, не позволяя добавить к системе все необходимые аксиомы. Разумеется, рекурсивно перечислимыми являются системы аксиом геометрии и арифметики, а также, в общем случае, все системы, содержащие конечное число аксиом. Также существуют рекурсивно перечислимые системы с бесконечным множеством аксиом, поскольку основной особенностью таких систем является не число аксиом, а то, что корректность любого доказательства, составленного на их основе, можно подтвердить за конечное число действий.
* * *
РАЗРЕШИМАЯ СИСТЕМА С БЕСКОНЕЧНЫМ ЧИСЛОМ АКСИОМ
Одну из возможных рекурсивно перечислимых систем с бесконечным числом аксиом можно получить, если развернуть одну из аксиом Пеано в бесконечное число утверждений. Аксиому «О не следует ни за каким натуральным числом»» можно считать сжатой формой множества высказываний: «О не следует за нулем», «О не следует за единицей», «О не следует за двойкой» и т. д. до бесконечности. Предположим, что мы хотим определить, является ли некоторое высказывание одной из этих аксиом. Разумеется, оно будет принадлежать приведенному выше списку, если будет начинаться со слов «О не следует за…», а далее будет указано некоторое число. Напомним, что «единица»» в действительности означает «число, следующее за нулем», «два» — «число, следующее за числом, следующим за нулем» и т. д. Нам останется только подсчитать, сколько раз в нашем высказывании встречается слово «следующее». Следовательно, рассматриваемая нами система аксиом является рекурсивно перечислимой.
* * *
Подведем итог. Аксиоматический метод появился примерно в 300 году до н. э., с написанием «Начал». Евклид считал, что аксиомы являются очевидными истинами, соответствующими нашим представлениям о предметах в физическом мире, однако открытие новых геометрий в середине XIX века покончило с этим реалистическим подходом. С того времени аксиомами называются всего лишь высказывания, выбранные из соображений удобства в качестве основы математической теории.