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

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

А1: A-> (B ->A);

A2: ((A-> (B ->C)) -> ((A->B) -> (A->C)));

A3: A/\ B ->A;

A4: A/\ B ->B;

A5: A -> (B -> (A /\ B));

A6: A -> (A\/ B);

A7: B -> (A\/ B);

A8: (A->C) -> ((B-> C) -> ((A \/ B) -> C));

A9: -A -> (A->B);

A10: (A ->B) -> ((A-> -B) -> -A);

A11: A \/ -A.

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

A->B,A

---------

B

(Modus ponens)

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