演繹定理のソースを表示

'''演繹定理'''（えんえきていり、[[英語|英]]: '''Deduction theorem'''）とは、[[数理論理学]]において、論理式 E から 論理式 F が[[演繹]]可能ならば、[[論理包含|含意]] E → F が証明可能である（すなわち、空集合から演繹可能）、というもの。記号的に表すと、<math> E \vdash F </math> ならば、<math> \vdash E \rightarrow F </math> である。

演繹定理は、以下のように任意個の有限な前提論理式群に一般化できる。

<math> E_1, E_2, ... , E_{n-1}, E_n \vdash F </math> から
<math> E_1, E_2, ... , E_{n-1} \vdash E_n \rightarrow F </math> が推論でき、最終的に

<math> \vdash E_1\rightarrow(...(E_{n-1} \rightarrow (E_n \rightarrow F))...) </math> となる。

演繹定理は[[メタ定理]]である。つまり、理論自身の定理ではないが、その理論における演繹的証明に使われる。

演繹メタ定理は、メタ定理の中でも最も重要である。論理体系のなかには、これを推論規則（"→" の導入規則）として採用したもの（[[自然演繹]]）もある。そうでない体系でも、[[公理]]群から演繹定理を証明することでその論理体系が完全であることを示すのが一般的である。{{仮リンク|ヒルベルト流の体系|en|Hilbert_system}}で何かを証明する場合、演繹メタ定理なしでは証明が困難となる。逆に演繹メタ定理を使えば、証明は非常に簡単になる。

== 演繹の例 ==
「証明」 公理 1:
**''P'' 　1. 仮説
***''Q'' 　2. 仮説
***''P'' 　3. 1 の反復
**''Q''→''P'' 　4. 2 から 3 への演繹
*''P''→(''Q''→''P'') 　5. 1 から 4 への演繹 QED

「証明」 公理 2:
**''P''→(''Q''→''R'') 　1. 仮説
***''P''→''Q'' 　2. 仮説
****''P'' 　3. 仮説
****''Q'' 　4. 3と2による[[モーダスポネンス]]
****''Q''→''R'' 　5. 3と1によるモーダスポネンス
****''R'' 　6. 4と5によるモーダスポネンス
***''P''→''R'' 　7. 3から6への演繹
**(''P''→''Q'')→(''P''→''R'') 　8. 2から7への演繹
*(''P''→(''Q''→''R''))→((''P''→''Q'')→(''P''→''R'')) 　9. 1から8への演繹 QED

公理 1 を使って ((''P''→(''Q''→''P''))→''R'')→''R'' を示す:
**(''P''→(''Q''→''P''))→''R'' 　1. 仮説
**''P''→(''Q''→''P'') 　2. 公理 1
**''R'' 　3. 2と1によるモーダスポネンス
*((''P''→(''Q''→''P''))→''R'')→''R'' 　4. 1から3への演繹 QED

== 推論の仮想規則 ==
上記例では、3種類の仮想的（あるいは補助的かつ一時的）推論規則が通常の公理的論理に追加されている。それは、「仮説」、「反復」、「演繹」である。通常の推論規則（すなわち、「モーダスポネンス」などの各種公理）も有効である。

1. '''仮説'''とは、既にある前提に追加の前提を加えることである。したがって、前のステップ ''S'' が次のように演繹されたとする。
:<math> E_1, E_2, ... , E_{n-1}, E_n \vdash S </math>

そして、ここに新たな前提 ''H'' を加えると次のようになる。
:<math> E_1, E_2, ... , E_{n-1}, E_n, H \vdash H </math>

これを記号的に表すと、n番目のインデントからn+1番目のインデントになり、次のように表される。
**''S'' 前のステップ
***''H'' 仮説

2. '''反復'''とは、既出のステップを再利用することである。これは、直前の仮説でない既出の仮説を改めて示し、それを演繹の前ステップとして使う場合のみ必要となる。

3. '''演繹'''とは、直前の仮説を取り去り、それ以前のステップに前置することである。このとき、インデントが一段階戻される。
***''H'' 仮説
***......... （他のステップ）
***''C'' （''H'' から導きだされた結論）
**''H''→''C'' 演繹

== 演繹メタ定理を使った証明から公理的証明への変換 ==
公理的命題論理では、[[公理図式]]として次のものを使うのが一般的である（ここで、''P''、''Q''、''R'' は任意の命題）。
*公理 1 : ''P''→(''Q''→''P'')
*公理 2 : (''P''→(''Q''→''R''))→((''P''→''Q'')→(''P''→''R''))
*モーダスポネンス : ''P'' と ''P''→''Q'' から ''Q'' を推論する。
これらの公理から明らかに定理 ''P''→''P'' が得られる（[[命題論理]]参照）。簡単のため、定理 ''P''→''P'' も公理図式として採用することにする。これらの公理図式は、演繹定理が容易に導けるように選ばれている。従って、論点をはぐらかしているように見えるかもしれない。しかし、真理値表を使ってそれが[[恒真式]]であることを検証し、モーダスポネンスが妥当な推論であることを確認することで正当であることが確認できる。この体系は[[直観主義論理|直観主義命題論理]]の含意断片の完全な証明計算体系である。以下の議論はこの体系より強い任意の体系（例えば[[古典論理|古典命題論理]]）に対して適用できる。

ここで、Γと ''H'' から ''C'' を証明できるとき、Γから ''H''→''C'' を証明できることを示したいとする。Γ（反復ステップ）または公理における前提である演繹の各ステップ ''S'' について、公理1 ''S''→(''H''→''S'') にモーダスポネンスを適用でき、''H''→''S'' が得られる。ステップが ''H'' 自身（仮説ステップ）なら、公理図式を適用して ''H''→''H'' が得られる。ステップが ''A'' と ''A''→''S'' へのモーダスポネンスの適用結果であるとき、まずそれら前提が ''H''→''A'' と ''H''→(''A''→''S'') に変換できることを示してから、公理2 (''H''→(''A''→''S''))→((''H''→''A'')→(''H''→''S'')) を使い、モーダスポネンスを適用して (''H''→''A'')→(''H''→''S'') を得て、最終的に ''H''→''S'' を得る。最終的に ''H'' を前提とせず Γ だけを前提として、結論である ''H''→''C'' が得られる。これで演繹ステップは証明過程から払拭され、''H'' から導き出された結論であった事前ステップに統合される。

証明の複雑さを軽減するため、変換前に一種の前処理をすべきである。結論以外の任意のステップで ''H'' に実際には依存していないものは、仮説ステップの前に移動させ、インデントを1つ戻す。そして、他の不必要なステップ（結論を得るまでの過程で使われていないステップ）は除去すべきである（結論ではない反復など）。

変換において、モーダスポネンスの公理1への適用結果を演繹の初め（''H''→''H'' ステップの直後）に配置すると便利かもしれない。

モーダスポネンスを変換する場合、''A'' が ''H'' のスコープ外であるなら、公理1 ''A''→(''H''→''A'') を適用する必要があり、さらにモーダスポネンスを適用して ''H''→''A'' を得る。同様に、''A''→''S'' が ''H'' のスコープ外であるなら、公理1 (''A''→''S'')→(''H''→(''A''→''S'')) を適用し、モーダスポネンスを適用して ''H''→(''A''→''S'') を得る。モーダスポネンスが結論の場合以外は、これらを両方必要とするべきではない。なぜなら、両方がスコープ外なら、モーダスポネンスも ''H'' の前に移動でき、それもまたスコープ外になるからである。

[[カリー・ハワード対応]]では、上述の演繹メタ定理についての変換過程は、[[ラムダ計算]]の項から[[組合せ論理]]の項への変換に類似している。ここで、公理1がKコンビネータに対応し、公理2がSコンビネータに対応する。Iコンビネータは公理 ''A''→''A'' に対応する。

== 変換の例 ==
[[自然演繹]]を公理的証明形式に変換する過程を示すため、恒真式 ''Q''→((''Q''→''R'')→''R'') を使用する。変換が可能であることを見るには、これで十分である。これをまず自然演繹で証明し、それをもっと長い公理的証明に変換する。

第一に、[[自然演繹]]的手法で証明を書く。
**''Q'' 　1. 仮説
***''Q''→''R'' 　2. 仮説
***''R'' 　3. 1,2によるモーダスポネンス
**(''Q''→''R'')→''R'' 　4. 2から3への演繹
*''Q''→((''Q''→''R'')→''R'') 　5. 1から4への演繹 QED

第二に、内側の演繹を公理的証明に変換する。
*(''Q''→''R'')→(''Q''→''R'') 　1. 公理図式 (''A''→''A'')
*((''Q''→''R'')→(''Q''→''R''))→(((''Q''→''R'')→''Q'')→((''Q''→''R'')→''R'')) 　2. 公理 2
*((''Q''→''R'')→''Q'')→((''Q''→''R'')→''R'') 　3. 1,2によるモーダスポネンス
*''Q''→((''Q''→''R'')→''Q'') 　4. 公理 1
**''Q'' 　5. 仮説
**(''Q''→''R'')→''Q'' 　6. 5,4によるモーダスポネンス
**(''Q''→''R'')→''R'' 　7. 6,3によるモーダスポネンス
*''Q''→((''Q''→''R'')→''R'') 　8. 5から7への演繹 QED

第三に、外側の演繹を公理的証明に変換する。
*(''Q''→''R'')→(''Q''→''R'') 　1. 公理図式 (''A''→''A'')
*((''Q''→''R'')→(''Q''→''R''))→(((''Q''→''R'')→''Q'')→((''Q''→''R'')→''R'')) 　2. 公理 2
*((''Q''→''R'')→''Q'')→((''Q''→''R'')→''R'') 　3. 1,2によるモーダスポネンス
*''Q''→((''Q''→''R'')→''Q'') 　4. 公理 1
*[((''Q''→''R'')→''Q'')→((''Q''→''R'')→''R'')]→[''Q''→(((''Q''→''R'')→''Q'')→((''Q''→''R'')→''R''))] 　5. 公理 1
*''Q''→(((''Q''→''R'')→''Q'')→((''Q''→''R'')→''R'')) 　6. 3,5によるモーダスポネンス
*[''Q''→(((''Q''→''R'')→''Q'')→((''Q''→''R'')→''R''))]→([''Q''→((''Q''→''R'')→''Q'')]→[''Q''→((''Q''→''R'')→''R''))]) 　7. 公理 2
*[''Q''→((''Q''→''R'')→''Q'')]→[''Q''→((''Q''→''R'')→''R''))] 　8. 6,7によるモーダスポネンス
*''Q''→((''Q''→''R'')→''R'')) 　9. 4,8によるモーダスポネンス QED

この三段階は[[カリー・ハワード対応]]を使えば次のように簡潔に表せる。
*第一に、ラムダ計算において、関数 f = λa. λb. b a は、型 ''q'' → (''q'' → ''r'') → ''r'' を持つ。
*第二に、b についてラムダ除去すると f = λa. s i (k a)
*第三に、a についてラムダ除去すると f = s (k (s i)) k

== 帰納定理 ==
'''帰納定理'''（'''Resolution theorem'''）は、演繹定理の[[逆]]である。含意の除去規則である[[モーダスポネンス]]から即座に導ける。

== 関連項目 ==
*[[命題論理]]

== 参考文献 ==
{{参照方法|date=2023年8月}}
* [http://www.ltn.lv/~podnieks/mlog/ml.htm ''Introduction to Mathematical Logic'' by Vilnis Detlovs and Karlis Podnieks]  
* [http://schubert.cs.shinshu-u.ac.jp/~miyao/UD/Subjects/Kouri/node20.html 演繹定理] 師玉康成

{{デフォルトソート:えんえきていり}}
[[Category:演繹|ていり]]
[[Category:論理学]]
[[Category:数学基礎論の定理]]
[[Category:メタ定理]]
[[Category:数学に関する記事]]