Аксиоматическая система вывода

Логика высказываний, подобно другим математическим системам, может быть представлена как аксиоматическая система с логическими аксиомами и правилами вывода. Аксиомы — это некоторые тавтологии, правило вывода R выводит высказывание  из последовательности высказываний ₁, … ,_n .

Определение (аксиомы). Каждое высказывание следующего вида является аксиомой.

1. ()

2. (())  (()())

3. (  )  ()

Высказывания , ,  могут быть произвольными. Легко проверить, что все эти аксиомы являются правильно построенными формулами логики высказываний и, конечно, тавтологиями.

Определение (правило логического вывода Modus Ponens). Правило Modus Ponens утверждает, что высказывание  выводится из высказываний  и .

Правило Modus Ponens (правило заключения) своим названием обязано Диогену Лаэртскому и обозначается:

,  ⊢ 

Таким образом, любые новые высказывания выводятся из аксиом и правила заключения.

Пример. Докажем, что высказывание AA выводимо в аксиоматической системе, т.е., что ⊢ AA.

1. ⊢ A((BA)A)

(из 1-й аксиомы, где A, (BA))

2. ⊢ (A((BA)A))  ((A(BA))(AA))

(из 2-й аксиомы, где A, (BA), A)

3. ⊢ (A(BA))  (AA)

(из 1 и 2, по правилу Modus Ponens, где  A((BA)A), (A(BA))(AA))

4. ⊢ A(BA) (из 1-й аксиомы)

5. ⊢ (AA)

(из 4 и 3, по правилу Modus Ponens)

9