分出公理

前述した選出の公理 $scheme \ Fraenkel$を使って, 任意の集合$A$と関係式$P[x]$から,$A$の要素であって,関係式$P[x]$ が成り立つ$x$全体の集合

$$\{x\vert x \in A \ and\ P[x] \}$$

を構成するための公理図式(分出公理)が書かれています。

scheme Separation { A()-> set, P[set] } :
   ex X being set st for x being set 
   holds x in X iff x in A() & P[x]
 proof
A1: for x,y,z st x = y & P[y] & x = z & P[z] holds y = z;
   consider X such that
A2: for x holds x in X iff ex y st y in A() & y = x 
& P[x] from Fraenkel(A1);
  take X;
  let x;
   x in X iff ex y st y in A() & y = x & P[x] by A2;
  hence thesis;
 end;

まず,

scheme Separation { A()-> set, P[set] } :

で,この公理図式の名前が$Separation$であり,任意の集合$A$と 関係式$P[ \cdot ]$についての公理図式であることが宣言されています。 次に,その公理図式の中身

   ex X being set st for x being set holds x in X iff x in A() & P[x]

で,

$$(\exists X)(\forall x )(x \in X \Leftrightarrow x \in A \ and \ P[x])$$

すなわち, 「任意の$x$について,$x$が$X$の要素であることと, $x$が集合$A$の要素であって,かつ,関係式$P[x]$を充たすことが 同値である集合$X$が存在する」ことが書かれています。 以下は,その証明が書かれています。

 proof
A1: for x,y,z st x = y & P[y] & x = z & P[z] 
holds y = z;
   consider X such that
A2: for x holds x in X iff ex y st y in A() & y = x 
& P[x] from Fraenkel(A1);
  take X;
  let x;
   x in X iff ex y st y in A() & y = x & P[x] by A2;
  hence thesis;
 end;

$$x = y \ and \ P[y]$$

という関係式を$Q[x,y]$で置き換えてみると判りやすいでしょう。

$$A1: (\forall x,y,z)( (Q[x,y] \ and \ Q[x,z]) \Rightarrow \ (y = z))$$

すると,$A1$から公理図式$Fraenkel$によって

$$A2: (\forall x )( x \in X \Leftrightarrow (\exists y) (y \in A \ and \ y = x \ and \ P[x] )$$

となる集合$X$が少なくとも一つ存在します。 次の

  take X;

は,この条件を充たす集合$X$を選択する という意味です。次に続く

  let x;
   x in X iff ex y st y in A() & y = x & P[x] by A2;
  hence thesis;

は, $x$を任意にとると,$A2$により

$$x \in X \Leftrightarrow (\exists y)( y \in A \ and \ y = x \ and \ P[x] )$$

が成り立つことを示しています。さらに,

$$(\exists y)( y \in A \ and \ y = x \ and \ P[x] ) \Leftrightarrow x \in A \ and \ P[x]$$

ですが,このような,述語論理の単純な同値変形は$mizar$ システムが自動的に行いますので,

任意の$x$について

$$x \in X \Leftrightarrow x \in A \ and \ P[x]$$

が示されたことになり,証明が終了したことを示す。

  hence thesis

が書かれます。