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

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

===== 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$ という二つの要素をもつ集合 $\{y, z\}$ の定義です。

<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 \;\text{or}\; 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.miz>
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$ に対して,functor(作用)$\cup X$ とは,$X$ に,
任意の $x$ に対して

$(x \in \cup X) \Leftrightarrow((\exists Y)(x \in Y$ and $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$ and $\operatorname{not}(\exists x)(x \in X$ and $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]$ and $P[x, z] \Rightarrow y=z)$
が成り立つ関係 $P$ に対して, 集合 $X$ が存在して,
$(\forall x)(x \in x \Leftrightarrow(\exists y)(y \in$ and $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 集合の等濃度の定義 ====

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