PROFILPELAJAR.COM

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

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

Якщо $A\vdash B$ , то $\vdash A\Rightarrow B$ .
Якщо $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\}$ , в якому ні при якому застосуванні правила узагальнення^[en] до формул, залежних у цьому виведенні від формули $A$ , не зв'язується жодна з вільних змінних формули $A$ , то $\Gamma \vdash A\Rightarrow B$ .