3.6. Формальные аксиоматические теории

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

Естественно, что при построении формальной теории стремятся разграничить язык и логические средства формальной теории от языка и логических средств, на котором описывается и которыми пользуются при изучении этой теории. Теорию, предметом которой является данная формальная теория, и язык, на котором она описывается, называют соответственно метатеорией и метаязыком данной теории. К логическим средствам метатеории предъявляют требование надежности, что обычно отождествляют с требованием эффективности используемых при описании и изучении теории средств.

Чтобы удовлетворить условиям, предъявляемым к теории и ее метатеории, чаще всего при построении формальной теории исходят из конкретных знаков — исходных символов, а саму теорию представляют как систему весьма простых манипуляций над конечными последовательностями таких символов, называемых выражениями.

Предполагается, что:

а) никакая часть символа теории не является объектом теории;

б) любое выражение однозначно представляется в виде последовательности символов теории;

в) для любых двух выражений можно определить, равны они или нет;

г) в любое выражение вместо любой последовательности рядом стоящих символов можно подставить какое угодно выражение.

В классе всех выражений формальной теории выделяют класс формул. Некоторые формулы объявляют аксиомами. Наконец, во множестве формул определяют множество отношений — правил вывода. Определения формул, задание аксиом и правил вывода должны быть эффективными.

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

удовлетворяющую следующим условиям:

а) каждая формула последовательности (1) является либо аксиомой, либо получается путем применения одного из правил вывода к каким-нибудь предшествующим формулам той же последовательности;

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

Формальную теорию называют абсолютно непротиворечивой, если не все ее формулы — Теоремы. В случае, если среди символов теории имеется символ, интерпретируемый как отрицание, для теории можно пользоваться и обычным определением непротиворечивости.

Мы дадим описание простейшей формальной теории — исчисления высказываний. Предварительно заметим, что нетрудно указать способ эффективного задания счетной последовательности символов:

Поэтому при описании формальных теорий часто исходят из счетной последовательности символов и не останавливаются на выяснении способа образования этой последовательности.

Символы:

а) переменные высказывания: А, В, С, ...;

б) логические связки:

в) вспомогательные: (скобки).

Формулы:

а) переменное высказывание — формула;

б) если U и V — формулы (U и V — символы метатеории), то — формулы.

Примечание. В целях краткости записи формул вспомогательные символы иногда опускают.

Аксиомы.

Если U, V, W — формулы, то следующие формулы — аксиомы:

Правило вывода (правило отделения):

Мы не будем заниматься доказательством каких-либо теорем этой формальной теории, убедимся лишь в ее непротиворечивости.

На множестве всех формул данной теории определим функцию со значениями 0 и 1 следующим образом:

а) если А — переменное высказывание, то в качестве выбираем произвольно 0 или 1;

б) если для формул U и V значения функции определены, то полагаем, что:

Непосредственно проверяется, что для любой аксиомы, а затем, используя правило вывода, и для любой теоремы

С другой стороны, если то . Поэтому не всякая формула данного формального исчисления — теорема. Отсюда можно заключить об абсолютной непротиворечивости исчисления высказываний.

Что касается проблемы полноты формальных теорий, то нужно заметить следующее. Не всякую формулу теории рассматривают как ее высказывание, т. е. как формулу, в отношении которой вопрос о ее доказуемости или недоказуемости имеет смысл., Не уточняя сказанного здесь относительно любых формальных Теорий, отметим, что в рассмотренной нами теории за высказывание принимают лишь такую формулу для которой значение введенной выше функции не зависит от значения для всех входящих в U переменных высказываний. Оказывается, что если U такая формула, то либо U, либо ее отрицание доказуемы. В связи с этим говорят, что исчисление высказываний полно.

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