情報証明論 第3章 述語論理式と証明

第1節 全称記号の付いた式と証明

目次


第1節 全称記号の付いた式と証明

第2節 存在記号の付いた式と証明


テスト

Logをみる

Back
 

第3章 述語論理式と証明 第1節 全称記号の付いた式と証明

 (∀x)f(x)

 という全称記号∀が入った式はMizarでは

   for x holds f(x)

と書きます。また

  (∀x)(f(x) imp g(x))

という式は

  for x st f(x) holds g(x)

と書きます。これはまた

  for x holds f(x) implies g(x)

とも同等です。

 また変数x の型が宣言されていないときは、

  for x being set st f(x) holds g(x)

などと書きます。

 全称記号の式を証明するときは、

for x being set st f(x) holds g(x)
proof
 let x be set;
 assume f(x);
....
....
 hence g(x);
end;
のようになります。証明中では、 for x が let x に変わります。being set が

be set に変わります。結論はhence または thus のついた式です。

 なお、前章では全称記号の付いていない場合を示しましたが、見かけは全称記号が付いていなくても、本当は付いている、という場合があります。

 例えば、

reserve x for set;
theorem f(x) implies g(x);
というような定理は上の全称記号の付いた定理と同じなのです。このように全称記号を省略する場合もありますので注意してください。省略された場合の証明には、let x の部分は付けません。

 証明中で、now で始まるブロックが現れることがあります。例えば、

B1: now let x be set;
 assume f(x);
....
....
 hence g(x);
end;

このようなブロックはend で終わります。このときラベルB1 が now の前に付いていますが、このラベルB1 を後の方で引用すると、この引用は

B1: for x being set st f(x) holds g(x);

という式の引用と同じなのです。now は次のように、証明中にまた全称記号が付いた式を証明しなければいけないようなときに使います。

for y being set holds for x being set st x c= y & y c= x holds x=y
proof let y be set;
 now let x be set;
  assume x c= y & y c= x;
  hence x=y by XBOOLE_0:def 10;
 end;
 hence thesis;
end;
あるいは、thus+now は hereby という言葉で置き換えられるので、

for y being set holds for x being set st x c= y & y c= x holds x=y
proof let y be set;
 hereby let x be set;
  assume x c= y & y c= x;
  hence x=y by XBOOLE_0:def 10;
 end;
end;
としてもいいのです。

注) 実は述語論理的には

for y being set holds for x being set st x c= y & y c= x holds x=y

for x,y being set st x c= y & y c= x holds x=y

と同値なので、

for y being set holds for x being set st x c= y & y c= x holds x=y
 by XBOOLE_0:def 10;

と特別証明を付けなくても自明なのですが...