3.2 環境部

まず環境部について説明します．環境部には，その article で必要な環境設定を行います．具体的にはその article が引用する定義，定理，または vocabulary がある article のファイル名を書き宣言します．

環境部は次のような項目からなっています．

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

環境部の中のそれぞれの項目について説明します．

3.2.1 vocabulary部

vocabulary部には， articleの中で使われている vocabulary の登録されている vocabulary file（.VOC ファイル）のファイル名を大文字で書きます．ファイル名の拡張子は省略し，複数の vocabulary file を書く場合は，, で区切って書きます(HIDDEN.VOC に登録されている vocabulary については，vocabulary部に書かなくても使うことができます.) 行末には，セミコロンを書きます．また，vocabulary部以外もこれと同様に書きます．

Mizar ライブラリに登録されている article で使用されている vocabulary が登録されている vocabulary file は，1つの特殊な形式のファイルにまとめられています.

使用する vocabularyが登録されている vocabulary fileを探すには，

FINDVOC [vocabulary]

とします．また，vocabulary file に登録されている vocabulary を表示するには，

LISTVOC [vocabulary]

とします.

3.2.2 signature部

signature部には，vocabulary ファイル中に書いたシンボルを使用したい場合，そのシンボルが定義されている article のファイル名を ここに書いておきます．article の定義部（definitionの部分）では，そのシンボルの意味付けがなされています（どういうアーギュメントをいくつ持つのか，そのシンボル自身がどういうモードになるのか等).

例えば，article BOOLE と PRE_TOPC にはどちらにも ∩（インターセクション）が定義されています．しかし，そのシンボルの使われ方が異なっているのです．

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

BOOLE での ∩ は，それ自身 set を意味し，アーギュメントとして set を両側に持ちます．それに対して PRE_TOPC でのそれは，自分自身を TP （トポロジカルスペース）の Subsetとし，アーギュメントとして TP の Subset を両側に持ちます．

∩ を使った article をこれから書こうとする場合，それを set として使用したければ signature部に BOOLE と書き，TP の Subset としたければ PRE_TOPC と書かなければいけません.

3.2.3 definitions部

definitions部では，証明をする際の定義の拡張，証明の飛躍（definitional expansion）を可能にしたい場合に，その定義がなされてある article のファイル名を書きます． 例えば, X c= Yを証明するとき，∀a(a∈X implies a∈Y) を証明すればよいのですが，この定義は article TARSKIの中に以下のように定義されています．

pred X c=Y means x∈X implies x∈Y;

よって，definitions部に TARSKIと書いておけば， X c= Y を証明するとき，a ∈X implies a∈Y をいってしまえば X c= Y が証明されたことになります．

3.2.4 theorems部

theorems部では，articleに引用する定理，定義が書かれている articleのファイル名を書きます．

3.2.5 schemes部

schemes部では，引用するスキーム（証明の型）の書かれている article のファイル名を書きます．