Понятие выводимости

Пусть имеется конечная совокупность формул H = { A₁, A₂,…, A_n }. Говорят, что формула B выводима из совокупности H (можно записать как B ├ H), если:

либо B Î H,
либо B – доказуемая формула исчисления высказываний,
либо B получается по правилу Modus ponens из формул C и C ® B, которые выводимы из совокупности H.

Примеры

Рассмотрим, как можно установить доказуемость формул, используя правило подстановки и правило Modus ponens.

Доказать A Ú A ® A

Возьмем аксиому (α ® γ) ® ((b ® γ) ® ((α Ú b) ® γ)) и сделаем в ней подстановку (α, γ, b ò A, A, A). Получим: (A ® A) ® ((A ® A) ® ((A Ú A) ® A));
Докажем выводимость A ® A:

Возьмем аксиому (α ® (b ® γ)) ® ((α ® b) ® (α ® γ)) и сделаем в ней подстановку (α, γ, b ò x, y, x). Получим: (x ® (y ® x)) ® ((x ® y) ® (x ® x));
Из аксиомы x ® (y ® x) и правила Modus ponens имеем: (x ® y) ® (x ® x);
Выполним подстановку (y ò ØØ x). Получим: (x ® ØØ x) ® (x ® x);
Из аксиомы x ® ØØ x и правила Modus ponens имеем: x ® x;

Из формулы x ® x и правила Modus ponens имеем: (A ® A) ® ((A Ú A) ® A);
Аналогично: (A Ú A) ® A;