en:example
Differences
This shows you the differences between two versions of the page.
| Both sides previous revisionPrevious revisionNext revision | Previous revision | ||
| en:example [2025/04/08 02:52] – superuser | en:example [2025/04/08 03:19] (current) – [1.1.4 Definition of the Union of Sets] superuser | ||
|---|---|---|---|
| Line 8: | Line 8: | ||
| From now on, we will begin to decipher **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. | 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 | \(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 | consideration are either sets or their elements; however, sets and elements are not | ||
| - | formally distinguished. Thus, the term ``set'' | + | formally distinguished. Thus, the term “set” denotes an arbitrary object. |
| <mizar ta> | <mizar ta> | ||
| Line 73: | Line 73: | ||
| ==== 1.1.2 Definition of an Unordered Pair ==== | ==== 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, | + | The following description defines the singleton set \(\{x\}\) (a set containing only \(x\)) and the unordered pair (a set containing two elements, |
| <mizar ta> | <mizar ta> | ||
| Line 115: | Line 115: | ||
| </ | </ | ||
| - | 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, | Furthermore, | ||
| - | $$\{y, z\} = \{z, y\}.$$ | + | \[\{y, z\} = \{z, y\}.\] |
| ==== 1.1.3 Definition of the Inclusion Relation ==== | ==== 1.1.3 Definition of the Inclusion Relation ==== | ||
| - | Below is the definition of the predicate stating that " | + | Below is the definition of the predicate stating that " |
| <mizar ta> | <mizar ta> | ||
| Line 134: | Line 134: | ||
| </ | </ | ||
| - | 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 ==== | ==== 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> | <mizar ta> | ||
| Line 167: | Line 167: | ||
| </ | </ | ||
| - | For any $X$, the functor (operation) | + | For any \(X\), the functor (operation) |
| - | $$(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: | ||
| </ | </ | ||
| - | 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 | + | 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 |
| <mizar ta> | <mizar ta> | ||
| Line 206: | Line 206: | ||
| ==== 1.1.6 Axiom of Selection (Fraenkel' | ==== 1.1.6 Axiom of Selection (Fraenkel' | ||
| - | The following is an axiom schema that describes the procedure for constructing a set $X$ from a set $A$ and a relational formula | + | The following is an axiom schema that describes the procedure for constructing a set \(X\) from a set \(A\) and a relational formula |
| <mizar ta> | <mizar ta> | ||
| scheme Replacement{ A() -> set, P[object, | scheme Replacement{ A() -> set, P[object, | ||
en/example.1744080743.txt.gz · Last modified: 2025/04/08 02:52 by superuser