About: 演繹定理

演繹定理（英: Deduction theorem）とは、数理論理学において、論理式 E から 論理式 F が演繹可能ならば、含意 E → F が証明可能である（すなわち、空集合から演繹可能）、というもの。記号的に表すと、 ならば、 である。 演繹定理は、以下のように任意個の有限な前提論理式群に一般化できる。 から が推論でき、最終的に となる。 演繹定理はである。つまり、理論自身の定理ではないが、その理論における演繹的証明に使われる。 演繹メタ定理は、メタ定理の中でも最も重要である。論理体系のなかには、これを推論規則（"→" の導入規則）として採用したもの（自然演繹）もある。そうでない体系でも、公理群から演繹定理を証明することでその論理体系が完全であることを示すのが一般的である。で何かを証明する場合、演繹メタ定理なしでは証明が困難となる。逆に演繹メタ定理を使えば、証明は非常に簡単になる。