Формулировка аксиоматической теории

В этом параграфе вводится понятия формулировки теории и независимости системы аксиом.

Как уже говорилось, неформальная теория T включает в себя некоторый список T₀ неопределяемых терминов, список T₁ определяемых терминов, список P₀ аксиом и список P₁ всех остальных высказываний, которые можно вывести из P₀ по некоторым фиксированным логическим правилам. Назначение множества T₀ состоит в том, чтобы получить из него множество T₀ È T₁ всех используемых в теории T терминов; аналогично, множество P₀ нужно для получения множества P₀ È P₁ всех теорем теории T. Упорядоченную пару <T₀, P₀ > обычно называют формулировкой теории T.

Изучение теории T может привести нас к обнаружению самых разнообразных и полезных других ее формулировок. Задание какой-либо из этих формулировок равносильно заданию некоторого подмножества множества T₀ È T₁ и подмножества множества P₀ È P₁, состоящего из высказываний, выразимых в терминах элементов множества , причем из высказываний, входящих в , можно вывести все остальные теоремы данной теории. Чтобы пара вида < T₀, P₀> была формулировкой теории T, достаточно, очевидно, чтобы термины из T₀ могли быть определены через термины из и чтобы высказывания из P₀ могли быть выведены из высказываний из .

Для многих общеизвестных аксиоматических теорий имеются различные формулировки. Различные формулировки какой-либо теории - это ни что иное, как различные возможные подходы к одной и той же математической структуре. В зависимости от принятых критериев можно предпочесть ту или иную из таких различных формулировок. Основаниями для такого предпочтения могут, например, служить соображения эстетического характера; важную роль может здесь играть и желание иметь как можно более простое множество аксиом, а также возможность более изящных доказательств теорем. Одни исследователи предпочитают какую-либо конкретную формулировку теории, находя ее более «естественной», нежели остальные. Другие стремятся располагать формулировкой, включающей минимальное количество первичных терминов или аксиом.

Казалось бы, от формулировки аксиоматической теории ничего не зависит. Две разные формулировки <T₀, P₀ > и <, > одной теории T определяют, очевидно, одно и то же множество теорем. Однако, исследователи, отправляясь от разных формулировок, часто развивают теорию в различных направлениях. При этом множество теорем, доказанных исследователями, взявшими за основу формулировку <T₀, P₀ >, может значительно отличаться от множества теорем, доказанных исследователями, взявшими за основу формулировку <, >. Различные формулировки теории во многих случаях определяют различные направления исследований. Так, например, теория графов и теория бинарных отношений значительно отличаются друг от друга наборами доказанных теорем, хотя по существу они являются различными формулировками одной и той же теории.

Формулировки неформальной теории можно характеризовать с помощью такого понятия, как независимость множества аксиом.

Определение 6.1. Множество аксиом называется независимым, если исключение любой аксиомы из этого множества приводит к уменьшению запаса теорем; в противном случае множество аксиом называют зависимым.

Отдельная аксиома (рассматриваемая как элемент множества аксиом некоторой формулировки) независима, если ее исключение из этого множества уменьшает запас теорем, и зависима в противном случае. Ясно, что независимая аксиома не может быть выведена из остальных аксиом. Разумеется, независимость какого-либо множества аксиом равносильна тому, что независима каждая аксиома из этого множества.

Рассмотрим непротиворечивую теорию T с формулировкой <T₀, P₀ >, и пусть A – одна из ее аксиом. Чтобы убедиться в независимости аксиомы A от остальных аксиом , надо доказать, что ни A, ни нельзя вывести из . Для этого достаточно построить две модели теории с формулировкой <T₀, > так, чтобы в одной из них выполнялось предложение A (это будет модель теории T), а в другой - . Так как непротиворечивость теории T считается установленной ранее, то первую модель уже фактически строить не надо. Достаточно построить вторую модель – модель теории с формулировкой .

Например, независимость системы аксиом A1, A2, A3 теории аффинных плоскостей может быть доказана посредством построения трех интерпретаций теории, для каждой из которых не выполняется одна из аксиом A1, A2, A3, а две другие выполняются (рис. 6.1).

Рис. 6.1. Три интерпретации для доказательства независимости
аксиом A1, A2, A3 соответственно

Независимость не является обязательным требованием для системы аксиом. Независимость системы аксиом свидетельствует в известном смысле об изяществе содержащей эту систему формулировки теории. Не всегда для той или иной аксиоматической теории целесообразно выбирать независимую систему аксиом: изящество системы аксиом может привести к громоздкости доказательств теорем теории.