A Practical Guide To Mizar/The Environment

The environment of a Mizar article is in a sense the most difficult part to get right. That's why sometimes authors just copy the environment of existing articles and modify them to their needs.

The keywords under environ are called environment directives and their order is not specified by the Mizar Syntax. But there is a tradition of keeping to the following order:

• vocabularies
• notations
• constructors
• registrations
• requirements
• definitions
• equalities
• expansions
• theorems
• schemes

As seen in Installation none of these are mandatory for an article, but you are very likely to use the first five ones as well as theorems and sometimes schemes. definitions, equalities and expansions are basically syntactic sugar.

All articles listed behind an environment directive are written in ALL CAPS, separated by , and the directive ends with a ;.

Besides the Mizar keywords there are a lot of words that can have a certain meaning in your article, called symbols. They are kept in .voc files (which are plain text) associated with articles. For example, the tarski.voc looks like this:

Rc=
Ounion 128
Rare_equipotent

Note that each symbol in the file is prefixed with a single letter that indicates the type of the symbol and the symbol after O can be followed by a number. We will get into that later. For now recognize that this means the vocabulary of TARSKI consists of the three words c=, union and are_equipotent (without the prefix letters or the suffix number). To use the words in your article (devoid of any meaning for now), write:

environ
 vocabularies TARSKI;

begin

Since vocabularies only denotes the symbols to be imported without meaning attached to them, it is not uncommon to have articles in your vocabularies directive that don't show up in any other directive. For example, SEMI_AF1 has sum in its vocabulary, a very basic symbol. If you are not interested in Semi-Affine Spaces, you will never see it in any other directive.

Any symbol is defined in exactly one vocabulary file, so sometimes you need to search where the symbol you want to use comes from. Luckily, Mizar has a command for that: findvoc myvoc lists all articles that have a symbol containing the string myvoc, with that symbol written out. findvoc -w myvoc looks for a symbol myvoc and will return at most one article. For more options, execute the command findvoc. For example, findvoc -w sum has an output like this:

FindVoc, Mizar Ver. 8.1.14 (Linux/FPC)
Copyright (c) 1990-2023 Association of Mizar Users
vocabulary: SEMI_AF1
Osum

findvoc is case-sensitive.

To get all symbols defined in a vocabulary file, the listvoc myarticle command can be used. For example, listvoc HIDDEN has an output like this:

List of Vocabularies, Mizar Ver. 8.1.14 (Linux/FPC)
Copyright (c) 1990-2023 Association of Mizar Users
Vocabulary: HIDDEN

Mobject
R<>
Rin
Vstrict

listvoc is case-insensitive, i.e. listvoc myarticle returns the same as listvoc MYARTICLE.

HIDDEN is, as the name implies, hidden and does not need to be included in your vocabulary directive ever, because it is automatically there.

The notations directive is what gives the symbols imported with vocabularies meaning. If the mathematical notation you want to use is defined in an article, that article is included in notations. If you want to use the c= notation from TARSKI for example, your code might look like this:

environ
 vocabularies TARSKI;
 notations TARSKI;

begin

However, running mizf text/test now reports an error:

Make Environment, Mizar Ver. 8.1.14 (Linux/FPC)
Copyright (c) 1990-2023 Association of Mizar Users

-Vocabularies  [   2]
-Constructors  [   1]
-Requirements  [   1]
-Registrations [   1]
-Notations     [   3 *1]

**** 1 error detected

Your Mizar article now looks like this:

environ
 vocabularies TARSKI;
 notations TARSKI;
::>             *830

begin
::>
::> 830: Nothing imported from notations

Mizar is complaining that apparently no notation from the cited article is used in yours. You can get rid of that error by adding the cited article to constructors as well. Some authors just put everything they put in notations also in constructors, but this behavior is discouraged, as it is often not needed.

The following article compiles again without errors:

environ
 vocabularies TARSKI;
 notations TARSKI;
 constructors TARSKI;

begin

HIDDEN is included automatically.

The theorems directive is filled with all articles from which you use theorems with the by keyword, like TARSKI:1 or TARSKI:def 1. So your article could look like this:

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

begin

for x being object holds x is set by TARSKI:1;

This article compiles. It will not if you leave theorems TARSKI; out of it.