差分

このページの2つのバージョン間の差分を表示します。

--- start [2025/03/17 08:25] – 作成 superuser
+++ start [2025/03/18 04:17] (現在) – [part 2] 153.170.74.128
@@ 行 1: / 行 1: @@
-====== 第1章 TARSKIの公理系 ======
+==== part 1 ====
-このテキストは，集合論を題材に，mizar を使った，数学定理の記述が，実際にどのようになされているかを説明します。
+regular content
-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 =====
+<mizar my_article_name>
+  article part 1
-これから,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 はその後に続く, 変数の型がなんであるかを示します。この例では
+==== part 2 ====
-$x, y, z, u, N, M, X, Y, Z$
-は任意の集合 set になっています。集合論では, 取り扱う対象は集合か, そ
-の要素ですが, 集合も要素も, 形式上は区別されません。ですから,set とい
-うのは, 任意の対象を意味しています。
-<mizar ta>
+regular content
-theorem :: Everything is a set
-  for x being object holds x is set by TARSKI_0:1;
-</mizar>
-==== 1.1.1 外延性の公理 ====
+<mizar my_article_name>
+  article part 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>
-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日閲覧