Differences

This shows you the differences between two versions of the page.

--- en:example [2025/04/07 07:19] – created superuser
+++ en:example [2025/04/08 03:19] (current) – [1.1.4 Definition of the Union of Sets] superuser
@@ Line 3: / Line 3: @@
 This text explains how the description of mathematical theorems is actually carried out using Mizar with set theory as the subject matter. In Mizar, texts written in its mathematical description language are called **articles**. The Mizar system and the grammar of the mathematical language it uses are explained in the \emph{Mizar Lecture Notes, Third Edition} by Professor Yatsusaku Nakamura http://markun.cs.shinshu-u.ac.jp/kiso/projects2/proofchecker/mizar/Mizar-J/Miz-tit.html. Moreover, the Mizar system for PC download as well as the web-based Mizar system can be found at　http://markun.cs.shinshu-u.ac.jp/kiso/projects2/proofchecker/mizar/index-j.html.
-In this text, we describe the basic articles on set theory from the Mizar library (a database of mathematical theorems written in Mizar), namely $\texttt{TARSKI.miz}$, $\texttt{XBOOLl0.miz}$, and $\texttt{XBOOLl1.miz}$.
+In this text, we describe the basic articles on set theory from the Mizar library (a database of mathematical theorems written in Mizar), namely **TARSKI.miz**, **XBOOLl0.miz**, and **XBOOLl1.miz**.
 ===== 1.1 TARSKI.miz =====
 From now on, we will begin to decipher **TARSKI.miz**. \\
-First, there is the following environment section. This section declares that the vocabulary used in this article is specified in a file called **TARSKI.voc**$. \\
+First, there is the following environment section. This section declares that the vocabulary used in this article is specified in a file called **TARSKI.voc**. \\
 Then, starting with the declaration of **begin**, the content of this article begins.
@@ Line 43: / Line 43: @@
 \(x, y, z, u, N, M, X, Y, Z\) are arbitrary sets. In set theory, the objects under
 consideration are either sets or their elements; however, sets and elements are not
-formally distinguished. Thus, the term ``set'' denotes an arbitrary object.
+formally distinguished. Thus, the term “set” denotes an arbitrary object.
 <mizar ta>
@@ Line 73: / Line 73: @@
 ==== 1.1.2 Definition of an Unordered Pair ====
-The following description defines the singleton set $\{x\}$ (a set containing only $x$) and the unordered pair (a set containing two elements, $x$ and $y$) denoted as $\{x, y\}$.
+The following description defines the singleton set \(\{x\}\) (a set containing only \(x\)) and the unordered pair (a set containing two elements, \(x\) and \(y\)) denoted as \(\{x, y\}\).
 <mizar ta>
@@ Line 115: / Line 115: @@
 </mizar>
-For any $y$, the singleton set $\{y\}$ is defined as the set that satisfies, for every $x$
+For any \(y\), the singleton set \(\{y\}\) is defined as the set that satisfies, for every \(x\)
-$$x \in \{y\} \Leftrightarrow x = y.$$
+\[x \in \{y\} \Leftrightarrow x = y.\]
-For any $y$ and $z$, the unordered pair $\{y, z\}$ is defined as the set that satisfies, for every $x$,
+For any \(y\) and \(z\), the unordered pair \(\{y, z\}\) is defined as the set that satisfies, for every \(x\),
-$$x \in \{y, z\} \Leftrightarrow x = y \lor x = z.$$
+\[x \in \{y, z\} \Leftrightarrow x = y \lor x = z.\]
 Furthermore, **commutativity** is expressed by the equality
-$$\{y, z\} = \{z, y\}.$$
+\[\{y, z\} = \{z, y\}.\]
 ==== 1.1.3 Definition of the Inclusion Relation ====
-Below is the definition of the predicate stating that "set $X$ is a subset of set $Y$" or equivalently, "set $X$ is contained in set $Y$".
+Below is the definition of the predicate stating that "set \(X\) is a subset of set \(Y\)" or equivalently, "set \(X\) is contained in set \(Y\)".
 <mizar ta>
@@ Line 134: / Line 134: @@
 </mizar>
-For any sets $X$ and $Y$, we say that
+For any sets \(X\) and \(Y\), we say that
-$$X \subseteq Y$$
+\[X \subseteq Y\]
-if and only if, for every $x$, the implication
+if and only if, for every \(x\), the implication
-$$x \in X \Rightarrow x \in Y$$
+\[x \in X \Rightarrow x \in Y\]
-holds. **Reflexivity** means that for any set $X$, it holds that
+holds. **Reflexivity** means that for any set \(X\), it holds that
-$$X \subseteq X.$$
+\[X \subseteq X.\]
 ==== 1.1.4 Definition of the Union of Sets ====
-For any family of sets (i.e., a set of sets) $X$, the union of all sets belonging to　$X$ is defined as the functor (operation) that maps $X$ to $\cup X$.
+For any family of sets (i.e., a set of sets) \(X\), the union of all sets belonging to　\(X\) is defined as the functor (operation) that maps \(X\) to \(\cup X\).
 <mizar ta>
@@ Line 167: / Line 167: @@
 </mizar>
-For any $X$, the functor (operation) $\cup X$ is defined as the mapping that associates to $X$ the set satisfying, for any $x$ に対して
+For any \(X\), the functor (operation) \(\cup X\) is defined as the mapping that associates to \(X\) the set satisfying, for any \(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 \land Y \in X)).\]
@@ Line 182: / Line 182: @@
 </mizar>
-In symbolic logic, for any set $X$, it is written as
+In symbolic logic, for any set \(X\), it is written as
-$$(x \in X) \Rightarrow (\exists Y)(Y \in X \land \neg (\exists x)(x \in X \land x \in Y)).$$
+\[(x \in X) \Rightarrow (\exists Y)(Y \in X \land \neg (\exists x)(x \in X \land x \in Y)).\]
-This expresses the claim that if $x$ is an element of the set $X$, then there does not exist any $Y$  that is both an element of $X$ and contains $x$ as one of its elements.
+This expresses the claim that if \(x\) is an element of the set \(X\), then there does not exist any \(Y\)  that is both an element of \(X\) and contains \(x\) as one of its elements.
 <mizar ta>
@@ Line 203: / Line 203: @@
 end;
 </mizar>
 ==== 1.1.6 Axiom of Selection (Fraenkel's Axiom Schema) ====
-The following is an axiom schema that describes the procedure for constructing a set $X$ from a set $A$ and a relational formula $P[x, y]$.
+The following is an axiom schema that describes the procedure for constructing a set \(X\) from a set \(A\) and a relational formula \(P[x, y]\).
 <mizar ta>
 scheme Replacement{ A() -> set, P[object,object] }:
@@ Line 271: / Line 272: @@
 ==== Sources and References ====
 Shitama, Yasunari. [[http://cai3.cs.shinshu-u.ac.jp/Lecture/SetTheory3/mizar/mizar.pdf|Mizar and Set Theory]] Accessed on March 25, 2017.