演繹定理
⊢ E 1 → ( . . . ( E n − 1 → ( E n → F ) ) . . . ) {\displaystyle \vdash E_{1}\rightarrow (...(E_{n-1}\rightarrow (E_{n}\rightarrow F))...)} となる。
演繹定理はメタ定理である。つまり、理論自身の定理ではないが、その理論における演繹的証明に使われる。
演繹メタ定理は、メタ定理の中でも最も重要である。論理体系のなかには、これを推論規則("→" の導入規則)として採用したもの(自然演繹)もある。そうでない体系でも、公理群から演繹定理を証明することでその論理体系が完全であることを示すのが一般的である。ヒルベルト流の体系(英語版)で何かを証明する場合、演繹メタ定理なしでは証明が困難となる。逆に演繹メタ定理を使えば、証明は非常に簡単になる。