空集合の定義と一意性

definition
  func {} -> set means
:Def1:   not ex x being set st x in it;
  existence
    proof
      consider X;
      consider Y such that
A1:    x in Y iff x in X & contradiction from Separation;
     take Y;
     thus thesis by A1;
    end;
  uniqueness
    proof
     let X,Y; 
     assume (not ex x st x in X) & (not ex x st x in Y);
      then x in Y iff x in X;
     hence thesis by TARSKI:2;
    end;

ここでは,空集合を引数のない作用$\{\}$として定義しています。

definition
  func {} -> set means
:Def1:   not ex x being set st x in it;

がその定義で,

$$not \ (\exists x)(x \in \{\})$$

が成り立つもの,すなわち,それに含まれる要素がない集合として 定義されます。この定義が正しいものとされるためには, このような集合の存在と,それが唯一つに定まっている必要が あります。

  existence

に続く記述がその存在を証明しています。

まず,適当な集合$X$を選び,次に,分出の公理$Separation$ によって,

$$A1:x \in Y \Leftrightarrow x \in X \ and \ contradiction$$

となる集合$Y$を作ります。$contradiction$は記号論理でいう 恒偽命題です。この$Y$を選べば,$\{\}$の条件を充たしますので, 証明終了の記述

     thus thesis by A1;

が書かれます。次に,一意性の証明が続きます。

  uniqueness

に続く記述がその証明です。

$X,Y$を任意の集合として,

     assume (not ex x st x in X) & (not ex x st x in Y);

によって,$X,Y$が共に空集合の条件を充たすこと,すなわち,

$$not (\exists x )( x \in X) \ and \ not (\exists x )( x \in Y)$$

を仮定します。

 then x in Y iff x in X;
     hence thesis by TARSKI:2;

は,その仮定を使うと

$$x \in Y \leftrightarrow x \in X$$

が成り立つことが示されます。最後に$TARSKI$というファイルの 既に証明済みの定理$TARSKI:2$

theorem
 (for x holds x in X iff x in Y) implies X = Y;

$$((\forall x )(x \in X \Leftrightarrow x \in Y) ) \Rightarrow X = Y$$

によって

$$X=Y$$

が示され,証明が終ります。