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

Теорема о дедукции (лемма о дедукции, теорема дедукции) — один из фундаментальных результатов в теории доказательств, формализует способ рассуждения, при котором для установления импликации $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\}$ , в котором ни при каком применении правила обобщения к формулам, зависящим в этом выводе от формулы $A$ , не связывается ни одна из свободных переменных формулы $A$ , то $\Gamma \vdash A\Rightarrow B$ .

См. также

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

Примечания

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

Литература

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

This article is issued from Wikipedia. The text is licensed under Creative Commons - Attribution - Sharealike. Additional terms may apply for the media files.

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