Теорема о дедукции

Теорема о дедукции (лемма о дедукции, теорема дедукции) — один из фундаментальных результатов в теории доказательств, формализует способ рассуждения, при котором для установления импликации ${\displaystyle A\Rightarrow B}$ используется ${\displaystyle A}$ в качестве необходимого условия вывода. Используется для установления существования выводов и доказательств, не используя их построения. Впервые была явно сформулирована и доказана в 1930 году Эрбраном, а без доказательств использовалась Эрбраном в 1928 году. Независимо этот принцип был сформулирован Тарским в 1930 году. По сообщению Тарского, он знал и применял этот принцип еще в 1921 году^[1].

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\}}$, в котором ни при каком применении правила обобщения^[англ.] к формулам, зависящим в этом выводе от формулы ${\displaystyle A}$, не связывается ни одна из свободных переменных формулы ${\displaystyle A}$, то ${\displaystyle \Gamma \vdash A\Rightarrow B}$.

• Теоремы Эрбрана

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