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

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

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 есть теорема данной теории.

Выводом (в данной теории) называется последовательность формул Ф₁, Ф₂,..., Ф_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