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

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

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

1. Если $A⊢<!--\; ⊢\; -->B$$A \vdash B$ , то $⊢<!--\; ⊢\; -->A\Rightarrow <!--\; \Rightarrow \; -->B$$\vdash A\Rightarrow B$ .
2. Если $A_1,...,A_{m-<!--\; -\; -->1},A_m⊢<!--\; ⊢\; -->B$$A_{1},...,A_{m-1},A_{m}\vdash B$ , то $A_1,...,A_{m-<!--\; -\; -->1}⊢<!--\; ⊢\; -->A_m\Rightarrow <!--\; \Rightarrow \; -->B$$A_{1},...,A_{m-1}\vdash A_{m}\Rightarrow B$ .

Здесь $A,B,A_1,...,A_{m-<!--\; -\; -->1},A_m$$A,B,A_{1},...,A_{m-1},A_{m}$  — логические формулы (формальной теории $L$$L$  для исчисления высказываний), $A⊢<!--\; ⊢\; -->B$$A \vdash B$  означает, что формула $B$$B$  выводится из формулы $A$$A$  (в теории $L$$L$ ), а $⊢<!--\; ⊢\; -->B$$\vdash B$  означает, что формула $B$$B$  доказуема (является теоремой теории $L$$L$ ). Знак $A\Rightarrow <!--\; \Rightarrow \; -->B$$A\Rightarrow B$  означает логическую операцию импликации.

Формулировка для теорий первого порядкаПравить

Пусть $\mathrm{\Gamma <!--\; \Gamma \; -->}$$\Gamma$  — подмножество (возможно пустое) формул некоторой теории первого порядка $K$$K$ , $A$$A$  и $B$$B$  — формулы теории $K$$K$ . Тогда если существует такой вывод формулы $B$$B$  из множества формул $\mathrm{\Gamma <!--\; \Gamma \; -->}\cup <!--\; \cup \; -->\{A\}$$\Gamma \cup \{A\}$ , в котором ни при каком применении правила обобщения^[en] к формулам, зависящим в этом выводе от формулы $A$$A$ , не связывается ни одна из свободных переменных формулы $A$$A$ , то $\mathrm{\Gamma <!--\; \Gamma \; -->}⊢<!--\; ⊢\; -->A\Rightarrow <!--\; \Rightarrow \; -->B$$\Gamma \vdash A\Rightarrow B$ .

См. такжеПравить

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

ЛитератураПравить

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