このテキストは，集合論を題材に，mizar を使った，数学定理の記述が，実際にどのようになされているかを説明します。 mizar では，その数学記述言語によって書かれたテキストを article と称します。 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$ という二つの要素をもつ集合 $\{y, z\}$ の定義です。

任意の $y$ に対して $\{y\}$ とは, 任意の $x$ について $x \in \{y\} \Leftrightarrow x = y$ を充たす集合であり, 任意の $y$, $z$ に対して $\{y, z\}$ とは, 任意の $x$ について $x \in \{y, z\} \Leftrightarrow x = y \;\text{or}\; 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$ に対して,functor(作用)$\cup X$ とは,$X$ に, 任意の $x$ に対して

$(x \in \cup X) \Leftrightarrow((\exists Y)(x \in Y$ and $Y \in X))$

となる集合を対応させる作用であること表しています。

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

記号論理で書けば, 任意の $X$ に対して $(x \in X) \Rightarrow(\exists Y)(Y \in X$ and $\operatorname{not}(\exists x)(x \in X$ and $x \in Y))$ を表しています。$x$ が集合 $X$ の要素であれば, 集合 $X$ の要素であって, し かも,$x$ をその要素として含むような $Y$ は存在しないという主張を表してい ます。

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

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

任意の \(x\), \(y\) に対して $\{\{x, y\},\{x\}\}$ を \([x, y]\) で表すことを \(x\), \(y\) から \([x, y]\) を作り出す functor（作用）として定義します。

以下は, 二つの集合 \(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日閲覧