A Practical Guide To Mizar/Syntax and Sets

Axioms

Nowadays everything in the Mizar Mathematical Library is proven based on earlier works. Except of course the axioms. An axiom is an evident truth that needs no proof. Mathematicians try to keep the number of axioms in an axiomatic system low and independent of one another. A commonly used axiomatic system is Zermelo-Fraenkel (ZFC), but Mizar uses Tarski-Grothendieck (TG), which implies ZFC. Hence the axiomatic articles hidden.miz, tarski_0.miz and tarski_a.miz don't contain proofs in opposite to all other MIZ articles.

So what are these axioms?

First, lets call anything we come across in Mizar an object. For any two objects a and b, we can either say that a = b or a <> b (which is the same as not a = b), there is no in-between. A set is an unordered collection of objects. For any object a and any set A (sets are usually denoted with capital letters), we have either a in A or not a in A. By earlier definition, a set is also an object.

The first axiom states that every object is also a set:

:: Set axiom
theorem :: TARSKI_0:1
  for x being object holds x is set;

Why differ between objects and sets then? There are reasons, but these are best left to set theorists.

The second axiom states that two sets are equal exactly when they contain the same objects:

:: Extensionality axiom
theorem :: TARSKI_0:2
  (for x being object holds x in X iff x in Y) implies X = Y;

The third axiom states that for every two objects, there exist a set containing only these two:

:: Axiom of pair
theorem :: TARSKI_0:3
  for x,y being object ex z being set st
    for a being object holds
      a in z iff a = x or a = y;

The fourth axiom states that the union of a set exists, i.e. the set Z containing all objects x that are in any set Y contained in a given set X:

:: Axiom of union
theorem :: TARSKI_0:4
  for X being set
   ex Z being set st
    for x being object holds
      x in Z iff ex Y being set st x in Y & Y in X;

The fiveth axiom states that a set X, if it is not empty, must contain a set Y such that no object x is in both X and Y:

:: Axiom of regularity
theorem :: TARSKI_0:5
  x in X implies ex Y st Y in X & not ex x st x in X & x in Y;

This is a technical axiom that ensures that we don't have something like "a set containing only itself", because these things lead to trouble down the road.

The sixth axiom states that we can get a new set by exchanging objects in a set with other objects.

:: Fraenkel's scheme
scheme :: TARSKI_0:sch 1
 Replacement { A() -> set, P[object, object] }:
  ex X st for x holds x in X iff ex y st y in A() & P[y,x]
 provided
  for x,y,z being object st P[x,y] & P[x,z] holds y = z;

You can see that this one looks a bit different from the others, scheme instead of theorem etc. Schemes will be explained in Relations and Functions.

The seventh and last axiom is very technical and you don't need to understand it. It basically states that "big" sets with certain properties exist:

:: Tarski's axiom
theorem :: TARSKI_A:1
  ex M st N in M &
     (for X,Y holds X in M & Y c= X implies Y in M) &
     (for X st X in M ex Z st Z in M & for Y st Y c= X holds Y in Z) &
     (for X holds X c= M implies X,M are_equipotent or X in M);

In practice we will hardly ever use TARSKI_0 or TARSKI_A and instead use TARSKI quite often.

Syntax

For this section, this will be the environment used:

environ
 vocabularies TARSKI;
 notations TARSKI;
 constructors TARSKI;
 theorems TARSKI;

begin

As seen above, one way to specify a property P holds for all objects of some type is like this:

theorem
  for X being set holds P[X];

(For this to compile replace P[X] with an actual property like X = X for example.)

If you have several objects you can specify them like:

theorem
  for X being set for Y being set holds P[X,Y];

This can be shortened to:

theorem
  for X being set, Y being set holds P[X,Y];

And in case you have several object of the same type, you can shorten it further to:

theorem
  for X, Y being set holds P[X, Y];

With the use of reserve you can shorten it even more like:

reserve X, Y for set;

theorem
  for X, Y holds P[X, Y];

theorem
  for X holds P[X];

And finally, Mizar can infer the types from reserve, so you leave out the for:

reserve X, Y for set;

theorem
  P[X, Y];

theorem
  P[X];

Similarly, to specify that an object (or several) of some type fulfilling a property P exists, one can use any of the following styles:

theorem
  ex X being set st P[X];

theorem
  ex X being set st ex Y being set st P[X,Y];

theorem
  ex X being set ex Y being set st P[X,Y];

theorem
  ex X being set, Y being set st P[X,Y];

theorem
  ex X, Y being set st P[X,Y];

reserve X, Y for set;

theorem
  ex X st P[X];

theorem
  ex X st ex Y st P[X,Y];

theorem
  ex X ex Y st P[X,Y];

theorem
  ex X, Y st P[X,Y];