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

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

Формулировка для исчисления высказываний

1. Если $A⊢B$, то $⊢A\Rightarrow B$.
2. Если $A_1,\mathrm{...},A_{m-1},A_m⊢B$, то $A_1,\mathrm{...},A_{m-1}⊢A_m\Rightarrow B$.

Здесь $A,B,A_1,\mathrm{...},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\}$, в котором ни при каком применении Шаблон:Iw к формулам, зависящим в этом выводе от формулы $A$, не связывается ни одна из свободных переменных формулы $A$, то $\mathrm{\Gamma }⊢A\Rightarrow B$.

См. также

• Шаблон:D-I

Литература

• Шаблон:Книга