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

第1節 関係式と論理変数

目次


第1節 関係式と論理変数

第2節 定理と証明の形

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

 第4節 環境部notation,contructors

第5節  環境部残り部分

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


テスト

Logをみる

Back
 

第1章 論理式と証明の構造 第1節 関係式と論理変数

 高校の数学の教科書では次のような文脈が見られます。

(x-a)(x+a)=0

 よって

 x=a または x=-a

 ここにおける (x-a)(x+a)=0 や x=a や x=-a は数式ですが、真か偽かが 決まるもので、「関係式」、とも言われます。それらは論理学で勉強した、「論理変数」で表せます。従って上の3行は

A imp B or C

という論理式で書けます。この論理式を変形していっても、「True」にはなりませんね。つまり高校では当たり前の文脈も、論理的にはそのままでは明らかでないものがあります(前提となる知識が必要!)。

 しかし中には論理的にも正しいものがあります。

例1 次の文脈は論理的に正しいか(x^n はxのn乗。以下同じ)?

 「x^2 = 1 となる条件は x=1 または x=-1 となることである。

よって x^3 = 1 かつ x^2 =1 ならば x=1 または x=-1 である」。

解)各関係式を次のように論理変数で表す。

   A: x^2 = 1
   B: x=1
   C: x=-1
   D: x^3 = 1

 すると問題の文脈は

   (A imp B or C) imp (A and D imp B or C)

となる。これは

   = not((not A)or B or C)or (not(A and D) or (B or C))
   = A and not B and not C or not A or not D or B or C
   = A and not B and not C or not(A and not B and not C) or not D
   = True or not D
   = True

と変形でき、最後は恒真命題True になるので、論理的に正しい。

例2 次の文脈は論理的に正しいか?

 「x^2 = 1 となる条件は x=1 または x=-1 となることである。よって x^2=1 かつ x ≧ 0 ならば x=1 である」。

解)A,B,C を例1と同じとし、

  E: x ≧ 0

とする。ならば問題の文脈は

   (A imp B or C) imp (A and E imp B)

となる。これは変形してゆくと

  = (not A or B or C) imp (not(A and E) or B)
  = not(not A or B or C) or (not(A and E) or B)
  = A and not B and not C or not A or not E or B
  = not B and not C or not A or not E or B  (A and F or not A=F or not A より)
  = not B and not C or B or not A or not E
  = not C or B or not A or not E

最後の式は C=True, B=False, A=True, E=True のときFalse になるので、恒真命題ではない。よって論理的には正しくない。

例2において 「x=-1 imp not x≧0」という命題を付け加えれば論理的に正しくなります。つまり直感的に正しいと思われる文脈でもその背後には前提となるいくつもの命題が隠されていることが多いのです。