Специальная математика. Соловьев А.Е. - 31 стр.

                          2.3. Аксиоматические теории
           2.3.1. Аксиоматическая теория исчисления высказываний

Для того чтобы задать аксиоматическую теорию необходимо задать язык, аксиомы и
правила вывода данной теории.
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)

                                       — 31 —