演繹定理
演繹定理(えんえきていり、英: Deduction theorem)とは、数理論理学において、論理式 E から 論理式 F が演繹可能ならば、含意 E → F が証明可能である(すなわち、空集合から演繹可能)、というもの。記号的に表すと、 E ⊢ F {\displaystyle E\vdash F} ならば、 ⊢ E → F {\displaystyle \vdash E\rightarrow F} である。
演繹定理は、以下のように任意個の有限な前提論理式群に一般化できる。
E 1 , E 2 , . . . , E n − 1 , E n ⊢ F {\displaystyle E_{1},E_{2},...,E_{n-1},E_{n}\vdash F} から E 1 , E 2 , . . . , E n − 1 ⊢ E n → F {\displaystyle E_{1},E_{2},...,E_{n-1}\vdash E_{n}\rightarrow F} が推論でき、最終的に
上記例では、3種類の仮想的(あるいは補助的かつ一時的)推論規則が通常の公理的論理に追加されている。それは、「仮説」、「反復」、「演繹」である。通常の推論規則(すなわち、「モーダスポネンス」などの各種公理)も有効である。
1. 仮説とは、既にある前提に追加の前提を加えることである。したがって、前のステップ S が次のように演繹されたとする。
E 1 , E 2 , . . . , E n − 1 , E n ⊢ S {\displaystyle E_{1},E_{2},...,E_{n-1},E_{n}\vdash S}
そして、ここに新たな前提 H を加えると次のようになる。
E 1 , E 2 , . . . , E n − 1 , E n , H ⊢ H {\displaystyle E_{1},E_{2},...,E_{n-1},E_{n},H\vdash H}
これを記号的に表すと、n番目のインデントからn+1番目のインデントになり、次のように表される。
S 前のステップ H 仮説
2. 反復とは、既出のステップを再利用することである。これは、直前の仮説でない既出の仮説を改めて示し、それを演繹の前ステップとして使う場合のみ必要となる。
3. 演繹とは、直前の仮説を取り去り、それ以前のステップに前置することである。このとき、インデントが一段階戻される。
H 仮説 ......... (他のステップ) C (H から導きだされた結論) H→C 演繹