Введение

Метатеорема в математической логикеВ математической логике теорема о дедукции — это метатеорема, обосновывающая доказательство условных утверждений из гипотезы в системах, которые не аксиоматизируют эту гипотезу явно, то есть для доказательства импликации A → B достаточно предположить A как гипотезу и затем вывести B. Теоремы о дедукции существуют как для пропозициональной, так и для логики первого порядка. Теорема о дедукции является важным инструментом в системах дедукции в стиле Гильберта, поскольку она позволяет строить более понятные и, как правило, значительно более короткие доказательства, чем без неё. В некоторых других формальных системах доказательств такое же удобство обеспечивается явным правилом вывода; например, в естественной дедукции это называется введением импликации. Более конкретно, теорема о дедукции для пропозициональной логики утверждает, что если формула выводима из множества предположений Γ, то импликация A → B выводима из Γ; в символах, Γ ⊢ A → B. В частном случае, когда Γ является пустым множеством, утверждение теоремы о дедукции можно записать более компактно: ⊢ A → B. Теорема о дедукции для логики предикатов аналогична, но имеет некоторые дополнительные ограничения (например, они выполняются, если A является замкнутой формулой). В общем случае теорема о дедукции должна учитывать все логические детали рассматриваемой теории, поэтому каждая логическая система технически нуждается в своей собственной теореме о дедукции, хотя различия обычно незначительны. Теорема о дедукции верна для всех теорий первого порядка с обычными дедуктивными системами для логики первого порядка. Однако существуют системы первого порядка, в которых добавляются новые правила вывода, для которых теорема о дедукции не выполняется. Наиболее заметным примером является квантовая логика Бирхоффа — фон Неймана, где линейные подпространства гильбертова пространства образуют нераспределительную решётку.