# 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. The mathematical symbol for <> is "≠". 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. The mathematical symbol for in is "∊". By earlier definition, a set is also an object.
The first axiom states that every object is also a 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:
The third axiom states that for every two objects, there exist a set containing only these two:
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:
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:
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.
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:
In practice we will hardly ever use TARSKI_0 or TARSKI_A and instead use TARSKI quite often.

## Qualifiers

For this section, this will be the environment used:
As seen above, one way to specify a property P holds for all objects of some type is like this:
(For this to compile replace P[X] with an actual property like X = X for example.)
The mathematical symbol for for is "∀".
If you have several objects you can specify them like:
This can be shortened to:
And in case you have several object of the same type, you can shorten it further to:
With the use of reserve you can shorten it even more like:
And finally, Mizar can infer the types from reserve, so you leave out the for:
Similarly, to specify that an object (or several) of some type fulfilling a property P exists, one can use any of the following styles:
The mathematical symbol for ex is "∃".
When we want to prove these theorems, the corresponding syntax looks like this:
where [something] is an expression of some kind. The reconsider line is not necessarily needed if X is already known as the needed type (a set in this case) or a subtype thereof. take is surprisingly flexible, which we will see later. For example, in case [something] is recognized to be of the needed type, we can drop the reconsider line and replace all X following afterwards with [something].
In case of several quantifiers of the same kind you can mix and match the following syntax:
With the reserve keyword the proofs can become even shorter:
If we want to use these theorems, we do it like this:
Let's look a bit closer at this example. Theorems (as well as lemmata, which are like theorems but without the theorem keyword) can be given labels. Usually these are given names like Th1 (and Lm1), but anything not a keyword can be used. We can use a for statement simply by using the by keyword and the label of the theorem to use, but to use a ex statement we need syntax in the form consider … such that in connection with the by reference of the theorem.

## The empty set and basic set operations

For this section, this will be the environment used:
The first definition of XBOOLE_0 is the property of a set to be empty, i.e. not containing any elements (x is reserved as an object at this point):
A property P an object A of a certain type can have is defined using the attr A is P means construct (followed by the definiens). attr is short for "attribute", which will be used instead of this kind of property from now on.
Note that this definition compiles if you copy it. This is because attributes can be defined with any definiens, even if it can never be fulfilled. A nonsense definition could be for example:
You can use that definition in theorems like for x being object st x is empty holds P[x];, no matter what P[x] is (for example x <> x). That statement will be readily accepted by the checker because it sees that x is empty is a contradiction, and we can infer anything from a contradiction.
Let's agree to avoid nonsense attribute definitions.
To show that an attribute can indeed be fulfilled, one can use a so-called existential cluster registration. The one in XBOOLE_0 following the empty definition reads:
When you try to copy this registration from the abstract of XBOOLE_0 to your article, the parser will complain with a *73 error that a correctness condition is missing. To get rid of this error, we can add a proof skeleton like this:
That will now compile with the exception of *4, marking the actual proof as missing. We will not prove the existence here, it basically follows from Fraenkel's scheme. The interested reader can check it out in XBOOLE_0.
Now that the empty attribute is clustered for sets, we can use expressions like for X being empty set …, reserve X for empty set or the empty set. The latter describes the empty set that was used to prove the existence of empty sets, but it should be thought of "an arbitrary empty set".
Set operations are ways to generate new sets from existing ones. The arity of an operation indicates how many input parameters are needed to produce the output. The next definition in XBOOLE_0 is a nullary set operation and reads:
Since the output of this operation (right side of the ->) is a set as well as the definiens, we don't have to prove anything here and the compiler will be satisfied with the form:
func is short for "functor". In mathematical notation, the symbol "∅" is sometimes used instead of "". XBOOLE_0 also contains the functional cluster registration:
which will be accepted with a coherence condition added in XBOOLE_0 because the checker can see inside the definition that was made in the same article, unlike definitions made in other articles (without additional environment work). Clusters are an easy way to add attribute inferences to the checker without having to cite a specific theorem with by: Just add other articles to your article environment behind the registrations keyword and all registrations (existential, functional and conditional) from these articles will be added to yours. For pure sets this is not very powerful, but that will change with Relations and Functions.
The set that only contains a certain object y, or "{y}" in short, is an unary operator and the first definition in TARSKI:
it is the placeholder for the object we are defining. Since our functor definition doesn't use equals but means here, we have different correctness conditions, that are:
Both existence and uniqueness are proven in TARSKI using the axioms. existence means an object of the correct type (right of ->) fulfilling the definiens must exist. uniqueness means if two objects of the same type fulfill the definiens, they must be the same. If we want to only guarantee existence but not uniqueness, we can use a mode instead, which defines a subtype of a given type fulfilling a certain definiens. object and set are modes, but their existence is not proven, instead taken as an axiom of Mizar. They are defined in HIDDEN and can automatically used in any article (HIDDEN is included automatically).
In XBOOLE_0 there is a functional cluster saying that {y} is non empty.
It is very important to understand that a set X is not the same as the set containing only X. The former does not contain X (because of the Regularity Axiom) and the latter does, making them different. Math beginners often don't get the difference when X is the empty set, but we can in fact prove that {} <>:
In the second line of the proof we use that the empty set doesn't contain any elements, not even itself, but since {} does contain an element (proven in the line before, the element being the empty set), they cannot be the same. Also note that instead of then thus we write hence. thesis is a placeholder for the statement we are currently proving. The use of then means "use the statement from the previous line in your reasoning". It is the same as writing:
Similar to TARSKI:def 1 we have the next definition in TARSKI, just this time as a binary operator:
commutativity means that {y,z} is the same as {z,y}, which is apparent from the definition, since the logical arguments of or commute as well. For the parser existence and uniqueness are needed again, as they always are with the func … -> … means construct.
In XBOOLE_0 there is a functional cluster saying that {y, z} is non empty.
If you are looking for more sets defined explicitly by their concrete elements, check out ENUMSET1.
XBOOLE_0 gives us more binary set operations:
idempotence means that if both parameters are the same, the output is the same as well. The idempotence for X \/ Y and X /\ Y is apparent from their definiens because the logical operations or and & (which means "and") are idempotent as well. X \/ Y is the union of X and Y (also written as "X ∪ Y"), X /\ Y is the intersection of X and Y (also written as "X ∩ Y"). X \ Y is the difference of X and Y (sometimes written as "X - Y"). Note that it is neither marked as commutative nor as idempotent, because it doesn't fulfill these properties in general, as we will prove below. X \+\ Y is the symmetric difference of X and Y (sometimes written as "X ∆ Y", "X ⊕ Y" or "X ⊖ Y"). It is commutative (again apparent from the definition because X \/ Y is), but not idempotent. Note that we can put several definitions into one definition block but we had to use another for X \+\ Y so we could use the previous definitions in its definiens.
Union and intersection are associative, i.e.
Note that Mizar reads operations from left to right, so A \/ B \/ C is the same as (A \/ B) \/ C. The associativity of the two operations follows directly from the definitions because the logical operators or and & are associative. However, to prove this in Mizar, a little bit of work is necessary. For example:
We can see that this is mostly work with definitions. One can spot that we didn't write e.g.:
because Mizar is able to do that step itself (as it is often the case when no by or from keyword is used). Furthermore, that means it didn't matter if we wrote x in A or x in B or x in C or x in A or (x in B or x in C) in either of these places.
About the notation: We used TARSKI:2 here which reads
We wanted to use the part X = Y, which means we had to supply the part before the implies. That is why we have the statement:
in our proof and continued to prove that statement "instead" of A \/ B \/ C = A \/ (B \/ C). For two statements P, Q the statement P iff Q is equivalent to (P implies Q) & (Q implies P). To prove a statement of the form R & S for two statements R, S, we write it like this:
Exercise 1: Prove A /\ B /\ C = A /\ (B /\ C), based on the proof above and using XBOOLE_0:def 4 instead.
If you want to use them, the associativity laws are in the MML under XBOOLE_1:4 and XBOOLE_1:16 respectively.
Another important property that can be directly inferred from the logical operations behind the union and intersection is the distributivity. We have (A /\ B) \/ C = (A /\ C) \/ (B /\ C) and (A \/ B) /\ C = (A \/ C) /\ (B \/ C):
Again it doesn't matter if we write (x in A or x in B) & x in C or (x in A & x in C) or (x in B & x in C); Mizar can exchange these expressions by itself.
Exercise 2: Prove (A /\ B) \/ C = (A \/ C) /\ (B \/ C) based on the proof above.
If you want to use them, the distributivity laws are in the MML under XBOOLE_1:23 and XBOOLE_1:24 respectively.
We have now seen some examples of a direct proof, but sometimes a proof by contradiction is easier to write. Let's proof X \/ Y = implies X = (XBOOLE_1:15):
So instead of showing that X = we assume the opposite (X <>) and lead that to a contradiction with another assumption. Since all steps since assuming the opposite were correct, our opposite assumption must have been wrong (or math is not contradiction-free, which would be the discovery of the millennium). XBOOLE_0:7 itself follows from the definition of the empty set and reads:
Therefore we can use the consider … such that construct as discussed in the previous section. Note that we cannot use then after a consider, we have to work with labels. When X in X it is also true that x in X or x in Y, so we can go to the next step showing that x in X \/ Y via XBOOLE_0:def 3. That set however was assumed to be empty, hence we get our contradiction after throwing in the definition of the empty set and. We could have omitted XBOOLE_0:def 2 if we had registrations XBOOLE_0; in our environment, since then Mizar would have inferred by itself (using the cluster discussed above) that is indeed empty.
Note that we don't need a theorem for X, Y being set holds X \/ Y = implies Y = because X \/ Y is commutative, i.e. Mizar can infer that on its own given XBOOLE_1:15.
Exercise 3: Prove X /\ = by contradiction.
Exercise 4: Prove X \ X = by contradiction. This shows that the difference of sets is not idempotent.
We will now prove that X \+\ X = directly, using Exercise 4 (labelled Ex4). This shows that the symmetric difference of sets is not idempotent:
What we did here was using an equality chain. After the first = and the justification with by or from we don't add a semicolon but instead a .=. We repeat that until we reach what we wanted to reach, in this case (the last step Mizar infers from the idempotence of the union of sets). This is syntactical sugar, we could also just write:
But one form is easier to read than the other.
To see that the difference of sets is not symmetric, we prove a <> b implies {a,b} \ {a} = {b} and leave the other variant to the reader:
Exercise 5: Prove {a} \ {a,b} =.
Note that we only need the condition a <> b in the former statement. That is because, if we had a = b, then {a,b} = {a,a} = {a} (by ENUMSET1:29) and therefore {a,b} \ {a} = (by Ex4). Since we already know that {b} <>, we have proven that the set difference is not symmetric in general.
Note that the symmetric set difference is associative (XBOOLE_1:91).

## Ordered Pairs and the Cartesian Product

For this section, this will be the environment used:
The registrations XBOOLE_0; was commented on in the previous section. requirements BOOLE; ensures that Mizar automatically understands how the empty set interacts with the basic set operations from XBOOLE_0.
We noted in the previous section that {x,y} commutes, i.e. {x,y} = {y,x}. This is why {x,y} is also called an unordered pair. But there are many circumstances when we would want an ordered pair, such that [x,y] = [y,x] iff x = y. There are actually several ways to describe such a pair mathematically, but for now we will be satisfied with the fundamental one from TARSKI:
x = y implies [x,y] = [y,x] is understood by Mizar intrinsically. The other direction is given by the stronger:
We can now define the Cartesian product of two sets as follows:
[: X,Y :] is usually written as "X ⨯ Y" in mathematical notation, the pair [x,y] is usually written as "(x,y)" or "⟨x,y⟩". We can also define for example triples, quadruples (which is done in XTUPLE_0 and ZFMISC_1) and more, but pairs will be enough for a while.
To understand new definitions it is often helpful to see some simple examples.
Exercise 6: Prove [:{x},{y}:] = {[x,y]} (ZFMISC_1:29) using TARSKI:def 1 and ZFMISC_1:def 2.
We will use the next example to show how to write proofs with or:
Given a statement of the form P or Q we can use the per cases construct in combination with the keyword suppose:
It is also possible to exclude a case, like this:
When we want to prove a statement P or Q we can either do it directly as in the example above, if Mizar is up to it, or we can do it like this:
Exercise 7: Prove [:{x,y},{z}:] = {[x,z],[y,z]} based on the proof above.
The previous two statements can be found under ZFMISC_1:30.
It's also often a good exercise to see how something new interacts with something already known.
Exercise 8: Prove [:X \/ Y, Z:] = [:X, Z:] \/ [:Y, Z:]. This statement together with [:Z, X \/ Y:] = [:Z, X:] \/ [:Z, Y:] can be found under ZFMISC_1:97.
Exercise 9: Prove [:Z, X /\ Y:] = [:Z, X:] /\ [:Z , Y:]. This statement together with [:X /\ Y, Z:] = [:X, Z:] /\ [:Y, Z:] can be found under ZFMISC_1:99.
Exercise 10: Prove [:X \ Y, Z:] = [:X, Z:] \ [:Y, Z:]. This statement together with [:Z, X \ Y:] = [:Z, X:] \ [:Z, Y:] can be found under ZFMISC_1:102.
Note that a Cartesian product is empty if and only if at least one of its factors is (ZFMISC_1:90). Also note that the Cartesian product is neither commutative (cf. ZFMISC_1:110) nor idempotent (cf. ZFMISC_1:93).

## Subsets and the power set

For this section, this will be the environment used:
We have a couple of ways now to generate new sets from old ones. However, the only way we have to relate these sets to each other is via = and <>. Time to introduce the subset predicate:
Read as "X is a subset of Y". pred is short for predicate. X c= Y is usually written as "X ⊂ Y" or "X ⊆ Y" in mathematical notation. reflexivity means that X c= X always holds and that Mizar can recognize that. Again the reflexivity is pretty obvious from the definition when we replace Y with X.
The reflexivity is also indicating that a set is a subset of itself, which may sound a bit unneeded but does in fact help a lot with mathematical statements. If we want to exclude the reflexivity case, we can use the notation for a proper subset:
Read as "X is a proper subset of Y". X c< Y is usually written as "X ⊊ Y" or "X ⊂ Y" in mathematical notation. The reader will have noticed that "X ⊂ Y" can mean both, subset and proper subset. The difference depends on the author of the work one is reading and is usually cleared early on. irreflexivity means that X c< X can never happen and Mizar can recognize that. asymmetry means that X c< Y always implies not Y c< X.
An imminent property of the subset property is that the empty set is a subset of every set:
Mizar can recognize this immediately from the definition of the empty set and the subset predicate because it is vacuously true: for x being object holds x in implies x in Y is true because x in is false and we can follow anything from a false statement.
Another easy corollary of the subset predicate is the so-called "modus barbara":
Such a property is also called transitivity. Mizar can infer XBOOLE_1:1 from the definition of the subset predicate as well because the logical implies used in TARSKI:def 3 is also transitive (i.e. for three statements A,B,C we have (A implies B) & (B implies C) implies (A implies C)). Note that c< is transitive as well (XBOOLE_1:56).
Some more easy observations are X c= X \/ Y (XBOOLE_1:7) and X /\ Y c= X (XBOOLE_1:17). Add in the transitivity and we immediately get X /\ Y c= X \/ Z (XBOOLE_1:29). A slightly more difficult example would be XBOOLE_1:8:
Exercise 11: Prove Z c= X & Z c= Y implies Z c= X /\ Y (XBOOLE_1:19).
Two important statements are the Absorption laws: X c= Y implies X \/ Y = Y & X /\ Y = X (XBOOLE_1:12, 28):
Exercise 12: Prove X c= Y implies X \/ Y = Y (XBOOLE_1:12).
Exercise 13: Prove X c= Y implies X \ Z c= Y \ Z & Z \ Y c= Z \ X (XBOOLE_1:33, 34). For the second part you can use the fact that for statements P,Q holds (P implies Q) iff (not Q implies not P). Use that with TARSKI:def 3.
Exercise 14: Prove X1 c= Y1 & X2 c= Y2 implies [:X1,X2:] c= [:Y1,Y2:] (ZFMISC_1:96).
If you look close at the definition of the subset predicate, you will notice that it's very close to the equality of sets (TARSKI:2). And indeed:
redefine means that an existing attr, pred, mode or func (if properly imported via notations) is getting overwritten with an equivalent definition that might be more practical to use. It's very close to a simple theorem.
Another unary set operation is the power set, which contains all subsets of a given set:
where Z is reserved as a set. bool X is written as "P(X)" or "2$^X$" in mathematical notation. Its existence follows from the Tarski-Axiom. Observe ZFMISC_1:1:
As we have discussed earlier, this means that the power set of the empty set is not empty. The hereby construct is a placeholder for thus … where the … is the statement inferred from the keywords until the closing end;, so in this case … is x in bool implies x =. There is a variant without thus: now instead of hereby. In both cases you cannot use thesis to refer to the current statement to be proven.
Exercise 15: Prove bool { x } = { , { x }} (ZFMISC_1:24) using now and hereby.
Exercise 16: Prove A c= B implies bool A c= bool B (ZFMISC_1:67) using now and hereby.
As you can see, using now and hereby can make the code more compact. If this affects readability positively or negatively depends: It's especially good for short lemmata within a proof but less than optimal for very long lemmata.
Since the empty set and the original set itself are both a subset of the original set, the power set always contains those two elements. If the original set 'is' the empty set, those elements are the same. As a corollary, a power set is never empty.
Speaking of elements, it would be nice to have a type to specify something is an element of a set instead of writing for x being object st x in X. There is indeed such a mode, there is just one catch: modes must be inhabited, i.e. existence needs to be proven, but there is no element in the empty set! One way would be to define the mode only for non empty sets, but then many theorems would become more verbose. Instead, the MML gets around the problem by defining a default Element for the empty set:
So we end up with the situation where both not in and is Element of are true. Don't worry about it, the second variant basically never comes up. The if … otherwise construct is a convenient way to split up definitions. sethood means all instances of this mode form a set and can be used in Fraenkel operators (more about those in Relations and Functions).
A mode for subsets is defined in SUBSET_1 as well:
Note that the otherwise part of the definition doesn't come into play here because the power set is never empty. We also get the definition of proper subsets:
The equivalence between the Subset mode and the c= predicate as well as the Element mode and the in predicate are given via the SUBSET requirement.

## Exercise Solutions

Exercise 1:
Exercise 2:
Exercise 3:
Exercise 4:
Exercise 5:
Exercise 6:
Exercise 7:
Exercise 8:
Exercise 9:
Exercise 10:
Exercise 11:
Exercise 12:
Exercise 13:
Exercise 14:
Exercise 15:
Exercise 16: