3.3　本体部

3.3.1　文

　次に本体部の説明をします．本体部は，基本的には文からなり，文の並んだものです．文は次のような構造をしています．


　　　　　L1:　A=B　　　　　by　··· ;
　　　　　L2:　B=C　　　　　by　··· ;
　　　　　L3:　A=C　　　　　by　L1,L2;
　　　　ラベル　式　　　　　　引用部


　ラベルは必要な文(後で引用する文)だけつけます．また，by···　 の部分を引用部といい，その式を導くのに必要な文のラベルを書きます．　引用部. by···　 では，その article 中のラベルと他の article からの引用のラベルを混ぜることができます.例えば,

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


というふうに,その article 中のラベルはそのまま，他の article からの引用の場合は，article 名 : 数字です．また定義を引用する場合，article 名 :def　数字です．
　さらに，引用部の代わりに，

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


というふうに，proof〜end ではさんだいくつかの文で証明をつけることもできます．この場合，これ全体で1つの大きな文とみなせます．このとき，proof 〜 end の end の直前には thus もしくは hence という文を必要とします．これは，いま証明を付けている最初の式がこの文の式によっていえています，ということです．thus と hence の違いですが，hence は then + thus になっています．
　then はここではじめて出てきましたが，直前の式を引用するときに使います．例で説明すると，

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

となっているとします.このときに,

　　　　L3:A=C by L1,L2;

と書く代わりに，L2 の式は直前の式ですから，L3 の文の引用部から L2 を取り除いて，then を使って，

　　　　then L3:A=C by L1;

と書くことができます．
　then を使う理由には，ラベルの数をなるべく減らそうということがあります．ふつう証明では直前の式を引用することが非常に多くあります．直前の式を引用するときにも，ラベルをつけて，by ラベルとすると，たくさんのラベルを必要とします．ですから，直前の式を引用するときはラベルを使って書く書きかたも間違いではありませんが，then と書いた方が良いわけです．

　また，article を Mizar ライブラリに登録するときに使う article の改良のためのチェッカー (Chapter??参照) でチェックするときに，証明は正しくても上記のラベルを使って書く方式は，皆エラーになってしまいます．そのエラーがある限り，Mizar ライブラリには登録させてもらえませんから，結局のところ書いてはいけないということです．then が使えるときにはラベルを使わないで then を使います．このため，proof 〜 end の end の直前の文で，その直前の式を引用するときは hence を使います．