Mizar/構文

書き方

集合論から全ての証明を行っているので、『A→B』 の証明をするには、以下の書き方をする

environ

begin
 for A,B being set st A holds B
proof
 let A,B be set;
 assume A1: A;
 thus B by A1;
end;

証明のトートロジーより『A→B』と同値なものとして、『￢A∨B』が得られる。

この処理系では正しいことを『１』、正しくないことを『０』とします。 従って、処理系の内部では、上記の処理は以下の処理のように取り扱われる。

{A,B⊂集合|A→B}
証明
 A,B⊂集合
 ￢A ∨ B

型と書式の確認をした後で、

A=1,B=1;
not(A) and B;

の処理を行い。

0 and 1

の結果は

1

となり、正しいということになる。 だから、『assume』は英訳では仮定なのだが、Mizarの処理系では『not』となり、 『thus ～ by ラベル』 は 『ラベル and ～ 』となる。