集合の等号 = の再定義

以下は,既に$TARSKI:2$で定義されている,２つの集合 $X,Y$についての等号関係$X=Y$を

$$(X \subseteq Y)\ and \ (Y \subseteq X)$$

が成り立つことという述語として再定義しています。

 redefine pred X = Y means
  X c= Y & Y c= X;
  compatibility
   proof
    thus X = Y implies X c= Y & Y c= X;
    assume  X c= Y & Y c= X;
     then for x holds x in X iff x in Y by TARSKI:def 3;
    hence X = Y by TARSKI:2;
   end;
end;

 redefine

は再定義の宣言です。

  compatibility

以下は,この再定義が,$TARSKI:2$での定義と 矛盾しないこと(替えることができること)の証明です。 まず,

$$X = Y \Rightarrow (X \subseteq Y)\ and \ (Y \subseteq= X)$$

は自明です。(左辺の$=$は$TARSKI:2$の定義での等号です。) 逆に,

$$(X \subseteq Y) \ and \ (Y \subseteq = X)$$

を仮定すると,$TARSKI:def 3$により,

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

従って,$TARSKI:2$により

$$X=Y$$

が成り立ちます。