Теорема о дедукции
Теорема о дедукции (лемма о дедукции, теорема дедукции) — один из фундаментальных результатов в теории доказательств, формализует способ рассуждения, при котором для установления импликации используется в качестве необходимого условия вывода. Используется для установления существования выводов и доказательств, не используя их построения. Впервые была явно сформулирована и доказана в 1930 году Эрбраном, а без доказательств использовалась Эрбраном в 1928 году. Независимо этот принцип был сформулирован Тарским в 1930 году. По сообщению Тарского, он знал и применял этот принцип еще в 1921 году[1].
Формулировка для исчисления высказываний
[править | править код]- Если , то .
- Если , то .
Здесь — логические формулы (формальной теории для исчисления высказываний), означает, что формула выводится из формулы (в теории ), а означает, что формула доказуема (является теоремой теории ). Знак означает логическую операцию импликации.
Формулировка для теорий первого порядка
[править | править код]Пусть — подмножество (возможно пустое) формул некоторой теории первого порядка , и — формулы теории . Тогда если существует такой вывод формулы из множества формул , в котором ни при каком применении правила обобщения[англ.] к формулам, зависящим в этом выводе от формулы , не связывается ни одна из свободных переменных формулы , то .
См. также
[править | править код]Примечания
[править | править код]- ↑ Математическая логика, 1973, с. 54-55.
Литература
[править | править код]- Клини С. К. Математическая логика. — М.: Мир, 1973. — 480 с.