差分

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

--- example [2025/04/07 07:20] – [1.1 TARSKI.miz] superuser
+++ example [2025/05/29 06:35] (現在) – superuser
@@ 行 1: / 行 1: @@
 ====== 第1章 TARSKIの公理系 ======
-このテキストは，集合論を題材に，mizar を使った，数学定理の記述が，実際にどのようになされているかを説明します。
+このテキストは集合論を題材に mizar を使った数学定理の記述が実際にどのようになされているかを説明します。
 mizar では，その数学記述言語によって書かれたテキストを **articles** と称します。
 mizar システムやそれで使われる数学記述言語の文法については，中村八束教授著の mizar 講義録第３版
@@ 行 17: / 行 17: @@
 これは, この article で, 使われる, 用語 (vocabulary) が **TARSKI.voc** とい
 うファイルに記述されていることを宣言しています。
-次の,begin の宣言からこの article の内容の記述が始まります。
+次の **begin** の宣言からこの article の内容の記述が始まります。
 <mizar ta>
@@ 行 49: / 行 49: @@
 **reserve** はその後に続く, 変数の型がなんであるかを示します。この例では
-$x, y, z, u, N, M, X, Y, Z$
+\(x, y, z, u, N, M, X, Y, Z\)
 は任意の集合 set になっています。集合論では, 取り扱う対象は集合か, そ
 の要素ですが, 集合も要素も, 形式上は区別されません。ですから'set' とい
@@ 行 74: / 行 74: @@
 \]
 です。これは, 外延性の公理として知られるものです。
-すなわち，任意の $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 非順序対の定義 ====
-次の記述は $x$ 一つだけからなる集合 $\{x\}$ と $x$, $y$ という二つの要素をもつ集合 $\{x, y\}$ の定義です。
+次の記述は \(x\) 一つだけからなる集合 \(\{x\}\) と \(x\), \(y\) という二つの要素をもつ集合 \(\{x, y\}\) の定義です。
 <mizar ta>
@@ 行 122: / 行 122: @@
 </mizar>
-任意の $y$ に対して $\{y\}$ とは, 任意の $x$ について
+任意の \(y\) に対して \(\{y\}\) とは, 任意の \(x\) について
 \[
 x \in \{y\} \Leftrightarrow x = y
 \]
 を満たす集合であり,
-任意の $y$, $z$ に対して $\{y, z\}$ とは, 任意の $x$ について
+任意の \(y\), \(z\) に対して \(\{y, z\}\) とは, 任意の \(x\) について
 \[
 x \in \{y, z\} \Leftrightarrow x = y \lor x = z
@@ 行 139: / 行 139: @@
 ==== 1.1.3 包含関係の定義 ====
-次は,「集合 $X$ が集合 $Y$ の部分集合である」または「集合 $X$ が集合 $Y$ に含まれる」という述語の定義を示しています。
+次は,「集合 \(X\) が集合 \(Y\) の部分集合である」または「集合 \(X\) が集合 \(Y\) に含まれる」という述語の定義を示しています。
 <mizar ta>
@@ 行 163: / 行 163: @@
 ==== 1.1.4 集合の合弁の定義 ====
-任意の集合族 (すなわち集合の集合)$X$ に対して,$X$ に属する 集合のすべての合弁は、集合族 $X$ から $\cup X$ をつくる functor(作用) として定義されています。
+任意の集合族 (すなわち集合の集合)\(X\) に対して,\(X\) に属する 集合のすべての合弁は、集合族 \(X\) から \(\cup X\) をつくる作用 (functor) として定義されています。
 <mizar ta>
@@ 行 208: / 行 208: @@
 という命題になります。
-これは　\(x\) が集合 \(X\) の要素であれば、集合 $X$ の要素であって, しかも,$x$ をその要素として含むような $Y$ は存在しないという主張を表しています。
+これは \(x\) が集合 \(X\) の要素であれば、集合 \(X\) の要素であって, しかも \(x\) をその要素として含むような \(Y\) は存在しないという主張を表しています。
 <mizar ta>
 definition let x, X be set;
@@ 行 226: / 行 226: @@
 end;
 </mizar>
 ==== 1.1.6 選出の公理 (Fraenkel の公理式) ====
-集合 $A$ と, 関係式 $P[x, y]$ から集合 $X$ を構成する手続きを scheme(公理図式) として記述したのものが以下です。
+集合 \(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 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
 A1: for x,y,z being object st P[x,y] & P[x,z] holds y = z
@@ 行 251: / 行 252: @@
 \]
 が成り立つことを表しています。
 ==== 1.1.7 順序対の定義 ====
-任意の \(x\), \(y\) に対して、集合 \(\{\{x, y\}, \{x\}\}\) を順序対 \([x, y]\) と表します。
+任意の \(x\), \(y\) に対して、集合 \(\{\{x, y\}, \{x\}\}\) を**順序対** \([x, y]\) と表します。
-これは、\(x\) と \(y\) から順序対 \([x, y]\) を構成する作用(functor)として定義されます。
+これは、\(x\) と \(y\) から順序対 \([x, y]\) を構成する作用 (functor) として定義されます。
 <mizar ta>
@@ 行 278: / 行 280: @@
 </mizar>
-すなわち, 任意の \(X\), \(Y\) に対して, これらが, 等濃度（equipotent)であるとは
+すなわち, 任意の \(X\), \(Y\) に対して, これらが, **等濃度（equipotent)**であるとは
 \(\exists Z \left\{
 \begin{aligned}
@@ 行 289: / 行 291: @@
 ==== 出典・参考文献 ====
   - 師玉, 康成 "[[http://cai3.cs.shinshu-u.ac.jp/Lecture/SetTheory3/mizar/mizar.pdf|mizarと集合論]]" 2017年3月25日閲覧