目次

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

テスト

Logをみる

Back
　

　（∃x）f(x)

　という存在記号∃が入った式はＭｉｚａｒでは

　　　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の使い方はＭｉｚａｒ講義録にあります。

あるいは、

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　なる式を満たす、ということを示すことで証明は終わります。