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

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

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

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

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

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

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

Див. також

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

Література

• Клини С. К. Математическая логика. — М. : Мир, 1973. — 480 с.