====== 第1章 TARSKIの公理系 ======

このテキストは集合論を題材に 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** について説明します。

===== 1.1 TARSKI.miz =====

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

<mizar ta>
:: Tarski {G}rothendieck Set Theory
::  by Andrzej Trybulec
::
:: Received January 1, 1989
:: Copyright (c) 1990-2021 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies TARSKI;
 theorems TARSKI_0;
 schemes TARSKI_0;

begin
</mizar>

<mizar ta>
 reserve x,y,z,u for object;
 reserve N,M,X,Y,Z for set;
</mizar>

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

<mizar ta>
theorem :: Everything is a set
  for x being object holds x is set by TARSKI_0:1;
</mizar>

==== 1.1.1 外延性の公理 ====

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

<mizar ta>
theorem :: Extensionality
  (for x being object holds x in X iff x in Y) implies X = Y by TARSKI_0:2;
</mizar>

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

==== 1.1.2 非順序対の定義 ====

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

<mizar ta>
definition let y be object;
  func { y } -> set means
    for x being object holds x in it iff x = y;
  existence
  proof
    consider X being set such that
A1: for x being object holds
      x in X iff x = y or x = y by TARSKI_0:3;
    take X;
    thus thesis by A1;
  end;
  uniqueness
  proof
    let X1, X2 be set such that
A1: for z being object holds z in X1 iff z = y and
A2: for z being object holds z in X2 iff z = y;
    for z being object holds z in X1 iff z in X2 by A1,A2;
    hence thesis by TARSKI_0:2;
  end;
  let z be object;
  func { y, z } -> set means :Def2:
    x in it iff x = y or x = z;
  existence by TARSKI_0:3;
  uniqueness
  proof
    let X1, X2 be set such that
A1: for x being object holds x in X1 iff x = y or x = z and
A2: for x being object holds x in X2 iff x = y or x = z;
    now
      let x be object;
      x in X1 iff x = y or x = z by A1;
      hence x in X1 iff x in X2 by A2;
    end;
    hence thesis by TARSKI_0:2;
  end;
  commutativity;
end;
</mizar>

任意の \(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\}
\]
が成り立つことを表しています。

==== 1.1.3 包含関係の定義 ====

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

<mizar ta>
definition let X,Y;
  pred X c= Y means
   for x being object holds x in X implies x in Y;
  reflexivity;
end;
</mizar>

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

==== 1.1.4 集合の合弁の定義 ====

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

<mizar ta>
definition let X;
  func union X -> set means
    x in it iff ex Y st x in Y & Y in X;
  existence by TARSKI_0:4;
  uniqueness
  proof
    let X1, X2 be set such that
A1: for x being object holds
      x in X1 iff ex Y being set st x in Y & Y in X and
A2: for x being object holds
      x in X2 iff ex Y being set st x in Y & Y in X;
    now
      let x be object;
      x in X1 iff ex Y being set st x in Y & Y in X by A1;
      hence x in X1 iff x in X2 by A2;
    end;
    hence thesis by TARSKI_0:2;
  end;
end;
</mizar>

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

==== 1.1.5 正則性の公理 ====

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

<mizar ta>
theorem :: Regularity
  x in X implies
   ex Y st Y in X & not ex x st x in X & x in Y by TARSKI_0:5;
</mizar>

記号論理で表すと、任意の集合 \(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\) は存在しないという主張を表しています。
<mizar ta>
definition let x, X be set;
  redefine pred x in X;
  asymmetry
  proof
    let a,b be set;
    assume
A1: a in b & b in a;
    set X = {a,b};
A3: a in X & b in X by Def2;
    consider Y being set such that
A4: Y in X & not ex x being object st x in X & x in Y by A3,TARSKI_0:5;
    Y = a or Y = b by A4,Def2;
    hence thesis by A1,A3,A4;
  end;
end;
</mizar>

==== 1.1.6 選出の公理 (Fraenkel の公理式) ====

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

<mizar ta>
scheme Replacement{ A() -> set, P[object,object] }:
  ex X st for x being object holds x in X iff
    ex y being object st y in A() & P[y,x]
  provided
A1: for x,y,z being object st P[x,y] & P[x,z] holds y = z
  proof
    thus thesis from TARSKI_0:sch 1(A1);
  end;
  
</mizar>

任意の集合 \(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]))
\]
が成り立つことを表しています。

==== 1.1.7 順序対の定義 ====

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

<mizar ta>
definition let x,y be object;
  func [x,y] -> object equals
    { { x,y }, { x } };
  coherence;
end;
</mizar>

==== 1.1.8 集合の等濃度の定義 ====

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

<mizar ta>
definition let X,Y;
  pred X,Y are_equipotent means
   ex Z st
   (for x st x in X ex y st y in Y & [x,y] in Z) &
   (for y st y in Y ex x st x in X & [x,y] in Z) &
   for x,y,z,u st [x,y] in Z & [z,u] in Z holds x = z iff y = u;
end;
</mizar>

すなわち, 任意の \(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\}\)
が成り立つことを言います。

==== 出典・参考文献 ====

  - 師玉, 康成 "[[http://cai3.cs.shinshu-u.ac.jp/Lecture/SetTheory3/mizar/mizar.pdf|mizarと集合論]]" 2017年3月25日閲覧