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

Для более точного представления математических теорий широко используются символы. В формальных теориях символизация доведена до такой крайней степени, при которой никакие слова вообще не допускаются - они заменяются символами. Более того, в формальной теории символы воспринимаются просто как значки, с которыми обращаются согласно определенным правилам, зависящим лишь от формы выражений, образованных из символов. Таким образом, в отличие от обычного употребления символов в математике, символы в формальных теориях не заменяют собой никаких других объектов. И еще одна важнейшая отличительная черта формальных теорий состоит в том, что предполагаемая логическая система явным образом включается в теорию.

К формальным теориям, к рассмотрению которых мы сейчас переходим, мы предъявим еще дополнительные требования. Эти требования связаны с одним вспомогательным понятием, — которое мы прежде всего и опишем. Речь идет о понятии эффективной процедуры (или эффективного метода)- так мы будем называть совокупность предписаний, позволяющую чисто механическим путем в конечное число шагов получить ответ на любой вопрос из некоторого класса вопросов. Эффективная процедура — это нечто вроде рецепта, в котором указано, что именно надо делать на каждом шаге, причем для пользования таким рецептом не требуется никакой мыслительной работы. В принципе для выполнения такого рода предписаний всегда можно построить специальную машину.

Формальные теории, с которыми мы будем иметь дело, — это аксиоматические теории. Формулы в такой теории представляют собой определенного рода строчки (т. е. конечные последовательности) символов. Мы потребуем, чтобы формулы обладали следующими свойствами:

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

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

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

В такой формальной аксиоматической теории оказывается эффективным и понятие доказательства; иными словами, в такой теории имеется эффективная процедура, позволяющая для произвольной конечной последовательности формул решить, является ли она доказательством. Из существования такой эффективной процедуры отнюдь не следует наличие метода, позволяющего открывать новые доказательства. Но если нам уже предъявлена некоторая последовательность формул, являющаяся по предположению доказательством, то эта эффективная процедура позволяет подтвердить (или отклонить) это предположение.

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

При описании формальной аксиоматической теории нам приходится решать проблему точного выявления используемой в ней логической системы. Один из очевидных путей ее решения состоит в задании определенных правил вывода. Во всех представляющих интерес системах множество правил бесконечно, и возникает проблема, каким образом описать это множество, чтобы можно было определить, относится ли любое конкретное правило к этому множеству. Решение этой проблемы, которого мы будем придерживаться, состоит в том, что выделяется конечное число правил вывода, к которым присоединяются логические аксиомы данной аксиоматической теории, из которых затем уже можно получить теоремы, выражающие дальнейшие логические принципы. Иначе говоря, решение это означает объединение аксиоматизированной системы логики с данной аксиоматической теорией, в результате чего и получается формальная аксиоматическая теория. Из логических систем, которые могут быть использованы для этой цели, мы остановим свой выбор на узком исчислении предикатов. Основанием для такого выбора служит то обстоятельство, что в исчислении предикатов получает свое формальное выражение большая часть логических принципов, принимаемых большинством математиков, и что это исчисление дает все логические средства, необходимые для построения многих математических теорий. Аксиоматизацию мы опишем в следующих двух параграфах.

Теорема 3.3 (теорема полноты). Если А есть тавтология, то А доказуема; иными словами, из |= А следует |— А.

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

Теорема 3.4. Если А доказуема, то А — тавтология; иными словами, из |— А следует |= A.

Доказательство. Прежде всего мы видим, что каждая формула, получаемая из любой аксиомной схемы, есть тавтология. Далее, по теореме 2.3 из |= А и |= A→В следует |= В. Поскольку каждая теорема есть либо аксиома, либо получается из аксиом посредством одного или нескольких применений modus ponens, то каждая теорема оказывается тавтологией.

Таким образом, понятия общезначимости и доказуемости для исчисления высказываний равнообъемны. Этот результат был получен в 1921 году американским логиком Эмилем Постом. Поскольку вопрос об общезначимости может быть эффективно решен для произвольной формулы, понятие теоремы в исчислении высказываний эффективно.

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

1) в число правил образования теории включаются правила: если А и В - формулы, то (А)(B) — формула;

Если A - формула, то ~ (А) — формула;

2) к аксиомам теории добавляются четыре аксиомные схемы, которые мы выбрали выше для формулировки исчисления высказываний;

3) к числу правил вывода присоединяют modus ponens. Формулы данной теории можно тогда рассматривать как формулы исчисления высказываний, в которых роль высказывательных букв играют формулы, не имеющие вида (А)(B) или ~ (А) (т. е. формулы, которые нельзя с помощью связок и ~ разложить вышеуказанным образом на более простые формулы).

В результате такого включения исчисления высказываний в аксиоматическую теорию каждая тавтология станет теоремой данной теории. Но более существенно то, что исчисление высказываний может играть роль теории логического вывода. Например, доказательство некоторой формулы В можно получить, убедившись, что А и ~В→~A суть теоремы. В самом деле, из тавтологии 2 из теоремы 2.4 вытекает, что A, ~B→A|— B. В качестве другого примера напомним, что во втором из примеров В из § 2.5 тавтология (~ В → С ~ С)→B использовалась для обоснования доказательств от противного. Эту тавтологию можно применять для той же цели и в теперешней ситуации. Другими словами, доказательство формулы В можно получить, установив, что ~ В|— С и ~.B|— С. Тогда ~ В|— С ~ С, или |— ~ B → (C ~ C). Но из упомянутой тавтологии мы теперь получаем ~ В → (С ~ С) |— В И, следовательно, |— В.

< Предыдущая		Следующая >