Теорема про дедукцію

Теоре́ма про деду́кцію (ле́ма про деду́кцію, теоре́ма деду́кції) — один із фундаментальних результатів у теорії доведення, формалізує спосіб міркування, за якого для встановлення імплікації $A\Rightarrow B$ використовується $A$ як необхідна умова виведення. Використовується для встановлення існування висновків і доведень без їх побудови. Вперше явно сформулював і довів 1930 року Ербран, а без доведення використовував її 1928 року. Незалежно цей принцип сформулював 1930 року Тарський. За повідомленням Тарського, він знав і застосовував цей принцип ще 1921 рокуШаблон:Sfn.

Формулювання для числення висловлень

1. Якщо $A⊢B$, то $⊢A\Rightarrow B$.
2. Якщо $A_1,...,A_{m-1},A_m⊢B$, то $A_1,...,A_{m-1}⊢A_m\Rightarrow B$.

Тут $A,B,A_1,...,A_{m-1},A_m$ — логічні формули (формальної теорії $L$ для числення висловлень), $A⊢B$ означає, що формула $B$ виводиться з формули $A$ (в теорії $L$), а $⊢B$ означає, що формулу $B$ доведено (є теоремою теорії $L$). Знак $A\Rightarrow B$ означає логічну операцію імплікації.

Формулювання для теорій першого порядку

Нехай $\mathrm{\Gamma }$ — підмножина (можливо порожня) формул деякої теорії першого порядку $K$, $A$ і $B$ — формули теорії $K$. Тоді, якщо існує таке виведення формули $B$ зі множини формул $\mathrm{\Gamma }\cup \{A\}$, в якому ні при якому застосуванні Шаблон:Не перекладено до формул, залежних у цьому виведенні від формули $A$, не зв'язується жодна з вільних змінних формули $A$, то $\mathrm{\Gamma }⊢A\Rightarrow B$.

Див. також

• Теорема Ербрана

Література

• Шаблон:КнигаШаблон:Бібліоінформація