Правило сложного заключения

Если формулы и доказуемы, то и формула L доказуема:

├А₁, ├А₂, …,├А_n, ├A₁→(A₂→(A₃→(...(A_n→L) …)))

├ L

Правило силлогизма

Если доказуемы формулы А→В и В→С, то доказуема формула А→С , т. е.

├А→В,├В→С

├А→С

Правило контр позиции

Если доказуема формула А→В, то доказуема формула , т. е.

├ А →В

├

Правило снятия двойного отрицания

Если доказуема формула , то доказуема формула .

Если доказуема формула , то доказуема формула :

├ А →

├ ,

├ →В

├ .

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

Если

j₁, j₂, …, j_n, j ├ ψ,

то

j₁, j₂, …, j_n├ (j → ψ).

Если нужно в некоторой ситуации установить, что , то допустим (введем гипотезу), что A верно, и докажем B, исходя из этой гипотезы.

Применяя к утверждению теоремы снова несколько раз теорему де­дукции, можно, очевидно, получить новые следствия:

j₁, j₂, …, j_n−1├ (j_n → (j → ψ));

…

├ (j₁ → … → (j_n−1 → (j_n → (j → ψ)))…).

Теорема, обратная к теореме о дедукции

Если

j₁, j₂, …, j_n├ (j → ψ),

то

j₁, j₂, …, j_n, j ├ ψ.,

то есть можно переносить левую часть формулы (посылку) за знак выводимости. Данное действие можно выполнять несколько раз (столько, сколько знаком следствия используется в формуле.

Теорема о полноте

Для того чтобы проверить выводимость формулы в ИВ (исчислении высказываний) достаточно проверить, будет ли формула являться тавтологией ЛВ (логики высказываний).

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

Упражнения

Построить вывод или обосновать выводимость формулы логики высказываний. Сделать проверку с помощью теоремы о полноте.

1. ;

2. ;

3. .