3.3　The Main Section

3.3.1　Sentences

Next, we will explain the main section. The main section basically consists of sentences and their line up. Sentences have the following structure.

        L1:　A=B　　　　　by　··· ;
        L2:　B=C　　　　　by　··· ;
        L3:　A=C　　　　　by　L1,L2;
      Label Formula  Citation Section

    We will attach only the necessary sentences (sentences that will be cited later) to labels. Also, we call by ... a citation section, and write labels of sentences that are necessary to lead that formula. In the citation section, by ... , we can mix labels in an article and cited labels from other articles. For example, labels in that article are untouched and when citing from other articles, we write a name of an article : a number as shown below.

　　　　 ·········　by L1,L2,TARSKI:5;


Also, in case of citing a definition, we write a name of an article : def a number.
    Moreover, for proof ∼ end, instead of the citation section, we can add a demonstration with some sentences like the following.

        L3:　　A=C
        proof
         ···
         ···
        hence thesis;
        end;


In this case, all of these are considered as one sentence. At this point, end in proof ∼ end needs thus or hence just before it. It means that this can be said about the first formula that has a demonstration attached currently by this sentence's formula. Concerning the difference between thus and hence: hence takes the form of then + thus.
    Even though then has appeared here for the first time, it is used when a formula stated before is cited. To explain with an example, let us assume the following.

        L1:A=B by　··· ;
        L2:B=C by　··· ;

At this point, instead of writing the following, because L2 formula is a formula stated before, we will take L2 away from the citation section of L3 sentence.

        L3:A=C by L1,L2;


    By using then, we can write the following.

        then L3:A=C by L1;


The reason why we use then is because we want to minimize the usage of labels. Normally with demonstrations, we often cite formulas stated before. Also, when citing formulas from the one stated before, we will need many labels if we attach labels and state by label. However, by using then here, we will not need to use labels when citing formulas from the one stated before. Therefore, we can reduce the number of labels. Thus, when we want to cite formulas from the one stated before, even though it is not wrong to write by using labels, it is better to use then.
    In addition, when checking with a checker (explained in Chapter 7) for improving an article used for registering in the Mizar library, everything will return an error if we write with the method of using the above labels even though the demonstrations are right. As long as that error exists, it will not be possible to register in the Mizar library. Therefore, it should not be written. Where then can be used, it should be used instead of labels. Because of this, hence should be used for citing formulas just before the end of proof ∼ end.