情報証明論 第1章 論理式と証明の構造

 第2節 定理と証明の形

目次


第1節 関係式と論理変数

第2節 定理と証明の形

第3節 コンピュータによるチェック −環境部vocabulary

 第4節 環境部notation,contructors

第5節  環境部残り部分

   第6節 実際のチェック実行


テスト

Logをみる

Back
 

第1章 論理式と証明の構造 第2節 定理と証明の形

 前節の2つの例によって、論理式と定理の形を説明しましょう。

まず例1のような文脈を定理の形にしてみます。定理や証明の記述はMizarという数学用の言語を用います。http://markun.cs.shinshu-u.ac.jp/mizar/

にその言語についての詳しい説明がありますが、ここではそれほど詳しい知識がなくても理解できるようにしています。


定理の例:

 theorem (x^2 = 1 implies x=1 or x=-1) implies
       (x^3 = 1 & x^2 =1 implies x=1 or x=-1)
 proof assume A1: (x^2 = 1 implies x=1 or x=-1);
  thus x^3 = 1 & x^2 =1 implies x=1 or x=-1
    proof assume x^3 = 1 & x^2 =1;
          hence x=1 or x=-1 by A1;
    end;
 end;

 これを説明します。まずtheorem というのは「定理」のことです。theorem の後には論理命題がきます。implies というのはimp と同じです。Mizar言語では論理式について、CAIの「論理学」で紹介した論理記号と少し異なった書き方をします。

 次に対照表を示します。

         CAI     Mizar
−−−−−−−−−−−−−−−−
     not     not
     and     &
     or      or
     imp     implies
     eqv     iff
     False    contradiction
     True     not contradiction

定理で命題を示した後、それがなぜ言えるのかを、その命題に引き続く証明の部分で示します。その形は

  theorem ... implies ***
  proof
   assume  ...;

   hence  ***;
  end;

のようになります。証明部はproofで始まり、end;で終わります。文の区切りはセミコロンですが、theoremやproofの後には付けません。

 命題「... implies ***」の前提となる命題は...で、結論となる命題は***です。証明部の中では前提となる命題はまずassume をつけて書きます。そして結論はhenceまたはthusを付けて最後の行に書きます(henceはthen+thusの役目をする。thenについては後述)。その2つの命題に挟まれた部分に中間的にいえる命題をいくつか書きます。

 中間的あるいは最終的な命題は、なぜそれがいえるのかをthenまたはbyを使って表します。byを使うときは、それより前に成立を証明したか、成立すると仮定したかの式に付けられた「ラベル label」を引用するときです。

 上の「定理の例」では、

proof assume A1: (x^2 = 1 implies x=1 or x=-1);

の所の A1 が命題 (x^2 = 1 implies x=1 or x=-1) に付けられたラベルです。英字で始まる任意の文字列を使用できます。

  hence x=1 or x=-1 by A1;

の部分にはby が使われ、A1の式が引用されています。この式は

      「従って直前の式とA1式より、結論としてx=1 or x=-1 がいえる」

ということを表しています。

 henceは「直前の式より、結論として」という意味があります。thenというのが「直前の式より」という意味です。thusというのが「結論として」という意味です。従ってhence=then+thusと覚えてください。

 定理の例の中で

 thus x^3 = 1 and x^2 =1 implies x=1 or x=-1
    proof assume x^3 = 1 and x^2 =1;
          hence x=1 or x=-1 by A1;
    end;

の部分は少し説明を要します。この定理は「...implies ***」の形が何度も使われています。このような形自体が結論になっています。そのようなとき、

 x^3 = 1 and x^2 =1 implies x=1 or x=-1

なる式が一応結論なので前にthus を付けておきます。しかし、この式自体に証明部を付けて、成立の理由を言いたいとします。そのときこの式がまた一つの定理のように思って証明部を付けていいのです。即ちproofで始まりend;で終わる、ということや、最終式にはthusまたはhenceを付ける、というルールは、定理の場合の証明部のルールと同じなのです。

 このような場合、

  hence x^3 = 1 & x^2 =1 implies x=1 or x=-1

proof assume x^3 = 1 & x^2 =1; hence x=1 or x=-1 by A1; end;

とは書きません。thusは使いますが、henceは使いません。それは、もし直前の式を使うなら、証明部の中で使う、というルールがあるためです。