メモ: Z の証明システムを使った証明の方法

      (2010/11/30 作成 by 亀山)
      (2010/12/02 修正 by 高島)
      (2010/12/03 修正 by 高島; コマンド Q? と A! の説明を追加)
      (2010/12/03 修正 by 亀山; pop規則の説明を修正)
      (2010/12/04, 13:45 修正 by 亀山; 最後の Q28証明例で :A, :B と誤
      記していたのを A, B に修正)

(1) 証明の基本構造

目標となる命題の証明を一歩一歩，構成する．
この「一歩」は，論理における「推論規則」に対応し，
Z においては，Proofクラスの method として実現されている．

たとえば，ユーザが (assume :x A) や (andI z :x) と入力すると，システム
は推論規則を1回適用して，それが成功すれば(つまり、その推論規則の適用に
誤りがなければ)適用後に得られる証明を返す．また，その適用の仕方が間違っ
ていると，エラーになる．

(2) 命題を構成する記号の一覧

A, B, C .... 基本命題，あるいは，原始命題
&&      .... 「かつ」 (and)
||      .... 「または」 (or)
=>      .... 「ならば」 (implies)
~~      .... 「。。。でない」 (not)
:false  .... 「矛盾」 (contradiction, false)

命題の例． (A && (B => :false)) ...   (A∧(B⊃⊥)) を表す。
            
(3) 推論規則の一覧

推論規則とは、「いくつかの証明等を受けとり、1つの証明を返す」もの
である。「いくつか」というのは 0個だったり、1個だったり、2個だった
りする。以下の推論規則の説明にあるように、証明以外にも :x や、命題
を受け取ることもある。推論規則が返すものは、(エラーをおこさない
限り必ず)、証明1つである。
 
(assume :x A)  ;; 「仮定」規則を適用する。言い換えると、命題 A を仮定
               ;; して、A を結論とする証明が得られる。この仮定に:x と
	       ;; いう名前をつける．

(andI p1 p2)   ;; 「&&の導入」規則を，証明p1 と証明p2 に適用する．
               ;; p1 の結論が A で，p2 の結論が B のとき，andI を
               ;; 適用すると，(A && B) を結論とする証明が得られる．

(andEL p1)     ;; 「&& の除去-左」規則を，証明p1 に適用する．
               ;; p1 の結論が (A && B) のとき，Aを結論とする
               ;; 証明が得られる．

(andER p1)     ;; 「&& の除去-右」規則を，証明p1 に適用する．
               ;; p1 の結論が (A && B) のとき，Bを結論とする
               ;; 証明が得られる．

(impE p1 p2)   ;; 「=> の除去」規則を，証明p1 と証明p2に適用する．
               ;; p1 の結論が (A => B) で、p2 の結論が A のとき，
               ;; B を結論とする証明が得られる．

(pop)          ;; 「=> の導入」規則を，直前の証明に適用する．
               ;; この規則の前で最後に行った仮定が (assume :x A) で，
               ;; 直前の証明の結論が B のとき，
               ;; (A => B) を結論とする証明が得られる．

(orI (A || B) p1)
               ;; 「|| の導入」規則を，証明p1 に適用する．
               ;; p1 の結論が A あるいは B のとき，
               ;; (A || B)を結論とする証明が得られる．

(orE p1 p2 p3) ;; 「|| の除去」規則を，証明p1, p2, p3 に適用する．
               ;; p1 の結論が (A || B) で，p2 の結論が (A => C)で，
               ;; p3 の結論が (B => C)のとき，C を結論とする証明が得
               ;; られる．

(falseE A p1)  ;; 「⊥の除去」規則を，証明p1 に適用する．
               ;; p1 の結論が :false のとき，A を結論とする証明が
               ;; 得られる．

(notI p1)      ;; 「~~の導入」規則を，証明p1 に適用する．
               ;; p1 の結論が (A => :false) のとき，(~~ A) を結論とす
               ;; る証明が得られる．

(notE p1 p2)   ;; 「~~の除去」規則を，証明p1, p2に適用する．
               ;; p1 の結論が (~~ A) で p2 の結論が A のとき，
               ;; :false を結論とする証明が得られる．


(4) 有用な変数と関数

z             ;; 直前の計算結果(証明など)を保持する変数。

(hyp p1)      ;; 証明 p1 の仮定列 (命題のリスト, hypothesis)を返す．

(ccl p1)      ;; 証明 p1 の結論(conclusion)となる命題を返す．

(proves? p1 h1 f1)
              ;; p1 が「仮定列 h1 のもとでの、命題 f1 の証明」になって
	      ;; いるかどうかを判定する．そうなっているとき、「正解!」
	      ;; と表示される．そうなっていないときは、エラーである。

(Q? n)        ;; 問題 n を表示する。

(A! n p1)     ;; 証明 p1 が 問題 n の解答になっているかを判定する。


(5) 証明の例.

問題 [28] の解答例 (これ以外の解答もある)

;; z1 >
(Q? 28)                   ;; 問題28を表示する．
;;  => "仮定 [(A && B)] のもとで
        (B && A) を証明せよ" : <String>
        
;; z2 >
(assume :x (A && B))      ;; (A && B) を仮定し(その名前を:xとする)
  ;; z2-1 >>
  :x
  ;;  => -- : <Proof> of (A && B)
  
  ;; z2-2 >>
  (andEL :x)              ;; 仮定した (A && B) の A を andEL で取り出す．
                          ;; A の証明が得られる．
  ;;  => -- : <Proof> of A
  
  ;; z2-3 >>
  (set! a z)              ;; 得られた A の証明に a と名前をつける．
                          ;; z はひとつ前の計算の結果を表す．
  ;;  => -- : <Proof> of A
  
  ;; z2-4 >>
  (andER :x)              ;; 同様に andER で B を取り出し，
  ;;  => -- : <Proof> of B
  
  ;; z2-5 >>
  (set! b z)              ;; 証明に b と名前をつける．
  ;;  => -- : <Proof> of B
  
  ;; z2-6 >>
  (andI b a)              ;; andI を使って，既に証明した b と a から (B & A) を証明する．
  ;;  => -- : <Proof> of (B && A)
  
  ;; z2-7 >>
  (A! 28 z)               ;; 証明すべき (B && A) が仮定列 [(A && B)] から得られたので、
                          ;; A! 関数で証明が正しいことを確認する。
  ;;  => "正解!" : <String>
  
  ;; z2-8 >>
  pop                     ;; 最後に (A && B) を仮定した世界から抜ける．
;;  => -- : <Proof> of ((A && B) => (B && A))