2.6. Формальная аксиоматическая теория.

2.6.1. Основные определения.

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

Формальная система — это совокупность абстрактных объектов, не связанных с внешним миром, в которой представлены правила оперирования множеством символов в строго синтаксической трактовке без учёта смыслового содержания, то есть семантики.

Многие научные теории (не обязательно математические) строятся по следующему принципу. Сначала предлагаются некоторые основные понятия и некоторые исходные законы (аксиомы), присущие основным понятиям. Далее формулируются производные понятия и по определенным правилам доказываются некоторые утверждения (теоремы), относящиеся к основным и производным понятиям. Совокупность основных и производных понятий, аксиом и теорем, построенная таким способом, называется аксиоматической системой. Часто аксиомы (а значит, и теоремы) аксиоматической системы сохраняют истинность при замене одних основных понятий другими (как, например, в теории колебаний, которая находит применение в механике, электронике, оптике). Это позволяет рассматривать аксиоматические системы с двух позиций: синтаксически (принципы построения правильных и истинных предложений) и семантически (связь смысла правильных и истинных предложений со смыслом основных понятий). Для исследования синтаксиса аксиоматической системы требуется ее полная формализация, т.е. символическое представление основных и производных понятий, аксиом, правил вывода и теорем. Поэтому формальная аксиоматическая теория (формальная система) - это синтаксический аспект (сторона) аксиоматической системы. Точное же определение понятия формальной аксиоматической теории включает следующие компоненты. Во-первых, каждая формальная аксиоматическая теория должна иметь свой формальный язык. Формальный язык считается полностью определенным, когда задано (счётное) множество его символов и описаны формулы языка. Любая конечная последовательность символов языка называется выражением этого языка. Среди всех возможных выражений выделяются формулы языка, под которыми подразумеваются правильно построенные, утверждающие нечто осмысленное предложения языка. Во-вторых, каждая формальная аксиоматическая теория должна иметь свою систему аксиом - подмножество заведомо истинных формул, из которых по правилам теории могут быть выведены все истинные предложения этой теории (обычно к системе аксиом предъявляются требования непротиворечивости, независимости и полноты, среди которых обязательным является лишь требование непротиворечивости). В-третьих, каждая формальная аксиоматическая теория должна располагать конечным множеством правил вывода. Каждое правило вывода содержит формулы-посылки и формулу-заключение, выводимую при определенных этим правилом условиях из формул-посылок. Формула-заключение называется непосредственным следствием формул-посылок по данному правилу вывода. Доказательством в формальной аксиоматической теории называется всякая последовательность формул, в которой каждая формула есть либо аксиома теории, либо непосредственное следствие каких-либо предыдущих формул этой последовательности по одному из правил вывода данной теории. Формула А называется теоремой теории (обозначается ├А) тогда и только тогда, когда существует доказательство, в котором А является заключительной формулой. Выводом из множества гипотез (посылок) Г в формальной аксиоматической теории называется всякая последовательность формул, в которой каждая формула есть либо аксиома теории, либо гипотеза из множества Г, либо непосредственное следствие каких-либо предыдущих формул этой последовательности по одному из правил вывода данной теории. Формула А называется следствием множества гипотез Г (обозначается Г├А) тогда и только тогда, когда существует вывод из множества гипотез Г, в котором А является заключительной формулой.

Т.О. Формальная теория считается определенной, если:

1. Задано конечное или счётное множество произвольных символов. Конечные последовательности символов называются выражениями теории.

2. Имеется подмножество выражений, называемых формулами.

3. Выделено подмножество формул, называемых аксиомами.

4. Имеется конечное множество отношений между формулами, называемых правилами вывода.

Обычно имеется эффективная процедура, позволяющая по данному выражению определить, является ли оно формулой. Часто множество формул задаётся индуктивным определением. Как правило, это множество бесконечно. Множество символов и множество формул в совокупности определяют язык или сигнатуру формальной теории.

Чаще всего имеется возможность эффективно выяснять, является ли данная формула аксиомой; в таком случае теория называется эффективно аксиоматизированной или аксиоматической. Множество аксиом может быть конечным или бесконечным. Если число аксиом конечно, то теория называется конечно аксиоматизируемой. Если множество аксиом бесконечно, то, как правило, оно задаётся с помощью конечного числа схем аксиом и правил порождения конкретных аксиом из схемы аксиом. Обычно аксиомы делятся на два вида: логические аксиомы (общие для целого класса формальных теорий) и нелогические или собственные аксиомы (определяющие специфику и содержание конкретной теории).

Для каждого правила вывода R и для каждой формулы A эффективно решается вопрос о том, находится ли выбранный набор формул в отношении R с формулой A, и если да, то A называется непосредственным следствием данных формул по правилу R.

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

Формула называется теоремой, если существует вывод, в котором эта формула является последней.

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

Теория, в которой не все формулы являются теоремами, называется абсолютно непротиворечивой.