Chapter 2

Mizar言語の概要

Mizar言語は，コンピュータを使って数学の証明を記述するための言語です．普段，証明を書くときに証明の書き方にしたがって書くように，Mizar article を書くときには Mizar言語で書かなければなりません．以下では Mizar言語を Mizar と略します．

Mizar では一般的なアスキーコードを使用します．通常使用する文字は，数字，英字，記号と，0 ，≦　など一部の拡張文字 (拡張文字とは，アスキーコード128以上の文字を言い，ALT-keyを押しながら，そのアスキーコードをテンキーで入力することにより入力することが出来ます．付録にアスキーコード表がありますので参照してください.)です. また，数学の記号を一般的なアスキーキャラクタを組みあわせたり，似たものを使うものもあります．

記号 Mizarでの表記法
⊆ c=
c ‘
∪ U
Ω [234]
0 [237]
∈ [238]
∩ [239]
≦ [243]
≠ <>

また，Mizarでは，英字の大文字と小文字は区別されることに注意してください．但し，article名など，MS-DOSのファイル名になっているものを article中に記述する場合，必ず大文字で書きます．この場合8文字までの英大文字，数字,＿,' で書きます．

数学の証明を書くときに，'したがって'，'定理'，'定義'，'証明終り' などの言葉を使うように，Mizarでもそれに対応する言葉を使って記述します．これらの言葉は予約語 になっています．Mizarのシステムとして,&,or,not の論理， = の概念，All，Existの述語論理は最初から備わっています．さらに，Mizarでは自分の証明（article）に，Mizarライブラリから自由に functor（関数記号），predicate（述語論理）などの定義，定理を引用し自分の証明を進めていきますが，その基本となるものが TARSKI.ABS，AXIOMS.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 implies A = 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) (f(x) = b ⇒ g(x) = c)

これは，任意のxについて，f（x）=b ならば g（x）=c という意味です．f（x）=bを満たすような，すべての x について g（x）=c が成立するということです．

なお，f[x]，g[x] とはxを含んだ述語ということで，こういう記法がシステムに備わっているわけではありません．

次に，

　

ex x st f[x]=b & g[x]=c;

と書くとこれは，

（∃x) (f(x) = b　& g(x) = c)

を意味します．つまり， f（x）=b and g（x）=c となるxが存在するという意味です．また，全称記号と存在記号を混在して使うこともできます．

　 for x ex y st f[x] = g[y] holds h[x] = i[y]

これは，

(∀x) (∃y) (f(x) = g(y) ⇒ h(x) = i(y))

を表します．

括弧は任意に使うことを許されています．たとえ括弧が必要ないときでも，わかりやすくするために括弧を使うことができます．