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

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

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

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

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

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

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

Див. також

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

Примітки

1. Математическая логика, 1973, с. 54-55.

Література

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