3.2.4 definitions部

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

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

よって,definitions 部に TARSKI と書いておけば x c= y を証明するとき,
a in x implies a in Y をいってしまえば x c= y が証明されたことになります.
 例,


     
 theorem X c=X \/ Y
       proof let x be set;
            assume  x in X;
          hence y in X \/ Y by BOOLE:def 2;
          end: