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

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

目次


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

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


テスト

Logをみる

Back
 

第3章 述語論理式と証明 第2節 存在記号の付いた式と証明

 (∃x)f(x)

 という存在記号∃が入った式はMizarでは

   ex x st f(x)

と書きます。

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

  ex x being set st f(x)

などと書きます。

 存在記号の付いた式の証明はいろいろ可能です。

例 ex x being set st for y being set holds not y in x 
  proof
    take {};
    for y being set holds not y in {} by XBOOLE_0:def 1;
   hence thesis;
  end;

ここにおけるtakeの使い方はMizar講義録にあります。

あるいは、

ex x being set st for y being set holds not y in x
  proof
    for y being set holds not y in {} by XBOOLE_0:def 1;
   hence thesis;
  end;
でもいいのです。ここでの要点は存在するものを具体的に示したことです。つまり

x={}

とすると for y being set holds not y in x なる式を満たす、ということを示すことで証明は終わります。