このテキストは，集合論を題材に，mizar を使った，数学定理の記述が，実際にどのようになされているかを説明します。 mizar では，その数学記述言語によって書かれたテキストを articles と称します。 mizar システムやそれで使われる数学記述言語の文法については，中村八束教授著の mizar 講義録第３版 http://markun.cs.shinshu-u.ac.jp/kiso/projects2/proofchecker/mizar/Mizar-J/Miz-tit.html に説明されています。 また，PC 用の mizar システムのダウンロード，WEB 上で使用できる mizar システムは http://markun.cs.shinshu-u.ac.jp/kiso/projects2/proofchecker/mizar/index-j.html にあります。 このテキストでは，mizar で記述された数学定理のデータベースであるライブラリ中の集合論についての，基礎的な article TARSKI.miz, XBOOLl0.miz, XBOOLl1.miz について説明します。

これから TARSKI.miz を読み解いていきます。
まず, 以下の環境部の記述があります。 これは, この article で, 使われる, 用語 (vocabulary) が TARSKI.voc とい うファイルに記述されていることを宣言しています。 次の begin の宣言からこの article の内容の記述が始まります。

reserve はその後に続く, 変数の型がなんであるかを示します。この例では \(x, y, z, u, N, M, X, Y, Z\) は任意の集合 set になっています。集合論では, 取り扱う対象は集合か, そ の要素ですが, 集合も要素も, 形式上は区別されません。ですから'set' とい うのは, 任意の対象を意味しています。

(２つの集合が等しいことの定義)
先ず以下の記述があります。

記号論理で書けば \[ ((\forall x)(x \in X \Leftrightarrow x \in Y)) \Rightarrow X=Y \] です。これは, 外延性の公理として知られるものです。 すなわち，任意の \(x\) に対して, \(x \in X \Leftrightarrow x \in Y\) であるならば, ２つの集合 \(X\), \(Y\) は等しい (すなわち \(X = Y\) である) ことを主張しています。

次の記述は \(x\) 一つだけからなる集合 \(\{x\}\) と \(x\), \(y\) という二つの要素をもつ集合 \(\{x, y\}\) の定義です。

任意の \(y\) に対して \(\{y\}\) とは, 任意の \(x\) について \[ x \in \{y\} \Leftrightarrow x = y \] を満たす集合であり, 任意の \(y\), \(z\) に対して \(\{y, z\}\) とは, 任意の \(x\) について \[ x \in \{y, z\} \Leftrightarrow x = y \lor x = z \] を満たす集合であることを意味します。また、可換性 (commutativity) は \[ \{y, z\} = \{z, y\} \] が成り立つことを表しています。

次は,「集合 \(X\) が集合 \(Y\) の部分集合である」または「集合 \(X\) が集合 \(Y\) に含まれる」という述語の定義を示しています。

任意の \(X\), \(Y\) に対して、 \(X \subseteq Y\) とは、任意の \(x\) に対して \[ x \in X \Rightarrow x \in Y \] が成り立つことをいいます。 また、反射律（reflexivity）とは、任意の \(X\) に対して \[ X \subseteq X \] が成り立つことを表しています。

任意の集合族 (すなわち集合の集合)\(X\) に対して,\(X\) に属する 集合のすべての合弁は、集合族 \(X\) から \(\cup X\) をつくる作用 (functor) として定義されています。

任意の集合族 \(X\) に対して、作用 \(\cup X\) は、次の条件を満たす集合を \(X\) に対応させる操作として定義されます。すなわち、任意の \(x\) に対して \[ x \in \cup X \Leftrightarrow (\exists Y)(x \in Y \land Y \in X). \]

以下は, 証明が省略された定理として, 記述されていますが, 正則性の公理として知られるものです。

記号論理で表すと、任意の集合 \(X\) に対して、 \[ (x \in X) \Rightarrow (\exists Y)(Y \in X \land \neg(\exists x)(x \in X \land x \in Y)) \] という命題になります。

これは \(x\) が集合 \(X\) の要素であれば、集合 \(X\) の要素であって, しかも \(x\) をその要素として含むような \(Y\) は存在しないという主張を表しています。

集合 \(A\) と, 関係式 \(P[x, y]\) から集合 \(X\) を構成する手続きを公理図式 (scheme) として記述したのものが以下です。

任意の集合 \(A\) と、 \[ (\forall x, y, z)\,(P[x, y] \land P[x, z] \Rightarrow y = z) \] が成り立つような関係 \(P\) に対して、ある集合 \(X\) が存在して、 \[ (\forall x)(x \in X \Leftrightarrow (\exists y)(y \in A \land P[y, x])) \] が成り立つことを表しています。

任意の \(x\), \(y\) に対して、集合 \(\{\{x, y\}, \{x\}\}\) を順序対 \([x, y]\) と表します。 これは、\(x\) と \(y\) から順序対 \([x, y]\) を構成する作用 (functor) として定義されます。

以下は2つの集合 \(X\)と\(Y\) の間に双射 (すなわち一対一 かつ上への写像）が存在するとき, 集合(X\)と\(Y\) の濃度が等しい(equipotent) と定義すること表しています。

すなわち, 任意の \(X\), \(Y\) に対して, これらが, 等濃度（equipotent)であるとは \(\exists Z \left\{ \begin{aligned} &\forall x \in X \, \exists y \in Y \, [x, y] \in Z \, \land \\ &\forall y \in Y \, \exists x \in X \, [x, y] \in Z \, \land \\ &\forall x, y, z, u \, \left( [x, y] \in Z \land [z, u] \in Z \right) \implies (x = z \Leftrightarrow y = u) \end{aligned} \right\}\) が成り立つことを言います。

1. 師玉, 康成 “mizarと集合論” 2017年3月25日閲覧