説明不足だが大事な用語
- 記述書式（format） 述語や関数を呼び出すときの記述形式、定義時に指定する。
- 座（ローカス、ローサイ）（locus, loci） 述語や関数のパラメータ宣言
- パターン 記述書式と関係あるようだが現在は不明
Mizarでは公理と定理の区別がなく、すべて定理：
- 公理定理： 証明なしで認める定理
- 定義定理： 述語定義から自動的に生成される定理。by definitionの根拠（justificatio）となる定理。
- 証明付き定理： proofブロックで正当化（justify）された定理
