====== Chapter 1 TARSKI's axiomatic system ======

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 **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**. \\
Then, starting with the declaration of **begin**, the content of this article begins.

<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** indicates the type of the variables that follow. In this example, 
\(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.

<mizar ta>
theorem :: Everything is a set
  for x being object holds x is set by TARSKI_0:1;
</mizar>

==== 1.1.1 Axiom of Extensionality ====

(Definition of the equality of two sets)\\
First, we have the following description.

<mizar ta>
theorem :: Extensionality
  (for x being object holds x in X iff x in Y) implies X = Y by TARSKI_0:2;
</mizar>

In symbolic logic, this is written as
\[
((\forall x)(x \in X \Leftrightarrow x \in Y)) \Rightarrow X = Y.
\]
This is known as the \textbf{Axiom of Extensionality}.  
It states that if, for every \(x\),
\[
x \in X \Leftrightarrow x \in Y,
\]
then the two sets \(X\) and \(Y\) are equal (i.e., \(X = Y\)).

==== 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\}\).

<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>

For any \(y\), the singleton set \(\{y\}\) is defined as the set that satisfies, for every \(x\)
\[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\),
\[x \in \{y, z\} \Leftrightarrow x = y \lor x = z.\]
Furthermore, **commutativity** is expressed by the equality
\[\{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\)".

<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>

For any sets \(X\) and \(Y\), we say that
\[X \subseteq Y\]
if and only if, for every \(x\), the implication
\[x \in X \Rightarrow x \in Y\]
holds. **Reflexivity** means that for any set \(X\), it holds that
\[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\).

<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>

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)).\]


==== 1.1.5 Axiom of Regularity ====

The following is stated as a theorem with its proof omitted; however, it is known as the Axiom of Regularity.

<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>

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)).\]
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>
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 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]\).
<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>


For any set \(A\) and any relation \(P\) satisfying
\[
(\forall x, y, z)(P[x,y] \land P[x,z] \Rightarrow y=z),
\]
there exists a set \(X\) such that
\[
(\forall x)(x \in X \Leftrightarrow (\exists y)(y \in A \land P[y,x])).
\]

==== 1.1.7 Definition of the Ordered Pair ====

For any \(x\) and \(y\), the ordered pair \([x, y]\) is defined by
\[
[x, y] := \{\{x, y\}, \{x\}\}.
\]
This definition treats the mapping from \(x\) and \(y\) to \([x, y]\) as a functor (operation) that constructs the ordered pair from \(x\) and \(y\).

<mizar ta>
definition let x,y be object;
  func [x,y] -> object equals
    { { x,y }, { x } };
  coherence;
end;
</mizar>

==== 1.1.8 Definition of Equipotency of Sets ====

The following definition states that two sets \(X\) and \(Y\) are said to be equipotent (i.e., have equal cardinalities) if there exists a bijection (a one-to-one and onto mapping) between them.

<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>

Namely, for any sets \(X\) and \(Y\), we say that \(X\) and \(Y\) are **equipotent** (i.e., have equal cardinalities) if and only if there exists a set \(Z\) such that
\[
\exists Z \left\{
\begin{aligned}
  &\forall x \in X\, \exists y \in Y\, \bigl([x, y] \in Z\bigr) \land \\
  &\forall y \in Y\, \exists x \in X\, \bigl([x, y] \in Z\bigr) \land \\
  &\forall x, y, z, u\, \Bigl( \bigl([x, y] \in Z \land [z, u] \in Z\bigr) \implies (x = z \Leftrightarrow y = u) \Bigr)
\end{aligned}
\right\}
\]
holds.

==== 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.