3.2.2 Notation Section and Constructors Section

In case of making a new theory, we sometimes want to use an old concept. For example, suppose that we want to use the concept of Function or Function-like. At this time, since these terms are registered into a vocabulary file called FUNC.VOC, we add FUNC to the vocabulary section. Moreover, since these terms are defined in FUNCT_1 (MIZ or ABS file), we add FUNCT-1 to the notation section. And in many cases, we add FUNCT_1 also to the constructors section.

Example;

environ

vocabulary FUNC;

notation FUNCT_1;

constructors FUNCT_1;

begin

reserve X for Function;

theorem X is Function-like;

About the difference between the notation section and the
constructors section, there was only one item called the signature section
in the version of old MIZAR and both were unified. From there, relations
such as the hierarchic structure between concepts and the definition of
each concept were expanded by the memory of a computer. However, since
the former had many overlapping parts, it was separated for saving memory.
The former was inserted into the constructors section. Therefore, when
there was a file with more inclusive structure, we could omit the file
of smaller structure from the constructors section, and it came to be able
to perform saving of memory. For example, even if as follows instead of
the previous example, an error does not come out.

environ

vocabulary FUNC;

notation FUNCT_1;

constructors TOPREAL1;

begin

reserve X for Function;

theorem X is Function-like;

Therefore, when TOPREAL1 is contained in the constructors section beforehand, we don't have to insert FUNCT_1 there.

At first, we can insert a file name into both the notation
section and the constructors section in order, after completion, if a more
basic file is deleted from the constructors section, we can simplify the
environ section more, and we can also save memory.

In the notation 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 (part of definition)
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 (the latter is redefined). However, the method
of using that symbol is different.

< article BOOLE >

definition

let X,Y;

func X /\ Y -> set means

x c= it iff x in X & x in Y;

end;

< article PRE_TOPC >

definition

let TP, P, Q;

redefine

func P /\ Q -> Subset of TP;

end;

/\(same as ∩) in BOOLE means the set itself, and it has a set on the both
sides as an argument. On the other hand, it 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 notation section, and if we want it to be a Subset of TP, we have to write PRE_TOPC.