Dynamically Verifiable Documentation of Mathematics using Mizar

Mizar を用いた動的検証可能な数学ドキュメンテーション

ユーザ用ツール

サイト用ツール

トレース:
example

差分

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

この比較画面へのリンク

次のリビジョン		前のリビジョン
example [2025/03/18 03:33] – 作成 153.170.74.128example [2025/05/29 06:35] (現在) – superuser
行 1: 行 1:
 ====== 第1章 TARSKIの公理系 ====== ====== 第1章 TARSKIの公理系 ======
  
-このテキストは，集合論を題材に，mizar を使った，数学定理の記述が，実際にどのようになされているかを説明します。 +このテキストは集合論を題材に mizar を使った数学定理の記述が実際にどのようになされているかを説明します。 
-mizar では，その数学記述言語によって書かれたテキストを article と称します。+mizar では，その数学記述言語によって書かれたテキストを **articles** と称します。
 mizar システムやそれで使われる数学記述言語の文法については，中村八束教授著の mizar 講義録第３版 mizar システムやそれで使われる数学記述言語の文法については，中村八束教授著の mizar 講義録第３版
 http://markun.cs.shinshu-u.ac.jp/kiso/projects2/proofchecker/mizar/Mizar-J/Miz-tit.html http://markun.cs.shinshu-u.ac.jp/kiso/projects2/proofchecker/mizar/Mizar-J/Miz-tit.html
行 9: 行 9:
 http://markun.cs.shinshu-u.ac.jp/kiso/projects2/proofchecker/mizar/index-j.html http://markun.cs.shinshu-u.ac.jp/kiso/projects2/proofchecker/mizar/index-j.html
 にあります。 にあります。
-このテキストでは，mizar で記述された数学定理のデータベースであるライブラリ中の集合論についての，基礎的な article TARSKI.miz, XBOOLl0.miz, XBOOLl1.miz について説明します。+このテキストでは，mizar で記述された数学定理のデータベースであるライブラリ中の集合論についての，基礎的な article  **TARSKI.miz**, **XBOOLl0.miz**, **XBOOLl1.miz** について説明します。
  
 ===== 1.1 TARSKI.miz ===== ===== 1.1 TARSKI.miz =====
  
-これから,TARSKI.miz を読み解いていきます。\\+これから **TARSKI.miz** を読み解いていきます。\\
 まず, 以下の環境部の記述があります。 まず, 以下の環境部の記述があります。
-これは, この article で, 使われる, 用語 (vocabulary) が TARSKI.voc とい+これは, この article で, 使われる, 用語 (vocabulary) が **TARSKI.voc** とい
 うファイルに記述されていることを宣言しています。 うファイルに記述されていることを宣言しています。
-次の,begin の宣言からこの article の内容の記述が始まります。+次の **begin** の宣言からこの article の内容の記述が始まります。
  
 <mizar ta> <mizar ta>
行 48: 行 48:
 </mizar> </mizar>
  
-reserve はその後に続く, 変数の型がなんであるかを示します。この例では +**reserve** はその後に続く, 変数の型がなんであるかを示します。この例では 
-$x, y, z, u, N, M, X, Y, Z$+\(x, y, z, u, N, M, X, Y, Z\)
 は任意の集合 set になっています。集合論では, 取り扱う対象は集合か, そ は任意の集合 set になっています。集合論では, 取り扱う対象は集合か, そ
-の要素ですが, 集合も要素も, 形式上は区別されません。ですから,set とい+の要素ですが, 集合も要素も, 形式上は区別されません。ですから'set' とい
 うのは, 任意の対象を意味しています。 うのは, 任意の対象を意味しています。
  
行 70: 行 70:
  
 記号論理で書けば 記号論理で書けば
- +\[ 
-$((\forall x)(x \in X \Leftrightarrow x \in Y)) \Rightarrow X=Y$ +((\forall x)(x \in X \Leftrightarrow x \in Y)) \Rightarrow X=Y 
 +\]
 です。これは, 外延性の公理として知られるものです。 です。これは, 外延性の公理として知られるものです。
-任意の $x$ に対して, +すなわち，任意の \(x\) に対して, 
-$x \in X \Leftrightarrow x \in Y$ +\(x \in X \Leftrightarrow x \in Y\) 
-であるならば, ２つの集合 $X$, $Y$ は等しい ($X = Y$ である) ことを主張しています。+であるならば, ２つの集合 \(X\), \(Y\) は等しい (すなわち \(X = Y\) である) ことを主張しています。
  
 ==== 1.1.2 非順序対の定義 ==== ==== 1.1.2 非順序対の定義 ====
  
-次の記述は,$x$ 一つだけからなる集合 $\{x\}$ と $x$, $y$ という二つの要素をもつ集合 $\{y, z\}$ の定義です。+次の記述は \(x\) 一つだけからなる集合 \(\{x\}\) と \(x\), \(y\) という二つの要素をもつ集合 \(\{x, y\}\) の定義です。
  
 <mizar ta> <mizar ta>
行 122: 行 122:
 </mizar> </mizar>
  
-任意の $y$ に対して $\{y\}$ とは, 任意の $x$ について +任意の \(y\) に対して \(\{y\}\) とは, 任意の \(x\) について 
-$x \in \{y\} \Leftrightarrow x = y$ +\[ 
-を充たす集合であり, +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\) に対して \(\{y, z\}\) とは, 任意の \(x\) について 
-$\{y, z\} = \{z, y\}$ +\[ 
-であることを表しています。+x \in \{y, z\} \Leftrightarrow x = y \lor x = z 
 +\] 
 +を満たす集合であることを意味します。また、**可換性 (commutativity)** は 
 +\[ 
 +\{y, z\} = \{z, y\} 
 +\] 
 +が成り立つことを表しています。
  
 ==== 1.1.3 包含関係の定義 ==== ==== 1.1.3 包含関係の定義 ====
  
-次は,「集合 $X$ が集合 $Y$ の部分集合である」あるは「集合 $X$ が集合 $Y$ に含まれる」という述語の定義が書かれています。+次は,「集合 \(X\) が集合 \(Y\) の部分集合である」または「集合 \(X\) が集合 \(Y\) に含まれる」という述語の定義を示しています。
  
 <mizar ta> <mizar ta>
行 143: 行 149:
 </mizar> </mizar>
  
-任意の $X$, $Y$ に対して +任意の \(X\), \(Y\) に対して、   
-$X \subseteq Y$ +\(X \subseteq Y\) とは、任意の \(x\) に対して 
-とは, 任意の $x$ について +\[ 
-$x \in X \Rightarrow x \in Y$ +x \in X \Rightarrow x \in Y 
-が成り立つことをいい,reflexivity は任意の $X$ に対してそれ自身 +\] 
-$X \subseteq X$+が成り立つことをいいます。   
 +また、**反射律（reflexivity）**とは、任意の \(X\) に対して 
 +\[ 
 +X \subseteq X 
 +\]
 が成り立つことを表しています。 が成り立つことを表しています。
  
 ==== 1.1.4 集合の合弁の定義 ==== ==== 1.1.4 集合の合弁の定義 ====
  
-任意の集合族 (集合の集合)$X$ に対して,$X$ に属する 集合の全ての合弁が,$X$ から $\cup X$ をつくる functor(作用) として定義されています。+任意の集合族 (すなわち集合の集合)\(X\) に対して,\(X\) に属する 集合のすべての合弁は、集合族 \(X\) から \(\cup X\) をつくる作用 (functor) として定義されています。
  
 <mizar ta> <mizar ta>
行 177: 行 187:
 </mizar> </mizar>
  
-任意の $X$ に対して,functor(作用)$\cup X$ とは,$X$ に, +任意の集合族 \(X\) に対して、作用 \(\cup X\) は、次の条件を満たす集合を \(X\) に対応させる操作として定義されます。すなわち、任意の \(x\) に対して 
-任意の $x$ に対して +\[ 
- +x \in \cup X \Leftrightarrow (\exists Y)(x \in Y \land Y \in X). 
-$(x \in \cup X) \Leftrightarrow((\exists Y)(x \in Y$ and $Y \in X))$ +\]
- +
-となる集合を対応させる作用であること表しています。+
  
 ==== 1.1.5 正則性の公理 ==== ==== 1.1.5 正則性の公理 ====
行 194: 行 202:
 </mizar> </mizar>
  
-記号論理で書けば, 任意の $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 \in X) \Rightarrow (\exists Y)(Y \in X \land \neg(\exists x)(x \in X \land x \in Y)) 
-かも,$x$ をその要素として含むような $Y$ は存在しないという主張を表してい +\] 
-ます。+という命題になります。
  
 +これは \(x\) が集合 \(X\) の要素であれば、集合 \(X\) の要素であって, しかも \(x\) をその要素として含むような \(Y\) は存在しないという主張を表しています。
 <mizar ta> <mizar ta>
 definition let x, X be set; definition let x, X be set;
行 217: 行 226:
 end; end;
 </mizar> </mizar>
 +
 ==== 1.1.6 選出の公理 (Fraenkel の公理式) ==== ==== 1.1.6 選出の公理 (Fraenkel の公理式) ====
  
-集合 $A$ と, 関係式 $P[x, y]$ から集合 $X$ を構成する手続きを scheme(公理図式) として記述したのものが以下です。+集合 \(A\) と, 関係式 \(P[x, y]\) から集合 \(X\) を構成する手続きを公理図式 (scheme) として記述したのものが以下です。
  
 <mizar ta> <mizar ta>
 scheme Replacement{ A() -> set, P[object,object] }: scheme Replacement{ A() -> set, P[object,object] }:
-  ex X st for x being object holds x in X iff +  ex X st for x being object holds x in X 
-    ex y being object st y in A() & P[y,x]+    iff ex y being object st y in A() & P[y,x]
   provided   provided
 A1: for x,y,z being object st P[x,y] & P[x,z] holds y = z A1: for x,y,z being object st P[x,y] & P[x,z] holds y = z
行 233: 行 243:
 </mizar> </mizar>
  
-任意の $A$ と, +任意の集合 \(A\) と、 
-$(\forall x, y, z)(P[x, y]$ and $P[x, z] \Rightarrow y=z)$ +\[ 
-が成り立つ関係 $P$ に対して, 集合 $X$ が存在して, +(\forall x, y, z)\,(P[x, y] \land P[x, z] \Rightarrow y = z) 
-$(\forall x)(x \in x \Leftrightarrow(\exists y)(y \in$ and $P[y, x]))$ +\] 
-となることを表しています。+が成り立つような関係 \(P\) に対して、ある集合 \(X\) が存在して、 
 +\[ 
 +(\forall x)(x \in X \Leftrightarrow (\exists y)(y \in A \land P[y, x])) 
 +\] 
 +が成り立つことを表しています。 
 ==== 1.1.7 順序対の定義 ==== ==== 1.1.7 順序対の定義 ====
  
-任意の \(x\), \(y\) に対して +任意の \(x\), \(y\) に対して、集合 \(\{\{x, y\}, \{x\}\}\) を**順序対** \([x, y]\) と表します。   
-$\{\{x, y\},\{x\}\}$ +これは、\(x\) と \(y\) から順序対 \([x, y]\) を構成する作用 (functor) として定義されます。
-を \([x, y]\) で表すことを \(x\), \(y\) から \([x, y]\) を作り出す functor（作用）として定義します。+
  
 <mizar ta> <mizar ta>
行 254: 行 268:
 ==== 1.1.8 集合の等濃度の定義 ==== ==== 1.1.8 集合の等濃度の定義 ====
  
-以下は, 二つの集合 \(X\), \(Y\) の間に, 双射 (一対一, かつ, 上への写像）が存 +以下は2つの集合 \(X\)と\(Y\) の間に双射 (すなわち一対一 かつ上への写像）が存在するとき, 集合(X\)と\(Y\) の**濃度が等しい(equipotent)** と定義すること表しています。
-在するとき, 「\(X\), \(Y\) の濃度が等しい」equipotent と定義すること表しています。+
  
 <mizar ta> <mizar ta>
行 267: 行 280:
 </mizar> </mizar>
  
-すなわち, 任意の \(X\), \(Y\) に対して, これらが, 等濃度である（equipotent で +すなわち, 任意の \(X\), \(Y\) に対して, これらが, **等濃度（equipotent)**であるとは
-ある）とは+
 \(\exists Z \left\{  \(\exists Z \left\{ 
 \begin{aligned} \begin{aligned}
行 279: 行 291:
  
 ==== 出典・参考文献 ==== ==== 出典・参考文献 ====
 +
   - 師玉, 康成 "[[http://cai3.cs.shinshu-u.ac.jp/Lecture/SetTheory3/mizar/mizar.pdf|mizarと集合論]]" 2017年3月25日閲覧   - 師玉, 康成 "[[http://cai3.cs.shinshu-u.ac.jp/Lecture/SetTheory3/mizar/mizar.pdf|mizarと集合論]]" 2017年3月25日閲覧
 +
example.1742268811.txt.gz · 最終更新: by 153.170.74.128