Для того чтобы задать аксиоматическую теорию необходимо задать язык, аксиомы и правила вывода данной теории.
1. Язык:
а) Символы теории, это
- буквы (для определенности, заглавные латинские): A, B, C, ... , Z
- специальные символы: (, ), ®, ¬
б) Последовательности символов образуют выражения.
Например, выражениями будут AB ¬® (B¬ или другое, более приятное глазу,
(A ® B) ® (¬B)
Формулами будем называть выражения, задаваемые индуктивно следующим образом:
а) Любая буква (A ... Z) есть формула.
б)Если А, В - формулы, то (А), ¬A, A ® B - также формулы.
2. Аксиомы зададим тремя схемами аксиом:
A ® (A ® B)
(A ® (B ® C)) ® ((A ® B) ® (A ® C))
(A ® B) ® (¬B ® ¬A)
В схемы аксиом вместо A, B, C могут быть подставлены любые формулы. В результате конкретных подстановок на основе схем аксиом будут появляться конкретные аксиомы.
3. Правила вывода: В данной конкретной версии аксиоматической теории используется всего одно (но самое известное) правило вывода modus ponens
(модус утверждающий) или кратко - mp. Это правило, учитывая особенность его работы, еще называют правилом отсечения.
A , A ® B ½¾ B
Символ ½¾ читается как "выводимо". То есть в данной теории из формул
A и A ® B выводима формула B или формула B есть теорема данной теории.
Выводом (в данной теории) называется последовательность формул Ф1, Ф2, ... , Фn, где каждая следующая формула является аксиомой, или следует по правилу вывода из предыдущих. Последняя формула вывода называется теоремой.
Важное замечание. При описании теории, в том числе и ее языка, использовались средства, не принадлежащие определяемому (целевому) языку: запятые, точки, слова русского языка и т.д. Совокупность средств, используемых при описании целевого языка, называется метаязыком.
Пример:
Лемма: ½¾ A ® A
Ф1: Возьмем схему аксиом 2 и подставим А = А, С = А, В = А ® А, в результате получим:
(A ® ((A ® A) ® A)) ® ((A ® (A ® A)) ® (A ® A))
Ф2 : Из схемы аксиом 1, при А = А, В = А ® А, получим :
(А ® ((А ® А) ® А))
из Ф1,Ф2 по m.p. получаем Ф3: (A ® (A ® A)) ® (A ® A)
Ф4 : Из схемы аксиом 1, при А = А, В = А, получим:
(А ® (А ® А))
из Ф3, Ф4 по m.p. получаем Ф5: A ® A
Нет ничего проще создания аксиоматических теорий! Как сказал один известный математик: "Аксиоматизация сродни воровству!".
Определив свой язык, придумав свои аксиомы и правила вывода, вы получаете
свою аксиоматическую теорию.
Например, в качестве языка возьмем любые последовательности символов @, единственной аксиомой объявим один символ @, а правило вывода будет
@ ½¾ @@.
Тогда в данной теории будет выводима любая последовательность из одного или более символов @.
Одно плохо, толку в таких теориях обычно никакого нет…
А вот рассмотренная ранее аксиоматическая теория исчисления высказываний имеет ряд важных (интересных, замечательных) свойств. Формулы этой теории можно интерпретировать как формулы алгебры высказываний, записанные с использованием (функционально полного набора!) операций: Ø и ® (отрицания и импликации).
Для этой теории доказано, что она полна.То есть в этой теории могут быть выведены все тавтологии логики высказываний (которые могут быть записаны с помощью Ø и ®).
Более того, данная теория непротиворечива. То есть в этой теории не могут быть выведены какая-то формула Ф и ее отрицание (ØФ).
Докажем непротиворечивость этой теории.
Прямой проверкой доказывается, что все аксиомы, получаемые из схем аксиом, являются тавтологиями. Например, для первой схемы аксиом:
А ® (В ® А)
А
В
Ф
А из тавтологий с помощью m.p. (A , A ® B ½¾ B ) можно получить только тавтологии. А поскольку любая полученная в этой теории формула Ф есть тавтология,
то ее отрицание ØФ было бы противоречием, которое не выводимо.
Полнота и непротиворечивость очень важные свойства. Увы, большинство более сложных аксиоматических теорий не может похвастаться полнотой (открытый Геделем принцип неполноты). В них могут существовать формулы, для которых невозможно доказать как выводимость, так и невыводимость…
Что же касается непротиворечивости, то это очень жесткое требование.
Стоит допустить в теории возможность хотя бы одного противоречия (для одной формулы Ф допустит возможность вывода и ØФ), как теория становится бессмысленной, так как тогда в ней можно вывести любую формулу. (Из ложной посылки может следовать что угодно).
