文書ロック中

この文書は、他のユーザーが編集中のためロックされています。編集が完了するか、ロックの期限が切れるまでお待ち下さい。
文書をロックしているユーザー： 216.73.216.46
ロック期限： 2025/05/24 23:26 (10 min)
この文書は読取専用です。文書のソースを閲覧することは可能ですが、変更はできません。もし変更したい場合は管理者に連絡してください。
====== 第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日閲覧====== 第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日閲覧