3.2 Environment Section

We will first explain the environment section. In the environment section, the necessary environmental set up for an article is conducted. Specifically, we write definitions, theorems, and vocabularies that the article phrases, and declare file names of the article that have them.

The environment section is constructed of the following items.

environ
vocabulary ...;
signature ...;
definitions ...;
theorems ...;
schemes ...;

We will explain each item in the environment section.

3.2.1 Vocabulary Section

In the vocabulary section, we write the names of the vocabulary files(.VOC file) that are registered and used in articles with capital letters. We omit the extension unit of a file name, and when writing many vocabulary files, we write by using commas (for vocabularies that are registered in HIDDEN.VOC, we can use them without writing them in the vocabulary section). At the end of sentences, we write semicolons. Also, we write the same way with places other than the vocabulary section.

The vocabulary file that has registered vocabularies that are used in an article registered in the Mizar library is summed up in a special file.

To look for the vocabulary file that has registered vocabularies that we want to use, we write the following.

FINDVOC [vocabulary]

Also, when we want to indicate vocabularies that are registered in the vocabulary file, we write the following.

LISTVOC [vocabulary]

3.2.2 Signature Section

In the signature section, when we want to use symbols written in the files, we write the file names of articles that have those symbols defined. In the definition section of an article, those symbols' meanings are added (things like what kind of argument they have and how many, or what kind of modes they themselves become).

For example, (intersection) is defined in both of the articles BOOLE and PRE_TOPC. However, the method of using that symbol is different.

definition definition
let X,Y;
let TP,P,Q;
func XY -> set means
redefine
x c= it iff x C X & x C Y;
func P Q -> Subset of TP;
end; end;
article BOOLE article PRE_TOPC

in BOOLE means the set itself, and it has a set on the both sides as an argument. On the other hand, in PRE_TOPC makes itself a Subset of TP(topological space), and it has Subsets of TP on both sides as an argument.

From now on, when we want to write articles using , if we want to use that as a set, we write BOOLE in the signature section, and if we want it to be a Subset of TP, we have to write set PRE_TOPC.

3.2.3 Definitions Section

In the definitions section, when we want definition extension and expansion possible, we write file names of articles that have their definitions. For instance, when demonstrating X c= Y, we just need to demonstrate Va(aCX implies aCY); however, this definition is defined in the article TARSKI as below.

pred X c=Y means xCX implies xCY;

Therefore, if we write TARSKI in the definitions section, when we demonstrate X c= Y, it means that we demonstrated X c= Y if we can say that aCX implies aCY.

3.2.4 Theorems Section

In the theorems section, we write the file names of articles with theorems and definitions for citing articles.

3.2.5 Schemes Section

In the schemes section, we write the file names of articles that have phrasing schemes (demonstration form) written.