$scheme\ Extensionality$

以下は,集合$X,Y$と関係式$P$について

$$(\forall x)(x \in X1 \Leftrightarrow P[x])\ and \ (\forall x)(x \in X2 \Leftrightarrow P[x]))$$

が成り立つとき,

$$X=Y$$

が成り立つことを表す$scheme$(公理図式)です。

scheme Extensionality { X,Y() -> set, P[set] } :
  X() = Y() provided
A1:  for x holds x in X() iff P[x] and
A2:  for x holds x in Y() iff P[x]
  proof
A3:  x in X() implies x in Y()
     proof assume x in X(); then P[x] by A1; hence x in Y() by A2; end;
    x in Y() implies x in X()
     proof assume x in Y(); then P[x] by A2; hence x in X() by A1; end;
   hence thesis by TARSKI:2,A3;
  end;

証明は,

$$A1: (\forall x)(x \in X1 \Leftrightarrow P[x])$$

$$A2: (\forall x)(x \in X2 \Leftrightarrow P[x])$$

を仮定すれば,

$$\begin{eqnarray*} &&x \in X \Rightarrow P[x] \\ &&P[x] \Rightarrow x \in Y \end{eqnarray*}$$

によって,

$$A3: x \in X \Rightarrow x \in Y$$

が成り立ち,同様に,

$$\begin{eqnarray*} &&x \in Y \Rightarrow P[x] \\ &&P[x] \Rightarrow x \in X \end{eqnarray*}$$

によって,

$$x \in Y \Rightarrow x \in X$$

が成り立つことが示され,これと,$TARSKI:2$及び$A3$から,証明終了です。