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

Система аксиом исчисления высказываний состоит из 11 аксиом (по сути представляющих собой тождественно истинные формулы алгебры логики), которые делятся на четыре группы.

Первая группа аксиом (содержащая только импликацию).

: . : .

Вторая группа аксиом (к импликации присоединилась конъюнкция):

: : . : .

Третья группа аксиом (к импликации присоединилась дизъюнкция):

: : : .

Четвертая группа аксиом (к импликации присоединилось отрицание):

: : :

Правила вывода.

1 Правило подстановки(ПП).

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

Операция замены в формуле А переменной х формулой В, носит название подстановки и символически записывается так:

или .

Уточним сформулированное правило:

а) если формула А есть собственно переменная х , то подстановка дает , очевидно, В;

б) если формула А есть переменная y , отличная от х ,то подстановка дает А;

в)подстановка формулы В вместо х в отрицание формулы А есть отрицание подстановки , т. е. подстановка дает ;

г) если А₁ и А₂- некоторые формулы, то подстановка дает * , где через символ * обозначен любой из символов операций конъюнкция, дизъюнкция или отрицание

Если А- выводимая (доказуемая ) формула, то будем писать, как и ранее, ├А. Тогда ПП можно записать схематически следующим образом:

├А____ .

├

И читается эта запись так: “Если формула А выводима (доказуема), то выводима (доказуема) и формула .

2 Правило заключения (ПЗ).

Если формулы А и А→В выводимы (доказуемы) в исчислении высказываний, то формула В также выводима (доказуема). Схематическая запись этого правила имеет вид:

├А;├А→В (Modus ponens)

├В

Правомерность этого правила очевидна: если импликация и посылка истинны, то заключение в импликации может быть только истинным(см. таблицу истинности операции “импликация”).