変換の例

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

変換の例

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

「演繹定理」の記事における「変換の例」の解説

自然演繹を公理的証明形式に変換する過程を示すため、恒真式 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. 公理 1Q 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