20. Формальные аксиоматические теории (фат).

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

Выводом формулы B называется такая последовательность формул ФАТ A1, A2 .. An (=B), в которой последнее совпадает с В и каждая формула или является аксиомой или получена по правилам вывода из предыдущих. Если для формулы В в рамках рассматриваемой теории есть цепочка вывода, то она называется выводимой в рамках данной теории или теоремой.

Для ФАТ аксиоматических теорий обычно рассматривается ряд вопросов:

1. Решение вопроса о полноте, совпадает ли множество теорем данной теории с множеством тождественно истинных утверждений или тавтологией теории, это вопрос о полноте в широком смысле

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

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

4. Разрешимость теории. Говорит о том, существует ли некий алгоритм, позволяющий проверить является ли некоторая правильная формула теоремой, рассматриваемой факт. Решается вопрос о разрешимости множества теорем данной теории. В рамках этого вопроса так же рассматриваются вопросы вида F1&F2&..&Fn -> B является ли данная формула тавтологией или теоремой данной теории в случае полноты, т.е. при наличии знаний F1..Fn можем ли мы вывести знания из F1,F2..Fn следует В. Если вся формула тавтология то В следует из F1, .. , Fn. В том случае, когда все формулы F1 .. Fn являются аксиомами либо теоремами в рамках теории, вопрос часто ставится о том, является ли теоремой В. Но среди формул Fi могут встречаться и истинные только при определенных условиях, такие формулы, как правило, не являются теоремами или аксиомами теории. Но их можно рассматривать в качестве гипотез и часто удается свести вопрос о логическом следовании формулы В из гипотез к вопросу о том, является ли вся записанная формула теоремой.

5. Независимость системы аксиом. Можно ли из этой теории выбросить 1 или несколько аксиом так, что множество теорем этой теории останется прежним. Этот вопрос эквивалентен выводимости аксиом друг из друга.

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