Chapter 2

Mizar言語の概要

 Mizar 言語は,コンピュータを使って数学の証明を記述するための言語です.普段,証明を書くときに証明の書き方にしたがって書くように, Mizar article を書くときには Mizar 言語で書かなければなりません.以下では Mizar 言語をMizarと略します.
 Mizar では一般的なアスキーコードを使用します.通常使用する文字は,数字, 英字, 記号です.また,数学の記号を一般的なアスキーキャラクタを組みあわせたり,似たものを使うものもあります.
 また, Mizar では, 英字の大文字と小文字は区別されることに注意してください.但し, article 名など, MS-DOS のファイル名になっているものを article 中に記述する場合, 必ず大文字で書きます.この場合8文字までの英大文字,数字,_, ' で書きます.
 数学の証明を書くときに, 'したがって', '定理', '定義', '証明終り' などの言葉を使うように, Mizar でもそれに対応する言葉を使って記述します.これらの言葉は予約語になっています.Mizar のシステムとして, &, or, not の論理, = の概念, All, Exist の述語論理は最初から備わっています.さらに, Mizar では自分の論文 (article) に, Mizar ライブラリから自由に functor (関数記号) ,predicate (述語論理)などの定義, 定理を引用し証明を進めていきますが, その基本となるものが HIDDEN.ABS に書かれています.ここに書かれていることは, それを公理として証明なしで認めています.それを引用してさまざまな定理が導かれていて Mizar ライブラリを構成しています.ユーザーが新たに article を書く場合,最初からシステムに備わっている論理や,TARSKI などをもとにして出来ているたくさんの定理を引用して記述していきます.
 ユーザーが新たに functor 函数などを定義する場合,その functor などを vocabulary file に登録し,article の中で functor を定義します.この場合,予約語とまったく同じ名前の functor は定義することはできません.具体的な定義のしかたについては第6章 定義で説明します.また, 付録に Mizar 予約語一覧表がありますので参照してください.
 Mizar のシステムに備わっている論理式と述語論理について説明します.Mizar では基本的な論理式, &, or, not, implies, iff を使うことができます例えば, &

  A & B
  A = B & B = C impliesA = C
  A & ( B or C ) iff A & B or A & C


と.書くことができます.& は論理式の中の場合 & を使い,式と式との関係の場合 and を使いますまた, implies は’ならば’, iff は if and only if ’同値’,を表します. 述語論理ですが,次のように全称記号と存在記号を使うことができます.

            for x st f[x] = b holds g[x] = c;

これは, 通常の述語論理の記法では次の式を表します.

             

これは, 任意のxについて, ƒ(x) = b ならば g (x) = cという意味です.ƒ(x)= b を満たすような, すべてのxについて g (x) = c が成立するということです.
 なお, f[x], g[x]とはxを含んだ述語ということで,こういう記法がシステムに備わっているわけではありません.
 次に,
               ex x st f[x] =b & g[x] =c ;
と書くとこれは,

            (∃x)(f (x) =b and g (x) =c )

を意味します.つまり ƒ(x) = b かつ g (x) = cとなるxが存在するという意味です.また, 全称記号と存在記号を混在して使うこともできます.

          for x ex y st f[x] = a & h [x] = i [y]

これは,

          

を表します.
 括弧は任意に使うことを許されています.たとえ括弧が必要ないときでも, わかりやすくするために括弧を使うことができます.
 なお,Mizar のシステムには,MS-DOS 版と Linux 版があります.さらに本質的にはLinux 版なのですが,Web ページから自由に使えるものもあります.