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

Одним из возможных вариантов аксиоматизации логики высказываний является следующая система аксиом:

;

; ; ; ; ;

; ;

. вместе с единственным правилом:

(Modus ponens)

Теорема корректности исчисления высказываний утверждает, что все перечисленные выше аксиомы являются тавтологиями, а с помощью правила modus ponens из истинных высказываний можно получить только истинные. Доказательство этой теоремы тривиально и сводится к непосредственной проверке. Куда более интересен тот факт, что все остальные тавтологии можно получить из аксиом с помощью правила вывода — это так называемая теорема полноты логики высказываний.

7. Лемма А à А.

├А→А
1) [A→((A→A)→A)]→[A→(A→A)→(A→A)] аксиома 2
2) A→[(A→A)→A] аксиома 1
3) [A→(A→A)]→(A→A) МР (1,2)
4) A→(A→A) аксиома 1
5) A→A МР (3,4)
Пусть Г множество формул. Тогда Г├φ (из Г выводима «фи») если существует последовательность формул φ1, φ2,…, φn, такие что φn= φ, либо φi доказуема, либо φi € Г, либо φi =МР (φk, φs) k,s<i

8. Понятие вывода в исчислении высказываний.

Определение. Выводом из конечной совокупности формул H называется всякая конечная последовательность формул , всякий член которой удовлетворяет одному из следующих трех условий: 1) является одной из формул совокупности H; 2) является доказуемой формулой; 3) получается по правилу заключения из двух любых предшествующих членов последовательности

Свойства вывода:

1) Всякий начальный отрезок вывода из совокупности H есть вывод из H.

2) Если между двумя соседними членами вывода из H вставить некоторый вывод из H, то полученная новая последовательность формул будет выводом из H.

3) Всякий член вывода из совокупности H, является формулой, выводимой из H.

Следствие. Всякий вывод из H является выводом его последней формулы.

4) Если , то всякий вывод из H является из W.

5) Для того, чтобы формула B была выводима из совокупности H, необходимо и достаточно, чтобы существовал вывод этой формулы из H.

9. Лемма Аà(BàC), B выводится Аà C.

10. Лемма АàB, BàC выводится Аà C.

11.Теорема о дедукции.

12. Леммы выводимости Bà B, BàB.

13. Леммы о выводимости (AàB) à( Bà A)

14. Лемма о выводимости A→[┐B (A B)]