演繹メタ定理を使った証明から公理的証明への変換

ウィキペディア小見出し辞書

演繹メタ定理を使った証明から公理的証明への変換

出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2019/10/07 10:04 UTC 版)

「演繹定理」の記事における「演繹メタ定理を使った証明から公理的証明への変換」の解説

公理的命題論理では、公理図式として次のものを使うのが一般的である（ここで、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 に対応する。