Getting to know the Mizar Mathematical Library

Question

I want to do some formalization of mathematics using Mizar. From their Bibliography site I have read "Writing a Mizar article in nine easy steps" by F. Wiedijk (very good for the basic understanding) and "Mizar in a Nutshell" by A. Grabowski, A. Kornilowicz and A. Naumowicz (for deeper understanding and very useful as reference book). So I know have some understanding how to get the semantics right. However, as Wiedijk wrote in his manual:

The most difficult part of writing Mizar is finding what you need in the MML which is the name of the Mizar Mathematical Library. Unfortunately that problem has no easy solution. You will discover that apart from that, writing a Mizar article is straight-forward.

I basically want to get used to working with the MML, but I don't exactly know where to start? There are over 1300 articles as of yet, and while this shows a tremendous amount of work towards the QED manifesto, I cannot be expected to read them all, now can I? I know of the MML Query tool, but it seems to take queries in yet another language which doesn't seem as intuitive as the Mizar language. Also I don't see how it would help me understanding the MML. I haven't studied it deeper yet.

Answer 1

I have worked with Mizar for over two years now and studied it basically on my own (with the help of your mentioned references as well as getting answers to occasional questions about errors I couldn't grasp answered by the very helpful Mizar User Service (see)). I'm about to submit my forth article to the MML these days and when I started I encountered similar problems like the ones you described. As far as I know, there is no introduction to the MML yet, so I'll do my best to write something up.

First of, on a historical note, all issues of Formalized Mathematics, the journal where the abstracts of Mizar articles are published, are available online. If you read it in chronological order (at least the start issues, I mean), you would get a feeling of how the MML was built from the ground up. I found that very interesting.

However, the MML has been revised over time, if not evolved. Most notably, a lot of facts given in the article AXIOMS have originally be built in as true axioms, mainly so people could get some "real" mathematics formalized, but have been removed from their axiomatic nature since then and instead constitute theorems today. Many theorems were also moved so the article is a lot shorter today. For more on the history, see here.

To the present. In your Mizar distribution there is a file of the name mml.lar. You can open that file with any text editor, just make sure not to accidently change its content. In this file, the articles of the MML are listed one under another in the order they are "read" into the system. So any article can only depend on those above it, never on those below. So it's save to say you can read the first say 40 articles to get an understanding of the current foundation of the MML. The GATES_ series, in my version starting from line 41 are the first I would savely consider "unimportant" unless you want to work with gates. Most of the articles before that are often important, sometimes not, but it's good to know they are there. I was surprised once to get to a point where I needed to prove that $x\in y\in z\in x$ isn't possible and if I had remembered XREGULAR at the time, I could have solved it much faster.

I will now highlight some articles and selected content of it which frequently turned up in my work and I consider generally important. On that note let it be said there is a MML Query site about most used theorems, which are most used for a reason. You will do well looking these up on the HTML-linked articles. But now to the highlights!

The set-theoretic articles

• TARSKI: While axiomatic, it provides the single most cited "theorem" by a large margin: the definition of $X\subseteq Y$. Also present: the definitions of $\{x\}$ (second most cited), $\{x,y\}$ (rank 22), $\bigcup X$ (rank 24), $(x,y)$ (ordered pair) as well as the extensionality axiom ($X=Y \Leftrightarrow \forall x:x\in X \Leftrightarrow x\in Y$) and the set cast (every object is a set).
• XBOOLE_0: Contains the definition of the empty set as well as boolean operations between sets, e.g. definitions of $X\cup Y$, $X\cap Y$, $X\setminus Y$, $X\triangle Y$ (symmetric difference), $X\subsetneq Y$
• XBOOLE_1: Contains many theorems about the operations introduced in XBOOLE_0, e.g. $X\subseteq Y\subseteq Z\Rightarrow X\subseteq Z$, $\emptyset\subseteq X$, distributive laws, $(X \cap Z) \setminus (Y \cap Z) = (X \setminus Y) \cap Z$ etc.
• SETFAM_1: Contains the notion of Subset-Family (as a non-indexed set of subsets of a given set) and the definition of $\bigcap X$ (in two variants for the case that $X=\emptyset$)
• ZFMISC_1: Contains definitions of the power set $\mathcal{P}(X)$ and the cartesian product $X\times Y$. Also many facts regarding singleton or unordered (e.g. $\{x\}\subseteq X\Leftrightarrow x\in X$ (ZFMISC:31)).
• XTUPLE_0: Definition of (ordered) triples and quadruples and how to get the elements/coordinates from them as well as from the pairs (i.e. projections). If you happen to need this, looking into MCART_1 may be helpful, too.
• ENUMSET1: If singleton and unordered pairs are not enough, this article contains definitions for explicit sets for up to 10 elements as well as a lot of statements about them like $\{x,x\}=\{x\}$ (ENUMSET1:29) or $\{x,y,z\}=\{x,z,y\}$ (ENUMSET1:57)
• PBOOLE: Contains the notion of a family of sets (called ManySortedSet) or functions (called ManySortedFunction) (as indexed sets/functions, i.e. they are functions defined on some index set mapping to sets/functions, so this one already builds on some of the function articles below) and also the appropriate operations between them ($\bigcup_{i\in I} X_i, \bigcap_{i\in I} X_i$, etc.)
• WELLORD2: Defines equipotence between sets (i.e. $|X|=|Y|$ as a direct predicate rather than the equality of two cardinalities) using a function, being a more practical definition than the original one in TARSKI
• ORDINAL1: Defines ordinal numbers in general and $\omega=\mathbb{N}_0$ specifically. By default Mizar makes a distinction between the modes Nat and Element of NAT and ORDINAL1:def 12 (definition of the attribute natural) often proved to be helpful for me to kindly remind the system that both are one and the same.
• CARD_1: Defines cardinal numbers as well as the cardinality of a set and holds many theorems regarding it. The notion of an $n$-element set is given here as well. Also check out FINSET_1, which deals with finite sets.
• TOPGEN_3: Contains the cardinalities of $\mathbb{Z}$ and $\mathbb{Q}$. Since $\omega=\mathbb{N}_0$ is a cardinal, and the cardinality of a cardinal is itself (shown in CARD_1), it is not explicitly mentioned. The cardinality of $\mathbb{R}$ is defined as continuum and shown to be equal to $|2^{\mathbb{N}_0}|$, (TOPGEN_3:29) therefore strictly greater as $\omega$ (TOPGEN_3:30).

Articles regarding numbers

If you need numbers, you should definitely search for `arytm_3` in `mml.lar` and skim through the next ~30 articles related to that. Searching for "definition" within the article will give you a feeling what's the foundation of numbers in Mizar. Be aware that a proper `requirements` in your article's `environ` can spare you from a lot of citations like $1\neq 2$. I'll now proceed to mention articles out of that scope or of special interest.

• The last three articles of the previous section would also fit in this section, as they introduce $\mathbb N$, show that the numbers are built up like von Neumann did (see CARD_1:49 ff.) and prove the cardinalities of the usual number sets. ORDINAL1 also introduces the attribute zero. The natural numbers in Mizar include zero, so a natural number possibly being $0$ is e.g. instanciated with let n be Nat, a natural number not being $0$ with let n be non zero Nat.
• ORDINAL2: Introduces ordinal arithmetic (+^ for $+$ and *^ for $\cdot$), which therefore can be used for natural numbers, although one usually uses + and * defined later for all complex numbers (henceforth called "basic operations"). ORDINAL2 comes about 20 lines before ARYTM_3, hence the special mention to understand how the numbers are built up.
• NUMBERS: Introduces $\mathbb{Q}$ and $\mathbb{R}$ based on $\mathbb{Q}_{\geq 0}$ and $\mathbb{R}_{\geq 0}$ introduced in the ARYTM_ series, as well as $\mathbb{Z}$, $\overline{\mathbb{R}}=\mathbb{R}\cup\{-\infty,+\infty\}$ and $\mathbb{C}$, and proves their (proper) inclusion chain, also in regard to $\mathbb{N}_0$.
• XCMPLX_0: Definition of the imaginary number $i$ (as <i>) and the basic operations. The operations will be redefined in subsequent articles, so Mizar knows that i.e. $n+m$ is a natural number (instead of just a complex one) when $n$ and $m$ are natural numbers.
• XCMPLX_1: Rules regarding basic operations, like $(c - a) - (c - b) = b - a$ (XCMPLX_1:23).
• COMPLEX1: The usual additional operations on complex numbers like $\Re(z)$, $\Im(z)$, $|z|$ etc.
• XXREAL_0: Definition of Elements of $\overline{\mathbb{R}}$, $-\infty$, $+\infty$ and the very, very important statements $a\leq b \land b\leq a \Rightarrow a=b$ (XXREAL_0:1) and $a\leq b \land b\leq c \Rightarrow a\leq c$ (XXREAL_0:2). These are so very important because you will not find variations of this in the MML. $a\leq b \land b < a$ can be shown to lead to a contradiction using XXREAL_0:1. $a\leq b \land b < c \Rightarrow a < c$ can be shown by XXREAL_0:2. Mizar is clever on how to use these two theorems and you need to know that before you try to find a substitute or prove it yourself.
• XREAL_0: Lots of clustering and redefinition, but $\max(a-b,0)$ is introduced as its own operation -', which becomes quite important when dealing with substraction of natural numbers.
• XREAL_1: Any inequality regarding real numbers and the basic operations.
• SQUARE_1: Definition of the square and the square root and their properties.
• ABSVALUE: Definition of $|x|$ and basic properties.
• NAT_1: Proof by Induction, Principle of Minimum, some properties of naturals, e.g. $\forall i,j\in\mathbb{N}_0\exists k\in\mathbb{N}_0:i\leq j\Rightarrow j=i+k$ (NAT_1:10).
• NAT_D: Divisibility of naturals, $\mathrm{div}$ and $\mathrm{mod}$.
• INT_1: Induction over integers, divisibility of integers, rounding up and down, some properties.
• INT_2: $\mathrm{lcm}$, $\gcd$, prime numbers.
• RAT_1: Concept of smallest integer numerator and denominator.
• ABIAN: Even and odd integers.
• NEWTON: $z^n$ with $z\in\mathbb{C}$ and $n\in\mathbb{N}$, $n!$, $\binom{n}{k}$. If you want to go deeper into number theory, I think the NEWTON series is a must read. Beyond that, I don't know.
• PREPOWER and POWER: $a^b$ for both real, $\sqrt[n]{a}$ for $n$ natural and $a$ nonnegative if $n$ is even, logarithm for reals, Euler's constant $e$.

Articles about relations and functions

Depending on your mathematical upbringing, maybe you haven't done much with relations except for equivalence relations. Let it be said that functions can be viewed as a special kind of relations and are exactly introduced that way in Mizar. The FUNCT_ series is worth completely reading in any case, but I'll highlight as usual.

• RELAT_1: Definition of a relation as a set of pairs. There doesn't have to be a specific superset $X\times Y$, the definition is sparse (and that is good). Since a lot of properties of functions also hold for relations, you should always check this article if you didn't find what you searched for in the FUNCT_ series. E.g. the domain and range* of relations is defined here and only the range gets a redefinition later in FUNCT_1. Also the composite of relations is defined here, so is the theorem $P\circ(Q\circ R)=(P\circ Q)\circ R$ (RELAT_1:36). Beware that in FUNCT_1 the order $f\circ g$ is switched to $g\circ f$, you have to keep that in mind when looking for composition-related theorems of functions in RELAT_1. Examples for pre-function definitions: Let $f$ be a Relation, then we have $f(A)$ as f.:A, $f|_A$ as f|A, $f^{-1}(A)$ as f"A. *range is defined in XTUPLE_0 as proj2 and just given a synonym in this article in the context of relations.
• FUNCT_1: Definition of a function as a special relation, (re)definition of closely related concepts (from RELAT_1), e.g. $f(x)$ as f.x (because we need the brackets for our functors in Mizar). Injectivity introduced as one-to-one as well as constant functions. One should note FUNCT_1 provides the neccessary schemes to construct your own functions.
• RELSET_1: Relations of $X,Y$ as subsets of $X\times Y$.
• PARTFUN1: Partial Functions of $X,Y$ as relations of $X,Y$ (from RELSET_1), which are also functions (from FUNCT_1). Introduction of f/.x which is basically f.x (i.e. $f(x)$) with the difference that, by default, f.x is seen as a set (since for a mere function in the sense of FUNCT_1 we don't know anything about its range), while f/.x is already seen as an Element of $Y$. This is one of the type casts in Mizar, which comes in handy sometimes. Try to use it only when needed, as it clutters proofs.
• FUNCT_2: Function of $X,Y$, which are basically total partial functions of X,Y. Also defines surjectivity as onto and $Y^X$ (set of functions from $X$ to $Y$).
• RELAT_2: Many properties of relations: (ir)reflexivity, (a/anti/-)symmetry, transitivity, being (strongly) connected.
• EQREL_1: Equivalence relations.
• ORDERS_2: Relational structures. If you want to dive deeper on this, pay special attention to the WAYBEL_ and YELLOW_ series.
• FUNCOP_1: Introduction of e.g. constant functions, but not by attribute (as in FUNCT_1), but by explicit creation, e.g. "Let $f\equiv a\in\mathbb{R}$ be defined on $\mathbb{R}$" translates to let a be Real; set f = REAL --> a;. I have found this most useful, but you should check out the other definitions in the article to, may become relevant. Explicitly worth noting is the IFEQ(x,y,a,b) functor.
• FUNCT_4: Given $f,g$ being functions, define $h$ by $$h(x)=\left\{\begin{matrix}g(x)&\mbox{if }x\in\mathrm{dom}\, g\\ f(x)&\mbox{else}\end{matrix}\right.$$ for $x\in\mathrm{dom}\, f\cup\mathrm{dom}\, g$. This is defined in this article by f +* g and most useful to built functions given other functions, which avoids using schemes from FUNCT_1 or FUNCT_2 and making the proofs therefore more readable. There is another version in FUNCT_7 which just changes one point of $f$.
• CARD_3: Definition of $\prod_{i\in I}A_i$ and the corrosponding projection besides other things. To be more precise, the product set of an arbitary function is defined, but when everything is a set, then every function is a set family indexed by its domain.

I think that concludes the basics. To be fair, I hadn't expected over 40 article myself, but it is much less than it sounds like. Most of the time, theorems encode obvious properties. If you only read the abstracts, i.e. the theorems without the proofs, you may have to translate one or another definition into what you are used to deal with, but besides that you will get really fast through the articles. And I don't really expect you to read through all of XREAL_1 for example. As you said, this is just to get familiar with the MML, not to remember every theorem. You will use grep or the MML Query for that (try Mizar(keyword) as a query, with keyword replaced by whatever troubles you).

Other articles of interest

- FINSEQ_ series: Finite sequences, i.e. ordered pairs, triples, quadruples, etc. but not explicitly up to a certain number like XTUPLE_0, but for arbitrary length, since they are given as functions (instead of simple sets) - SEQ_ series: Real (infinite) sequences. - SERIES_ series: Real series. - FCONT_ series: Continuous functions on $\mathbb R$. - FDIFF_ series: Differentiable functions on $\mathbb R$. - INTEGRA series: Integratable functions on $\mathbb R$. - MATRIX_ series: Matrices, building on top of finite sequences.

Note that some articles may start with an R or C to indicate they deal with $\mathbb R$ or $\mathbb C$, e.g. the RFUNCT_ series, CFDIFF_ series etc. Be sure to also check out the VALUED_ series and RVSUM_ series. Graphs are formalized several times, I would encourage you to go with GLIB_ (because I'm extending it). When you are going for any kind of structure (relational, group, field, vector space etc.) read STRUCT_0 and possibly ALGSTR_0. Topology starts with PRE_TOPC, but then scatters over the MML, you can find it in BORSUK_, BROUWER, JORDAN_, GOBOARD, T_0TOPSP, TEX_, TOPALG_, TOPGEN_, TOPREAL_, TOPS_, TSEP_, WAYBEL_, YELLOW_ and more. Mannifolds in MFOLD_. For vector spaces see VECTSP_ and RLVECT_ series. Measure theory starts with MEASURE and MESFUNC. Groups in GROUP_, ring in RING_ are further obvious example. Some are somewhat hidden, of course (binomial coefficients in NEWTON, complete graphs in CHORD), but with time and grep you will find them as well. I think the most difficult part is understanding where the MML starts, anyway.

When in doubt about something unknown you encounter, consult the HTML-liked articles and click yourself to the defintion, that is usually faster than backtracking the defintions through the notations file or grep.